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

Theorem rpvmasumlem 24404
 Description: Lemma for rpvmasum 24443. Calculate the "trivial case" estimate Λ , where is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (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
Assertion
Ref Expression
rpvmasumlem Λ
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,   ,,
Allowed substitution hints:   (,)

Proof of Theorem rpvmasumlem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 reex 9648 . . . . . 6
2 rpssre 11335 . . . . . 6
31, 2ssexi 4541 . . . . 5
43a1i 11 . . . 4
5 fzfid 12224 . . . . . . 7
6 elfznn 11854 . . . . . . . . . . 11
76adantl 473 . . . . . . . . . 10
8 vmacl 24124 . . . . . . . . . 10 Λ
97, 8syl 17 . . . . . . . . 9 Λ
109, 7nndivred 10680 . . . . . . . 8 Λ
1110recnd 9687 . . . . . . 7 Λ
125, 11fsumcl 13876 . . . . . 6 Λ
1312adantr 472 . . . . 5 Λ
14 relogcl 23604 . . . . . . 7
1514adantl 473 . . . . . 6
1615recnd 9687 . . . . 5
1713, 16subcld 10005 . . . 4 Λ
18 1re 9660 . . . . . . . . 9
19 rpvmasum.g . . . . . . . . . . . 12 DChr
20 rpvmasum.z . . . . . . . . . . . 12 ℤ/n
21 rpvmasum.1 . . . . . . . . . . . 12
22 eqid 2471 . . . . . . . . . . . 12
23 rpvmasum.a . . . . . . . . . . . 12
2419, 20, 21, 22, 23dchr1re 24270 . . . . . . . . . . 11
2524adantr 472 . . . . . . . . . 10
2623nnnn0d 10949 . . . . . . . . . . . 12
27 rpvmasum.l . . . . . . . . . . . . 13 RHom
2820, 22, 27znzrhfo 19195 . . . . . . . . . . . 12
29 fof 5806 . . . . . . . . . . . 12
3026, 28, 293syl 18 . . . . . . . . . . 11
31 elfzelz 11826 . . . . . . . . . . 11
32 ffvelrn 6035 . . . . . . . . . . 11
3330, 31, 32syl2an 485 . . . . . . . . . 10
3425, 33ffvelrnd 6038 . . . . . . . . 9
35 resubcl 9958 . . . . . . . . 9
3618, 34, 35sylancr 676 . . . . . . . 8
3736, 10remulcld 9689 . . . . . . 7 Λ
3837recnd 9687 . . . . . 6 Λ
395, 38fsumcl 13876 . . . . 5 Λ
4039adantr 472 . . . 4 Λ
41 eqidd 2472 . . . 4 Λ Λ
42 eqidd 2472 . . . 4 Λ Λ
434, 17, 40, 41, 42offval2 6567 . . 3 Λ Λ Λ Λ
4413, 16, 40sub32d 10037 . . . . 5 Λ Λ Λ Λ
455, 11, 38fsumsub 13926 . . . . . . . 8 Λ Λ Λ Λ
46 1cnd 9677 . . . . . . . . . . 11
4736recnd 9687 . . . . . . . . . . 11
4846, 47, 11subdird 10096 . . . . . . . . . 10 Λ Λ Λ
49 ax-1cn 9615 . . . . . . . . . . . 12
5034recnd 9687 . . . . . . . . . . . 12
51 nncan 9923 . . . . . . . . . . . 12
5249, 50, 51sylancr 676 . . . . . . . . . . 11
5352oveq1d 6323 . . . . . . . . . 10 Λ Λ
5411mulid2d 9679 . . . . . . . . . . 11 Λ Λ
5554oveq1d 6323 . . . . . . . . . 10 Λ Λ Λ Λ
5648, 53, 553eqtr3rd 2514 . . . . . . . . 9 Λ Λ Λ
5756sumeq2dv 13846 . . . . . . . 8 Λ Λ Λ
5845, 57eqtr3d 2507 . . . . . . 7 Λ Λ Λ
5958oveq1d 6323 . . . . . 6 Λ Λ Λ
6059adantr 472 . . . . 5 Λ Λ Λ
6144, 60eqtrd 2505 . . . 4 Λ Λ Λ
6261mpteq2dva 4482 . . 3 Λ Λ Λ
6343, 62eqtrd 2505 . 2 Λ Λ Λ
64 vmadivsum 24399 . . 3 Λ
652a1i 11 . . . 4
66 1red 9676 . . . 4
67 prmdvdsfi 24113 . . . . . 6
6823, 67syl 17 . . . . 5
69 elrabi 3181 . . . . . 6
70 prmnn 14704 . . . . . . . . . 10
7170adantl 473 . . . . . . . . 9
7271nnrpd 11362 . . . . . . . 8
7372relogcld 23651 . . . . . . 7
74 prmuz2 14721 . . . . . . . . 9
7574adantl 473 . . . . . . . 8
76 uz2m1nn 11256 . . . . . . . 8
7775, 76syl 17 . . . . . . 7
7873, 77nndivred 10680 . . . . . 6
7969, 78sylan2 482 . . . . 5
8068, 79fsumrecl 13877 . . . 4
81 fzfid 12224 . . . . . . 7
82 simpr 468 . . . . . . . . . . 11
83 0re 9661 . . . . . . . . . . 11
8482, 83syl6eqel 2557 . . . . . . . . . 10
85 eqid 2471 . . . . . . . . . . . 12 Unit Unit
8623ad3antrrr 744 . . . . . . . . . . . 12
87 rpvmasum.d . . . . . . . . . . . . . 14
8819dchrabl 24261 . . . . . . . . . . . . . . . 16
89 ablgrp 17513 . . . . . . . . . . . . . . . 16
9087, 21grpidcl 16772 . . . . . . . . . . . . . . . 16
9123, 88, 89, 904syl 19 . . . . . . . . . . . . . . 15
9291ad2antrr 740 . . . . . . . . . . . . . 14
9333adantlr 729 . . . . . . . . . . . . . 14
9419, 20, 87, 22, 85, 92, 93dchrn0 24257 . . . . . . . . . . . . 13 Unit
9594biimpa 492 . . . . . . . . . . . 12 Unit
9619, 20, 21, 85, 86, 95dchr1 24264 . . . . . . . . . . 11
9796, 18syl6eqel 2557 . . . . . . . . . 10
9884, 97pm2.61dane 2730 . . . . . . . . 9
9918, 98, 35sylancr 676 . . . . . . . 8
10010adantlr 729 . . . . . . . 8 Λ
10199, 100remulcld 9689 . . . . . . 7 Λ
10281, 101fsumrecl 13877 . . . . . 6 Λ
103 0le1 10158 . . . . . . . . . . 11
10482, 103syl6eqbr 4433 . . . . . . . . . 10
10518leidi 10169 . . . . . . . . . . 11
10696, 105syl6eqbr 4433 . . . . . . . . . 10
107104, 106pm2.61dane 2730 . . . . . . . . 9
108 subge0 10148 . . . . . . . . . 10
10918, 98, 108sylancr 676 . . . . . . . . 9
110107, 109mpbird 240 . . . . . . . 8
1119adantlr 729 . . . . . . . . 9 Λ
1126adantl 473 . . . . . . . . . 10
113 vmage0 24127 . . . . . . . . . 10 Λ
114112, 113syl 17 . . . . . . . . 9 Λ
115112nnred 10646 . . . . . . . . 9
116112nngt0d 10675 . . . . . . . . 9
117 divge0 10496 . . . . . . . . 9 Λ Λ Λ
118111, 114, 115, 116, 117syl22anc 1293 . . . . . . . 8 Λ
11999, 100, 110, 118mulge0d 10211 . . . . . . 7 Λ
12081, 101, 119fsumge0 13932 . . . . . 6 Λ
121102, 120absidd 13561 . . . . 5 Λ Λ
12268adantr 472 . . . . . . . 8
123 inss2 3644 . . . . . . . . 9
124 rabss2 3498 . . . . . . . . 9
125123, 124mp1i 13 . . . . . . . 8
126 ssfi 7810 . . . . . . . 8
127122, 125, 126syl2anc 673 . . . . . . 7
128 ssrab2 3500 . . . . . . . . . 10
129128, 123sstri 3427 . . . . . . . . 9
130129sseli 3414 . . . . . . . 8
13178adantlr 729 . . . . . . . 8
132130, 131sylan2 482 . . . . . . 7
133127, 132fsumrecl 13877 . . . . . 6
13480adantr 472 . . . . . 6
135 fveq2 5879 . . . . . . . . . . . 12
136135fveq2d 5883 . . . . . . . . . . 11
137136oveq2d 6324 . . . . . . . . . 10
138 fveq2 5879 . . . . . . . . . . 11 Λ Λ
139 id 22 . . . . . . . . . . 11
140138, 139oveq12d 6326 . . . . . . . . . 10 Λ Λ
141137, 140oveq12d 6326 . . . . . . . . 9 Λ Λ
142 rpre 11331 . . . . . . . . . 10
143142ad2antrl 742 . . . . . . . . 9
14438adantlr 729 . . . . . . . . 9 Λ
145 simprr 774 . . . . . . . . . . . . 13 Λ Λ
146145oveq1d 6323 . . . . . . . . . . . 12 Λ Λ
1476ad2antrl 742 . . . . . . . . . . . . . 14 Λ
148147nncnd 10647 . . . . . . . . . . . . 13 Λ
149147nnne0d 10676 . . . . . . . . . . . . 13 Λ
150148, 149div0d 10404 . . . . . . . . . . . 12 Λ
151146, 150eqtrd 2505 . . . . . . . . . . 11 Λ Λ
152151oveq2d 6324 . . . . . . . . . 10 Λ Λ
15347ad2ant2r 761 . . . . . . . . . . 11 Λ
154153mul01d 9850 . . . . . . . . . 10 Λ
155152, 154eqtrd 2505 . . . . . . . . 9 Λ Λ
156141, 143, 144, 155fsumvma2 24221 . . . . . . . 8 Λ Λ
157128a1i 11 . . . . . . . . 9
158 fzfid 12224 . . . . . . . . . . 11
15924ad2antrr 740 . . . . . . . . . . . . . . . 16
16030ad2antrr 740 . . . . . . . . . . . . . . . . 17
16170ad2antrl 742 . . . . . . . . . . . . . . . . . . 19
162 elfznn 11854 . . . . . . . . . . . . . . . . . . . . 21
163162ad2antll 743 . . . . . . . . . . . . . . . . . . . 20
164163nnnn0d 10949 . . . . . . . . . . . . . . . . . . 19
165161, 164nnexpcld 12475 . . . . . . . . . . . . . . . . . 18
166165nnzd 11062 . . . . . . . . . . . . . . . . 17
167160, 166ffvelrnd 6038 . . . . . . . . . . . . . . . 16
168159, 167ffvelrnd 6038 . . . . . . . . . . . . . . 15
169 resubcl 9958 . . . . . . . . . . . . . . 15
17018, 168, 169sylancr 676 . . . . . . . . . . . . . 14
171 vmacl 24124 . . . . . . . . . . . . . . . 16 Λ
172165, 171syl 17 . . . . . . . . . . . . . . 15 Λ
173172, 165nndivred 10680 . . . . . . . . . . . . . 14 Λ
174170, 173remulcld 9689 . . . . . . . . . . . . 13 Λ
175174anassrs 660 . . . . . . . . . . . 12 Λ
176175recnd 9687 . . . . . . . . . . 11 Λ
177158, 176fsumcl 13876 . . . . . . . . . 10 Λ
178130, 177sylan2 482 . . . . . . . . 9 Λ
179 breq1 4398 . . . . . . . . . . . 12
180179notbid 301 . . . . . . . . . . 11
181 notrab 3711 . . . . . . . . . . 11
182180, 181elrab2 3186 . . . . . . . . . 10
183123sseli 3414 . . . . . . . . . . 11
18423ad3antrrr 744 . . . . . . . . . . . . . . . . . 18
185 simplrr 779 . . . . . . . . . . . . . . . . . . . . 21
186 simplrl 778 . . . . . . . . . . . . . . . . . . . . . 22
187184nnzd 11062 . . . . . . . . . . . . . . . . . . . . . 22
188 coprm 14736 . . . . . . . . . . . . . . . . . . . . . 22
189186, 187, 188syl2anc 673 . . . . . . . . . . . . . . . . . . . . 21
190185, 189mpbid 215 . . . . . . . . . . . . . . . . . . . 20
191 prmz 14705 . . . . . . . . . . . . . . . . . . . . . 22
192186, 191syl 17 . . . . . . . . . . . . . . . . . . . . 21
193162adantl 473 . . . . . . . . . . . . . . . . . . . . . 22
194193nnnn0d 10949 . . . . . . . . . . . . . . . . . . . . 21
195 rpexp1i 14752 . . . . . . . . . . . . . . . . . . . . 21
196192, 187, 194, 195syl3anc 1292 . . . . . . . . . . . . . . . . . . . 20
197190, 196mpd 15 . . . . . . . . . . . . . . . . . . 19
198184nnnn0d 10949 . . . . . . . . . . . . . . . . . . . 20
199166anassrs 660 . . . . . . . . . . . . . . . . . . . . 21
200199adantlrr 735 . . . . . . . . . . . . . . . . . . . 20
20120, 85, 27znunit 19211 . . . . . . . . . . . . . . . . . . . 20 Unit
202198, 200, 201syl2anc 673 . . . . . . . . . . . . . . . . . . 19 Unit
203197, 202mpbird 240 . . . . . . . . . . . . . . . . . 18 Unit
20419, 20, 21, 85, 184, 203dchr1 24264 . . . . . . . . . . . . . . . . 17
205204oveq2d 6324 . . . . . . . . . . . . . . . 16
206 1m1e0 10700 . . . . . . . . . . . . . . . 16
207205, 206syl6eq 2521 . . . . . . . . . . . . . . 15
208207oveq1d 6323 . . . . . . . . . . . . . 14 Λ Λ
209173recnd 9687 . . . . . . . . . . . . . . . . 17 Λ
210209anassrs 660 . . . . . . . . . . . . . . . 16 Λ
211210adantlrr 735 . . . . . . . . . . . . . . 15 Λ
212211mul02d 9849 . . . . . . . . . . . . . 14 Λ
213208, 212eqtrd 2505 . . . . . . . . . . . . 13 Λ
214213sumeq2dv 13846 . . . . . . . . . . . 12 Λ
215 fzfid 12224 . . . . . . . . . . . . . 14
216215olcd 400 . . . . . . . . . . . . 13
217 sumz 13865 . . . . . . . . . . . . 13
218216, 217syl 17 . . . . . . . . . . . 12
219214, 218eqtrd 2505 . . . . . . . . . . 11 Λ
220183, 219sylanr1 664 . . . . . . . . . 10 Λ
221182, 220sylan2b 483 . . . . . . . . 9 Λ
222 ppifi 24111 . . . . . . . . . 10
223143, 222syl 17 . . . . . . . . 9
224157, 178, 221, 223fsumss 13868 . . . . . . . 8 Λ Λ
225156, 224eqtr4d 2508 . . . . . . 7 Λ Λ
226158, 175fsumrecl 13877 . . . . . . . . 9 Λ
227130, 226sylan2 482 . . . . . . . 8 Λ
22873adantlr 729 . . . . . . . . . . 11
22970adantl 473 . . . . . . . . . . . . . 14
230229nnrecred 10677 . . . . . . . . . . . . 13
231229nnrpd 11362 . . . . . . . . . . . . . . . 16
232231rpreccld 11374 . . . . . . . . . . . . . . 15
233 simplrl 778 . . . . . . . . . . . . . . . . . . 19
234233relogcld 23651 . . . . . . . . . . . . . . . . . 18
235229nnred 10646 . . . . . . . . . . . . . . . . . . 19
23674adantl 473 . . . . . . . . . . . . . . . . . . . 20
237 eluz2b2 11254 . . . . . . . . . . . . . . . . . . . . 21
238237simprbi 471 . . . . . . . . . . . . . . . . . . . 20
239236, 238syl 17 . . . . . . . . . . . . . . . . . . 19
240235, 239rplogcld 23657 . . . . . . . . . . . . . . . . . 18
241234, 240rerpdivcld 11392 . . . . . . . . . . . . . . . . 17
242241flcld 12067 . . . . . . . . . . . . . . . 16
243242peano2zd 11066 . . . . . . . . . . . . . . 15
244232, 243rpexpcld 12477 . . . . . . . . . . . . . 14
245244rpred 11364 . . . . . . . . . . . . 13
246230, 245resubcld 10068 . . . . . . . . . . . 12
247236, 76syl 17 . . . . . . . . . . . . . 14
248247nnrpd 11362 . . . . . . . . . . . . 13
249248, 231rpdivcld 11381 . . . . . . . . . . . 12
250246, 249rerpdivcld 11392 . . . . . . . . . . 11
251228, 250remulcld 9689 . . . . . . . . . 10
252172recnd 9687 . . . . . . . . . . . . . . . 16 Λ
253165nncnd 10647 . . . . . . . . . . . . . . . 16
254165nnne0d 10676 . . . . . . . . . . . . . . . 16
255252, 253, 254divrecd 10408 . . . . . . . . . . . . . . 15 Λ Λ
256 simprl 772 . . . . . . . . . . . . . . . . 17
257 vmappw 24122 . . . . . . . . . . . . . . . . 17 Λ
258256, 163, 257syl2anc 673 . . . . . . . . . . . . . . . 16 Λ
259161nncnd 10647 . . . . . . . . . . . . . . . . . 18
260161nnne0d 10676 . . . . . . . . . . . . . . . . . 18
261 elfzelz 11826 . . . . . . . . . . . . . . . . . . 19
262261ad2antll 743 . . . . . . . . . . . . . . . . . 18
263259, 260, 262exprecd 12462 . . . . . . . . . . . . . . . . 17
264263eqcomd 2477 . . . . . . . . . . . . . . . 16
265258, 264oveq12d 6326 . . . . . . . . . . . . . . 15 Λ
266255, 265eqtrd 2505 . . . . . . . . . . . . . 14 Λ
267266, 173eqeltrrd 2550 . . . . . . . . . . . . 13
268267anassrs 660 . . . . . . . . . . . 12
269 1red 9676 . . . . . . . . . . . . . . 15
270 vmage0 24127 . . . . . . . . . . . . . . . . 17 Λ
271165, 270syl 17 . . . . . . . . . . . . . . . 16 Λ
272165nnred 10646 . . . . . . . . . . . . . . . 16
273165nngt0d 10675 . . . . . . . . . . . . . . . 16
274 divge0 10496 . . . . . . . . . . . . . . . 16 Λ Λ Λ
275172, 271, 272, 273, 274syl22anc 1293 . . . . . . . . . . . . . . 15 Λ
27683leidi 10169 . . . . . . . . . . . . . . . . . 18
277 simpr 468 . . . . . . . . . . . . . . . . . 18
278276, 277syl5breqr 4432 . . . . . . . . . . . . . . . . 17
27923ad3antrrr 744 . . . . . . . . . . . . . . . . . . 19
28091ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21
28119, 20, 87, 22, 85, 280, 167dchrn0 24257 . . . . . . . . . . . . . . . . . . . 20 Unit
282281biimpa 492 . . . . . . . . . . . . . . . . . . 19 Unit
28319, 20, 21, 85, 279, 282dchr1 24264 . . . . . . . . . . . . . . . . . 18
284103, 283syl5breqr 4432 . . . . . . . . . . . . . . . . 17
285278, 284pm2.61dane 2730 . . . . . . . . . . . . . . . 16
286 subge02 10151 . . . . . . . . . . . . . . . . 17
28718, 168, 286sylancr 676 . . . . . . . . . . . . . . . 16
288285, 287mpbid 215 . . . . . . . . . . . . . . 15
289170, 269, 173, 275, 288lemul1ad 10568 . . . . . . . . . . . . . 14 Λ Λ
290209mulid2d 9679 . . . . . . . . . . . . . . 15 Λ Λ
291290, 266eqtrd 2505 . . . . . . . . . . . . . 14 Λ
292289, 291breqtrd 4420 . . . . . . . . . . . . 13 Λ
293292anassrs 660 . . . . . . . . . . . 12 Λ
294158, 175, 268, 293fsumle 13936 . . . . . . . . . . 11 Λ
295228recnd 9687 . . . . . . . . . . . . 13
296161nnrecred 10677 . . . . . . . . . . . . . . . 16
297296, 164reexpcld 12471 . . . . . . . . . . . . . . 15
298297recnd 9687 . . . . . . . . . . . . . 14
299298anassrs 660 . . . . . . . . . . . . 13
300158, 295, 299fsummulc2 13922 . . . . . . . . . . . 12
301 fzval3 12012 . . . . . . . . . . . . . . . 16 ..^
302242, 301syl 17 . . . . . . . . . . . . . . 15 ..^
303302sumeq1d 13844 . . . . . . . . . . . . . 14 ..^
304230recnd 9687 . . . . . . . . . . . . . . 15
305229nngt0d 10675 . . . . . . . . . . . . . . . . . 18
306 recgt1 10524 . . . . . . . . . . . . . . . . . 18
307235, 305, 306syl2anc 673 . . . . . . . . . . . . . . . . 17
308239, 307mpbid 215 . . . . . . . . . . . . . . . 16
309230, 308ltned 9788 . . . . . . . . . . . . . . 15
310 1nn0 10909 . . . . . . . . . . . . . . . 16
311310a1i 11 . . . . . . . . . . . . . . 15
312 log1 23614 . . . . . . . . . . . . . . . . . . . . 21
313 simprr 774 . . . . . . . . . . . . . . . . . . . . . 22
314 1rp 11329 . . . . . . . . . . . . . . . . . . . . . . 23
315 simprl 772 . . . . . . . . . . . . . . . . . . . . . . 23
316 logleb 23631 . . . . . . . . . . . . . . . . . . . . . . 23
317314, 315, 316sylancr 676 . . . . . . . . . . . . . . . . . . . . . 22
318313, 317mpbid 215 . . . . . . . . . . . . . . . . . . . . 21
319312, 318syl5eqbrr 4430 . . . . . . . . . . . . . . . . . . . 20
320319adantr 472 . . . . . . . . . . . . . . . . . . 19
321234, 240, 320divge0d 11401 . . . . . . . . . . . . . . . . . 18
322 flge0nn0 12087 . . . . . . . . . . . . . . . . . 18
323241, 321, 322syl2anc 673 . . . . . . . . . . . . . . . . 17
324 nn0p1nn 10933 . . . . . . . . . . . . . . . . 17
325323, 324syl 17 . . . . . . . . . . . . . . . 16
326 nnuz 11218 . . . . . . . . . . . . . . . 16
327325, 326syl6eleq 2559 . . . . . . . . . . . . . . 15
328304, 309, 311, 327geoserg 14001 . . . . . . . . . . . . . 14