Metamath Proof Explorer

Theorem telfsumo

Description: Sum of a telescoping series, using half-open intervals. (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 telfsumo 
|- ( ph -> sum_ j e. ( M ..^ N ) ( B - C ) = ( D - E ) )

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 sum0 
 |-  sum_ j e. (/) ( B - C ) = 0
8 3 eleq1d 
 |-  ( k = M -> ( A e. CC <-> D e. CC ) )
9 6 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
10 eluzfz1 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
11 5 10 syl 
 |-  ( ph -> M e. ( M ... N ) )
12 8 9 11 rspcdva 
 |-  ( ph -> D e. CC )
13 12 adantr 
 |-  ( ( ph /\ N = M ) -> D e. CC )
14 13 subidd 
 |-  ( ( ph /\ N = M ) -> ( D - D ) = 0 )
15 7 14 eqtr4id 
 |-  ( ( ph /\ N = M ) -> sum_ j e. (/) ( B - C ) = ( D - D ) )
16 oveq2 
 |-  ( N = M -> ( M ..^ N ) = ( M ..^ M ) )
17 16 adantl 
 |-  ( ( ph /\ N = M ) -> ( M ..^ N ) = ( M ..^ M ) )
18 fzo0 
 |-  ( M ..^ M ) = (/)
19 17 18 eqtrdi 
 |-  ( ( ph /\ N = M ) -> ( M ..^ N ) = (/) )
20 19 sumeq1d 
 |-  ( ( ph /\ N = M ) -> sum_ j e. ( M ..^ N ) ( B - C ) = sum_ j e. (/) ( B - C ) )
21 eqeq1 
 |-  ( k = N -> ( k = M <-> N = M ) )
22 4 eqeq1d 
 |-  ( k = N -> ( A = D <-> E = D ) )
23 21 22 imbi12d 
 |-  ( k = N -> ( ( k = M -> A = D ) <-> ( N = M -> E = D ) ) )
24 23 3 vtoclg 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M -> E = D ) )
25 24 imp 
 |-  ( ( N e. ( ZZ>= ` M ) /\ N = M ) -> E = D )
26 5 25 sylan 
 |-  ( ( ph /\ N = M ) -> E = D )
27 26 oveq2d 
 |-  ( ( ph /\ N = M ) -> ( D - E ) = ( D - D ) )
28 15 20 27 3eqtr4d 
 |-  ( ( ph /\ N = M ) -> sum_ j e. ( M ..^ N ) ( B - C ) = ( D - E ) )
29 fzofi 
 |-  ( M ..^ N ) e. Fin
30 29 a1i 
 |-  ( ph -> ( M ..^ N ) e. Fin )
31 1 eleq1d 
 |-  ( k = j -> ( A e. CC <-> B e. CC ) )
32 9 adantr 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> A. k e. ( M ... N ) A e. CC )
33 elfzofz 
 |-  ( j e. ( M ..^ N ) -> j e. ( M ... N ) )
34 33 adantl 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> j e. ( M ... N ) )
35 31 32 34 rspcdva 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> B e. CC )
36 2 eleq1d 
 |-  ( k = ( j + 1 ) -> ( A e. CC <-> C e. CC ) )
37 fzofzp1 
 |-  ( j e. ( M ..^ N ) -> ( j + 1 ) e. ( M ... N ) )
38 37 adantl 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> ( j + 1 ) e. ( M ... N ) )
39 36 32 38 rspcdva 
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> C e. CC )
40 30 35 39 fsumsub 
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( B - C ) = ( sum_ j e. ( M ..^ N ) B - sum_ j e. ( M ..^ N ) C ) )
41 40 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ j e. ( M ..^ N ) ( B - C ) = ( sum_ j e. ( M ..^ N ) B - sum_ j e. ( M ..^ N ) C ) )
42 1 cbvsumv 
 |-  sum_ k e. ( M ..^ N ) A = sum_ j e. ( M ..^ N ) B
43 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
44 5 43 syl 
 |-  ( ph -> M e. ZZ )
45 eluzp1m1 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
46 44 45 sylan 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )
47 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
48 5 47 syl 
 |-  ( ph -> N e. ZZ )
49 48 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N e. ZZ )
50 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
51 49 50 syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
52 fzossfz 
 |-  ( M ..^ N ) C_ ( M ... N )
53 51 52 eqsstrrdi 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( M ... ( N - 1 ) ) C_ ( M ... N ) )
54 53 sselda 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( M ... ( N - 1 ) ) ) -> k e. ( M ... N ) )
55 6 adantlr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( M ... N ) ) -> A e. CC )
56 54 55 syldan 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( M ... ( N - 1 ) ) ) -> A e. CC )
57 46 56 3 fsum1p 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( M ... ( N - 1 ) ) A = ( D + sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A ) )
58 51 sumeq1d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( M ..^ N ) A = sum_ k e. ( M ... ( N - 1 ) ) A )
59 fzoval 
 |-  ( N e. ZZ -> ( ( M + 1 ) ..^ N ) = ( ( M + 1 ) ... ( N - 1 ) ) )
60 49 59 syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( M + 1 ) ..^ N ) = ( ( M + 1 ) ... ( N - 1 ) ) )
61 60 sumeq1d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( ( M + 1 ) ..^ N ) A = sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A )
62 61 oveq2d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( D + sum_ k e. ( ( M + 1 ) ..^ N ) A ) = ( D + sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A ) )
63 57 58 62 3eqtr4d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( M ..^ N ) A = ( D + sum_ k e. ( ( M + 1 ) ..^ N ) A ) )
64 42 63 eqtr3id 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ j e. ( M ..^ N ) B = ( D + sum_ k e. ( ( M + 1 ) ..^ N ) A ) )
65 simpr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> N e. ( ZZ>= ` ( M + 1 ) ) )
66 fzp1ss 
 |-  ( M e. ZZ -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
67 44 66 syl 
 |-  ( ph -> ( ( M + 1 ) ... N ) C_ ( M ... N ) )
68 67 sselda 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> k e. ( M ... N ) )
69 68 6 syldan 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ... N ) ) -> A e. CC )
70 69 adantlr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ k e. ( ( M + 1 ) ... N ) ) -> A e. CC )
71 65 70 4 fsumm1 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( ( M + 1 ) ... N ) A = ( sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A + E ) )
72 1zzd 
 |-  ( ph -> 1 e. ZZ )
73 44 peano2zd 
 |-  ( ph -> ( M + 1 ) e. ZZ )
74 72 73 48 69 2 fsumshftm 
 |-  ( ph -> sum_ k e. ( ( M + 1 ) ... N ) A = sum_ j e. ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) C )
75 44 zcnd 
 |-  ( ph -> M e. CC )
76 ax-1cn 
 |-  1 e. CC
77 pncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
78 75 76 77 sylancl 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
79 78 oveq1d 
 |-  ( ph -> ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) = ( M ... ( N - 1 ) ) )
80 48 50 syl 
 |-  ( ph -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
81 79 80 eqtr4d 
 |-  ( ph -> ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) = ( M ..^ N ) )
82 81 sumeq1d 
 |-  ( ph -> sum_ j e. ( ( ( M + 1 ) - 1 ) ... ( N - 1 ) ) C = sum_ j e. ( M ..^ N ) C )
83 74 82 eqtrd 
 |-  ( ph -> sum_ k e. ( ( M + 1 ) ... N ) A = sum_ j e. ( M ..^ N ) C )
84 83 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ k e. ( ( M + 1 ) ... N ) A = sum_ j e. ( M ..^ N ) C )
85 48 59 syl 
 |-  ( ph -> ( ( M + 1 ) ..^ N ) = ( ( M + 1 ) ... ( N - 1 ) ) )
86 85 sumeq1d 
 |-  ( ph -> sum_ k e. ( ( M + 1 ) ..^ N ) A = sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A )
87 86 oveq1d 
 |-  ( ph -> ( sum_ k e. ( ( M + 1 ) ..^ N ) A + E ) = ( sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A + E ) )
88 fzofi 
 |-  ( ( M + 1 ) ..^ N ) e. Fin
89 88 a1i 
 |-  ( ph -> ( ( M + 1 ) ..^ N ) e. Fin )
90 elfzofz 
 |-  ( k e. ( ( M + 1 ) ..^ N ) -> k e. ( ( M + 1 ) ... N ) )
91 90 69 sylan2 
 |-  ( ( ph /\ k e. ( ( M + 1 ) ..^ N ) ) -> A e. CC )
92 89 91 fsumcl 
 |-  ( ph -> sum_ k e. ( ( M + 1 ) ..^ N ) A e. CC )
93 4 eleq1d 
 |-  ( k = N -> ( A e. CC <-> E e. CC ) )
94 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
95 5 94 syl 
 |-  ( ph -> N e. ( M ... N ) )
96 93 9 95 rspcdva 
 |-  ( ph -> E e. CC )
97 92 96 addcomd 
 |-  ( ph -> ( sum_ k e. ( ( M + 1 ) ..^ N ) A + E ) = ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) )
98 87 97 eqtr3d 
 |-  ( ph -> ( sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A + E ) = ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) )
99 98 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( sum_ k e. ( ( M + 1 ) ... ( N - 1 ) ) A + E ) = ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) )
100 71 84 99 3eqtr3d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ j e. ( M ..^ N ) C = ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) )
101 64 100 oveq12d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( sum_ j e. ( M ..^ N ) B - sum_ j e. ( M ..^ N ) C ) = ( ( D + sum_ k e. ( ( M + 1 ) ..^ N ) A ) - ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) ) )
102 12 96 92 pnpcan2d 
 |-  ( ph -> ( ( D + sum_ k e. ( ( M + 1 ) ..^ N ) A ) - ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) ) = ( D - E ) )
103 102 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( D + sum_ k e. ( ( M + 1 ) ..^ N ) A ) - ( E + sum_ k e. ( ( M + 1 ) ..^ N ) A ) ) = ( D - E ) )
104 41 101 103 3eqtrd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> sum_ j e. ( M ..^ N ) ( B - C ) = ( D - E ) )
105 uzp1 
 |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
106 5 105 syl 
 |-  ( ph -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )
107 28 104 106 mpjaodan 
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( B - C ) = ( D - E ) )