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

Theorem rpvmasumlem 21134
 Description: Lemma for rpvmasum 21173. 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 9037 . . . . . 6
2 rpssre 10578 . . . . . 6
31, 2ssexi 4308 . . . . 5
43a1i 11 . . . 4
5 fzfid 11267 . . . . . . 7
6 elfznn 11036 . . . . . . . . . . 11
76adantl 453 . . . . . . . . . 10
8 vmacl 20854 . . . . . . . . . 10 Λ
97, 8syl 16 . . . . . . . . 9 Λ
109, 7nndivred 10004 . . . . . . . 8 Λ
1110recnd 9070 . . . . . . 7 Λ
125, 11fsumcl 12482 . . . . . 6 Λ
1312adantr 452 . . . . 5 Λ
14 relogcl 20426 . . . . . . 7
1514adantl 453 . . . . . 6
1615recnd 9070 . . . . 5
1713, 16subcld 9367 . . . 4 Λ
18 1re 9046 . . . . . . . . 9
19 rpvmasum.g . . . . . . . . . . . 12 DChr
20 rpvmasum.z . . . . . . . . . . . 12 ℤ/n
21 rpvmasum.1 . . . . . . . . . . . 12
22 eqid 2404 . . . . . . . . . . . 12
23 rpvmasum.a . . . . . . . . . . . 12
2419, 20, 21, 22, 23dchr1re 21000 . . . . . . . . . . 11
2524adantr 452 . . . . . . . . . 10
2623nnnn0d 10230 . . . . . . . . . . . 12
27 rpvmasum.l . . . . . . . . . . . . 13 RHom
2820, 22, 27znzrhfo 16783 . . . . . . . . . . . 12
29 fof 5612 . . . . . . . . . . . 12
3026, 28, 293syl 19 . . . . . . . . . . 11
31 elfzelz 11015 . . . . . . . . . . 11
32 ffvelrn 5827 . . . . . . . . . . 11
3330, 31, 32syl2an 464 . . . . . . . . . 10
3425, 33ffvelrnd 5830 . . . . . . . . 9
35 resubcl 9321 . . . . . . . . 9
3618, 34, 35sylancr 645 . . . . . . . 8
3736, 10remulcld 9072 . . . . . . 7 Λ
3837recnd 9070 . . . . . 6 Λ
395, 38fsumcl 12482 . . . . 5 Λ
4039adantr 452 . . . 4 Λ
41 eqidd 2405 . . . 4 Λ Λ
42 eqidd 2405 . . . 4 Λ Λ
434, 17, 40, 41, 42offval2 6281 . . 3 Λ Λ Λ Λ
4413, 16, 40sub32d 9399 . . . . 5 Λ Λ Λ Λ
455, 11, 38fsumsub 12526 . . . . . . . 8 Λ Λ Λ Λ
46 ax-1cn 9004 . . . . . . . . . . . 12
4746a1i 11 . . . . . . . . . . 11
4836recnd 9070 . . . . . . . . . . 11
4947, 48, 11subdird 9446 . . . . . . . . . 10 Λ Λ Λ
5034recnd 9070 . . . . . . . . . . . 12
51 nncan 9286 . . . . . . . . . . . 12
5246, 50, 51sylancr 645 . . . . . . . . . . 11
5352oveq1d 6055 . . . . . . . . . 10 Λ Λ
5411mulid2d 9062 . . . . . . . . . . 11 Λ Λ
5554oveq1d 6055 . . . . . . . . . 10 Λ Λ Λ Λ
5649, 53, 553eqtr3rd 2445 . . . . . . . . 9 Λ Λ Λ
5756sumeq2dv 12452 . . . . . . . 8 Λ Λ Λ
5845, 57eqtr3d 2438 . . . . . . 7 Λ Λ Λ
5958oveq1d 6055 . . . . . 6 Λ Λ Λ
6059adantr 452 . . . . 5 Λ Λ Λ
6144, 60eqtrd 2436 . . . 4 Λ Λ Λ
6261mpteq2dva 4255 . . 3 Λ Λ Λ
6343, 62eqtrd 2436 . 2 Λ Λ Λ
64 vmadivsum 21129 . . 3 Λ
652a1i 11 . . . 4
6618a1i 11 . . . 4
67 prmdvdsfi 20843 . . . . . 6
6823, 67syl 16 . . . . 5
69 elrabi 3050 . . . . . 6
70 prmnn 13037 . . . . . . . . . 10
7170adantl 453 . . . . . . . . 9
7271nnrpd 10603 . . . . . . . 8
7372relogcld 20471 . . . . . . 7
74 prmuz2 13052 . . . . . . . . 9
7574adantl 453 . . . . . . . 8
76 uz2m1nn 10506 . . . . . . . 8
7775, 76syl 16 . . . . . . 7
7873, 77nndivred 10004 . . . . . 6
7969, 78sylan2 461 . . . . 5
8068, 79fsumrecl 12483 . . . 4
81 fzfid 11267 . . . . . . 7
82 simpr 448 . . . . . . . . . . 11
83 0re 9047 . . . . . . . . . . 11
8482, 83syl6eqel 2492 . . . . . . . . . 10
85 eqid 2404 . . . . . . . . . . . 12 Unit Unit
8623ad3antrrr 711 . . . . . . . . . . . 12
87 rpvmasum.d . . . . . . . . . . . . . 14
8819dchrabl 20991 . . . . . . . . . . . . . . . . 17
8923, 88syl 16 . . . . . . . . . . . . . . . 16
90 ablgrp 15372 . . . . . . . . . . . . . . . 16
9187, 21grpidcl 14788 . . . . . . . . . . . . . . . 16
9289, 90, 913syl 19 . . . . . . . . . . . . . . 15
9392ad2antrr 707 . . . . . . . . . . . . . 14
9433adantlr 696 . . . . . . . . . . . . . 14
9519, 20, 87, 22, 85, 93, 94dchrn0 20987 . . . . . . . . . . . . 13 Unit
9695biimpa 471 . . . . . . . . . . . 12 Unit
9719, 20, 21, 85, 86, 96dchr1 20994 . . . . . . . . . . 11
9897, 18syl6eqel 2492 . . . . . . . . . 10
9984, 98pm2.61dane 2645 . . . . . . . . 9
10018, 99, 35sylancr 645 . . . . . . . 8
10110adantlr 696 . . . . . . . 8 Λ
102100, 101remulcld 9072 . . . . . . 7 Λ
10381, 102fsumrecl 12483 . . . . . 6 Λ
104 0le1 9507 . . . . . . . . . . 11
10582, 104syl6eqbr 4209 . . . . . . . . . 10
10618leidi 9517 . . . . . . . . . . 11
10797, 106syl6eqbr 4209 . . . . . . . . . 10
108105, 107pm2.61dane 2645 . . . . . . . . 9
109 subge0 9497 . . . . . . . . . 10
11018, 99, 109sylancr 645 . . . . . . . . 9
111108, 110mpbird 224 . . . . . . . 8
1129adantlr 696 . . . . . . . . 9 Λ
1136adantl 453 . . . . . . . . . 10
114 vmage0 20857 . . . . . . . . . 10 Λ
115113, 114syl 16 . . . . . . . . 9 Λ
116113nnred 9971 . . . . . . . . 9
117113nngt0d 9999 . . . . . . . . 9
118 divge0 9835 . . . . . . . . 9 Λ Λ Λ
119112, 115, 116, 117, 118syl22anc 1185 . . . . . . . 8 Λ
120100, 101, 111, 119mulge0d 9559 . . . . . . 7 Λ
12181, 102, 120fsumge0 12529 . . . . . 6 Λ
122103, 121absidd 12180 . . . . 5 Λ Λ
12368adantr 452 . . . . . . . 8
124 inss2 3522 . . . . . . . . 9
125 rabss2 3386 . . . . . . . . 9
126124, 125mp1i 12 . . . . . . . 8
127 ssfi 7288 . . . . . . . 8
128123, 126, 127syl2anc 643 . . . . . . 7
129 ssrab2 3388 . . . . . . . . . 10
130129, 124sstri 3317 . . . . . . . . 9
131130sseli 3304 . . . . . . . 8
13278adantlr 696 . . . . . . . 8
133131, 132sylan2 461 . . . . . . 7
134128, 133fsumrecl 12483 . . . . . 6
13580adantr 452 . . . . . 6
136 fveq2 5687 . . . . . . . . . . . 12
137136fveq2d 5691 . . . . . . . . . . 11
138137oveq2d 6056 . . . . . . . . . 10
139 fveq2 5687 . . . . . . . . . . 11 Λ Λ
140 id 20 . . . . . . . . . . 11
141139, 140oveq12d 6058 . . . . . . . . . 10 Λ Λ
142138, 141oveq12d 6058 . . . . . . . . 9 Λ Λ
143 rpre 10574 . . . . . . . . . 10
144143ad2antrl 709 . . . . . . . . 9
14538adantlr 696 . . . . . . . . 9 Λ
146 simprr 734 . . . . . . . . . . . . 13 Λ Λ
147146oveq1d 6055 . . . . . . . . . . . 12 Λ Λ
1486ad2antrl 709 . . . . . . . . . . . . . 14 Λ
149148nncnd 9972 . . . . . . . . . . . . 13 Λ
150148nnne0d 10000 . . . . . . . . . . . . 13 Λ
151149, 150div0d 9745 . . . . . . . . . . . 12 Λ
152147, 151eqtrd 2436 . . . . . . . . . . 11 Λ Λ
153152oveq2d 6056 . . . . . . . . . 10 Λ Λ
15448ad2ant2r 728 . . . . . . . . . . 11 Λ
155154mul01d 9221 . . . . . . . . . 10 Λ
156153, 155eqtrd 2436 . . . . . . . . 9 Λ Λ
157142, 144, 145, 156fsumvma2 20951 . . . . . . . 8 Λ Λ
158129a1i 11 . . . . . . . . 9
159 fzfid 11267 . . . . . . . . . . 11
16024ad2antrr 707 . . . . . . . . . . . . . . . 16
16130ad2antrr 707 . . . . . . . . . . . . . . . . 17
16270ad2antrl 709 . . . . . . . . . . . . . . . . . . 19
163 elfznn 11036 . . . . . . . . . . . . . . . . . . . . 21
164163ad2antll 710 . . . . . . . . . . . . . . . . . . . 20
165164nnnn0d 10230 . . . . . . . . . . . . . . . . . . 19
166162, 165nnexpcld 11499 . . . . . . . . . . . . . . . . . 18
167166nnzd 10330 . . . . . . . . . . . . . . . . 17
168161, 167ffvelrnd 5830 . . . . . . . . . . . . . . . 16
169160, 168ffvelrnd 5830 . . . . . . . . . . . . . . 15
170 resubcl 9321 . . . . . . . . . . . . . . 15
17118, 169, 170sylancr 645 . . . . . . . . . . . . . 14
172 vmacl 20854 . . . . . . . . . . . . . . . 16 Λ
173166, 172syl 16 . . . . . . . . . . . . . . 15 Λ
174173, 166nndivred 10004 . . . . . . . . . . . . . 14 Λ
175171, 174remulcld 9072 . . . . . . . . . . . . 13 Λ
176175anassrs 630 . . . . . . . . . . . 12 Λ
177176recnd 9070 . . . . . . . . . . 11 Λ
178159, 177fsumcl 12482 . . . . . . . . . 10 Λ
179131, 178sylan2 461 . . . . . . . . 9 Λ
180 breq1 4175 . . . . . . . . . . . 12
181180notbid 286 . . . . . . . . . . 11
182 notrab 3578 . . . . . . . . . . 11
183181, 182elrab2 3054 . . . . . . . . . 10
184124sseli 3304 . . . . . . . . . . 11
18523ad3antrrr 711 . . . . . . . . . . . . . . . . . 18
186 simplrr 738 . . . . . . . . . . . . . . . . . . . . 21
187 simplrl 737 . . . . . . . . . . . . . . . . . . . . . 22
188185nnzd 10330 . . . . . . . . . . . . . . . . . . . . . 22
189 coprm 13055 . . . . . . . . . . . . . . . . . . . . . 22
190187, 188, 189syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21
191186, 190mpbid 202 . . . . . . . . . . . . . . . . . . . 20
192 prmz 13038 . . . . . . . . . . . . . . . . . . . . . 22
193187, 192syl 16 . . . . . . . . . . . . . . . . . . . . 21
194163adantl 453 . . . . . . . . . . . . . . . . . . . . . 22
195194nnnn0d 10230 . . . . . . . . . . . . . . . . . . . . 21
196 rpexp1i 13076 . . . . . . . . . . . . . . . . . . . . 21
197193, 188, 195, 196syl3anc 1184 . . . . . . . . . . . . . . . . . . . 20
198191, 197mpd 15 . . . . . . . . . . . . . . . . . . 19
199185nnnn0d 10230 . . . . . . . . . . . . . . . . . . . 20
200167anassrs 630 . . . . . . . . . . . . . . . . . . . . 21
201200adantlrr 702 . . . . . . . . . . . . . . . . . . . 20
20220, 85, 27znunit 16799 . . . . . . . . . . . . . . . . . . . 20 Unit
203199, 201, 202syl2anc 643 . . . . . . . . . . . . . . . . . . 19 Unit
204198, 203mpbird 224 . . . . . . . . . . . . . . . . . 18 Unit
20519, 20, 21, 85, 185, 204dchr1 20994 . . . . . . . . . . . . . . . . 17
206205oveq2d 6056 . . . . . . . . . . . . . . . 16
207 1m1e0 10024 . . . . . . . . . . . . . . . 16
208206, 207syl6eq 2452 . . . . . . . . . . . . . . 15
209208oveq1d 6055 . . . . . . . . . . . . . 14 Λ Λ
210174recnd 9070 . . . . . . . . . . . . . . . . 17 Λ
211210anassrs 630 . . . . . . . . . . . . . . . 16 Λ
212211adantlrr 702 . . . . . . . . . . . . . . 15 Λ
213212mul02d 9220 . . . . . . . . . . . . . 14 Λ
214209, 213eqtrd 2436 . . . . . . . . . . . . 13 Λ
215214sumeq2dv 12452 . . . . . . . . . . . 12 Λ
216 fzfid 11267 . . . . . . . . . . . . . 14
217216olcd 383 . . . . . . . . . . . . 13
218 sumz 12471 . . . . . . . . . . . . 13
219217, 218syl 16 . . . . . . . . . . . 12
220215, 219eqtrd 2436 . . . . . . . . . . 11 Λ
221184, 220sylanr1 634 . . . . . . . . . 10 Λ
222183, 221sylan2b 462 . . . . . . . . 9 Λ
223 ppifi 20841 . . . . . . . . . 10
224144, 223syl 16 . . . . . . . . 9
225158, 179, 222, 224fsumss 12474 . . . . . . . 8 Λ Λ
226157, 225eqtr4d 2439 . . . . . . 7 Λ Λ
227159, 176fsumrecl 12483 . . . . . . . . 9 Λ
228131, 227sylan2 461 . . . . . . . 8 Λ
22973adantlr 696 . . . . . . . . . . 11
23070adantl 453 . . . . . . . . . . . . . 14
231230nnrecred 10001 . . . . . . . . . . . . 13
232230nnrpd 10603 . . . . . . . . . . . . . . . 16
233232rpreccld 10614 . . . . . . . . . . . . . . 15
234 simplrl 737 . . . . . . . . . . . . . . . . . . 19
235234relogcld 20471 . . . . . . . . . . . . . . . . . 18
236230nnred 9971 . . . . . . . . . . . . . . . . . . 19
23774adantl 453 . . . . . . . . . . . . . . . . . . . 20
238 eluz2b2 10504 . . . . . . . . . . . . . . . . . . . . 21
239238simprbi 451 . . . . . . . . . . . . . . . . . . . 20
240237, 239syl 16 . . . . . . . . . . . . . . . . . . 19
241236, 240rplogcld 20477 . . . . . . . . . . . . . . . . . 18
242235, 241rerpdivcld 10631 . . . . . . . . . . . . . . . . 17
243242flcld 11162 . . . . . . . . . . . . . . . 16
244243peano2zd 10334 . . . . . . . . . . . . . . 15
245233, 244rpexpcld 11501 . . . . . . . . . . . . . 14
246245rpred 10604 . . . . . . . . . . . . 13
247231, 246resubcld 9421 . . . . . . . . . . . 12
248237, 76syl 16 . . . . . . . . . . . . . 14
249248nnrpd 10603 . . . . . . . . . . . . 13
250249, 232rpdivcld 10621 . . . . . . . . . . . 12
251247, 250rerpdivcld 10631 . . . . . . . . . . 11
252229, 251remulcld 9072 . . . . . . . . . 10
253173recnd 9070 . . . . . . . . . . . . . . . 16 Λ
254166nncnd 9972 . . . . . . . . . . . . . . . 16
255166nnne0d 10000 . . . . . . . . . . . . . . . 16
256253, 254, 255divrecd 9749 . . . . . . . . . . . . . . 15 Λ Λ
257 simprl 733 . . . . . . . . . . . . . . . . 17
258 vmappw 20852 . . . . . . . . . . . . . . . . 17 Λ
259257, 164, 258syl2anc 643 . . . . . . . . . . . . . . . 16 Λ
260162nncnd 9972 . . . . . . . . . . . . . . . . . 18
261162nnne0d 10000 . . . . . . . . . . . . . . . . . 18
262 elfzelz 11015 . . . . . . . . . . . . . . . . . . 19
263262ad2antll 710 . . . . . . . . . . . . . . . . . 18
264260, 261, 263exprecd 11486 . . . . . . . . . . . . . . . . 17
265264eqcomd 2409 . . . . . . . . . . . . . . . 16
266259, 265oveq12d 6058 . . . . . . . . . . . . . . 15 Λ
267256, 266eqtrd 2436 . . . . . . . . . . . . . 14 Λ
268267, 174eqeltrrd 2479 . . . . . . . . . . . . 13
269268anassrs 630 . . . . . . . . . . . 12
27018a1i 11 . . . . . . . . . . . . . . 15
271 vmage0 20857 . . . . . . . . . . . . . . . . 17 Λ
272166, 271syl 16 . . . . . . . . . . . . . . . 16 Λ
273166nnred 9971 . . . . . . . . . . . . . . . 16
274166nngt0d 9999 . . . . . . . . . . . . . . . 16
275 divge0 9835 . . . . . . . . . . . . . . . 16 Λ Λ Λ
276173, 272, 273, 274, 275syl22anc 1185 . . . . . . . . . . . . . . 15 Λ
27783leidi 9517 . . . . . . . . . . . . . . . . . 18
278 simpr 448 . . . . . . . . . . . . . . . . . 18
279277, 278syl5breqr 4208 . . . . . . . . . . . . . . . . 17
28023ad3antrrr 711 . . . . . . . . . . . . . . . . . . 19
28192ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
28219, 20, 87, 22, 85, 281, 168dchrn0 20987 . . . . . . . . . . . . . . . . . . . 20 Unit
283282biimpa 471 . . . . . . . . . . . . . . . . . . 19 Unit
28419, 20, 21, 85, 280, 283dchr1 20994 . . . . . . . . . . . . . . . . . 18
285104, 284syl5breqr 4208 . . . . . . . . . . . . . . . . 17
286279, 285pm2.61dane 2645 . . . . . . . . . . . . . . . 16
287 subge02 9499 . . . . . . . . . . . . . . . . 17
28818, 169, 287sylancr 645 . . . . . . . . . . . . . . . 16
289286, 288mpbid 202 . . . . . . . . . . . . . . 15
290171, 270, 174, 276, 289lemul1ad 9906 . . . . . . . . . . . . . 14 Λ Λ
291210mulid2d 9062 . . . . . . . . . . . . . . 15 Λ Λ
292291, 267eqtrd 2436 . . . . . . . . . . . . . 14 Λ
293290, 292breqtrd 4196 . . . . . . . . . . . . 13 Λ
294293anassrs 630 . . . . . . . . . . . 12 Λ
295159, 176, 269, 294fsumle 12533 . . . . . . . . . . 11 Λ
296229recnd 9070 . . . . . . . . . . . . 13
297162nnrecred 10001 . . . . . . . . . . . . . . . 16
298297, 165reexpcld 11495 . . . . . . . . . . . . . . 15
299298recnd 9070 . . . . . . . . . . . . . 14
300299anassrs 630 . . . . . . . . . . . . 13
301159, 296, 300fsummulc2 12522 . . . . . . . . . . . 12
302 fzval3 11135 . . . . . . . . . . . . . . . 16 ..^
303243, 302syl 16 . . . . . . . . . . . . . . 15 ..^
304303sumeq1d 12450 . . . . . . . . . . . . . 14 ..^
305231recnd 9070 . . . . . . . . . . . . . . 15
306230nngt0d 9999 . . . . . . . . . . . . . . . . . 18
307 recgt1 9862 . . . . . . . . . . . . . . . . . 18
308236, 306, 307syl2anc 643 . . . . . . . . . . . . . . . . 17
309240, 308mpbid 202 . . . . . . . . . . . . . . . 16
310231, 309ltned 9165 . . . . . . . . . . . . . . 15
311 1nn0 10193 . . . . . . . . . . . . . . . 16
312311a1i 11 . . . . . . . . . . . . . . 15
313 log1 20433 . . . . . . . . . . . . . . . . . . . . 21
314 simprr 734 . . . . . . . . . . . . . . . . . . . . . 22
315 1rp 10572 . . . . . . . . . . . . . . . . . . . . . . 23
316 simprl 733 . . . . . . . . . . . . . . . . . . . . . . 23
317 logleb 20451 . . . . . . . . . . . . . . . . . . . . . . 23
318315, 316, 317sylancr 645 . . . . . . . . . . . . . . . . . . . . . 22
319314, 318mpbid 202 . . . . . . . . . . . . . . . . . . . . 21
320313, 319syl5eqbrr 4206 . . . . . . . . . . . . . . . . . . . 20
321320adantr 452 . . . . . . . . . . . . . . . . . . 19
322235, 241, 321divge0d 10640 . . . . . . . . . . . . . . . . . 18
323 flge0nn0 11180 . . . . . . . . . . . . . . . . . 18
324242, 322, 323syl2anc 643 . . . . . . . . . . . . . . . . 17
325 nn0p1nn 10215 . . . . . . . . . . . . . . . . 17
326324, 325syl 16 . . . . . . . . . . . . . . . 16
327 nnuz 10477 . . . . . . . . . . . . . . . 16
328326, 327syl6eleq 2494 . . . . . . . . . . . . . . 15
329305, 310, 312, 328geoserg 12600 . . . . . . . . . . . . . 14