Theorem telfsum

Description: Sum of a telescoping series. (Contributed by Scott Fenton, 24-Apr-2014) (Revised by Mario Carneiro, 2-May-2016)

	Ref	Expression
Hypotheses	telfsum.1	|- ( k = j -> A = B )
	telfsum.2	|- ( k = ( j + 1 ) -> A = C )
	telfsum.3	|- ( k = M -> A = D )
	telfsum.4	|- ( k = ( N + 1 ) -> A = E )
	telfsum.5	|- ( ph -> N e. ZZ )
	telfsum.6	|- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
	telfsum.7	|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
Assertion	telfsum	|- ( ph -> sum_ j e. ( M ... N ) ( B - C ) = ( D - E ) )

Proof

Step	Hyp	Ref	Expression
1		telfsum.1	|- ( k = j -> A = B )
2		telfsum.2	|- ( k = ( j + 1 ) -> A = C )
3		telfsum.3	|- ( k = M -> A = D )
4		telfsum.4	|- ( k = ( N + 1 ) -> A = E )
5		telfsum.5	|- ( ph -> N e. ZZ )
6		telfsum.6	|- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
7		telfsum.7	|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
8		fzval3	|- ( N e. ZZ -> ( M ... N ) = ( M ..^ ( N + 1 ) ) )
9	5 8	syl	|- ( ph -> ( M ... N ) = ( M ..^ ( N + 1 ) ) )
10	9	sumeq1d	|- ( ph -> sum_ j e. ( M ... N ) ( B - C ) = sum_ j e. ( M ..^ ( N + 1 ) ) ( B - C ) )
11	1 2 3 4 6 7	telfsumo	|- ( ph -> sum_ j e. ( M ..^ ( N + 1 ) ) ( B - C ) = ( D - E ) )
12	10 11	eqtrd	|- ( ph -> sum_ j e. ( M ... N ) ( B - C ) = ( D - E ) )