Metamath Proof Explorer

Theorem telfsumo2

Description: Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016)

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

Proof

Step Hyp Ref Expression
1 telfsumo.1 
 |-  ( k = j -> A = B )
2 telfsumo.2 
 |-  ( k = ( j + 1 ) -> A = C )
3 telfsumo.3 
 |-  ( k = M -> A = D )
4 telfsumo.4 
 |-  ( k = N -> A = E )
5 telfsumo.5 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
6 telfsumo.6 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
7 1 negeqd 
 |-  ( k = j -> -u A = -u B )
8 2 negeqd 
 |-  ( k = ( j + 1 ) -> -u A = -u C )
9 3 negeqd 
 |-  ( k = M -> -u A = -u D )
10 4 negeqd 
 |-  ( k = N -> -u A = -u E )
11 6 negcld 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> -u A e. CC )
12 7 8 9 10 5 11 telfsumo 
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( -u B - -u C ) = ( -u D - -u E ) )
13 6 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
14 elfzofz 
 |-  ( j e. ( M ..^ N ) -> j e. ( M ... N ) )
15 1 eleq1d 
 |-  ( k = j -> ( A e. CC <-> B e. CC ) )
16 15 rspccva 
 |-  ( ( A. k e. ( M ... N ) A e. CC /\ j e. ( M ... N ) ) -> B e. CC )
17 13 14 16 syl2an 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> B e. CC )
18 fzofzp1 
 |-  ( j e. ( M ..^ N ) -> ( j + 1 ) e. ( M ... N ) )
19 2 eleq1d 
 |-  ( k = ( j + 1 ) -> ( A e. CC <-> C e. CC ) )
20 19 rspccva 
 |-  ( ( A. k e. ( M ... N ) A e. CC /\ ( j + 1 ) e. ( M ... N ) ) -> C e. CC )
21 13 18 20 syl2an 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> C e. CC )
22 17 21 neg2subd 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> ( -u B - -u C ) = ( C - B ) )
23 22 sumeq2dv 
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( -u B - -u C ) = sum_ j e. ( M ..^ N ) ( C - B ) )
24 3 eleq1d 
 |-  ( k = M -> ( A e. CC <-> D e. CC ) )
25 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
26 5 25 syl 
 |-  ( ph -> M e. ( M ... N ) )
27 24 13 26 rspcdva 
 |-  ( ph -> D e. CC )
28 4 eleq1d 
 |-  ( k = N -> ( A e. CC <-> E e. CC ) )
29 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
30 5 29 syl 
 |-  ( ph -> N e. ( M ... N ) )
31 28 13 30 rspcdva 
 |-  ( ph -> E e. CC )
32 27 31 neg2subd 
 |-  ( ph -> ( -u D - -u E ) = ( E - D ) )
33 12 23 32 3eqtr3d 
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( C - B ) = ( E - D ) )