[STATEMENT]
lemma sums_minus_ereal: "\<not> {- \<infinity>, \<infinity>} \<subseteq> f ` UNIV \<Longrightarrow> (\<lambda>n. - f n::ereal) sums x \<Longrightarrow> f sums - x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. - f n) sums x\<rbrakk> \<Longrightarrow> f sums - x
[PROOF STEP]
unfolding sums_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. \<Sum>n<n. - f n) \<longlonglongrightarrow> x\<rbrakk> \<Longrightarrow> (\<lambda>n. sum f {..<n}) \<longlonglongrightarrow> - x
[PROOF STEP]
apply (subst ereal_Lim_uminus)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. \<Sum>n<n. - f n) \<longlonglongrightarrow> x\<rbrakk> \<Longrightarrow> (\<lambda>x. - sum f {..<x}) \<longlonglongrightarrow> - (- x)
[PROOF STEP]
apply (subst (asm) setsum_negf_ereal)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>n. \<not> {- \<infinity>, \<infinity>} \<subseteq> range f \<Longrightarrow> \<not> {- \<infinity>, \<infinity>} \<subseteq> f ` {..<n}
 2. \<lbrakk>\<not> {- \<infinity>, \<infinity>} \<subseteq> range f; (\<lambda>n. - sum f {..<n}) \<longlonglongrightarrow> x\<rbrakk> \<Longrightarrow> (\<lambda>x. - sum f {..<x}) \<longlonglongrightarrow> - (- x)
[PROOF STEP]
apply auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done