Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sumnnodd Structured version   Visualization version   Unicode version

Theorem sumnnodd 37807
 Description: A series indexed by with only odd terms. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
sumnnodd.1
sumnnodd.even0
sumnnodd.sc
Assertion
Ref Expression
sumnnodd
Distinct variable groups:   ,   ,
Allowed substitution hint:   ()

Proof of Theorem sumnnodd
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1769 . . 3
2 nfcv 2612 . . 3
3 nfcv 2612 . . . 4
4 nfcv 2612 . . . 4
5 nfmpt1 4485 . . . 4
63, 4, 5nfseq 12261 . . 3
7 nfmpt1 4485 . . 3
8 nnuz 11218 . . 3
9 1zzd 10992 . . 3
10 seqex 12253 . . . 4
1110a1i 11 . . 3
12 sumnnodd.1 . . . . . 6
1312ffvelrnda 6037 . . . . 5
148, 9, 13serf 12279 . . . 4
1514ffvelrnda 6037 . . 3
16 sumnnodd.sc . . 3
17 1nn 10642 . . . . . . 7
18 oveq2 6316 . . . . . . . . 9
1918oveq1d 6323 . . . . . . . 8
20 eqid 2471 . . . . . . . 8
21 ovex 6336 . . . . . . . 8
2219, 20, 21fvmpt 5963 . . . . . . 7
2317, 22ax-mp 5 . . . . . 6
24 2t1e2 10781 . . . . . . 7
2524oveq1i 6318 . . . . . 6
26 2m1e1 10746 . . . . . 6
2723, 25, 263eqtri 2497 . . . . 5
2827, 17eqeltri 2545 . . . 4
2928a1i 11 . . 3
30 2z 10993 . . . . . . . 8
3130a1i 11 . . . . . . 7
32 nnz 10983 . . . . . . 7
3331, 32zmulcld 11069 . . . . . 6
3432peano2zd 11066 . . . . . . . 8
3531, 34zmulcld 11069 . . . . . . 7
36 1zzd 10992 . . . . . . 7
3735, 36zsubcld 11068 . . . . . 6
38 2re 10701 . . . . . . . . . 10
3938a1i 11 . . . . . . . . 9
40 nnre 10638 . . . . . . . . 9
4139, 40remulcld 9689 . . . . . . . 8
4241lep1d 10560 . . . . . . 7
43 2cnd 10704 . . . . . . . . . . 11
44 nncn 10639 . . . . . . . . . . 11
45 1cnd 9677 . . . . . . . . . . 11
4643, 44, 45adddid 9685 . . . . . . . . . 10
4724oveq2i 6319 . . . . . . . . . 10
4846, 47syl6eq 2521 . . . . . . . . 9
4948oveq1d 6323 . . . . . . . 8
5043, 44mulcld 9681 . . . . . . . . 9
5150, 43, 45addsubassd 10025 . . . . . . . 8
5226oveq2i 6319 . . . . . . . . 9
5352a1i 11 . . . . . . . 8
5449, 51, 533eqtrrd 2510 . . . . . . 7
5542, 54breqtrd 4420 . . . . . 6
56 eluz2 11188 . . . . . 6
5733, 37, 55, 56syl3anbrc 1214 . . . . 5
58 oveq2 6316 . . . . . . . . 9
5958oveq1d 6323 . . . . . . . 8
6059cbvmptv 4488 . . . . . . 7
6160a1i 11 . . . . . 6
62 oveq2 6316 . . . . . . . 8
6362oveq1d 6323 . . . . . . 7
6463adantl 473 . . . . . 6
65 peano2nn 10643 . . . . . 6
6661, 64, 65, 37fvmptd 5969 . . . . 5
6733, 36zsubcld 11068 . . . . . . . . 9
6820fvmpt2 5972 . . . . . . . . 9
6967, 68mpdan 681 . . . . . . . 8
7069oveq1d 6323 . . . . . . 7
7150, 45npcand 10009 . . . . . . 7
7270, 71eqtrd 2505 . . . . . 6
7372fveq2d 5883 . . . . 5
7457, 66, 733eltr4d 2564 . . . 4
76 seqex 12253 . . . 4
7776a1i 11 . . 3
78 incom 3616 . . . . . . . . . 10
79 inss2 3644 . . . . . . . . . . 11
80 ssrin 3648 . . . . . . . . . . 11
8179, 80ax-mp 5 . . . . . . . . . 10
8278, 81eqsstri 3448 . . . . . . . . 9
83 disjdif 3830 . . . . . . . . 9
8482, 83sseqtri 3450 . . . . . . . 8
85 ss0 3768 . . . . . . . 8
8684, 85mp1i 13 . . . . . . 7
87 uncom 3569 . . . . . . . . 9
88 inundif 3836 . . . . . . . . 9
8987, 88eqtr2i 2494 . . . . . . . 8
9089a1i 11 . . . . . . 7
91 fzfid 12224 . . . . . . 7
9212adantr 472 . . . . . . . . 9
93 elfznn 11854 . . . . . . . . . 10
9493adantl 473 . . . . . . . . 9
9592, 94ffvelrnd 6038 . . . . . . . 8
9695adantlr 729 . . . . . . 7
9786, 90, 91, 96fsumsplit 13883 . . . . . 6
98 simpl 464 . . . . . . . . . . . 12
99 ssrab2 3500 . . . . . . . . . . . . . 14
10079sseli 3414 . . . . . . . . . . . . . 14
10199, 100sseldi 3416 . . . . . . . . . . . . 13
102101adantl 473 . . . . . . . . . . . 12
103 oveq1 6315 . . . . . . . . . . . . . . . 16
104103eleq1d 2533 . . . . . . . . . . . . . . 15
105 oveq1 6315 . . . . . . . . . . . . . . . . . 18
106105eleq1d 2533 . . . . . . . . . . . . . . . . 17
107106elrab 3184 . . . . . . . . . . . . . . . 16
108107simprbi 471 . . . . . . . . . . . . . . 15
109104, 108vtoclga 3099 . . . . . . . . . . . . . 14
110100, 109syl 17 . . . . . . . . . . . . 13
111110adantl 473 . . . . . . . . . . . 12
112 eleq1 2537 . . . . . . . . . . . . . . 15
113112, 1043anbi23d 1368 . . . . . . . . . . . . . 14
114 fveq2 5879 . . . . . . . . . . . . . . 15
115114eqeq1d 2473 . . . . . . . . . . . . . 14
116113, 115imbi12d 327 . . . . . . . . . . . . 13
117 sumnnodd.even0 . . . . . . . . . . . . 13
118116, 117chvarv 2120 . . . . . . . . . . . 12
11998, 102, 111, 118syl3anc 1292 . . . . . . . . . . 11
120119sumeq2dv 13846 . . . . . . . . . 10
121 fzfid 12224 . . . . . . . . . . . . 13
122 inss1 3643 . . . . . . . . . . . . . 14
123122a1i 11 . . . . . . . . . . . . 13
124 ssfi 7810 . . . . . . . . . . . . 13
125121, 123, 124syl2anc 673 . . . . . . . . . . . 12
126125olcd 400 . . . . . . . . . . 11
127 sumz 13865 . . . . . . . . . . 11
128126, 127syl 17 . . . . . . . . . 10
129120, 128eqtrd 2505 . . . . . . . . 9
130129adantr 472 . . . . . . . 8
131130oveq2d 6324 . . . . . . 7
132 fzfi 12223 . . . . . . . . . . . 12
133 difss 3549 . . . . . . . . . . . 12
134 ssfi 7810 . . . . . . . . . . . 12
135132, 133, 134mp2an 686 . . . . . . . . . . 11
136135a1i 11 . . . . . . . . . 10
137133sseli 3414 . . . . . . . . . . . 12
138137, 95sylan2 482 . . . . . . . . . . 11
139138adantlr 729 . . . . . . . . . 10
140136, 139fsumcl 13876 . . . . . . . . 9
141140addid1d 9851 . . . . . . . 8
142 fveq2 5879 . . . . . . . . 9
143142cbvsumv 13839 . . . . . . . 8
144141, 143syl6eq 2521 . . . . . . 7
145131, 144eqtrd 2505 . . . . . 6
146 fveq2 5879 . . . . . . 7
147 fzfid 12224 . . . . . . 7
148 1zzd 10992 . . . . . . . . . . . . . 14
14967adantr 472 . . . . . . . . . . . . . 14
15030a1i 11 . . . . . . . . . . . . . . . . 17
151 elfzelz 11826 . . . . . . . . . . . . . . . . 17
152150, 151zmulcld 11069 . . . . . . . . . . . . . . . 16
153 1zzd 10992 . . . . . . . . . . . . . . . 16
154152, 153zsubcld 11068 . . . . . . . . . . . . . . 15
155154adantl 473 . . . . . . . . . . . . . 14
156148, 149, 1553jca 1210 . . . . . . . . . . . . 13
15725, 26eqtr2i 2494 . . . . . . . . . . . . . . . 16
158 1re 9660 . . . . . . . . . . . . . . . . . . 19
15938, 158remulcli 9675 . . . . . . . . . . . . . . . . . 18
160159a1i 11 . . . . . . . . . . . . . . . . 17
161152zred 11063 . . . . . . . . . . . . . . . . 17
162 1red 9676 . . . . . . . . . . . . . . . . 17
163151zred 11063 . . . . . . . . . . . . . . . . . 18
16438a1i 11 . . . . . . . . . . . . . . . . . 18
165 0le2 10722 . . . . . . . . . . . . . . . . . . 19
166165a1i 11 . . . . . . . . . . . . . . . . . 18
167 elfzle1 11828 . . . . . . . . . . . . . . . . . 18
168162, 163, 164, 166, 167lemul2ad 10569 . . . . . . . . . . . . . . . . 17
169160, 161, 162, 168lesub1dd 10250 . . . . . . . . . . . . . . . 16
170157, 169syl5eqbr 4429 . . . . . . . . . . . . . . 15
171170adantl 473 . . . . . . . . . . . . . 14
172161adantl 473 . . . . . . . . . . . . . . 15
17341adantr 472 . . . . . . . . . . . . . . 15
174 1red 9676 . . . . . . . . . . . . . . 15
175163adantl 473 . . . . . . . . . . . . . . . 16
17640adantr 472 . . . . . . . . . . . . . . . 16
17738a1i 11 . . . . . . . . . . . . . . . 16
178165a1i 11 . . . . . . . . . . . . . . . 16
179 elfzle2 11829 . . . . . . . . . . . . . . . . 17
180179adantl 473 . . . . . . . . . . . . . . . 16
181175, 176, 177, 178, 180lemul2ad 10569 . . . . . . . . . . . . . . 15
182172, 173, 174, 181lesub1dd 10250 . . . . . . . . . . . . . 14
183171, 182jca 541 . . . . . . . . . . . . 13
184 elfz2 11817 . . . . . . . . . . . . 13
185156, 183, 184sylanbrc 677 . . . . . . . . . . . 12
186152zcnd 11064 . . . . . . . . . . . . . . . . . 18
187 1cnd 9677 . . . . . . . . . . . . . . . . . 18
188 2cnd 10704 . . . . . . . . . . . . . . . . . 18
189 2ne0 10724 . . . . . . . . . . . . . . . . . . 19
190189a1i 11 . . . . . . . . . . . . . . . . . 18
191186, 187, 188, 190divsubdird 10444 . . . . . . . . . . . . . . . . 17
192151zcnd 11064 . . . . . . . . . . . . . . . . . . 19
193192, 188, 190divcan3d 10410 . . . . . . . . . . . . . . . . . 18
194193oveq1d 6323 . . . . . . . . . . . . . . . . 17
195191, 194eqtrd 2505 . . . . . . . . . . . . . . . 16
196151, 153zsubcld 11068 . . . . . . . . . . . . . . . . . 18
197164, 190rereccld 10456 . . . . . . . . . . . . . . . . . . 19
198 halflt1 10854 . . . . . . . . . . . . . . . . . . . 20
199198a1i 11 . . . . . . . . . . . . . . . . . . 19
200197, 162, 163, 199ltsub2dd 10247 . . . . . . . . . . . . . . . . . 18
201 2rp 11330 . . . . . . . . . . . . . . . . . . . . 21
202 rpreccl 11349 . . . . . . . . . . . . . . . . . . . . 21
203201, 202mp1i 13 . . . . . . . . . . . . . . . . . . . 20
204163, 203ltsubrpd 11393 . . . . . . . . . . . . . . . . . . 19
205192, 187npcand 10009 . . . . . . . . . . . . . . . . . . 19
206204, 205breqtrrd 4422 . . . . . . . . . . . . . . . . . 18
207 btwnnz 11035 . . . . . . . . . . . . . . . . . 18
208196, 200, 206, 207syl3anc 1292 . . . . . . . . . . . . . . . . 17
209 nnz 10983 . . . . . . . . . . . . . . . . 17
210208, 209nsyl 125 . . . . . . . . . . . . . . . 16
211195, 210eqneltrd 2568 . . . . . . . . . . . . . . 15
212211intnand 930 . . . . . . . . . . . . . 14
213 oveq1 6315 . . . . . . . . . . . . . . . 16
214213eleq1d 2533 . . . . . . . . . . . . . . 15
215214elrab 3184 . . . . . . . . . . . . . 14
216212, 215sylnibr 312 . . . . . . . . . . . . 13
217216adantl 473 . . . . . . . . . . . 12
218185, 217eldifd 3401 . . . . . . . . . . 11
219 eqid 2471 . . . . . . . . . . 11
220218, 219fmptd 6061 . . . . . . . . . 10
221 eqidd 2472 . . . . . . . . . . . . . . . . . 18
222 oveq2 6316 . . . . . . . . . . . . . . . . . . . 20
223222oveq1d 6323 . . . . . . . . . . . . . . . . . . 19
224223adantl 473 . . . . . . . . . . . . . . . . . 18
225 id 22 . . . . . . . . . . . . . . . . . 18
226 ovex 6336 . . . . . . . . . . . . . . . . . . 19
227226a1i 11 . . . . . . . . . . . . . . . . . 18
228221, 224, 225, 227fvmptd 5969 . . . . . . . . . . . . . . . . 17
229228eqcomd 2477 . . . . . . . . . . . . . . . 16
230229ad2antrr 740 . . . . . . . . . . . . . . 15
231 simpr 468 . . . . . . . . . . . . . . 15
232 eqidd 2472 . . . . . . . . . . . . . . . . 17
233 oveq2 6316 . . . . . . . . . . . . . . . . . . 19
234233oveq1d 6323 . . . . . . . . . . . . . . . . . 18
235234adantl 473 . . . . . . . . . . . . . . . . 17
236 id 22 . . . . . . . . . . . . . . . . 17
237 ovex 6336 . . . . . . . . . . . . . . . . . 18
238237a1i 11 . . . . . . . . . . . . . . . . 17
239232, 235, 236, 238fvmptd 5969 . . . . . . . . . . . . . . . 16
240239ad2antlr 741 . . . . . . . . . . . . . . 15
241230, 231, 2403eqtrd 2509 . . . . . . . . . . . . . 14
242 2cnd 10704 . . . . . . . . . . . . . . . . . 18
243 elfzelz 11826 . . . . . . . . . . . . . . . . . . 19
244243zcnd 11064 . . . . . . . . . . . . . . . . . 18
245242, 244mulcld 9681 . . . . . . . . . . . . . . . . 17
246245ad2antrr 740 . . . . . . . . . . . . . . . 16
247 2cnd 10704 . . . . . . . . . . . . . . . . . 18
248 elfzelz 11826 . . . . . . . . . . . . . . . . . . 19
249248zcnd 11064 . . . . . . . . . . . . . . . . . 18
250247, 249mulcld 9681 . . . . . . . . . . . . . . . . 17
251250ad2antlr 741 . . . . . . . . . . . . . . . 16
252 1cnd 9677 . . . . . . . . . . . . . . . 16
253 simpr 468 . . . . . . . . . . . . . . . 16
254246, 251, 252, 253subcan2d 10047 . . . . . . . . . . . . . . 15
255244ad2antrr 740 . . . . . . . . . . . . . . . 16
256249ad2antlr 741 . . . . . . . . . . . . . . . 16
257 2cnd 10704 . . . . . . . . . . . . . . . 16
258189a1i 11 . . . . . . . . . . . . . . . 16
259 simpr 468 . . . . . . . . . . . . . . . 16
260255, 256, 257, 258, 259mulcanad 10269 . . . . . . . . . . . . . . 15
261254, 260syldan 478 . . . . . . . . . . . . . 14
262241, 261syldan 478 . . . . . . . . . . . . 13
263262adantll 728 . . . . . . . . . . . 12
264263ex 441 . . . . . . . . . . 11
265264ralrimivva 2814 . . . . . . . . . 10
266 dff13 6177 . . . . . . . . . 10
267220, 265, 266sylanbrc 677 . . . . . . . . 9
268 1zzd 10992 . . . . . . . . . . . . . . . 16
26932adantr 472 . . . . . . . . . . . . . . . 16
270 fzssz 11827 . . . . . . . . . . . . . . . . . . . 20
271270, 137sseldi 3416 . . . . . . . . . . . . . . . . . . 19
272 zeo 11044 . . . . . . . . . . . . . . . . . . 19
273271, 272syl 17 . . . . . . . . . . . . . . . . . 18
274273adantl 473 . . . . . . . . . . . . . . . . 17
275 eldifn 3545 . . . . . . . . . . . . . . . . . . 19
276137, 93syl 17 . . . . . . . . . . . . . . . . . . . . 21
277276adantr 472 . . . . . . . . . . . . . . . . . . . 20
278 simpr 468 . . . . . . . . . . . . . . . . . . . . 21
279277nnred 10646 . . . . . . . . . . . . . . . . . . . . . 22
28038a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
281277nngt0d 10675 . . . . . . . . . . . . . . . . . . . . . 22
282 2pos 10723 . . . . . . . . . . . . . . . . . . . . . . 23
283282a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
284279, 280, 281, 283divgt0d 10564 . . . . . . . . . . . . . . . . . . . . 21
285 elnnz 10971 . . . . . . . . . . . . . . . . . . . . 21
286278, 284, 285sylanbrc 677 . . . . . . . . . . . . . . . . . . . 20
287 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . 22
288287eleq1d 2533 . . . . . . . . . . . . . . . . . . . . 21
289288elrab 3184 . . . . . . . . . . . . . . . . . . . 20
290277, 286, 289sylanbrc 677 . . . . . . . . . . . . . . . . . . 19
291275, 290mtand 671 . . . . . . . . . . . . . . . . . 18
292291adantl 473 . . . . . . . . . . . . . . . . 17
293 pm2.53 380 . . . . . . . . . . . . . . . . 17
294274, 292, 293sylc 61 . . . . . . . . . . . . . . . 16
295268, 269, 2943jca 1210 . . . . . . . . . . . . . . 15
296 1p1e2 10745 . . . . . . . . . . . . . . . . . . . 20
297296oveq1i 6318 . . . . . . . . . . . . . . . . . . 19
298 2div2e1 10755 . . . . . . . . . . . . . . . . . . 19
299297, 298eqtr2i 2494 . . . . . . . . . . . . . . . . . 18
300 1red 9676 . . . . . . . . . . . . . . . . . . . 20
301300, 300readdcld 9688 . . . . . . . . . . . . . . . . . . 19
30293nnred 10646 . . . . . . . . . . . . . . . . . . . 20
303302, 300readdcld 9688 . . . . . . . . . . . . . . . . . . 19
304201a1i 11 . . . . . . . . . . . . . . . . . . 19
305 elfzle1 11828 . . . . . . . . . . . . . . . . . . . 20
306300, 302, 300, 305leadd1dd 10248 . . . . . . . . . . . . . . . . . . 19
307301, 303, 304, 306lediv1dd 11419 . . . . . . . . . . . . . . . . . 18
308299, 307syl5eqbr 4429 . . . . . . . . . . . . . . . . 17
309137, 308syl 17 . . . . . . . . . . . . . . . 16
310309adantl 473 . . . . . . . . . . . . . . 15
311 elfzel2 11824 . . . . . . . . . . . . . . . . . . . . 21
312311zred 11063 . . . . . . . . . . . . . . . . . . . 20
313312, 300readdcld 9688 . . . . . . . . . . . . . . . . . . 19
314 elfzle2 11829 . . . . . . . . . . . . . . . . . . . 20
315302, 312, 300, 314leadd1dd 10248 . . . . . . . . . . . . . . . . . . 19
316303, 313, 304, 315lediv1dd 11419 . . . . . . . . . . . . . . . . . 18
317316adantl 473 . . . . . . . . . . . . . . . . 17
31850adantr 472 . . . . . . . . . . . . . . . . . . . 20
319 1cnd 9677 . . . . . . . . . . . . . . . . . . . 20
320318, 319npcand 10009 . . . . . . . . . . . . . . . . . . 19
321320oveq1d 6323 . . . . . . . . . . . . . . . . . 18
322189a1i 11 . . . . . . . . . . . . . . . . . . . 20
32344, 43, 322divcan3d 10410 . . . . . . . . . . . . . . . . . . 19
324323adantr 472 . . . . . . . . . . . . . . . . . 18
325321, 324eqtrd 2505 . . . . . . . . . . . . . . . . 17
326317, 325breqtrd 4420 . . . . . . . . . . . . . . . 16
327137, 326sylan2 482 . . . . . . . . . . . . . . 15
328295, 310, 327jca32 544 . . . . . . . . . . . . . 14
329 elfz2 11817 . . . . . . . . . . . . . 14
330328, 329sylibr 217 . . . . . . . . . . . . 13
331276nncnd 10647 . . . . . . . . . . . . . . 15
332 peano2cn 9823 . . . . . . . . . . . . . . . . . 18
333 2cnd 10704 . . . . . . . . . . . . . . . . . 18
334189a1i 11 . . . . . . . . . . . . . . . . . 18
335332, 333, 334divcan2d 10407 . . . . . . . . . . . . . . . . 17
336335oveq1d 6323 . . . . . . . . . . . . . . . 16
337 pncan1 10064 . . . . . . . . . . . . . . . 16
338336, 337eqtr2d 2506 . . . . . . . . . . . . . . 15
339331, 338syl 17 . . . . . . . . . . . . . 14
340339adantl 473 . . . . . . . . . . . . 13
341 oveq2 6316 . . . . . . . . . . . . . . . 16
342341oveq1d 6323 . . . . . . . . . . . . . . 15
343342eqeq2d 2481 . . . . . . . . . . . . . 14
344343rspcev 3136 . . . . . . . . . . . . 13
345330, 340, 344syl2anc 673 . . . . . . . . . . . 12
346 eqidd 2472 . . . . . . . . . . . . . . . . 17
347 oveq2 6316 . . . . . . . . . . . . . . . . . . 19
348347oveq1d 6323 . . . . . . . . . . . . . . . . . 18
349348adantl 473 . . . . . . . . . . . . . . . . 17
350 simpl 464 . . . . . . . . . . . . . . . . 17
351 ovex 6336 . . . . . . . . . . . . . . . . . 18
352351a1i 11 . . . . . . . . . . . . . . . . 17
353346, 349, 350, 352fvmptd 5969 . . . . . . . . . . . . . . . 16
354 id 22 . . . . . . . . . . . . . . . . . 18
355354eqcomd 2477 . . . . . . . . . . . . . . . . 17
356355adantl 473 . . . . . . . . . . . . . . . 16
357353, 356eqtr2d 2506 . . . . . . . . . . . . . . 15
358357ex 441 . . . . . . . . . . . . . 14
359358adantl 473 . . . . . . . . . . . . 13
360359reximdva 2858 . . . . . . . . . . . 12
361345, 360mpd 15 . . . . . . . . . . 11
362361ralrimiva 2809 . . . . . . . . . 10
363 dffo3 6052 . . . . . . . . . 10
364220, 362, 363sylanbrc 677 . . . . . . . . 9
365 df-f1o 5596 . . . . . . . . 9
366267, 364, 365sylanbrc 677 . . . . . . . 8
367366adantl 473 . . . . . . 7
368 eqidd 2472 . . . . . . . . 9
369 oveq2 6316 . . . . . . . . . . 11
370369oveq1d 6323 . . . . . . . . . 10
371370adantl 473 . . . . . . . . 9
372 id 22 . . . . . . . . 9
373 ovex 6336 . . . . . . . . . 10
374373a1i 11 . . . . . . . . 9
375368, 371, 372, 374fvmptd 5969 . . . . . . . 8
376375adantl 473 . . . . . . 7
377 eleq1 2537 . . . . . . . . . 10
378377anbi2d 718 . . . . . . . . 9
379142eleq1d 2533 . . . . . . . . 9
380378, 379imbi12d 327 . . . . . . . 8
381380, 139chvarv 2120 . . . . . . 7
382146, 147, 367, 376, 381fsumf1o 13866 . . . . . 6
38397, 145, 3823eqtrrd 2510 . . . . 5
384 ovex 6336 . . . . . . . . . 10
38520fvmpt2 5972 . . . . . . . . . 10
386384, 385mpan2 685 . . . . . . . . 9
387386oveq2d 6324 . . . . . . . 8
388387eqcomd 2477 . . . . . . 7
389388sumeq1d 13844 . . . . . 6
390389adantl 473 . . . . 5
391383, 390eqtrd 2505 . . . 4
392 elfznn 11854 . . . . . . 7
393392adantl 473 . . . . . 6
39412adantr 472 . . . . . . . 8
39530a1i 11 . . . . . . . . . . . 12
396 elfzelz 11826 . . . . . . . . . . . 12
397395, 396zmulcld 11069 . . . . . . . . . . 11
398 1zzd 10992 . . . . . . . . . . 11
399397, 398zsubcld 11068 . . . . . . . . . 10
400 0red 9662 . . . . . . . . . . 11
40138a1i 11 . . . . . . . . . . . . 13
40224, 401syl5eqel 2553 . . . . . . . . . . . 12
403 1red 9676 . . . . . . . . . . . 12
404402, 403resubcld 10068 . . . . . . . . . . 11
405399zred 11063 . . . . . . . . . . 11
406 0lt1 10157 . . . . . . . . . . . 12
407157a1i 11 . . . . . . . . . . . 12
408406, 407syl5breq 4431 . . . . . . . . . . 11
409397zred 11063 . . . . . . . . . . . 12
410392nnred 10646 . . . . . . . . . . . . 13
411165a1i 11 . . . . . . . . . . . . 13
412 elfzle1 11828 . . . . . . . . . . . . 13
413403, 410, 401, 411, 412lemul2ad 10569 . . . . . . . . . . . 12
414402, 409, 403, 413lesub1dd 10250 . . . . . . . . . . 11
415400, 404, 405, 408, 414ltletrd 9812 . . . . . . . . . 10
416 elnnz 10971 . . . . . . . . . 10
417399, 415, 416sylanbrc 677 . . . . . . . . 9
418417adantl 473 . . . . . . . 8
419394, 418ffvelrnd 6038 . . . . . . 7
420419adantlr 729 . . . . . 6
42159fveq2d 5883 . . . . . . . 8
422421cbvmptv 4488 . . . . . . 7
423422fvmpt2 5972 . . . . . 6