Metamath Proof Explorer


Theorem esumpcvgval

Description: The value of the extended sum when the corresponding series sum is convergent. (Contributed by Thierry Arnoux, 31-Jul-2017)

Ref Expression
Hypotheses esumpcvgval.1 φ k A 0 +∞
esumpcvgval.2 k = l A = B
esumpcvgval.3 φ n k = 1 n A dom
Assertion esumpcvgval φ * k A = k A

Proof

Step Hyp Ref Expression
1 esumpcvgval.1 φ k A 0 +∞
2 esumpcvgval.2 k = l A = B
3 esumpcvgval.3 φ n k = 1 n A dom
4 xrltso < Or *
5 4 a1i φ < Or *
6 nnuz = 1
7 1zzd φ 1
8 eqcom k = l l = k
9 eqcom A = B B = A
10 2 8 9 3imtr3i l = k B = A
11 10 cbvmptv l B = k A
12 1 11 fmptd φ l B : 0 +∞
13 12 ffvelrnda φ x l B x 0 +∞
14 elrege0 l B x 0 +∞ l B x 0 l B x
15 14 simplbi l B x 0 +∞ l B x
16 13 15 syl φ x l B x
17 6 7 16 serfre φ seq 1 + l B :
18 12 adantr φ n l B : 0 +∞
19 simpr φ n n
20 19 peano2nnd φ n n + 1
21 18 20 ffvelrnd φ n l B n + 1 0 +∞
22 elrege0 l B n + 1 0 +∞ l B n + 1 0 l B n + 1
23 22 simprbi l B n + 1 0 +∞ 0 l B n + 1
24 21 23 syl φ n 0 l B n + 1
25 17 ffvelrnda φ n seq 1 + l B n
26 22 simplbi l B n + 1 0 +∞ l B n + 1
27 21 26 syl φ n l B n + 1
28 25 27 addge01d φ n 0 l B n + 1 seq 1 + l B n seq 1 + l B n + l B n + 1
29 24 28 mpbid φ n seq 1 + l B n seq 1 + l B n + l B n + 1
30 19 6 eleqtrdi φ n n 1
31 seqp1 n 1 seq 1 + l B n + 1 = seq 1 + l B n + l B n + 1
32 30 31 syl φ n seq 1 + l B n + 1 = seq 1 + l B n + l B n + 1
33 29 32 breqtrrd φ n seq 1 + l B n seq 1 + l B n + 1
34 simpr φ k k
35 11 fvmpt2 k A 0 +∞ l B k = A
36 34 1 35 syl2anc φ k l B k = A
37 rge0ssre 0 +∞
38 37 1 sseldi φ k A
39 17 feqmptd φ seq 1 + l B = n seq 1 + l B n
40 simpll φ n k 1 n φ
41 elfznn k 1 n k
42 41 adantl φ n k 1 n k
43 40 42 36 syl2anc φ n k 1 n l B k = A
44 38 recnd φ k A
45 40 42 44 syl2anc φ n k 1 n A
46 43 30 45 fsumser φ n k = 1 n A = seq 1 + l B n
47 46 eqcomd φ n seq 1 + l B n = k = 1 n A
48 47 mpteq2dva φ n seq 1 + l B n = n k = 1 n A
49 39 48 eqtr2d φ n k = 1 n A = seq 1 + l B
50 49 3 eqeltrrd φ seq 1 + l B dom
51 6 7 36 38 50 isumrecl φ k A
52 1zzd φ n 1
53 fzfid φ n 1 n Fin
54 fzssuz 1 n 1
55 54 6 sseqtrri 1 n
56 55 a1i φ n 1 n
57 36 adantlr φ n k l B k = A
58 38 adantlr φ n k A
59 1 adantlr φ n k A 0 +∞
60 elrege0 A 0 +∞ A 0 A
61 60 simprbi A 0 +∞ 0 A
62 59 61 syl φ n k 0 A
63 50 adantr φ n seq 1 + l B dom
64 6 52 53 56 57 58 62 63 isumless φ n k = 1 n A k A
65 46 64 eqbrtrrd φ n seq 1 + l B n k A
66 65 ralrimiva φ n seq 1 + l B n k A
67 brralrspcev k A n seq 1 + l B n k A s n seq 1 + l B n s
68 51 66 67 syl2anc φ s n seq 1 + l B n s
69 6 7 17 33 68 climsup φ seq 1 + l B sup ran seq 1 + l B <
70 6 7 69 25 climrecl φ sup ran seq 1 + l B <
71 70 rexrd φ sup ran seq 1 + l B < *
72 eqid b 𝒫 Fin k b A = b 𝒫 Fin k b A
73 sumex k b A V
74 72 73 elrnmpti x ran b 𝒫 Fin k b A b 𝒫 Fin x = k b A
75 ssnnssfz b 𝒫 Fin m b 1 m
76 fzfid φ b 1 m 1 m Fin
77 elfznn k 1 m k
78 77 1 sylan2 φ k 1 m A 0 +∞
79 60 simplbi A 0 +∞ A
80 78 79 syl φ k 1 m A
81 80 adantlr φ b 1 m k 1 m A
82 78 61 syl φ k 1 m 0 A
83 82 adantlr φ b 1 m k 1 m 0 A
84 simpr φ b 1 m b 1 m
85 76 81 83 84 fsumless φ b 1 m k b A k = 1 m A
86 85 ex φ b 1 m k b A k = 1 m A
87 86 reximdv φ m b 1 m m k b A k = 1 m A
88 87 imp φ m b 1 m m k b A k = 1 m A
89 75 88 sylan2 φ b 𝒫 Fin m k b A k = 1 m A
90 breq1 x = k b A x k = 1 m A k b A k = 1 m A
91 90 rexbidv x = k b A m x k = 1 m A m k b A k = 1 m A
92 89 91 syl5ibrcom φ b 𝒫 Fin x = k b A m x k = 1 m A
93 92 rexlimdva φ b 𝒫 Fin x = k b A m x k = 1 m A
94 93 imp φ b 𝒫 Fin x = k b A m x k = 1 m A
95 74 94 sylan2b φ x ran b 𝒫 Fin k b A m x k = 1 m A
96 simpr φ b 𝒫 Fin x = k b A x = k b A
97 inss2 𝒫 Fin Fin
98 simpr φ b 𝒫 Fin b 𝒫 Fin
99 97 98 sseldi φ b 𝒫 Fin b Fin
100 simpll φ b 𝒫 Fin k b φ
101 inss1 𝒫 Fin 𝒫
102 simplr φ b 𝒫 Fin k b b 𝒫 Fin
103 101 102 sseldi φ b 𝒫 Fin k b b 𝒫
104 103 elpwid φ b 𝒫 Fin k b b
105 simpr φ b 𝒫 Fin k b k b
106 104 105 sseldd φ b 𝒫 Fin k b k
107 100 106 1 syl2anc φ b 𝒫 Fin k b A 0 +∞
108 107 79 syl φ b 𝒫 Fin k b A
109 99 108 fsumrecl φ b 𝒫 Fin k b A
110 109 adantr φ b 𝒫 Fin x = k b A k b A
111 96 110 eqeltrd φ b 𝒫 Fin x = k b A x
112 111 r19.29an φ b 𝒫 Fin x = k b A x
113 74 112 sylan2b φ x ran b 𝒫 Fin k b A x
114 113 adantr φ x ran b 𝒫 Fin k b A m x k = 1 m A x
115 fzfid φ 1 m Fin
116 115 80 fsumrecl φ k = 1 m A
117 116 ad2antrr φ x ran b 𝒫 Fin k b A m x k = 1 m A k = 1 m A
118 70 ad2antrr φ x ran b 𝒫 Fin k b A m x k = 1 m A sup ran seq 1 + l B <
119 simprr φ x ran b 𝒫 Fin k b A m x k = 1 m A x k = 1 m A
120 17 frnd φ ran seq 1 + l B
121 120 ad2antrr φ x ran b 𝒫 Fin k b A m x k = 1 m A ran seq 1 + l B
122 1nn 1
123 122 ne0ii
124 dm0rn0 dom seq 1 + l B = ran seq 1 + l B =
125 17 fdmd φ dom seq 1 + l B =
126 125 eqeq1d φ dom seq 1 + l B = =
127 124 126 syl5bbr φ ran seq 1 + l B = =
128 127 necon3bid φ ran seq 1 + l B
129 123 128 mpbiri φ ran seq 1 + l B
130 129 ad2antrr φ x ran b 𝒫 Fin k b A m x k = 1 m A ran seq 1 + l B
131 1z 1
132 seqfn 1 seq 1 + l B Fn 1
133 131 132 ax-mp seq 1 + l B Fn 1
134 6 fneq2i seq 1 + l B Fn seq 1 + l B Fn 1
135 133 134 mpbir seq 1 + l B Fn
136 dffn5 seq 1 + l B Fn seq 1 + l B = n seq 1 + l B n
137 135 136 mpbi seq 1 + l B = n seq 1 + l B n
138 fvex seq 1 + l B n V
139 137 138 elrnmpti z ran seq 1 + l B n z = seq 1 + l B n
140 r19.29 n seq 1 + l B n s n z = seq 1 + l B n n seq 1 + l B n s z = seq 1 + l B n
141 breq1 z = seq 1 + l B n z s seq 1 + l B n s
142 141 biimparc seq 1 + l B n s z = seq 1 + l B n z s
143 142 rexlimivw n seq 1 + l B n s z = seq 1 + l B n z s
144 140 143 syl n seq 1 + l B n s n z = seq 1 + l B n z s
145 139 144 sylan2b n seq 1 + l B n s z ran seq 1 + l B z s
146 145 ralrimiva n seq 1 + l B n s z ran seq 1 + l B z s
147 146 reximi s n seq 1 + l B n s s z ran seq 1 + l B z s
148 68 147 syl φ s z ran seq 1 + l B z s
149 148 ad2antrr φ x ran b 𝒫 Fin k b A m x k = 1 m A s z ran seq 1 + l B z s
150 simpr φ m m
151 simpll φ m k 1 m φ
152 77 adantl φ m k 1 m k
153 151 152 36 syl2anc φ m k 1 m l B k = A
154 150 6 eleqtrdi φ m m 1
155 151 152 1 syl2anc φ m k 1 m A 0 +∞
156 155 79 syl φ m k 1 m A
157 156 recnd φ m k 1 m A
158 153 154 157 fsumser φ m k = 1 m A = seq 1 + l B m
159 fveq2 n = m seq 1 + l B n = seq 1 + l B m
160 159 rspceeqv m k = 1 m A = seq 1 + l B m n k = 1 m A = seq 1 + l B n
161 150 158 160 syl2anc φ m n k = 1 m A = seq 1 + l B n
162 137 138 elrnmpti k = 1 m A ran seq 1 + l B n k = 1 m A = seq 1 + l B n
163 161 162 sylibr φ m k = 1 m A ran seq 1 + l B
164 163 ad2ant2r φ x ran b 𝒫 Fin k b A m x k = 1 m A k = 1 m A ran seq 1 + l B
165 suprub ran seq 1 + l B ran seq 1 + l B s z ran seq 1 + l B z s k = 1 m A ran seq 1 + l B k = 1 m A sup ran seq 1 + l B <
166 121 130 149 164 165 syl31anc φ x ran b 𝒫 Fin k b A m x k = 1 m A k = 1 m A sup ran seq 1 + l B <
167 114 117 118 119 166 letrd φ x ran b 𝒫 Fin k b A m x k = 1 m A x sup ran seq 1 + l B <
168 95 167 rexlimddv φ x ran b 𝒫 Fin k b A x sup ran seq 1 + l B <
169 70 adantr φ x ran b 𝒫 Fin k b A sup ran seq 1 + l B <
170 113 169 lenltd φ x ran b 𝒫 Fin k b A x sup ran seq 1 + l B < ¬ sup ran seq 1 + l B < < x
171 168 170 mpbid φ x ran b 𝒫 Fin k b A ¬ sup ran seq 1 + l B < < x
172 simpr1r φ x * x < sup ran seq 1 + l B < 0 x x = +∞ x < sup ran seq 1 + l B <
173 172 3anassrs φ x * x < sup ran seq 1 + l B < 0 x x = +∞ x < sup ran seq 1 + l B <
174 71 ad3antrrr φ x * x < sup ran seq 1 + l B < 0 x x = +∞ sup ran seq 1 + l B < *
175 pnfnlt sup ran seq 1 + l B < * ¬ +∞ < sup ran seq 1 + l B <
176 174 175 syl φ x * x < sup ran seq 1 + l B < 0 x x = +∞ ¬ +∞ < sup ran seq 1 + l B <
177 breq1 x = +∞ x < sup ran seq 1 + l B < +∞ < sup ran seq 1 + l B <
178 177 notbid x = +∞ ¬ x < sup ran seq 1 + l B < ¬ +∞ < sup ran seq 1 + l B <
179 178 adantl φ x * x < sup ran seq 1 + l B < 0 x x = +∞ ¬ x < sup ran seq 1 + l B < ¬ +∞ < sup ran seq 1 + l B <
180 176 179 mpbird φ x * x < sup ran seq 1 + l B < 0 x x = +∞ ¬ x < sup ran seq 1 + l B <
181 173 180 pm2.21dd φ x * x < sup ran seq 1 + l B < 0 x x = +∞ y ran b 𝒫 Fin k b A x < y
182 simplll φ x * x < sup ran seq 1 + l B < 0 x x < +∞ φ
183 simpr1l φ x * x < sup ran seq 1 + l B < 0 x x < +∞ x *
184 183 3anassrs φ x * x < sup ran seq 1 + l B < 0 x x < +∞ x *
185 simplr φ x * x < sup ran seq 1 + l B < 0 x x < +∞ 0 x
186 simpr φ x * x < sup ran seq 1 + l B < 0 x x < +∞ x < +∞
187 0xr 0 *
188 pnfxr +∞ *
189 elico1 0 * +∞ * x 0 +∞ x * 0 x x < +∞
190 187 188 189 mp2an x 0 +∞ x * 0 x x < +∞
191 184 185 186 190 syl3anbrc φ x * x < sup ran seq 1 + l B < 0 x x < +∞ x 0 +∞
192 simpr1r φ x * x < sup ran seq 1 + l B < 0 x x < +∞ x < sup ran seq 1 + l B <
193 192 3anassrs φ x * x < sup ran seq 1 + l B < 0 x x < +∞ x < sup ran seq 1 + l B <
194 120 adantr φ x 0 +∞ x < sup ran seq 1 + l B < ran seq 1 + l B
195 129 adantr φ x 0 +∞ x < sup ran seq 1 + l B < ran seq 1 + l B
196 148 adantr φ x 0 +∞ x < sup ran seq 1 + l B < s z ran seq 1 + l B z s
197 194 195 196 3jca φ x 0 +∞ x < sup ran seq 1 + l B < ran seq 1 + l B ran seq 1 + l B s z ran seq 1 + l B z s
198 simprl φ x 0 +∞ x < sup ran seq 1 + l B < x 0 +∞
199 37 198 sseldi φ x 0 +∞ x < sup ran seq 1 + l B < x
200 simprr φ x 0 +∞ x < sup ran seq 1 + l B < x < sup ran seq 1 + l B <
201 suprlub ran seq 1 + l B ran seq 1 + l B s z ran seq 1 + l B z s x x < sup ran seq 1 + l B < y ran seq 1 + l B x < y
202 201 biimpa ran seq 1 + l B ran seq 1 + l B s z ran seq 1 + l B z s x x < sup ran seq 1 + l B < y ran seq 1 + l B x < y
203 197 199 200 202 syl21anc φ x 0 +∞ x < sup ran seq 1 + l B < y ran seq 1 + l B x < y
204 41 ssriv 1 n
205 ovex 1 n V
206 205 elpw 1 n 𝒫 1 n
207 204 206 mpbir 1 n 𝒫
208 fzfi 1 n Fin
209 elin 1 n 𝒫 Fin 1 n 𝒫 1 n Fin
210 207 208 209 mpbir2an 1 n 𝒫 Fin
211 210 a1i φ n y = seq 1 + l B n 1 n 𝒫 Fin
212 simpr φ n y = seq 1 + l B n y = seq 1 + l B n
213 46 adantr φ n y = seq 1 + l B n k = 1 n A = seq 1 + l B n
214 212 213 eqtr4d φ n y = seq 1 + l B n y = k = 1 n A
215 sumeq1 b = 1 n k b A = k = 1 n A
216 215 rspceeqv 1 n 𝒫 Fin y = k = 1 n A b 𝒫 Fin y = k b A
217 211 214 216 syl2anc φ n y = seq 1 + l B n b 𝒫 Fin y = k b A
218 217 ex φ n y = seq 1 + l B n b 𝒫 Fin y = k b A
219 218 rexlimdva φ n y = seq 1 + l B n b 𝒫 Fin y = k b A
220 137 138 elrnmpti y ran seq 1 + l B n y = seq 1 + l B n
221 72 73 elrnmpti y ran b 𝒫 Fin k b A b 𝒫 Fin y = k b A
222 219 220 221 3imtr4g φ y ran seq 1 + l B y ran b 𝒫 Fin k b A
223 222 ssrdv φ ran seq 1 + l B ran b 𝒫 Fin k b A
224 ssrexv ran seq 1 + l B ran b 𝒫 Fin k b A y ran seq 1 + l B x < y y ran b 𝒫 Fin k b A x < y
225 223 224 syl φ y ran seq 1 + l B x < y y ran b 𝒫 Fin k b A x < y
226 225 imp φ y ran seq 1 + l B x < y y ran b 𝒫 Fin k b A x < y
227 203 226 syldan φ x 0 +∞ x < sup ran seq 1 + l B < y ran b 𝒫 Fin k b A x < y
228 182 191 193 227 syl12anc φ x * x < sup ran seq 1 + l B < 0 x x < +∞ y ran b 𝒫 Fin k b A x < y
229 simplrl φ x * x < sup ran seq 1 + l B < 0 x x *
230 xrlelttric +∞ * x * +∞ x x < +∞
231 188 230 mpan x * +∞ x x < +∞
232 xgepnf x * +∞ x x = +∞
233 232 orbi1d x * +∞ x x < +∞ x = +∞ x < +∞
234 231 233 mpbid x * x = +∞ x < +∞
235 229 234 syl φ x * x < sup ran seq 1 + l B < 0 x x = +∞ x < +∞
236 181 228 235 mpjaodan φ x * x < sup ran seq 1 + l B < 0 x y ran b 𝒫 Fin k b A x < y
237 0elpw 𝒫
238 0fin Fin
239 elin 𝒫 Fin 𝒫 Fin
240 237 238 239 mpbir2an 𝒫 Fin
241 sum0 k A = 0
242 241 eqcomi 0 = k A
243 sumeq1 b = k b A = k A
244 243 rspceeqv 𝒫 Fin 0 = k A b 𝒫 Fin 0 = k b A
245 240 242 244 mp2an b 𝒫 Fin 0 = k b A
246 72 73 elrnmpti 0 ran b 𝒫 Fin k b A b 𝒫 Fin 0 = k b A
247 245 246 mpbir 0 ran b 𝒫 Fin k b A
248 breq2 y = 0 x < y x < 0
249 248 rspcev 0 ran b 𝒫 Fin k b A x < 0 y ran b 𝒫 Fin k b A x < y
250 247 249 mpan x < 0 y ran b 𝒫 Fin k b A x < y
251 250 adantl φ x * x < sup ran seq 1 + l B < x < 0 y ran b 𝒫 Fin k b A x < y
252 xrlelttric 0 * x * 0 x x < 0
253 187 252 mpan x * 0 x x < 0
254 253 ad2antrl φ x * x < sup ran seq 1 + l B < 0 x x < 0
255 236 251 254 mpjaodan φ x * x < sup ran seq 1 + l B < y ran b 𝒫 Fin k b A x < y
256 5 71 171 255 eqsupd φ sup ran b 𝒫 Fin k b A * < = sup ran seq 1 + l B <
257 nfv k φ
258 nfcv _ k
259 nnex V
260 259 a1i φ V
261 icossicc 0 +∞ 0 +∞
262 261 1 sseldi φ k A 0 +∞
263 elex b 𝒫 Fin b V
264 263 adantl φ b 𝒫 Fin b V
265 107 fmpttd φ b 𝒫 Fin k b A : b 0 +∞
266 esumpfinvallem b V k b A : b 0 +∞ fld k b A = 𝑠 * 𝑠 0 +∞ k b A
267 264 265 266 syl2anc φ b 𝒫 Fin fld k b A = 𝑠 * 𝑠 0 +∞ k b A
268 108 recnd φ b 𝒫 Fin k b A
269 99 268 gsumfsum φ b 𝒫 Fin fld k b A = k b A
270 267 269 eqtr3d φ b 𝒫 Fin 𝑠 * 𝑠 0 +∞ k b A = k b A
271 257 258 260 262 270 esumval φ * k A = sup ran b 𝒫 Fin k b A * <
272 6 7 36 44 69 isumclim φ k A = sup ran seq 1 + l B <
273 256 271 272 3eqtr4d φ * k A = k A