[STATEMENT]
lemma telescope_sums:
  fixes c :: "'a::real_normed_vector"
  assumes "f \<longlonglongrightarrow> c"
  shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (Suc n) - f n) sums (c - f 0)
[PROOF STEP]
unfolding sums_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<Sum>n<n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
proof (subst filterlim_sequentially_Suc [symmetric])
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)
[PROOF STEP]
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] sum_Suc_diff)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
also
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
have "\<dots> \<longlonglongrightarrow> c - f 0"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<lambda>n. f (Suc n) - f 0) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const)
[PROOF STATE]
proof (state)
this:
(\<lambda>n. f (Suc n) - f 0) \<longlonglongrightarrow> c - f 0

goal (1 subgoal):
 1. (\<lambda>x. \<Sum>n<Suc x. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
finally
[PROOF STATE]
proof (chain)
picking this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0"
[PROOF STATE]
proof (prove)
using this:
(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) \<longlonglongrightarrow> c - f 0

goal (1 subgoal):
 1. (\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0
[PROOF STEP]
.
[PROOF STATE]
proof (state)
this:
(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0

goal:
No subgoals!
[PROOF STEP]
qed