Metamath Proof Explorer


Theorem sumnnodd

Description: A series indexed by NN with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses sumnnodd.1 φF:
sumnnodd.even0 φkk2Fk=0
sumnnodd.sc φseq1+FB
Assertion sumnnodd φseq1+kF2k1BkFk=kF2k1

Proof

Step Hyp Ref Expression
1 sumnnodd.1 φF:
2 sumnnodd.even0 φkk2Fk=0
3 sumnnodd.sc φseq1+FB
4 nfv kφ
5 nfcv _kseq1+F
6 nfcv _k1
7 nfcv _k+
8 nfmpt1 _kkF2k1
9 6 7 8 nfseq _kseq1+kF2k1
10 nfmpt1 _kk2k1
11 nnuz =1
12 1zzd φ1
13 seqex seq1+FV
14 13 a1i φseq1+FV
15 1 ffvelrnda φkFk
16 11 12 15 serf φseq1+F:
17 16 ffvelrnda φkseq1+Fk
18 1nn 1
19 oveq2 k=12k=21
20 19 oveq1d k=12k1=211
21 eqid k2k1=k2k1
22 ovex 211V
23 20 21 22 fvmpt 1k2k11=211
24 18 23 ax-mp k2k11=211
25 2t1e2 21=2
26 25 oveq1i 211=21
27 2m1e1 21=1
28 24 26 27 3eqtri k2k11=1
29 28 18 eqeltri k2k11
30 29 a1i φk2k11
31 2z 2
32 31 a1i k2
33 nnz kk
34 32 33 zmulcld k2k
35 33 peano2zd kk+1
36 32 35 zmulcld k2k+1
37 1zzd k1
38 36 37 zsubcld k2k+11
39 2re 2
40 39 a1i k2
41 nnre kk
42 40 41 remulcld k2k
43 42 lep1d k2k2k+1
44 2cnd k2
45 nncn kk
46 1cnd k1
47 44 45 46 adddid k2k+1=2k+21
48 25 oveq2i 2k+21=2k+2
49 47 48 eqtrdi k2k+1=2k+2
50 49 oveq1d k2k+11=2k+2-1
51 44 45 mulcld k2k
52 51 44 46 addsubassd k2k+2-1=2k+2-1
53 27 oveq2i 2k+2-1=2k+1
54 53 a1i k2k+2-1=2k+1
55 50 52 54 3eqtrrd k2k+1=2k+11
56 43 55 breqtrd k2k2k+11
57 eluz2 2k+112k2k2k+112k2k+11
58 34 38 56 57 syl3anbrc k2k+112k
59 oveq2 k=j2k=2j
60 59 oveq1d k=j2k1=2j1
61 60 cbvmptv k2k1=j2j1
62 oveq2 j=k+12j=2k+1
63 62 oveq1d j=k+12j1=2k+11
64 peano2nn kk+1
65 61 63 64 38 fvmptd3 kk2k1k+1=2k+11
66 34 37 zsubcld k2k1
67 21 fvmpt2 k2k1k2k1k=2k1
68 66 67 mpdan kk2k1k=2k1
69 68 oveq1d kk2k1k+1=2k-1+1
70 51 46 npcand k2k-1+1=2k
71 69 70 eqtrd kk2k1k+1=2k
72 71 fveq2d kk2k1k+1=2k
73 58 65 72 3eltr4d kk2k1k+1k2k1k+1
74 73 adantl φkk2k1k+1k2k1k+1
75 seqex seq1+kF2k1V
76 75 a1i φseq1+kF2k1V
77 incom 12k1n|n212k1n|n2=12k1n|n212k1n|n2
78 inss2 12k1n|n2n|n2
79 ssrin 12k1n|n2n|n212k1n|n212k1n|n2n|n212k1n|n2
80 78 79 ax-mp 12k1n|n212k1n|n2n|n212k1n|n2
81 77 80 eqsstri 12k1n|n212k1n|n2n|n212k1n|n2
82 disjdif n|n212k1n|n2=
83 81 82 sseqtri 12k1n|n212k1n|n2
84 ss0 12k1n|n212k1n|n212k1n|n212k1n|n2=
85 83 84 mp1i φk12k1n|n212k1n|n2=
86 uncom 12k1n|n212k1n|n2=12k1n|n212k1n|n2
87 inundif 12k1n|n212k1n|n2=12k1
88 86 87 eqtr2i 12k1=12k1n|n212k1n|n2
89 88 a1i φk12k1=12k1n|n212k1n|n2
90 fzfid φk12k1Fin
91 1 adantr φj12k1F:
92 elfznn j12k1j
93 92 adantl φj12k1j
94 91 93 ffvelrnd φj12k1Fj
95 94 adantlr φkj12k1Fj
96 85 89 90 95 fsumsplit φkj=12k1Fj=j12k1n|n2Fj+j12k1n|n2Fj
97 simpl φj12k1n|n2φ
98 ssrab2 n|n2
99 78 sseli j12k1n|n2jn|n2
100 98 99 sselid j12k1n|n2j
101 100 adantl φj12k1n|n2j
102 oveq1 k=jk2=j2
103 102 eleq1d k=jk2j2
104 oveq1 n=kn2=k2
105 104 eleq1d n=kn2k2
106 105 elrab kn|n2kk2
107 106 simprbi kn|n2k2
108 103 107 vtoclga jn|n2j2
109 99 108 syl j12k1n|n2j2
110 109 adantl φj12k1n|n2j2
111 eleq1w k=jkj
112 111 103 3anbi23d k=jφkk2φjj2
113 fveqeq2 k=jFk=0Fj=0
114 112 113 imbi12d k=jφkk2Fk=0φjj2Fj=0
115 114 2 chvarvv φjj2Fj=0
116 97 101 110 115 syl3anc φj12k1n|n2Fj=0
117 116 sumeq2dv φj12k1n|n2Fj=j12k1n|n20
118 fzfid φ12k1Fin
119 inss1 12k1n|n212k1
120 119 a1i φ12k1n|n212k1
121 ssfi 12k1Fin12k1n|n212k112k1n|n2Fin
122 118 120 121 syl2anc φ12k1n|n2Fin
123 122 olcd φ12k1n|n2C12k1n|n2Fin
124 sumz 12k1n|n2C12k1n|n2Finj12k1n|n20=0
125 123 124 syl φj12k1n|n20=0
126 117 125 eqtrd φj12k1n|n2Fj=0
127 126 adantr φkj12k1n|n2Fj=0
128 127 oveq2d φkj12k1n|n2Fj+j12k1n|n2Fj=j12k1n|n2Fj+0
129 fzfi 12k1Fin
130 difss 12k1n|n212k1
131 ssfi 12k1Fin12k1n|n212k112k1n|n2Fin
132 129 130 131 mp2an 12k1n|n2Fin
133 132 a1i φk12k1n|n2Fin
134 130 sseli j12k1n|n2j12k1
135 134 94 sylan2 φj12k1n|n2Fj
136 135 adantlr φkj12k1n|n2Fj
137 133 136 fsumcl φkj12k1n|n2Fj
138 137 addid1d φkj12k1n|n2Fj+0=j12k1n|n2Fj
139 fveq2 j=iFj=Fi
140 139 cbvsumv j12k1n|n2Fj=i12k1n|n2Fi
141 138 140 eqtrdi φkj12k1n|n2Fj+0=i12k1n|n2Fi
142 128 141 eqtrd φkj12k1n|n2Fj+j12k1n|n2Fj=i12k1n|n2Fi
143 fveq2 i=2j1Fi=F2j1
144 fzfid φk1kFin
145 1zzd ki1k1
146 66 adantr ki1k2k1
147 31 a1i i1k2
148 elfzelz i1ki
149 147 148 zmulcld i1k2i
150 1zzd i1k1
151 149 150 zsubcld i1k2i1
152 151 adantl ki1k2i1
153 26 27 eqtr2i 1=211
154 1re 1
155 39 154 remulcli 21
156 155 a1i i1k21
157 149 zred i1k2i
158 1red i1k1
159 148 zred i1ki
160 39 a1i i1k2
161 0le2 02
162 161 a1i i1k02
163 elfzle1 i1k1i
164 158 159 160 162 163 lemul2ad i1k212i
165 156 157 158 164 lesub1dd i1k2112i1
166 153 165 eqbrtrid i1k12i1
167 166 adantl ki1k12i1
168 157 adantl ki1k2i
169 42 adantr ki1k2k
170 1red ki1k1
171 159 adantl ki1ki
172 41 adantr ki1kk
173 39 a1i ki1k2
174 161 a1i ki1k02
175 elfzle2 i1kik
176 175 adantl ki1kik
177 171 172 173 174 176 lemul2ad ki1k2i2k
178 168 169 170 177 lesub1dd ki1k2i12k1
179 145 146 152 167 178 elfzd ki1k2i112k1
180 149 zcnd i1k2i
181 1cnd i1k1
182 2cnd i1k2
183 2ne0 20
184 183 a1i i1k20
185 180 181 182 184 divsubdird i1k2i12=2i212
186 148 zcnd i1ki
187 186 182 184 divcan3d i1k2i2=i
188 187 oveq1d i1k2i212=i12
189 185 188 eqtrd i1k2i12=i12
190 148 150 zsubcld i1ki1
191 160 184 rereccld i1k12
192 halflt1 12<1
193 192 a1i i1k12<1
194 191 158 159 193 ltsub2dd i1ki1<i12
195 2rp 2+
196 rpreccl 2+12+
197 195 196 mp1i i1k12+
198 159 197 ltsubrpd i1ki12<i
199 186 181 npcand i1ki-1+1=i
200 198 199 breqtrrd i1ki12<i-1+1
201 btwnnz i1i1<i12i12<i-1+1¬i12
202 190 194 200 201 syl3anc i1k¬i12
203 nnz i12i12
204 202 203 nsyl i1k¬i12
205 189 204 eqneltrd i1k¬2i12
206 205 intnand i1k¬2i12i12
207 oveq1 n=2i1n2=2i12
208 207 eleq1d n=2i1n22i12
209 208 elrab 2i1n|n22i12i12
210 206 209 sylnibr i1k¬2i1n|n2
211 210 adantl ki1k¬2i1n|n2
212 179 211 eldifd ki1k2i112k1n|n2
213 212 fmpttd ki1k2i1:1k12k1n|n2
214 eqidd x1ki1k2i1=i1k2i1
215 oveq2 i=x2i=2x
216 215 oveq1d i=x2i1=2x1
217 216 adantl x1ki=x2i1=2x1
218 id x1kx1k
219 ovexd x1k2x1V
220 214 217 218 219 fvmptd x1ki1k2i1x=2x1
221 220 eqcomd x1k2x1=i1k2i1x
222 221 ad2antrr x1ky1ki1k2i1x=i1k2i1y2x1=i1k2i1x
223 simpr x1ky1ki1k2i1x=i1k2i1yi1k2i1x=i1k2i1y
224 eqidd y1ki1k2i1=i1k2i1
225 oveq2 i=y2i=2y
226 225 oveq1d i=y2i1=2y1
227 226 adantl y1ki=y2i1=2y1
228 id y1ky1k
229 ovexd y1k2y1V
230 224 227 228 229 fvmptd y1ki1k2i1y=2y1
231 230 ad2antlr x1ky1ki1k2i1x=i1k2i1yi1k2i1y=2y1
232 222 223 231 3eqtrd x1ky1ki1k2i1x=i1k2i1y2x1=2y1
233 2cnd x1k2
234 elfzelz x1kx
235 234 zcnd x1kx
236 233 235 mulcld x1k2x
237 236 ad2antrr x1ky1k2x1=2y12x
238 2cnd y1k2
239 elfzelz y1ky
240 239 zcnd y1ky
241 238 240 mulcld y1k2y
242 241 ad2antlr x1ky1k2x1=2y12y
243 1cnd x1ky1k2x1=2y11
244 simpr x1ky1k2x1=2y12x1=2y1
245 237 242 243 244 subcan2d x1ky1k2x1=2y12x=2y
246 235 ad2antrr x1ky1k2x=2yx
247 240 ad2antlr x1ky1k2x=2yy
248 2cnd x1ky1k2x=2y2
249 183 a1i x1ky1k2x=2y20
250 simpr x1ky1k2x=2y2x=2y
251 246 247 248 249 250 mulcanad x1ky1k2x=2yx=y
252 245 251 syldan x1ky1k2x1=2y1x=y
253 232 252 syldan x1ky1ki1k2i1x=i1k2i1yx=y
254 253 adantll kx1ky1ki1k2i1x=i1k2i1yx=y
255 254 ex kx1ky1ki1k2i1x=i1k2i1yx=y
256 255 ralrimivva kx1ky1ki1k2i1x=i1k2i1yx=y
257 dff13 i1k2i1:1k1-112k1n|n2i1k2i1:1k12k1n|n2x1ky1ki1k2i1x=i1k2i1yx=y
258 213 256 257 sylanbrc ki1k2i1:1k1-112k1n|n2
259 1zzd kj12k1n|n21
260 33 adantr kj12k1n|n2k
261 134 elfzelzd j12k1n|n2j
262 zeo jj2j+12
263 261 262 syl j12k1n|n2j2j+12
264 263 adantl kj12k1n|n2j2j+12
265 eldifn j12k1n|n2¬jn|n2
266 134 92 syl j12k1n|n2j
267 266 adantr j12k1n|n2j2j
268 simpr j12k1n|n2j2j2
269 267 nnred j12k1n|n2j2j
270 39 a1i j12k1n|n2j22
271 267 nngt0d j12k1n|n2j20<j
272 2pos 0<2
273 272 a1i j12k1n|n2j20<2
274 269 270 271 273 divgt0d j12k1n|n2j20<j2
275 elnnz j2j20<j2
276 268 274 275 sylanbrc j12k1n|n2j2j2
277 oveq1 n=jn2=j2
278 277 eleq1d n=jn2j2
279 278 elrab jn|n2jj2
280 267 276 279 sylanbrc j12k1n|n2j2jn|n2
281 265 280 mtand j12k1n|n2¬j2
282 281 adantl kj12k1n|n2¬j2
283 pm2.53 j2j+12¬j2j+12
284 264 282 283 sylc kj12k1n|n2j+12
285 1p1e2 1+1=2
286 285 oveq1i 1+12=22
287 2div2e1 22=1
288 286 287 eqtr2i 1=1+12
289 1red j12k11
290 289 289 readdcld j12k11+1
291 92 nnred j12k1j
292 291 289 readdcld j12k1j+1
293 195 a1i j12k12+
294 elfzle1 j12k11j
295 289 291 289 294 leadd1dd j12k11+1j+1
296 290 292 293 295 lediv1dd j12k11+12j+12
297 288 296 eqbrtrid j12k11j+12
298 134 297 syl j12k1n|n21j+12
299 298 adantl kj12k1n|n21j+12
300 elfzel2 j12k12k1
301 300 zred j12k12k1
302 301 289 readdcld j12k12k-1+1
303 elfzle2 j12k1j2k1
304 291 301 289 303 leadd1dd j12k1j+12k-1+1
305 292 302 293 304 lediv1dd j12k1j+122k-1+12
306 305 adantl kj12k1j+122k-1+12
307 51 adantr kj12k12k
308 1cnd kj12k11
309 307 308 npcand kj12k12k-1+1=2k
310 309 oveq1d kj12k12k-1+12=2k2
311 183 a1i k20
312 45 44 311 divcan3d k2k2=k
313 312 adantr kj12k12k2=k
314 310 313 eqtrd kj12k12k-1+12=k
315 306 314 breqtrd kj12k1j+12k
316 134 315 sylan2 kj12k1n|n2j+12k
317 259 260 284 299 316 elfzd kj12k1n|n2j+121k
318 266 nncnd j12k1n|n2j
319 peano2cn jj+1
320 2cnd j2
321 183 a1i j20
322 319 320 321 divcan2d j2j+12=j+1
323 322 oveq1d j2j+121=j+1-1
324 pncan1 jj+1-1=j
325 323 324 eqtr2d jj=2j+121
326 318 325 syl j12k1n|n2j=2j+121
327 326 adantl kj12k1n|n2j=2j+121
328 oveq2 m=j+122m=2j+12
329 328 oveq1d m=j+122m1=2j+121
330 329 rspceeqv j+121kj=2j+121m1kj=2m1
331 317 327 330 syl2anc kj12k1n|n2m1kj=2m1
332 eqidd m1kj=2m1i1k2i1=i1k2i1
333 oveq2 i=m2i=2m
334 333 oveq1d i=m2i1=2m1
335 334 adantl m1kj=2m1i=m2i1=2m1
336 simpl m1kj=2m1m1k
337 ovexd m1kj=2m12m1V
338 332 335 336 337 fvmptd m1kj=2m1i1k2i1m=2m1
339 id j=2m1j=2m1
340 339 eqcomd j=2m12m1=j
341 340 adantl m1kj=2m12m1=j
342 338 341 eqtr2d m1kj=2m1j=i1k2i1m
343 342 ex m1kj=2m1j=i1k2i1m
344 343 adantl kj12k1n|n2m1kj=2m1j=i1k2i1m
345 344 reximdva kj12k1n|n2m1kj=2m1m1kj=i1k2i1m
346 331 345 mpd kj12k1n|n2m1kj=i1k2i1m
347 346 ralrimiva kj12k1n|n2m1kj=i1k2i1m
348 dffo3 i1k2i1:1konto12k1n|n2i1k2i1:1k12k1n|n2j12k1n|n2m1kj=i1k2i1m
349 213 347 348 sylanbrc ki1k2i1:1konto12k1n|n2
350 df-f1o i1k2i1:1k1-1 onto12k1n|n2i1k2i1:1k1-112k1n|n2i1k2i1:1konto12k1n|n2
351 258 349 350 sylanbrc ki1k2i1:1k1-1 onto12k1n|n2
352 351 adantl φki1k2i1:1k1-1 onto12k1n|n2
353 eqidd j1ki1k2i1=i1k2i1
354 oveq2 i=j2i=2j
355 354 oveq1d i=j2i1=2j1
356 355 adantl j1ki=j2i1=2j1
357 id j1kj1k
358 ovexd j1k2j1V
359 353 356 357 358 fvmptd j1ki1k2i1j=2j1
360 359 adantl φkj1ki1k2i1j=2j1
361 eleq1w j=ij12k1n|n2i12k1n|n2
362 361 anbi2d j=iφkj12k1n|n2φki12k1n|n2
363 139 eleq1d j=iFjFi
364 362 363 imbi12d j=iφkj12k1n|n2Fjφki12k1n|n2Fi
365 364 136 chvarvv φki12k1n|n2Fi
366 143 144 352 360 365 fsumf1o φki12k1n|n2Fi=j=1kF2j1
367 96 142 366 3eqtrrd φkj=1kF2j1=j=12k1Fj
368 ovex 2k1V
369 21 fvmpt2 k2k1Vk2k1k=2k1
370 368 369 mpan2 kk2k1k=2k1
371 370 oveq2d k1k2k1k=12k1
372 371 eqcomd k12k1=1k2k1k
373 372 sumeq1d kj=12k1Fj=j=1k2k1kFj
374 373 adantl φkj=12k1Fj=j=1k2k1kFj
375 367 374 eqtrd φkj=1kF2j1=j=1k2k1kFj
376 elfznn j1kj
377 376 adantl φkj1kj
378 1 adantr φj1kF:
379 31 a1i j1k2
380 elfzelz j1kj
381 379 380 zmulcld j1k2j
382 1zzd j1k1
383 381 382 zsubcld j1k2j1
384 0red j1k0
385 39 a1i j1k2
386 25 385 eqeltrid j1k21
387 1red j1k1
388 386 387 resubcld j1k211
389 383 zred j1k2j1
390 0lt1 0<1
391 153 a1i j1k1=211
392 390 391 breqtrid j1k0<211
393 381 zred j1k2j
394 376 nnred j1kj
395 161 a1i j1k02
396 elfzle1 j1k1j
397 387 394 385 395 396 lemul2ad j1k212j
398 386 393 387 397 lesub1dd j1k2112j1
399 384 388 389 392 398 ltletrd j1k0<2j1
400 elnnz 2j12j10<2j1
401 383 399 400 sylanbrc j1k2j1
402 401 adantl φj1k2j1
403 378 402 ffvelrnd φj1kF2j1
404 403 adantlr φkj1kF2j1
405 60 fveq2d k=jF2k1=F2j1
406 405 cbvmptv kF2k1=jF2j1
407 406 fvmpt2 jF2j1kF2k1j=F2j1
408 377 404 407 syl2anc φkj1kkF2k1j=F2j1
409 simpr φkk
410 409 11 eleqtrdi φkk1
411 408 410 404 fsumser φkj=1kF2j1=seq1+kF2k1k
412 eqidd φkj1k2k1kFj=Fj
413 155 a1i k21
414 1red k1
415 161 a1i k02
416 nnge1 k1k
417 414 41 40 415 416 lemul2ad k212k
418 413 42 414 417 lesub1dd k2112k1
419 153 418 eqbrtrid k12k1
420 eluz2 2k1112k112k1
421 37 66 419 420 syl3anbrc k2k11
422 68 421 eqeltrd kk2k1k1
423 422 adantl φkk2k1k1
424 simpll φkj1k2k1kφ
425 simpr kj1k2k1kj1k2k1k
426 371 adantr kj1k2k1k1k2k1k=12k1
427 425 426 eleqtrd kj1k2k1kj12k1
428 427 adantll φkj1k2k1kj12k1
429 424 428 94 syl2anc φkj1k2k1kFj
430 412 423 429 fsumser φkj=1k2k1kFj=seq1+Fk2k1k
431 375 411 430 3eqtr3d φkseq1+kF2k1k=seq1+Fk2k1k
432 4 5 9 10 11 12 14 17 3 30 74 76 431 climsuse φseq1+kF2k1B
433 eqidd φkFk=Fk
434 11 12 433 15 isum φkFk=seq1+F
435 climrel Rel
436 435 releldmi seq1+FBseq1+Fdom
437 3 436 syl φseq1+Fdom
438 climdm seq1+Fdomseq1+Fseq1+F
439 437 438 sylib φseq1+Fseq1+F
440 climuni seq1+Fseq1+Fseq1+FBseq1+F=B
441 439 3 440 syl2anc φseq1+F=B
442 435 a1i φRel
443 releldm Relseq1+kF2k1Bseq1+kF2k1dom
444 442 432 443 syl2anc φseq1+kF2k1dom
445 climdm seq1+kF2k1domseq1+kF2k1seq1+kF2k1
446 444 445 sylib φseq1+kF2k1seq1+kF2k1
447 406 a1i φkF2k1=jF2j1
448 447 seqeq3d φseq1+kF2k1=seq1+jF2j1
449 448 fveq2d φseq1+kF2k1=seq1+jF2j1
450 446 449 breqtrd φseq1+kF2k1seq1+jF2j1
451 climuni seq1+kF2k1Bseq1+kF2k1seq1+jF2j1B=seq1+jF2j1
452 432 450 451 syl2anc φB=seq1+jF2j1
453 eqidd φkjF2j1=jF2j1
454 eqcom k=jj=k
455 eqcom F2k1=F2j1F2j1=F2k1
456 405 454 455 3imtr3i j=kF2j1=F2k1
457 456 adantl φkj=kF2j1=F2k1
458 1 adantr φkF:
459 421 11 eleqtrrdi k2k1
460 459 adantl φk2k1
461 458 460 ffvelrnd φkF2k1
462 453 457 409 461 fvmptd φkjF2j1k=F2k1
463 11 12 462 461 isum φkF2k1=seq1+jF2j1
464 452 463 eqtr4d φB=kF2k1
465 434 441 464 3eqtrd φkFk=kF2k1
466 432 465 jca φseq1+kF2k1BkFk=kF2k1