This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) )