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

Theorem dchrvmasumiflem1 24418
 Description: Lemma for dchrvmasumif 24420. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z ℤ/n
rpvmasum.l RHom
rpvmasum.a
rpvmasum.g DChr
rpvmasum.d
rpvmasum.1
dchrisum.b
dchrisum.n1
dchrvmasumif.f
dchrvmasumif.c
dchrvmasumif.s
dchrvmasumif.1
dchrvmasumif.g
dchrvmasumif.e
dchrvmasumif.t
dchrvmasumif.2
Assertion
Ref Expression
dchrvmasumiflem1
Distinct variable groups:   ,,,   ,,,   ,,,,   ,,,,   ,,,   ,,   ,,,   ,,,   ,,,   ,,,,   ,,,   ,,,   ,,,,,   ,,,,,
Allowed substitution hints:   (,)   (,)   (,)   ()   (,)   (,)   (,)   ()   (,,,,)   (,,)   (,)   (,)

Proof of Theorem dchrvmasumiflem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 rpvmasum.z . 2 ℤ/n
2 rpvmasum.l . 2 RHom
3 rpvmasum.a . 2
4 rpvmasum.g . 2 DChr
5 rpvmasum.d . 2
6 rpvmasum.1 . 2
7 dchrisum.b . 2
8 dchrisum.n1 . 2
9 fzfid 12224 . . 3
10 simpl 464 . . . . 5
11 elfznn 11854 . . . . 5
127adantr 472 . . . . . 6
13 nnz 10983 . . . . . . 7
1413adantl 473 . . . . . 6
154, 1, 5, 2, 12, 14dchrzrhcl 24252 . . . . 5
1610, 11, 15syl2an 485 . . . 4
17 simpr 468 . . . . . . . 8
1811nnrpd 11362 . . . . . . . 8
19 ifcl 3914 . . . . . . . 8
2017, 18, 19syl2an 485 . . . . . . 7
2120relogcld 23651 . . . . . 6
2211adantl 473 . . . . . 6
2321, 22nndivred 10680 . . . . 5
2423recnd 9687 . . . 4
2516, 24mulcld 9681 . . 3
269, 25fsumcl 13876 . 2
27 fveq2 5879 . . . 4
2827oveq2d 6324 . . 3
29 ifeq1 3876 . . . . . . 7
3029fveq2d 5883 . . . . . 6
3130oveq1d 6323 . . . . 5
3231oveq2d 6324 . . . 4
3428, 33sumeq12rdv 13850 . 2
35 dchrvmasumif.c . . 3
36 dchrvmasumif.e . . 3
3735, 36ifcld 3915 . 2
38 0cn 9653 . . 3
39 dchrvmasumif.t . . . 4
40 climcl 13640 . . . 4
4139, 40syl 17 . . 3
42 ifcl 3914 . . 3
4338, 41, 42sylancr 676 . 2
44 nnuz 11218 . . . . . . . . 9
45 1zzd 10992 . . . . . . . . 9
46 nncn 10639 . . . . . . . . . . . . 13
4746adantl 473 . . . . . . . . . . . 12
48 nnne0 10664 . . . . . . . . . . . . 13
4948adantl 473 . . . . . . . . . . . 12
5015, 47, 49divcld 10405 . . . . . . . . . . 11
51 dchrvmasumif.f . . . . . . . . . . . 12
52 fveq2 5879 . . . . . . . . . . . . . . 15
5352fveq2d 5883 . . . . . . . . . . . . . 14
54 id 22 . . . . . . . . . . . . . 14
5553, 54oveq12d 6326 . . . . . . . . . . . . 13
5655cbvmptv 4488 . . . . . . . . . . . 12
5751, 56eqtri 2493 . . . . . . . . . . 11
5850, 57fmptd 6061 . . . . . . . . . 10
59 ffvelrn 6035 . . . . . . . . . 10
6058, 59sylan 479 . . . . . . . . 9
6144, 45, 60serf 12279 . . . . . . . 8
6261ad2antrr 740 . . . . . . 7
63 3re 10705 . . . . . . . . . . 11
64 elicopnf 11755 . . . . . . . . . . 11
6563, 64mp1i 13 . . . . . . . . . 10
6665simprbda 635 . . . . . . . . 9
67 1red 9676 . . . . . . . . . 10
6863a1i 11 . . . . . . . . . 10
69 1le3 10849 . . . . . . . . . . 11
7069a1i 11 . . . . . . . . . 10
7165simplbda 636 . . . . . . . . . 10
7267, 68, 66, 70, 71letrd 9809 . . . . . . . . 9
73 flge1nn 12088 . . . . . . . . 9
7466, 72, 73syl2anc 673 . . . . . . . 8
7574adantr 472 . . . . . . 7
7662, 75ffvelrnd 6038 . . . . . 6
7776abscld 13575 . . . . 5
78 simpl 464 . . . . . . . 8
79 0red 9662 . . . . . . . . . 10
80 3pos 10725 . . . . . . . . . . 11
8180a1i 11 . . . . . . . . . 10
8279, 68, 66, 81, 71ltletrd 9812 . . . . . . . . 9
8366, 82elrpd 11361 . . . . . . . 8
8478, 83jca 541 . . . . . . 7
85 elrege0 11764 . . . . . . . . . 10
8685simplbi 467 . . . . . . . . 9
8735, 86syl 17 . . . . . . . 8
88 rerpdivcl 11353 . . . . . . . 8
8987, 88sylan 479 . . . . . . 7
9084, 89syl 17 . . . . . 6
9190adantr 472 . . . . 5
9283relogcld 23651 . . . . . . 7
9366, 72logge0d 23658 . . . . . . 7
9492, 93jca 541 . . . . . 6
9594adantr 472 . . . . 5
96 oveq2 6316 . . . . . . . 8
9761adantr 472 . . . . . . . . . 10
9897, 74ffvelrnd 6038 . . . . . . . . 9
9998subid1d 9994 . . . . . . . 8
10096, 99sylan9eqr 2527 . . . . . . 7
101100fveq2d 5883 . . . . . 6
102 1re 9660 . . . . . . . . . 10
103 elicopnf 11755 . . . . . . . . . 10
104102, 103ax-mp 5 . . . . . . . . 9
10566, 72, 104sylanbrc 677 . . . . . . . 8
106 dchrvmasumif.1 . . . . . . . . 9
107106adantr 472 . . . . . . . 8
108 fveq2 5879 . . . . . . . . . . . . 13
109108fveq2d 5883 . . . . . . . . . . . 12
110109oveq1d 6323 . . . . . . . . . . 11
111110fveq2d 5883 . . . . . . . . . 10
112 oveq2 6316 . . . . . . . . . 10
113111, 112breq12d 4408 . . . . . . . . 9
114113rspcv 3132 . . . . . . . 8
115105, 107, 114sylc 61 . . . . . . 7
116115adantr 472 . . . . . 6
117101, 116eqbrtrrd 4418 . . . . 5
118 lemul2a 10482 . . . . 5
11977, 91, 95, 117, 118syl31anc 1295 . . . 4
120 iftrue 3878 . . . . . . . . . . . . . . 15
121120fveq2d 5883 . . . . . . . . . . . . . 14
122121oveq1d 6323 . . . . . . . . . . . . 13
123122ad2antlr 741 . . . . . . . . . . . 12
124123oveq2d 6324 . . . . . . . . . . 11
12516adantlr 729 . . . . . . . . . . . 12
126 relogcl 23604 . . . . . . . . . . . . . . 15
127126adantl 473 . . . . . . . . . . . . . 14
128127recnd 9687 . . . . . . . . . . . . 13
129128ad2antrr 740 . . . . . . . . . . . 12
13011adantl 473 . . . . . . . . . . . . 13
131130nncnd 10647 . . . . . . . . . . . 12
132130nnne0d 10676 . . . . . . . . . . . 12
133125, 129, 131, 132div12d 10441 . . . . . . . . . . 11
134124, 133eqtrd 2505 . . . . . . . . . 10
135134sumeq2dv 13846 . . . . . . . . 9
136 iftrue 3878 . . . . . . . . . . 11
137136oveq2d 6324 . . . . . . . . . 10
13826subid1d 9994 . . . . . . . . . 10
139137, 138sylan9eqr 2527 . . . . . . . . 9
140 ovex 6336 . . . . . . . . . . . . . 14
14155, 51, 140fvmpt 5963 . . . . . . . . . . . . 13
14222, 141syl 17 . . . . . . . . . . . 12
14358adantr 472 . . . . . . . . . . . . 13
144143, 11, 59syl2an 485 . . . . . . . . . . . 12
145142, 144eqeltrrd 2550 . . . . . . . . . . 11
1469, 128, 145fsummulc2 13922 . . . . . . . . . 10
147146adantr 472 . . . . . . . . 9
148135, 139, 1473eqtr4d 2515 . . . . . . . 8
14984, 148sylan 479 . . . . . . 7
15084, 142sylan 479 . . . . . . . . . 10
15174, 44syl6eleq 2559 . . . . . . . . . 10
15278, 11, 50syl2an 485 . . . . . . . . . 10
153150, 151, 152fsumser 13873 . . . . . . . . 9
154153adantr 472 . . . . . . . 8
155154oveq2d 6324 . . . . . . 7
156149, 155eqtrd 2505 . . . . . 6
157156fveq2d 5883 . . . . 5
158126ad2antlr 741 . . . . . . . 8
159158recnd 9687 . . . . . . 7
16084, 159sylan 479 . . . . . 6
161160, 76absmuld 13593 . . . . 5
16292, 93absidd 13561 . . . . . . 7
163162oveq1d 6323 . . . . . 6
164163adantr 472 . . . . 5
165157, 161, 1643eqtrd 2509 . . . 4
166 iftrue 3878 . . . . . . . 8
167166adantl 473 . . . . . . 7
168167oveq1d 6323 . . . . . 6
16987recnd 9687 . . . . . . . 8
170169ad2antrr 740 . . . . . . 7
171 rpcnne0 11342 . . . . . . . 8
172171ad2antlr 741 . . . . . . 7
173 div12 10314 . . . . . . 7
174170, 159, 172, 173syl3anc 1292 . . . . . 6
175168, 174eqtrd 2505 . . . . 5
17684, 175sylan 479 . . . 4
177119, 165, 1763brtr4d 4426 . . 3
178 dchrvmasumif.2 . . . . . 6
179108fveq2d 5883 . . . . . . . . . 10
180179oveq1d 6323 . . . . . . . . 9
181180fveq2d 5883 . . . . . . . 8
182 fveq2 5879 . . . . . . . . . 10
183 id 22 . . . . . . . . . 10
184182, 183oveq12d 6326 . . . . . . . . 9
185184oveq2d 6324 . . . . . . . 8
186181, 185breq12d 4408 . . . . . . 7
187186rspccva 3135 . . . . . 6
188178, 187sylan 479 . . . . 5
189188adantr 472 . . . 4
190 fveq2 5879 . . . . . . . . . . . 12
191190, 54oveq12d 6326 . . . . . . . . . . 11
19253, 191oveq12d 6326 . . . . . . . . . 10
193 dchrvmasumif.g . . . . . . . . . 10
194 ovex 6336 . . . . . . . . . 10
195192, 193, 194fvmpt 5963 . . . . . . . . 9
19611, 195syl 17 . . . . . . . 8
197 ifnefalse 3884 . . . . . . . . . . . . 13
198197fveq2d 5883 . . . . . . . . . . . 12
199198oveq1d 6323 . . . . . . . . . . 11
200199oveq2d 6324 . . . . . . . . . 10
201200adantl 473 . . . . . . . . 9
202201eqcomd 2477 . . . . . . . 8
203196, 202sylan9eqr 2527 . . . . . . 7
204151adantr 472 . . . . . . 7
205 nnrp 11334 . . . . . . . . . . . . . . . 16
206205adantl 473 . . . . . . . . . . . . . . 15
207206relogcld 23651 . . . . . . . . . . . . . 14
208207recnd 9687 . . . . . . . . . . . . 13
209208, 47, 49divcld 10405 . . . . . . . . . . . 12
21015, 209mulcld 9681 . . . . . . . . . . 11
211192cbvmptv 4488 . . . . . . . . . . . 12
212193, 211eqtri 2493 . . . . . . . . . . 11
213210, 212fmptd 6061 . . . . . . . . . 10
214213ad2antrr 740 . . . . . . . . 9
215 ffvelrn 6035 . . . . . . . . 9
216214, 11, 215syl2an 485 . . . . . . . 8
217203, 216eqeltrrd 2550 . . . . . . 7
218203, 204, 217fsumser 13873 . . . . . 6
219 ifnefalse 3884 . . . . . . 7
220219adantl 473 . . . . . 6
221218, 220oveq12d 6326 . . . . 5
222221fveq2d 5883 . . . 4
223 ifnefalse 3884 . . . . . 6
224223adantl 473 . . . . 5
225224oveq1d 6323 . . . 4
226189, 222, 2253brtr4d 4426 . . 3
227177, 226pm2.61dane 2730 . 2
228 fzfid 12224 . . . 4
2297adantr 472 . . . . . . 7
230 elfzelz 11826 . . . . . . . 8
231230adantl 473 . . . . . . 7
2324, 1, 5, 2, 229, 231dchrzrhcl 24252 . . . . . 6
233232abscld 13575 . . . . 5
23463, 80elrpii 11328 . . . . . . 7
235 relogcl 23604 . . . . . . 7
236234, 235ax-mp 5 . . . . . 6
237 elfznn 11854 . . . . . . 7
238237adantl 473 . . . . . 6
239 nndivre 10667 . . . . . 6
240236, 238, 239sylancr 676 . . . . 5
241233, 240remulcld 9689 . . . 4
242228, 241fsumrecl 13877 . . 3
24343abscld 13575 . . 3
245 simpl 464 . . . . . . 7
24663rexri 9711 . . . . . . . . . . 11
247 elico2 11723 . . . . . . . . . . 11
248102, 246, 247mp2an 686 . . . . . . . . . 10
249248simp1bi 1045 . . . . . . . . 9
250249adantl 473 . . . . . . . 8
251 0red 9662 . . . . . . . . 9
252 1red 9676 . . . . . . . . 9
253 0lt1 10157 . . . . . . . . . 10
254253a1i 11 . . . . . . . . 9
255248simp2bi 1046 . . . . . . . . . 10
256255adantl 473 . . . . . . . . 9
257251, 252, 250, 254, 256ltletrd 9812 . . . . . . . 8
258250, 257elrpd 11361 . . . . . . 7
259245, 258jca 541 . . . . . 6
26043adantr 472 . . . . . . 7
26126, 260subcld 10005 . . . . . 6
262259, 261syl 17 . . . . 5
263262abscld 13575 . . . 4
264259, 26syl 17 . . . . . 6
265264abscld 13575 . . . . 5
266243adantr 472 . . . . 5
267265, 266readdcld 9688 . . . 4
268242adantr 472 . . . . 5
269268, 266readdcld 9688 . . . 4
27026, 260abs2dif2d 13597 . . . . 5
271259, 270syl 17 . . . 4
27225abscld 13575 . . . . . . . 8
2739, 272fsumrecl 13877 . . . . . . 7
274259, 273syl 17 . . . . . 6
2759, 25fsumabs 13938 . . . . . . 7
276259, 275syl 17 . . . . . 6
277 fzfid 12224 . . . . . . . . 9
278232adantlr 729 . . . . . . . . . . 11
27917adantr 472 . . . . . . . . . . . . . . 15
280237adantl 473 . . . . . . . . . . . . . . . 16
281280nnrpd 11362 . . . . . . . . . . . . . . 15
282279, 281ifcld 3915 . . . . . . . . . . . . . 14
283282relogcld 23651 . . . . . . . . . . . . 13
284283, 280nndivred 10680 . . . . . . . . . . . 12
285284recnd 9687 . . . . . . . . . . 11
286278, 285mulcld 9681 . . . . . . . . . 10
287286abscld 13575 . . . . . . . . 9
288277, 287fsumrecl 13877 . . . . . . . 8
289259, 288syl 17 . . . . . . 7
290 fzfid 12224 . . . . . . . 8
291259, 286sylan 479 . . . . . . . . 9
292291abscld 13575 . . . . . . . 8
293291absge0d 13583 . . . . . . . 8
294250flcld 12067 . . . . . . . . . 10
295 2z 10993 . . . . . . . . . . 11
296295a1i 11 . . . . . . . . . 10
297248simp3bi 1047 . . . . . . . . . . . . . 14
298297adantl 473 . . . . . . . . . . . . 13
299 3z 10994 . . . . . . . . . . . . . 14
300 fllt 12075 . . . . . . . . . . . . . 14
301250, 299, 300sylancl 675 . . . . . . . . . . . . 13
302298, 301mpbid 215 . . . . . . . . . . . 12
303 df-3 10691 . . . . . . . . . . . 12
304302, 303syl6breq 4435 . . . . . . . . . . 11
305 rpre 11331 . . . . . . . . . . . . . . 15
306305adantl 473 . . . . . . . . . . . . . 14
307306flcld 12067 . . . . . . . . . . . . 13
308 zleltp1 11011 . . . . . . . . . . . . 13
309307, 295, 308sylancl 675 . . . . . . . . . . . 12
310259, 309syl 17 . . . . . . . . . . 11
311304, 310mpbird 240 . . . . . . . . . 10
312 eluz2 11188 . . . . . . . . . 10
313294, 296, 311, 312syl3anbrc 1214 . . . . . . . . 9
314 fzss2 11864 . . . . . . . . 9
315313, 314syl 17 . . . . . . . 8
316290, 292, 293, 315fsumless 13933 . . . . . . 7
317241adantlr 729 . . . . . . . 8
318278, 285absmuld 13593 . . . . . . . . . 10
319259, 318sylan 479 . . . . . . . . 9
320259, 284sylan 479 . . . . . . . . . . . 12
321259, 283sylan 479 . . . . . . . . . . . . 13
322 log1 23614 . . . . . . . . . . . . . 14
323 elfzle1 11828 . . . . . . . . . . . . . . . 16
324 breq2 4399 . . . . . . . . . . . . . . . . 17
325 breq2 4399 . . . . . . . . . . . . . . . . 17
326324, 325ifboth 3908 . . . . . . . . . . . . . . . 16
327256, 323, 326syl2an 485 . . . . . . . . . . . . . . 15
328 1rp 11329 . . . . . . . . . . . . . . . . 17
329 logleb 23631 . . . . . . . . . . . . . . . . 17
330328, 282, 329sylancr 676 . . . . . . . . . . . . . . . 16
331259, 330sylan 479 . . . . . . . . . . . . . . 15
332327, 331mpbid 215 . . . . . . . . . . . . . 14
333322, 332syl5eqbrr 4430 . . . . . . . . . . . . 13
334281rpregt0d 11370 . . . . . . . . . . . . . 14
335259, 334sylan 479 . . . . . . . . . . . . 13
336 divge0 10496 . . . . . . . . . . . . 13
337321, 333, 335, 336syl21anc 1291 . . . . . . . . . . . 12
338320, 337absidd 13561 . . . . . . . . . . 11
339338, 320eqeltrd 2549 . . . . . . . . . 10
340240adantlr 729 . . . . . . . . . 10
341233adantlr 729 . . . . . . . . . . . 12
342278absge0d 13583 . . . . . . . . . . . 12
343341, 342jca 541 . . . . . . . . . . 11
344259, 343sylan 479 . . . . . . . . . 10
345297ad2antlr 741 . . . . . . . . . . . . . . 15
346280nnred 10646 . . . . . . . . . . . . . . . . 17
347 2re 10701 . . . . . . . . . . . . . . . . . 18
348347a1i 11 . . . . . . . . . . . . . . . . 17
34963a1i 11 . . . . . . . . . . . . . . . . 17
350 elfzle2 11829 . . . . . . . . . . . . . . . . . 18
351350adantl 473 . . . . . . . . . . . . . . . . 17
352 2lt3 10800 . . . . . . . . . . . . . . . . . 18
353352a1i 11 . . . . . . . . . . . . . . . . 17
354346, 348, 349, 351, 353lelttrd 9810 . . . . . . . . . . . . . . . 16
355259, 354sylan 479 . . . . . . . . . . . . . . 15
356 breq1 4398 . . . . . . . . . . . . . . . 16
357 breq1 4398 . . . . . . . . . . . . . . . 16
358356, 357ifboth 3908 . . . . . . . . . . . . . . 15
359345, 355, 358syl2anc 673 . . . . . . . . . . . . . 14
360282rpred 11364 . . . . . . . . . . . . . . . 16
361 ltle 9740 . . . . . . . . . . . . . . . 16
362360, 63, 361sylancl 675 . . . . . . . . . . . . . . 15
363259, 362sylan 479 . . . . . . . . . . . . . 14
364359, 363mpd 15 . . . . . . . . . . . . 13
365 logleb 23631 . . . . . . . . . . . . . . 15
366282, 234, 365sylancl 675 . . . . . . . . . . . . . 14
367259, 366sylan 479 . . . . . . . . . . . . 13
368364, 367mpbid 215 . . . . . . . . . . . 12
369236a1i 11 . . . . . . . . . . . . . 14
370283, 369, 281lediv1d 11407 . . . . . . . . . . . . 13
371259, 370sylan 479 . . . . . . . . . . . 12
372368, 371mpbid 215 . . . . . . . . . . 11
373338, 372eqbrtrd 4416 . . . . . . . . . 10
374 lemul2a 10482 . . . . . . . . . 10
375339, 340, 344, 373, 374syl31anc 1295 . . . . . . . . 9
376319, 375eqbrtrd 4416 . . . . . . . 8
377290, 292, 317, 376fsumle 13936 . . . . . . 7
378274, 289, 268, 316, 377letrd 9809 . . . . . 6
379265, 274, 268, 276, 378letrd 9809 . . . . 5
38026abscld 13575 . . . . . . 7
381242adantr 472 . . . . . . 7
382260abscld 13575 . . . . . . 7
383380, 381, 382leadd1d 10228 . . . . . 6
384259, 383syl 17 . . . . 5
385379, 384mpbid 215 . . . 4
386263, 267, 269, 271, 385letrd 9809 . . 3