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

Theorem dchrvmasumiflem1 21200
 Description: Lemma for dchrvmasumif 21202. (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 11317 . . 3
10 simpl 445 . . . . 5
11 elfznn 11085 . . . . 5
127adantr 453 . . . . . 6
13 nnz 10308 . . . . . . 7
1413adantl 454 . . . . . 6
154, 1, 5, 2, 12, 14dchrzrhcl 21034 . . . . 5
1610, 11, 15syl2an 465 . . . 4
17 simpr 449 . . . . . . . 8
1811nnrpd 10652 . . . . . . . 8
19 ifcl 3777 . . . . . . . 8
2017, 18, 19syl2an 465 . . . . . . 7
2120relogcld 20523 . . . . . 6
2211adantl 454 . . . . . 6
2321, 22nndivred 10053 . . . . 5
2423recnd 9119 . . . 4
2516, 24mulcld 9113 . . 3
269, 25fsumcl 12532 . 2
27 fveq2 5731 . . . 4
2827oveq2d 6100 . . 3
29 ifeq1 3745 . . . . . . 7
3029fveq2d 5735 . . . . . 6
3130oveq1d 6099 . . . . 5
3231oveq2d 6100 . . . 4
3428, 33sumeq12rdv 12506 . 2
35 dchrvmasumif.c . . . 4
37 dchrvmasumif.e . . . 4
3936, 38ifclda 3768 . 2
40 0cn 9089 . . 3
41 dchrvmasumif.t . . . 4
42 climcl 12298 . . . 4
4341, 42syl 16 . . 3
44 ifcl 3777 . . 3
4540, 43, 44sylancr 646 . 2
46 nnuz 10526 . . . . . . . . 9
47 1z 10316 . . . . . . . . . 10
4847a1i 11 . . . . . . . . 9
49 nncn 10013 . . . . . . . . . . . . 13
5049adantl 454 . . . . . . . . . . . 12
51 nnne0 10037 . . . . . . . . . . . . 13
5251adantl 454 . . . . . . . . . . . 12
5315, 50, 52divcld 9795 . . . . . . . . . . 11
54 dchrvmasumif.f . . . . . . . . . . . 12
55 fveq2 5731 . . . . . . . . . . . . . . 15
5655fveq2d 5735 . . . . . . . . . . . . . 14
57 id 21 . . . . . . . . . . . . . 14
5856, 57oveq12d 6102 . . . . . . . . . . . . 13
5958cbvmptv 4303 . . . . . . . . . . . 12
6054, 59eqtri 2458 . . . . . . . . . . 11
6153, 60fmptd 5896 . . . . . . . . . 10
62 ffvelrn 5871 . . . . . . . . . 10
6361, 62sylan 459 . . . . . . . . 9
6446, 48, 63serf 11356 . . . . . . . 8
6564ad2antrr 708 . . . . . . 7
66 3re 10076 . . . . . . . . . . 11
67 elicopnf 11005 . . . . . . . . . . 11
6866, 67mp1i 12 . . . . . . . . . 10
6968simprbda 608 . . . . . . . . 9
70 1re 9095 . . . . . . . . . . 11
7170a1i 11 . . . . . . . . . 10
7266a1i 11 . . . . . . . . . 10
73 1lt3 10149 . . . . . . . . . . . 12
7470, 66, 73ltleii 9201 . . . . . . . . . . 11
7574a1i 11 . . . . . . . . . 10
7668simplbda 609 . . . . . . . . . 10
7771, 72, 69, 75, 76letrd 9232 . . . . . . . . 9
78 flge1nn 11231 . . . . . . . . 9
7969, 77, 78syl2anc 644 . . . . . . . 8
8079adantr 453 . . . . . . 7
8165, 80ffvelrnd 5874 . . . . . 6
8281abscld 12243 . . . . 5
83 simpl 445 . . . . . . . 8
84 0re 9096 . . . . . . . . . . 11
8584a1i 11 . . . . . . . . . 10
86 3pos 10089 . . . . . . . . . . 11
8786a1i 11 . . . . . . . . . 10
8885, 72, 69, 87, 76ltletrd 9235 . . . . . . . . 9
8969, 88elrpd 10651 . . . . . . . 8
9083, 89jca 520 . . . . . . 7
91 elrege0 11012 . . . . . . . . . 10
9291simplbi 448 . . . . . . . . 9
9335, 92syl 16 . . . . . . . 8
94 rerpdivcl 10644 . . . . . . . 8
9593, 94sylan 459 . . . . . . 7
9690, 95syl 16 . . . . . 6
9796adantr 453 . . . . 5
9889relogcld 20523 . . . . . . 7
9969, 77logge0d 20530 . . . . . . 7
10098, 99jca 520 . . . . . 6
101100adantr 453 . . . . 5
102 oveq2 6092 . . . . . . . 8
10364adantr 453 . . . . . . . . . 10
104103, 79ffvelrnd 5874 . . . . . . . . 9
105104subid1d 9405 . . . . . . . 8
106102, 105sylan9eqr 2492 . . . . . . 7
107106fveq2d 5735 . . . . . 6
108 elicopnf 11005 . . . . . . . . . 10
10970, 108ax-mp 5 . . . . . . . . 9
11069, 77, 109sylanbrc 647 . . . . . . . 8
111 dchrvmasumif.1 . . . . . . . . 9
112111adantr 453 . . . . . . . 8
113 fveq2 5731 . . . . . . . . . . . . 13
114113fveq2d 5735 . . . . . . . . . . . 12
115114oveq1d 6099 . . . . . . . . . . 11
116115fveq2d 5735 . . . . . . . . . 10
117 oveq2 6092 . . . . . . . . . 10
118116, 117breq12d 4228 . . . . . . . . 9
119118rspcv 3050 . . . . . . . 8
120110, 112, 119sylc 59 . . . . . . 7
121120adantr 453 . . . . . 6
122107, 121eqbrtrrd 4237 . . . . 5
123 lemul2a 9870 . . . . 5
12482, 97, 101, 122, 123syl31anc 1188 . . . 4
125 iftrue 3747 . . . . . . . . . . . . . . 15
126125fveq2d 5735 . . . . . . . . . . . . . 14
127126oveq1d 6099 . . . . . . . . . . . . 13
128127ad2antlr 709 . . . . . . . . . . . 12
129128oveq2d 6100 . . . . . . . . . . 11
13016adantlr 697 . . . . . . . . . . . 12
131 relogcl 20478 . . . . . . . . . . . . . . 15
132131adantl 454 . . . . . . . . . . . . . 14
133132recnd 9119 . . . . . . . . . . . . 13
134133ad2antrr 708 . . . . . . . . . . . 12
13511adantl 454 . . . . . . . . . . . . 13
136135nncnd 10021 . . . . . . . . . . . 12
137135nnne0d 10049 . . . . . . . . . . . 12
138130, 134, 136, 137div12d 9831 . . . . . . . . . . 11
139129, 138eqtrd 2470 . . . . . . . . . 10
140139sumeq2dv 12502 . . . . . . . . 9
141 iftrue 3747 . . . . . . . . . . 11
142141oveq2d 6100 . . . . . . . . . 10
14326subid1d 9405 . . . . . . . . . 10
144142, 143sylan9eqr 2492 . . . . . . . . 9
145 ovex 6109 . . . . . . . . . . . . . 14
14658, 54, 145fvmpt 5809 . . . . . . . . . . . . 13
14722, 146syl 16 . . . . . . . . . . . 12
14861adantr 453 . . . . . . . . . . . . 13
149148, 11, 62syl2an 465 . . . . . . . . . . . 12
150147, 149eqeltrrd 2513 . . . . . . . . . . 11
1519, 133, 150fsummulc2 12572 . . . . . . . . . 10
152151adantr 453 . . . . . . . . 9
153140, 144, 1523eqtr4d 2480 . . . . . . . 8
15490, 153sylan 459 . . . . . . 7
15590, 147sylan 459 . . . . . . . . . 10
15679, 46syl6eleq 2528 . . . . . . . . . 10
15783, 11, 53syl2an 465 . . . . . . . . . 10
158155, 156, 157fsumser 12529 . . . . . . . . 9
159158adantr 453 . . . . . . . 8
160159oveq2d 6100 . . . . . . 7
161154, 160eqtrd 2470 . . . . . 6
162161fveq2d 5735 . . . . 5
163131ad2antlr 709 . . . . . . . 8
164163recnd 9119 . . . . . . 7
16590, 164sylan 459 . . . . . 6
166165, 81absmuld 12261 . . . . 5
16798, 99absidd 12230 . . . . . . 7
168167oveq1d 6099 . . . . . 6
169168adantr 453 . . . . 5
170162, 166, 1693eqtrd 2474 . . . 4
171 iftrue 3747 . . . . . . . 8
172171adantl 454 . . . . . . 7
173172oveq1d 6099 . . . . . 6
17493recnd 9119 . . . . . . . 8
175174ad2antrr 708 . . . . . . 7
176 rpcnne0 10634 . . . . . . . 8
177176ad2antlr 709 . . . . . . 7
178 div12 9705 . . . . . . 7
179175, 164, 177, 178syl3anc 1185 . . . . . 6
180173, 179eqtrd 2470 . . . . 5
18190, 180sylan 459 . . . 4
182124, 170, 1813brtr4d 4245 . . 3
183 dchrvmasumif.2 . . . . . 6
184113fveq2d 5735 . . . . . . . . . 10
185184oveq1d 6099 . . . . . . . . 9
186185fveq2d 5735 . . . . . . . 8
187 fveq2 5731 . . . . . . . . . 10
188 id 21 . . . . . . . . . 10
189187, 188oveq12d 6102 . . . . . . . . 9
190189oveq2d 6100 . . . . . . . 8
191186, 190breq12d 4228 . . . . . . 7
192191rspccva 3053 . . . . . 6
193183, 192sylan 459 . . . . 5
194193adantr 453 . . . 4
195 fveq2 5731 . . . . . . . . . . . 12
196195, 57oveq12d 6102 . . . . . . . . . . 11
19756, 196oveq12d 6102 . . . . . . . . . 10
198 dchrvmasumif.g . . . . . . . . . 10
199 ovex 6109 . . . . . . . . . 10
200197, 198, 199fvmpt 5809 . . . . . . . . 9
20111, 200syl 16 . . . . . . . 8
202 ifnefalse 3749 . . . . . . . . . . . . 13
203202fveq2d 5735 . . . . . . . . . . . 12
204203oveq1d 6099 . . . . . . . . . . 11
205204oveq2d 6100 . . . . . . . . . 10
206205adantl 454 . . . . . . . . 9
207206eqcomd 2443 . . . . . . . 8
208201, 207sylan9eqr 2492 . . . . . . 7
209156adantr 453 . . . . . . 7
210 nnrp 10626 . . . . . . . . . . . . . . . 16
211210adantl 454 . . . . . . . . . . . . . . 15
212211relogcld 20523 . . . . . . . . . . . . . 14
213212recnd 9119 . . . . . . . . . . . . 13
214213, 50, 52divcld 9795 . . . . . . . . . . . 12
21515, 214mulcld 9113 . . . . . . . . . . 11
216197cbvmptv 4303 . . . . . . . . . . . 12
217198, 216eqtri 2458 . . . . . . . . . . 11
218215, 217fmptd 5896 . . . . . . . . . 10
219218ad2antrr 708 . . . . . . . . 9
220 ffvelrn 5871 . . . . . . . . 9
221219, 11, 220syl2an 465 . . . . . . . 8
222208, 221eqeltrrd 2513 . . . . . . 7
223208, 209, 222fsumser 12529 . . . . . 6
224 ifnefalse 3749 . . . . . . 7
225224adantl 454 . . . . . 6
226223, 225oveq12d 6102 . . . . 5
227226fveq2d 5735 . . . 4
228 ifnefalse 3749 . . . . . 6
229228adantl 454 . . . . 5
230229oveq1d 6099 . . . 4
231194, 227, 2303brtr4d 4245 . . 3
232182, 231pm2.61dane 2684 . 2
233 fzfid 11317 . . . 4
2347adantr 453 . . . . . . 7
235 elfzelz 11064 . . . . . . . 8
236235adantl 454 . . . . . . 7
2374, 1, 5, 2, 234, 236dchrzrhcl 21034 . . . . . 6
238237abscld 12243 . . . . 5
23966, 86elrpii 10620 . . . . . . 7
240 relogcl 20478 . . . . . . 7
241239, 240ax-mp 5 . . . . . 6
242 elfznn 11085 . . . . . . 7
243242adantl 454 . . . . . 6
244 nndivre 10040 . . . . . 6
245241, 243, 244sylancr 646 . . . . 5
246238, 245remulcld 9121 . . . 4
247233, 246fsumrecl 12533 . . 3
24845abscld 12243 . . 3
250 simpl 445 . . . . . . 7
25166rexri 9142 . . . . . . . . . . 11
252 elico2 10979 . . . . . . . . . . 11
25370, 251, 252mp2an 655 . . . . . . . . . 10
254253simp1bi 973 . . . . . . . . 9
255254adantl 454 . . . . . . . 8
25684a1i 11 . . . . . . . . 9
25770a1i 11 . . . . . . . . 9
258 0lt1 9555 . . . . . . . . . 10
259258a1i 11 . . . . . . . . 9
260253simp2bi 974 . . . . . . . . . 10
261260adantl 454 . . . . . . . . 9
262256, 257, 255, 259, 261ltletrd 9235 . . . . . . . 8
263255, 262elrpd 10651 . . . . . . 7
264250, 263jca 520 . . . . . 6
26545adantr 453 . . . . . . 7
26626, 265subcld 9416 . . . . . 6
267264, 266syl 16 . . . . 5
268267abscld 12243 . . . 4
269264, 26syl 16 . . . . . 6
270269abscld 12243 . . . . 5
271248adantr 453 . . . . 5
272270, 271readdcld 9120 . . . 4
273247adantr 453 . . . . 5
274273, 271readdcld 9120 . . . 4
27526, 265abs2dif2d 12265 . . . . 5
276264, 275syl 16 . . . 4
27725abscld 12243 . . . . . . . 8
2789, 277fsumrecl 12533 . . . . . . 7
279264, 278syl 16 . . . . . 6
2809, 25fsumabs 12585 . . . . . . 7
281264, 280syl 16 . . . . . 6
282 fzfid 11317 . . . . . . . . 9
283237adantlr 697 . . . . . . . . . . 11
28417adantr 453 . . . . . . . . . . . . . . 15
285242adantl 454 . . . . . . . . . . . . . . . 16
286285nnrpd 10652 . . . . . . . . . . . . . . 15
287284, 286, 19syl2anc 644 . . . . . . . . . . . . . 14
288287relogcld 20523 . . . . . . . . . . . . 13
289288, 285nndivred 10053 . . . . . . . . . . . 12
290289recnd 9119 . . . . . . . . . . 11
291283, 290mulcld 9113 . . . . . . . . . 10
292291abscld 12243 . . . . . . . . 9
293282, 292fsumrecl 12533 . . . . . . . 8
294264, 293syl 16 . . . . . . 7
295 fzfid 11317 . . . . . . . 8
296264, 291sylan 459 . . . . . . . . 9
297296abscld 12243 . . . . . . . 8
298296absge0d 12251 . . . . . . . 8
299255flcld 11212 . . . . . . . . . 10
300 2z 10317 . . . . . . . . . . 11
301300a1i 11 . . . . . . . . . 10
302253simp3bi 975 . . . . . . . . . . . . . 14
303302adantl 454 . . . . . . . . . . . . 13
304 3nn 10139 . . . . . . . . . . . . . . 15
305304nnzi 10310 . . . . . . . . . . . . . 14
306 fllt 11220 . . . . . . . . . . . . . 14
307255, 305, 306sylancl 645 . . . . . . . . . . . . 13
308303, 307mpbid 203 . . . . . . . . . . . 12
309 df-3 10064 . . . . . . . . . . . 12
310308, 309syl6breq 4254 . . . . . . . . . . 11
311 rpre 10623 . . . . . . . . . . . . . . 15
312311adantl 454 . . . . . . . . . . . . . 14
313312flcld 11212 . . . . . . . . . . . . 13
314 zleltp1 10331 . . . . . . . . . . . . 13
315313, 300, 314sylancl 645 . . . . . . . . . . . 12
316264, 315syl 16 . . . . . . . . . . 11
317310, 316mpbird 225 . . . . . . . . . 10
318 eluz2 10499 . . . . . . . . . 10
319299, 301, 317, 318syl3anbrc 1139 . . . . . . . . 9
320 fzss2 11097 . . . . . . . . 9
321319, 320syl 16 . . . . . . . 8
322295, 297, 298, 321fsumless 12580 . . . . . . 7
323246adantlr 697 . . . . . . . 8
324283, 290absmuld 12261 . . . . . . . . . 10
325264, 324sylan 459 . . . . . . . . 9
326264, 289sylan 459 . . . . . . . . . . . 12
327264, 288sylan 459 . . . . . . . . . . . . 13
328 log1 20485 . . . . . . . . . . . . . 14
329 elfzle1 11065 . . . . . . . . . . . . . . . 16
330 breq2 4219 . . . . . . . . . . . . . . . . 17
331 breq2 4219 . . . . . . . . . . . . . . . . 17
332330, 331ifboth 3772 . . . . . . . . . . . . . . . 16
333261, 329, 332syl2an 465 . . . . . . . . . . . . . . 15
334 1rp 10621 . . . . . . . . . . . . . . . . 17
335 logleb 20503 . . . . . . . . . . . . . . . . 17
336334, 287, 335sylancr 646 . . . . . . . . . . . . . . . 16
337264, 336sylan 459 . . . . . . . . . . . . . . 15
338333, 337mpbid 203 . . . . . . . . . . . . . 14
339328, 338syl5eqbrr 4249 . . . . . . . . . . . . 13
340286rpregt0d 10659 . . . . . . . . . . . . . 14
341264, 340sylan 459 . . . . . . . . . . . . 13
342 divge0 9884 . . . . . . . . . . . . 13
343327, 339, 341, 342syl21anc 1184 . . . . . . . . . . . 12
344326, 343absidd 12230 . . . . . . . . . . 11
345344, 326eqeltrd 2512 . . . . . . . . . 10
346245adantlr 697 . . . . . . . . . 10
347238adantlr 697 . . . . . . . . . . . 12
348283absge0d 12251 . . . . . . . . . . . 12
349347, 348jca 520 . . . . . . . . . . 11
350264, 349sylan 459 . . . . . . . . . 10
351302ad2antlr 709 . . . . . . . . . . . . . . 15
352285nnred 10020 . . . . . . . . . . . . . . . . 17
353 2re 10074 . . . . . . . . . . . . . . . . . 18
354353a1i 11 . . . . . . . . . . . . . . . . 17
35566a1i 11 . . . . . . . . . . . . . . . . 17
356 elfzle2 11066 . . . . . . . . . . . . . . . . . 18
357356adantl 454 . . . . . . . . . . . . . . . . 17
358 2lt3 10148 . . . . . . . . . . . . . . . . . 18
359358a1i 11 . . . . . . . . . . . . . . . . 17
360352, 354, 355, 357, 359lelttrd 9233 . . . . . . . . . . . . . . . 16
361264, 360sylan 459 . . . . . . . . . . . . . . 15
362 breq1 4218 . . . . . . . . . . . . . . . 16
363 breq1 4218 . . . . . . . . . . . . . . . 16
364362, 363ifboth 3772 . . . . . . . . . . . . . . 15
365351, 361, 364syl2anc 644 . . . . . . . . . . . . . 14
366287rpred 10653 . . . . . . . . . . . . . . . 16
367 ltle 9168 . . . . . . . . . . . . . . . 16
368366, 66, 367sylancl 645 . . . . . . . . . . . . . . 15
369264, 368sylan 459 . . . . . . . . . . . . . 14
370365, 369mpd 15 . . . . . . . . . . . . 13
371 logleb 20503 . . . . . . . . . . . . . . 15
372287, 239, 371sylancl 645 . . . . . . . . . . . . . 14
373264, 372sylan 459 . . . . . . . . . . . . 13
374370, 373mpbid 203 . . . . . . . . . . . 12
375241a1i 11 . . . . . . . . . . . . . 14
376288, 375, 286lediv1d 10695 . . . . . . . . . . . . 13
377264, 376sylan 459 . . . . . . . . . . . 12
378374, 377mpbid 203 . . . . . . . . . . 11
379344, 378eqbrtrd 4235 . . . . . . . . . 10
380 lemul2a 9870 . . . . . . . . . 10
381345, 346, 350, 379, 380syl31anc 1188 . . . . . . . . 9
382325, 381eqbrtrd 4235 . . . . . . . 8
383295, 297, 323, 382fsumle 12583 . . . . . . 7
384279, 294, 273, 322, 383letrd 9232 . . . . . 6
385270, 279, 273, 281, 384letrd 9232 . . . . 5
38626abscld 12243 . . . . . . 7
387247adantr 453 . . . . . . 7
388265abscld 12243 . . . . . . 7
389386, 387, 388leadd1d 9625 . . . . . 6
390264, 389syl 16 . . . . 5
391385, 390mpbid 203 . . . 4