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=jA=B
telfsumo.2 k=j+1A=C
telfsumo.3 k=MA=D
telfsumo.4 k=NA=E
telfsumo.5 φNM
telfsumo.6 φkMNA
Assertion telfsumo φjM..^NBC=DE

Proof

Step Hyp Ref Expression
1 telfsumo.1 k=jA=B
2 telfsumo.2 k=j+1A=C
3 telfsumo.3 k=MA=D
4 telfsumo.4 k=NA=E
5 telfsumo.5 φNM
6 telfsumo.6 φkMNA
7 sum0 jBC=0
8 3 eleq1d k=MAD
9 6 ralrimiva φkMNA
10 eluzfz1 NMMMN
11 5 10 syl φMMN
12 8 9 11 rspcdva φD
13 12 adantr φN=MD
14 13 subidd φN=MDD=0
15 7 14 eqtr4id φN=MjBC=DD
16 oveq2 N=MM..^N=M..^M
17 16 adantl φN=MM..^N=M..^M
18 fzo0 M..^M=
19 17 18 eqtrdi φN=MM..^N=
20 19 sumeq1d φN=MjM..^NBC=jBC
21 eqeq1 k=Nk=MN=M
22 4 eqeq1d k=NA=DE=D
23 21 22 imbi12d k=Nk=MA=DN=ME=D
24 23 3 vtoclg NMN=ME=D
25 24 imp NMN=ME=D
26 5 25 sylan φN=ME=D
27 26 oveq2d φN=MDE=DD
28 15 20 27 3eqtr4d φN=MjM..^NBC=DE
29 fzofi M..^NFin
30 29 a1i φM..^NFin
31 1 eleq1d k=jAB
32 9 adantr φjM..^NkMNA
33 elfzofz jM..^NjMN
34 33 adantl φjM..^NjMN
35 31 32 34 rspcdva φjM..^NB
36 2 eleq1d k=j+1AC
37 fzofzp1 jM..^Nj+1MN
38 37 adantl φjM..^Nj+1MN
39 36 32 38 rspcdva φjM..^NC
40 30 35 39 fsumsub φjM..^NBC=jM..^NBjM..^NC
41 40 adantr φNM+1jM..^NBC=jM..^NBjM..^NC
42 1 cbvsumv kM..^NA=jM..^NB
43 eluzel2 NMM
44 5 43 syl φM
45 eluzp1m1 MNM+1N1M
46 44 45 sylan φNM+1N1M
47 eluzelz NMN
48 5 47 syl φN
49 48 adantr φNM+1N
50 fzoval NM..^N=MN1
51 49 50 syl φNM+1M..^N=MN1
52 fzossfz M..^NMN
53 51 52 eqsstrrdi φNM+1MN1MN
54 53 sselda φNM+1kMN1kMN
55 6 adantlr φNM+1kMNA
56 54 55 syldan φNM+1kMN1A
57 46 56 3 fsum1p φNM+1k=MN1A=D+k=M+1N1A
58 51 sumeq1d φNM+1kM..^NA=k=MN1A
59 fzoval NM+1..^N=M+1N1
60 49 59 syl φNM+1M+1..^N=M+1N1
61 60 sumeq1d φNM+1kM+1..^NA=k=M+1N1A
62 61 oveq2d φNM+1D+kM+1..^NA=D+k=M+1N1A
63 57 58 62 3eqtr4d φNM+1kM..^NA=D+kM+1..^NA
64 42 63 eqtr3id φNM+1jM..^NB=D+kM+1..^NA
65 simpr φNM+1NM+1
66 fzp1ss MM+1NMN
67 44 66 syl φM+1NMN
68 67 sselda φkM+1NkMN
69 68 6 syldan φkM+1NA
70 69 adantlr φNM+1kM+1NA
71 65 70 4 fsumm1 φNM+1k=M+1NA=k=M+1N1A+E
72 1zzd φ1
73 44 peano2zd φM+1
74 72 73 48 69 2 fsumshftm φk=M+1NA=j=M+1-1N1C
75 44 zcnd φM
76 ax-1cn 1
77 pncan M1M+1-1=M
78 75 76 77 sylancl φM+1-1=M
79 78 oveq1d φM+1-1N1=MN1
80 48 50 syl φM..^N=MN1
81 79 80 eqtr4d φM+1-1N1=M..^N
82 81 sumeq1d φj=M+1-1N1C=jM..^NC
83 74 82 eqtrd φk=M+1NA=jM..^NC
84 83 adantr φNM+1k=M+1NA=jM..^NC
85 48 59 syl φM+1..^N=M+1N1
86 85 sumeq1d φkM+1..^NA=k=M+1N1A
87 86 oveq1d φkM+1..^NA+E=k=M+1N1A+E
88 fzofi M+1..^NFin
89 88 a1i φM+1..^NFin
90 elfzofz kM+1..^NkM+1N
91 90 69 sylan2 φkM+1..^NA
92 89 91 fsumcl φkM+1..^NA
93 4 eleq1d k=NAE
94 eluzfz2 NMNMN
95 5 94 syl φNMN
96 93 9 95 rspcdva φE
97 92 96 addcomd φkM+1..^NA+E=E+kM+1..^NA
98 87 97 eqtr3d φk=M+1N1A+E=E+kM+1..^NA
99 98 adantr φNM+1k=M+1N1A+E=E+kM+1..^NA
100 71 84 99 3eqtr3d φNM+1jM..^NC=E+kM+1..^NA
101 64 100 oveq12d φNM+1jM..^NBjM..^NC=D+kM+1..^NA-E+kM+1..^NA
102 12 96 92 pnpcan2d φD+kM+1..^NA-E+kM+1..^NA=DE
103 102 adantr φNM+1D+kM+1..^NA-E+kM+1..^NA=DE
104 41 101 103 3eqtrd φNM+1jM..^NBC=DE
105 uzp1 NMN=MNM+1
106 5 105 syl φN=MNM+1
107 28 104 106 mpjaodan φjM..^NBC=DE