Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  dchrisumlem2 Structured version   Visualization version   Unicode version

Theorem dchrisumlem2 24407
 Description: Lemma for dchrisum 24409. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z ℤ/n
rpvmasum.l RHom
rpvmasum.a
rpvmasum.g DChr
rpvmasum.d
rpvmasum.1
dchrisum.b
dchrisum.n1
dchrisum.2
dchrisum.3
dchrisum.4
dchrisum.5
dchrisum.6
dchrisum.7
dchrisum.9
dchrisum.10 ..^ ..^
dchrisumlem2.1
dchrisumlem2.2
dchrisumlem2.3
dchrisumlem2.4
dchrisumlem2.5
Assertion
Ref Expression
dchrisumlem2
Distinct variable groups:   ,,   ,,   ,,,   ,,,   ,,,   ,   ,,,   ,,,   ,,,   ,,,   ,   ,,   ,,   ,,,   ,,,   ,,,
Allowed substitution hints:   (,)   (,)   ()   ()   (,,)   ()

Proof of Theorem dchrisumlem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzodisj 11979 . . . . . . . . 9 ..^ ..^
21a1i 11 . . . . . . . 8 ..^ ..^
3 dchrisumlem2.4 . . . . . . . . . . . 12
43peano2nnd 10648 . . . . . . . . . . 11
5 nnuz 11218 . . . . . . . . . . 11
64, 5syl6eleq 2559 . . . . . . . . . 10
7 dchrisumlem2.5 . . . . . . . . . . 11
8 eluzp1p1 11208 . . . . . . . . . . 11
97, 8syl 17 . . . . . . . . . 10
10 elfzuzb 11820 . . . . . . . . . 10
116, 9, 10sylanbrc 677 . . . . . . . . 9
12 fzosplit 11978 . . . . . . . . 9 ..^ ..^ ..^
1311, 12syl 17 . . . . . . . 8 ..^ ..^ ..^
14 fzofi 12225 . . . . . . . . 9 ..^
1514a1i 11 . . . . . . . 8 ..^
16 elfzouz 11951 . . . . . . . . . 10 ..^
1716, 5syl6eleqr 2560 . . . . . . . . 9 ..^
18 rpvmasum.g . . . . . . . . . . 11 DChr
19 rpvmasum.z . . . . . . . . . . 11 ℤ/n
20 rpvmasum.d . . . . . . . . . . 11
21 rpvmasum.l . . . . . . . . . . 11 RHom
22 dchrisum.b . . . . . . . . . . . 12
2322adantr 472 . . . . . . . . . . 11
24 nnz 10983 . . . . . . . . . . . 12
2524adantl 473 . . . . . . . . . . 11
2618, 19, 20, 21, 23, 25dchrzrhcl 24252 . . . . . . . . . 10
27 nnrp 11334 . . . . . . . . . . . . 13
28 rpvmasum.a . . . . . . . . . . . . . . 15
29 rpvmasum.1 . . . . . . . . . . . . . . 15
30 dchrisum.n1 . . . . . . . . . . . . . . 15
31 dchrisum.2 . . . . . . . . . . . . . . 15
32 dchrisum.3 . . . . . . . . . . . . . . 15
33 dchrisum.4 . . . . . . . . . . . . . . 15
34 dchrisum.5 . . . . . . . . . . . . . . 15
35 dchrisum.6 . . . . . . . . . . . . . . 15
36 dchrisum.7 . . . . . . . . . . . . . . 15
3719, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 24405 . . . . . . . . . . . . . 14
3837simpld 466 . . . . . . . . . . . . 13
3927, 38syl5 32 . . . . . . . . . . . 12
4039imp 436 . . . . . . . . . . 11
4140recnd 9687 . . . . . . . . . 10
4226, 41mulcld 9681 . . . . . . . . 9
4317, 42sylan2 482 . . . . . . . 8 ..^
442, 13, 15, 43fsumsplit 13883 . . . . . . 7 ..^ ..^ ..^
45 eluzelz 11192 . . . . . . . . 9
46 fzval3 12012 . . . . . . . . 9 ..^
477, 45, 463syl 18 . . . . . . . 8 ..^
4847sumeq1d 13844 . . . . . . 7 ..^
493nnzd 11062 . . . . . . . . . 10
50 fzval3 12012 . . . . . . . . . 10 ..^
5149, 50syl 17 . . . . . . . . 9 ..^
5251sumeq1d 13844 . . . . . . . 8 ..^
5352oveq1d 6323 . . . . . . 7 ..^ ..^ ..^
5444, 48, 533eqtr4d 2515 . . . . . 6 ..^
55 elfznn 11854 . . . . . . . 8
56 simpr 468 . . . . . . . . 9
57 nfcv 2612 . . . . . . . . . 10
58 nfcv 2612 . . . . . . . . . . 11
59 nfcv 2612 . . . . . . . . . . 11
60 nfcsb1v 3365 . . . . . . . . . . 11
6158, 59, 60nfov 6334 . . . . . . . . . 10
62 fveq2 5879 . . . . . . . . . . . 12
6362fveq2d 5883 . . . . . . . . . . 11
64 csbeq1a 3358 . . . . . . . . . . 11
6563, 64oveq12d 6326 . . . . . . . . . 10
6657, 61, 65, 36fvmptf 5981 . . . . . . . . 9
6756, 42, 66syl2anc 673 . . . . . . . 8
6855, 67sylan2 482 . . . . . . 7
693, 5syl6eleq 2559 . . . . . . . 8
70 uztrn 11199 . . . . . . . 8
717, 69, 70syl2anc 673 . . . . . . 7
7255, 42sylan2 482 . . . . . . 7
7368, 71, 72fsumser 13873 . . . . . 6
7454, 73eqtr3d 2507 . . . . 5 ..^
75 elfznn 11854 . . . . . . 7
7675, 67sylan2 482 . . . . . 6
7775, 42sylan2 482 . . . . . 6
7876, 69, 77fsumser 13873 . . . . 5
7974, 78oveq12d 6326 . . . 4 ..^
80 fzfid 12224 . . . . . 6
8180, 77fsumcl 13876 . . . . 5
82 fzofi 12225 . . . . . . 7 ..^
8382a1i 11 . . . . . 6 ..^
84 ssun2 3589 . . . . . . . . 9 ..^ ..^ ..^
8584, 13syl5sseqr 3467 . . . . . . . 8 ..^ ..^
8685sselda 3418 . . . . . . 7 ..^ ..^
8786, 43syldan 478 . . . . . 6 ..^
8883, 87fsumcl 13876 . . . . 5 ..^
8981, 88pncan2d 10007 . . . 4 ..^ ..^
9079, 89eqtr3d 2507 . . 3 ..^
9190fveq2d 5883 . 2 ..^
9288abscld 13575 . . 3 ..^
93 2re 10701 . . . . . 6
9493a1i 11 . . . . 5
95 dchrisum.9 . . . . 5
9694, 95remulcld 9689 . . . 4
9740ralrimiva 2809 . . . . 5
98 csbeq1 3352 . . . . . . 7
9998eleq1d 2533 . . . . . 6
10099rspcv 3132 . . . . 5
1014, 97, 100sylc 61 . . . 4
10296, 101remulcld 9689 . . 3
103 dchrisumlem2.1 . . . . 5
10433ralrimiva 2809 . . . . 5
105 nfcsb1v 3365 . . . . . . 7
106105nfel1 2626 . . . . . 6
107 csbeq1a 3358 . . . . . . 7
108107eleq1d 2533 . . . . . 6
109106, 108rspc 3130 . . . . 5
110103, 104, 109sylc 61 . . . 4
11196, 110remulcld 9689 . . 3
11271, 5syl6eleqr 2560 . . . . . . . . . . . 12
113112peano2nnd 10648 . . . . . . . . . . 11
114113nnrpd 11362 . . . . . . . . . 10
11519, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 24405 . . . . . . . . . . 11
116115simpld 466 . . . . . . . . . 10
117114, 116mpd 15 . . . . . . . . 9
118117recnd 9687 . . . . . . . 8
119 fzofi 12225 . . . . . . . . . 10 ..^
120119a1i 11 . . . . . . . . 9 ..^
121 elfzoelz 11947 . . . . . . . . . 10 ..^
12222adantr 472 . . . . . . . . . . 11
123 simpr 468 . . . . . . . . . . 11
12418, 19, 20, 21, 122, 123dchrzrhcl 24252 . . . . . . . . . 10
125121, 124sylan2 482 . . . . . . . . 9 ..^
126120, 125fsumcl 13876 . . . . . . . 8 ..^
127118, 126mulcld 9681 . . . . . . 7 ..^
128101recnd 9687 . . . . . . . 8
129 fzofi 12225 . . . . . . . . . 10 ..^
130129a1i 11 . . . . . . . . 9 ..^
131 elfzoelz 11947 . . . . . . . . . 10 ..^
132131, 124sylan2 482 . . . . . . . . 9 ..^
133130, 132fsumcl 13876 . . . . . . . 8 ..^
134128, 133mulcld 9681 . . . . . . 7 ..^
135127, 134subcld 10005 . . . . . 6 ..^ ..^
136135abscld 13575 . . . . 5 ..^ ..^
13786, 17syl 17 . . . . . . . 8 ..^
138 peano2nn 10643 . . . . . . . . . . . . 13
139138nnrpd 11362 . . . . . . . . . . . 12
140 nfcsb1v 3365 . . . . . . . . . . . . . . 15
141140nfel1 2626 . . . . . . . . . . . . . 14
142 csbeq1a 3358 . . . . . . . . . . . . . . 15
143142eleq1d 2533 . . . . . . . . . . . . . 14
144141, 143rspc 3130 . . . . . . . . . . . . 13
145144impcom 437 . . . . . . . . . . . 12
146104, 139, 145syl2an 485 . . . . . . . . . . 11
147146, 40resubcld 10068 . . . . . . . . . 10
148147recnd 9687 . . . . . . . . 9
149 fzofi 12225 . . . . . . . . . . . 12 ..^
150149a1i 11 . . . . . . . . . . 11 ..^
151 elfzoelz 11947 . . . . . . . . . . . 12 ..^
152151, 124sylan2 482 . . . . . . . . . . 11 ..^
153150, 152fsumcl 13876 . . . . . . . . . 10 ..^
154153adantr 472 . . . . . . . . 9 ..^
155148, 154mulcld 9681 . . . . . . . 8 ..^
156137, 155syldan 478 . . . . . . 7 ..^ ..^
15783, 156fsumcl 13876 . . . . . 6 ..^ ..^
158157abscld 13575 . . . . 5 ..^ ..^
159136, 158readdcld 9688 . . . 4 ..^ ..^ ..^ ..^
16026, 41mulcomd 9682 . . . . . . . . . 10
161 nnnn0 10900 . . . . . . . . . . . . . . . 16
162161adantl 473 . . . . . . . . . . . . . . 15
163 nn0uz 11217 . . . . . . . . . . . . . . 15
164162, 163syl6eleq 2559 . . . . . . . . . . . . . 14
165 elfzelz 11826 . . . . . . . . . . . . . . 15
166124adantlr 729 . . . . . . . . . . . . . . 15
167165, 166sylan2 482 . . . . . . . . . . . . . 14
168164, 167, 63fzosump1 13890 . . . . . . . . . . . . 13 ..^ ..^
169168oveq1d 6323 . . . . . . . . . . . 12 ..^ ..^ ..^ ..^
170 fzofi 12225 . . . . . . . . . . . . . . 15 ..^
171170a1i 11 . . . . . . . . . . . . . 14 ..^
172 elfzoelz 11947 . . . . . . . . . . . . . . 15 ..^
173172, 166sylan2 482 . . . . . . . . . . . . . 14 ..^
174171, 173fsumcl 13876 . . . . . . . . . . . . 13 ..^
175174, 26pncan2d 10007 . . . . . . . . . . . 12 ..^ ..^
176169, 175eqtr2d 2506 . . . . . . . . . . 11 ..^ ..^
177176oveq2d 6324 . . . . . . . . . 10 ..^ ..^
178160, 177eqtrd 2505 . . . . . . . . 9 ..^ ..^
179137, 178syldan 478 . . . . . . . 8 ..^ ..^ ..^
180179sumeq2dv 13846 . . . . . . 7 ..^ ..^ ..^ ..^
181 csbeq1 3352 . . . . . . . . 9
182 oveq2 6316 . . . . . . . . . 10 ..^ ..^
183182sumeq1d 13844 . . . . . . . . 9 ..^ ..^
184181, 183jca 541 . . . . . . . 8 ..^ ..^
185 csbeq1 3352 . . . . . . . . 9
186 oveq2 6316 . . . . . . . . . 10 ..^ ..^
187186sumeq1d 13844 . . . . . . . . 9 ..^ ..^
188185, 187jca 541 . . . . . . . 8 ..^ ..^
189 csbeq1 3352 . . . . . . . . 9
190 oveq2 6316 . . . . . . . . . 10 ..^ ..^
191190sumeq1d 13844 . . . . . . . . 9 ..^ ..^
192189, 191jca 541 . . . . . . . 8 ..^ ..^
193 csbeq1 3352 . . . . . . . . 9
194 oveq2 6316 . . . . . . . . . 10 ..^ ..^
195194sumeq1d 13844 . . . . . . . . 9 ..^ ..^
196193, 195jca 541 . . . . . . . 8 ..^ ..^
197 elfzuz 11822 . . . . . . . . . 10
198 eluznn 11252 . . . . . . . . . 10
1994, 197, 198syl2an 485 . . . . . . . . 9
20041ralrimiva 2809 . . . . . . . . . 10
201 csbeq1 3352 . . . . . . . . . . . 12
202201eleq1d 2533 . . . . . . . . . . 11
203202rspccva 3135 . . . . . . . . . 10
204200, 203sylan 479 . . . . . . . . 9
205199, 204syldan 478 . . . . . . . 8
206 fzofi 12225 . . . . . . . . . . 11 ..^
207206a1i 11 . . . . . . . . . 10 ..^
208 elfzoelz 11947 . . . . . . . . . . 11 ..^
209208, 124sylan2 482 . . . . . . . . . 10 ..^
210207, 209fsumcl 13876 . . . . . . . . 9 ..^
211210adantr 472 . . . . . . . 8 ..^
212184, 188, 192, 196, 9, 205, 211fsumparts 13943 . . . . . . 7 ..^ ..^ ..^ ..^ ..^ ..^ ..^
213180, 212eqtrd 2505 . . . . . 6 ..^ ..^ ..^ ..^ ..^
214213fveq2d 5883 . . . . 5 ..^ ..^ ..^ ..^ ..^
215135, 157abs2dif2d 13597 . . . . 5 ..^ ..^ ..^ ..^ ..^ ..^ ..^ ..^
216214, 215eqbrtrd 4416 . . . 4 ..^ ..^ ..^ ..^ ..^
217117, 101readdcld 9688 . . . . . . 7
218217, 95remulcld 9689 . . . . . 6
219181, 185, 189, 193, 9, 205telfsumo 13939 . . . . . . . 8 ..^
220137, 40syldan 478 . . . . . . . . . 10 ..^
221137, 146syldan 478 . . . . . . . . . 10 ..^
222220, 221resubcld 10068 . . . . . . . . 9 ..^
22383, 222fsumrecl 13877 . . . . . . . 8 ..^
224219, 223eqeltrrd 2550 . . . . . . 7
225224, 95remulcld 9689 . . . . . 6
226127abscld 13575 . . . . . . . 8 ..^
227134abscld 13575 . . . . . . . 8 ..^
228226, 227readdcld 9688 . . . . . . 7 ..^ ..^
229127, 134abs2dif2d 13597 . . . . . . 7 ..^ ..^ ..^ ..^
230117, 95remulcld 9689 . . . . . . . . 9
231101, 95remulcld 9689 . . . . . . . . 9
232118, 126absmuld 13593 . . . . . . . . . . 11 ..^ ..^
233 eluzelre 11193 . . . . . . . . . . . . . . . . . . 19
234233adantl 473 . . . . . . . . . . . . . . . . . 18
235 eluzle 11195 . . . . . . . . . . . . . . . . . . 19
236235adantl 473 . . . . . . . . . . . . . . . . . 18
23732nnred 10646 . . . . . . . . . . . . . . . . . . . 20
238237adantr 472 . . . . . . . . . . . . . . . . . . 19
239 elicopnf 11755 . . . . . . . . . . . . . . . . . . 19
240238, 239syl 17 . . . . . . . . . . . . . . . . . 18
241234, 236, 240mpbir2and 936 . . . . . . . . . . . . . . . . 17
242241ex 441 . . . . . . . . . . . . . . . 16
243242ssrdv 3424 . . . . . . . . . . . . . . 15
24432nnzd 11062 . . . . . . . . . . . . . . . . 17
24549peano2zd 11066 . . . . . . . . . . . . . . . . 17
246103rpred 11364 . . . . . . . . . . . . . . . . . 18
2474nnred 10646 . . . . . . . . . . . . . . . . . 18
248 dchrisumlem2.2 . . . . . . . . . . . . . . . . . 18
249 dchrisumlem2.3 . . . . . . . . . . . . . . . . . 18
250237, 246, 247, 248, 249letrd 9809 . . . . . . . . . . . . . . . . 17
251 eluz2 11188 . . . . . . . . . . . . . . . . 17
252244, 245, 250, 251syl3anbrc 1214 . . . . . . . . . . . . . . . 16
253 uztrn 11199 . . . . . . . . . . . . . . . 16
2549, 252, 253syl2anc 673 . . . . . . . . . . . . . . 15
255243, 254sseldd 3419 . . . . . . . . . . . . . 14
256115simprd 470 . . . . . . . . . . . . . 14
257255, 256mpd 15 . . . . . . . . . . . . 13
258117, 257absidd 13561 . . . . . . . . . . . 12
259258oveq1d 6323 . . . . . . . . . . 11 ..^ ..^
260232, 259eqtrd 2505 . . . . . . . . . 10 ..^ ..^
261126abscld 13575 . . . . . . . . . . 11 ..^
262113nnnn0d 10949 . . . . . . . . . . . 12
263 dchrisum.10 . . . . . . . . . . . . 13 ..^ ..^
26419, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 24406 . . . . . . . . . . . 12 ..^
265262, 264mpdan 681 . . . . . . . . . . 11 ..^
266261, 95, 117, 257, 265lemul2ad 10569 . . . . . . . . . 10 ..^
267260, 266eqbrtrd 4416 . . . . . . . . 9 ..^
268128, 133absmuld 13593 . . . . . . . . . . 11 ..^ ..^
269243, 252sseldd 3419 . . . . . . . . . . . . . 14
27019, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36dchrisumlema 24405 . . . . . . . . . . . . . . 15
271270simprd 470 . . . . . . . . . . . . . 14
272269, 271mpd 15 . . . . . . . . . . . . 13
273101, 272absidd 13561 . . . . . . . . . . . 12
274273oveq1d 6323 . . . . . . . . . . 11 ..^ ..^
275268, 274eqtrd 2505 . . . . . . . . . 10 ..^ ..^
276133abscld 13575 . . . . . . . . . . 11 ..^
2774nnnn0d 10949 . . . . . . . . . . . 12
27819, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 24406 . . . . . . . . . . . 12 ..^
279277, 278mpdan 681 . . . . . . . . . . 11 ..^
280276, 95, 101, 272, 279lemul2ad 10569 . . . . . . . . . 10 ..^
281275, 280eqbrtrd 4416 . . . . . . . . 9 ..^
282226, 227, 230, 231, 267, 281le2addd 10253 . . . . . . . 8 ..^ ..^
28395recnd 9687 . . . . . . . . 9
284118, 128, 283adddird 9686 . . . . . . . 8
285282, 284breqtrrd 4422 . . . . . . 7 ..^ ..^
286136, 228, 218, 229, 285letrd 9809 . . . . . 6 ..^ ..^
287156abscld 13575 . . . . . . . 8 ..^ ..^
28883, 287fsumrecl 13877 . . . . . . 7 ..^ ..^
28983, 156fsumabs 13938 . . . . . . 7 ..^ ..^ ..^ ..^
29095adantr 472 . . . . . . . . . 10 ..^
291222, 290remulcld 9689 . . . . . . . . 9 ..^
292137, 148syldan 478 . . . . . . . . . . . 12 ..^
293153adantr 472 . . . . . . . . . . . 12 ..^ ..^
294292, 293absmuld 13593 . . . . . . . . . . 11 ..^ ..^ ..^
295 elfzouz 11951 . . . . . . . . . . . . . . 15 ..^
296 uztrn 11199 . . . . . . . . . . . . . . 15
297295, 252, 296syl2anr 486 . . . . . . . . . . . . . 14 ..^
298 eluznn 11252 . . . . . . . . . . . . . . . . 17
29932, 298sylan 479 . . . . . . . . . . . . . . . 16
300299, 139syl 17 . . . . . . . . . . . . . . 15
301299nnrpd 11362 . . . . . . . . . . . . . . . 16
302343expia 1233 . . . . . . . . . . . . . . . . . 18
303302ralrimivva 2814 . . . . . . . . . . . . . . . . 17
304303adantr 472 . . . . . . . . . . . . . . . 16
305 nfcv 2612 . . . . . . . . . . . . . . . . . 18
306 nfv 1769 . . . . . . . . . . . . . . . . . . 19
307 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
308 nfcv 2612 . . . . . . . . . . . . . . . . . . . 20
309307, 308, 60nfbr 4440 . . . . . . . . . . . . . . . . . . 19
310306, 309nfim 2023 . . . . . . . . . . . . . . . . . 18
311305, 310nfral 2789 . . . . . . . . . . . . . . . . 17
312 breq2 4399 . . . . . . . . . . . . . . . . . . . 20
313 breq1 4398 . . . . . . . . . . . . . . . . . . . 20
314312, 313anbi12d 725 . . . . . . . . . . . . . . . . . . 19
31564breq2d 4407 . . . . . . . . . . . . . . . . . . 19
316314, 315imbi12d 327 . . . . . . . . . . . . . . . . . 18
317316ralbidv 2829 . . . . . . . . . . . . . . . . 17
318311, 317rspc 3130 . . . . . . . . . . . . . . . 16
319301, 304, 318sylc 61 . . . . . . . . . . . . . . 15
320234lep1d 10560 . . . . . . . . . . . . . . . 16
321236, 320jca 541 . . . . . . . . . . . . . . 15
322 breq2 4399 . . . . . . . . . . . . . . . . . 18
323322anbi2d 718 . . . . . . . . . . . . . . . . 17
324 eqvisset 3039 . . . . . . . . . . . . . . . . . . . 20
325 eqtr3 2492 . . . . . . . . . . . . . . . . . . . . 21
32631equcoms 1872 . . . . . . . . . . . . . . . . . . . . 21
327325, 326syl 17 . . . . . . . . . . . . . . . . . . . 20
328324, 327csbied 3376 . . . . . . . . . . . . . . . . . . 19
329328eqcomd 2477 . . . . . . . . . . . . . . . . . 18
330329breq1d 4405 . . . . . . . . . . . . . . . . 17
331323, 330imbi12d 327 . . . . . . . . . . . . . . . 16
332331rspcv 3132 . . . . . . . . . . . . . . 15
333300, 319, 321, 332syl3c 62 . . . . . . . . . . . . . 14
334297, 333syldan 478 . . . . . . . . . . . . 13 ..^
335221, 220, 334abssuble0d 13571 . . . . . . . . . . . 12 ..^
336335oveq1d 6323 . . . . . . . . . . 11 ..^ ..^ ..^
337294, 336eqtrd 2505 . . . . . . . . . 10 ..^ ..^ ..^
338293abscld 13575 . . . . . . . . . . 11 ..^ ..^
339220, 221subge0d 10224 . . . . . . . . . . . 12 ..^
340334, 339mpbird 240 . . . . . . . . . . 11 ..^
341137peano2nnd 10648 . . . . . . . . . . . . 13 ..^
342341nnnn0d 10949 . . . . . . . . . . . 12 ..^
34319, 21, 28, 18, 20, 29, 22, 30, 31, 32, 33, 34, 35, 36, 95, 263dchrisumlem1 24406 . . . . . . . . . . . 12 ..^
344342, 343syldan 478 . . . . . . . . . . 11 ..^ ..^
345338, 290, 222, 340, 344lemul2ad 10569 . . . . . . . . . 10 ..^ ..^
346337, 345eqbrtrd 4416 . . . . . . . . 9 ..^ ..^
34783, 287, 291, 346fsumle 13936 . . . . . . . 8 ..^ ..^ ..^
348222recnd 9687 . . . . . . . . . 10 ..^
34983, 283, 348fsummulc1 13923 . . . . . . . . 9 ..^ ..^
350219oveq1d 6323 . . . . . . . . 9 ..^
351349, 350eqtr3d 2507 . . . . . . . 8 ..^
352347, 351breqtrd 4420 . . . . . . 7 ..^ ..^
353158, 288, 225, 289, 352letrd 9809 . . . . . 6 ..^ ..^
354136, 158, 218, 225, 286, 353le2addd 10253 . . . . 5 ..^ ..^ ..^ ..^
3551282timesd 10878 . . . . . . . 8
356128, 118, 128ppncand 10045 . . . . . . . 8
357128, 118addcomd 9853 . . . . . . . . 9
358357oveq1d 6323 . . . . . . . 8
359355, 356, 3583eqtr2d 2511 . . . . . . 7
360359oveq1d 6323 . . . . . 6
361 2cnd 10704 . . . . . . 7
362361, 128, 283mul32d 9861 . . . . . 6
363217recnd 9687 . . . . . . 7
364224recnd 9687 . . . . . . 7
365363, 364, 283adddird 9686 . . . . . 6
366360, 362, 3653eqtr3d 2513 . . . . 5
367354, 366breqtrrd 4422 . . . 4 ..^ ..^ ..^ ..^
36892, 159, 102, 216, 367letrd 9809 . . 3 ..^
369 2nn0 10910 . . . . . 6
370 nn0ge0 10919 . . . . . 6
371369, 370mp1i 13 . . . . 5
372 0red 9662 . . . . . 6
373126absge0d 13583 . . . . . 6 ..^
374372, 261, 95, 373, 265letrd 9809 . . . . 5
37594, 95, 371, 374mulge0d 10211 . . . 4
3764nnrpd 11362 . . . . 5
377 nfv 1769 . . . . . . . . 9
378307, 308, 105nfbr 4440 . . . . . . . . 9
379377, 378nfim 2023 . . . . . . . 8
380305, 379nfral 2789 . . . . . . 7
381 breq2 4399 . . . . . . . . . 10
382 breq1 4398 . . . . . . . . . 10
383381, 382anbi12d 725 . . . . . . . . 9
384107breq2d 4407 . . . . . . . . 9
385383, 384imbi12d 327 . . . . . . . 8
386385ralbidv 2829 . . . . . . 7
387380, 386rspc 3130 . . . . . 6
388103, 303, 387sylc 61 . . . . 5
389248, 249jca 541 . . . . 5
390 breq2 4399 . . . . . . . 8
391390anbi2d 718 . . . . . . 7
392 eqvisset 3039 . . . . . . . . . 10
393 eqtr3 2492 . . . . . . . . . . 11
394393, 326syl 17 . . . . . . . . . 10
395392, 394csbied 3376 . . . . . . . . 9
396395eqcomd 2477 . . . . . . . 8
397396breq1d 4405 . . . . . . 7
398391, 397imbi12d 327 . . . . . 6
399398rspcv 3132 . . . . 5
400376, 388, 389, 399syl3c 62 . . . 4
401101, 110, 96, 375, 400lemul2ad 10569 . . 3
40292, 102, 111, 368, 401letrd 9809 . 2 ..^
40391, 402eqbrtrd 4416 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   w3a 1007   wceq 1452   wcel 1904   wne 2641  wral 2756  cvv 3031  csb 3349   cun 3388   cin 3389  c0 3722   class class class wbr 4395   cmpt 4454  cfv 5589  (class class class)co 6308  cfn 7587  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562   cpnf 9690   cle 9694   cmin 9880  cn 10631  c2 10681  cn0 10893  cz 10961  cuz 11182  crp 11325  cico 11662  cfz 11810  ..^cfzo 11942   cseq 12251  cabs 13374   crli 13626  csu 13829  cbs 15199  c0g 15416  RHomczrh 19148  ℤ/nℤczn 19151 &