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

Theorem rpvmasum2 24429
 Description: A partial result along the lines of rpvmasum 24443. The sum of the von Mangoldt function over those integers (mod ) is asymptotic to , where is the number of non-principal Dirichlet characters with . Our goal is to show this set is empty. Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z ℤ/n
rpvmasum.l RHom
rpvmasum.a
rpvmasum2.g DChr
rpvmasum2.d
rpvmasum2.1
rpvmasum2.w
rpvmasum2.u Unit
rpvmasum2.b
rpvmasum2.t
rpvmasum2.z1
Assertion
Ref Expression
rpvmasum2 Λ
Distinct variable groups:   ,,,,,   ,,,,   ,   ,,,,,   ,,,,   ,,,,   ,,,   ,,   ,,,,,   ,,,,,   ,,,,,   ,
Allowed substitution hints:   ()   ()   (,)   (,,,)   (,,)

Proof of Theorem rpvmasum2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum.a . . . . . . 7
21adantr 472 . . . . . 6
3 rpvmasum2.g . . . . . . 7 DChr
4 rpvmasum2.d . . . . . . 7
53, 4dchrfi 24262 . . . . . 6
62, 5syl 17 . . . . 5
7 fzfid 12224 . . . . . 6
8 rpvmasum.z . . . . . . . . . . . . 13 ℤ/n
9 eqid 2471 . . . . . . . . . . . . 13
10 simpr 468 . . . . . . . . . . . . 13
113, 8, 4, 9, 10dchrf 24249 . . . . . . . . . . . 12
12 rpvmasum2.u . . . . . . . . . . . . . . 15 Unit
139, 12unitss 17966 . . . . . . . . . . . . . 14
14 rpvmasum2.b . . . . . . . . . . . . . 14
1513, 14sseldi 3416 . . . . . . . . . . . . 13
1615adantr 472 . . . . . . . . . . . 12
1711, 16ffvelrnd 6038 . . . . . . . . . . 11
1817cjcld 13336 . . . . . . . . . 10
1918adantlr 729 . . . . . . . . 9
2019adantrl 730 . . . . . . . 8
2111adantlr 729 . . . . . . . . . . . 12
2221adantlr 729 . . . . . . . . . . 11
231nnnn0d 10949 . . . . . . . . . . . . . . 15
24 rpvmasum.l . . . . . . . . . . . . . . . 16 RHom
258, 9, 24znzrhfo 19195 . . . . . . . . . . . . . . 15
26 fof 5806 . . . . . . . . . . . . . . 15
2723, 25, 263syl 18 . . . . . . . . . . . . . 14
2827adantr 472 . . . . . . . . . . . . 13
29 elfzelz 11826 . . . . . . . . . . . . 13
30 ffvelrn 6035 . . . . . . . . . . . . 13
3128, 29, 30syl2an 485 . . . . . . . . . . . 12
3231adantr 472 . . . . . . . . . . 11
3322, 32ffvelrnd 6038 . . . . . . . . . 10
3433anasss 659 . . . . . . . . 9
35 elfznn 11854 . . . . . . . . . . . . . 14
3635adantl 473 . . . . . . . . . . . . 13
37 vmacl 24124 . . . . . . . . . . . . 13 Λ
3836, 37syl 17 . . . . . . . . . . . 12 Λ
3938, 36nndivred 10680 . . . . . . . . . . 11 Λ
4039recnd 9687 . . . . . . . . . 10 Λ
4140adantrr 731 . . . . . . . . 9 Λ
4234, 41mulcld 9681 . . . . . . . 8 Λ
4320, 42mulcld 9681 . . . . . . 7 Λ
4443anass1rs 824 . . . . . 6 Λ
457, 44fsumcl 13876 . . . . 5 Λ
46 relogcl 23604 . . . . . . . . 9
4746adantl 473 . . . . . . . 8
4847recnd 9687 . . . . . . 7
4948adantr 472 . . . . . 6
50 ax-1cn 9615 . . . . . . 7
51 neg1cn 10735 . . . . . . . 8
52 0cn 9653 . . . . . . . 8
5351, 52keepel 3939 . . . . . . 7
5450, 53keepel 3939 . . . . . 6
55 mulcl 9641 . . . . . 6
5649, 54, 55sylancl 675 . . . . 5
576, 45, 56fsumsub 13926 . . . 4 Λ Λ
5842anass1rs 824 . . . . . . . 8 Λ
597, 58fsumcl 13876 . . . . . . 7 Λ
6019, 59, 56subdid 10095 . . . . . 6 Λ Λ
617, 19, 58fsummulc2 13922 . . . . . . 7 Λ Λ
6254a1i 11 . . . . . . . . 9
6319, 49, 62mul12d 9860 . . . . . . . 8
64 ovif2 6393 . . . . . . . . . 10
65 fveq1 5878 . . . . . . . . . . . . . . . . 17
66 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18
671ad2antrr 740 . . . . . . . . . . . . . . . . . 18
6814ad2antrr 740 . . . . . . . . . . . . . . . . . 18
693, 8, 66, 12, 67, 68dchr1 24264 . . . . . . . . . . . . . . . . 17
7065, 69sylan9eqr 2527 . . . . . . . . . . . . . . . 16
7170fveq2d 5883 . . . . . . . . . . . . . . 15
72 1re 9660 . . . . . . . . . . . . . . . 16
73 cjre 13279 . . . . . . . . . . . . . . . 16
7472, 73ax-mp 5 . . . . . . . . . . . . . . 15
7571, 74syl6eq 2521 . . . . . . . . . . . . . 14
7675oveq1d 6323 . . . . . . . . . . . . 13
77 1t1e1 10780 . . . . . . . . . . . . 13
7876, 77syl6eq 2521 . . . . . . . . . . . 12
7978ifeq1da 3902 . . . . . . . . . . 11
80 df-ne 2643 . . . . . . . . . . . . 13
81 ovif2 6393 . . . . . . . . . . . . . 14
82 simplll 776 . . . . . . . . . . . . . . . . . . . . . 22
83 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23
8483fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . 22
8582, 84sylan 479 . . . . . . . . . . . . . . . . . . . . 21
863, 8, 4dchrmhm 24248 . . . . . . . . . . . . . . . . . . . . . . . 24 mulGrp MndHom mulGrpfld
87 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . 24
8886, 87sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . 23 mulGrp MndHom mulGrpfld
89 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25 mulGrp mulGrp
90 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25
9189, 90ringidval 17815 . . . . . . . . . . . . . . . . . . . . . . . 24 mulGrp
92 eqid 2471 . . . . . . . . . . . . . . . . . . . . . . . . 25 mulGrpfld mulGrpfld
93 cnfld1 19070 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld
9492, 93ringidval 17815 . . . . . . . . . . . . . . . . . . . . . . . 24 mulGrpfld
9591, 94mhm0 16668 . . . . . . . . . . . . . . . . . . . . . . 23 mulGrp MndHom mulGrpfld
9688, 95syl 17 . . . . . . . . . . . . . . . . . . . . . 22
9796ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21
9885, 97eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20
9998fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
10099, 74syl6eq 2521 . . . . . . . . . . . . . . . . . 18
101100oveq1d 6323 . . . . . . . . . . . . . . . . 17
10251mulid2i 9664 . . . . . . . . . . . . . . . . 17
103101, 102syl6eq 2521 . . . . . . . . . . . . . . . 16
104103ifeq1da 3902 . . . . . . . . . . . . . . 15
10519adantr 472 . . . . . . . . . . . . . . . . 17
106105mul01d 9850 . . . . . . . . . . . . . . . 16
107106ifeq2d 3891 . . . . . . . . . . . . . . 15
108104, 107eqtrd 2505 . . . . . . . . . . . . . 14
10981, 108syl5eq 2517 . . . . . . . . . . . . 13
11080, 109sylan2br 484 . . . . . . . . . . . 12
111110ifeq2da 3903 . . . . . . . . . . 11
11279, 111eqtrd 2505 . . . . . . . . . 10
11364, 112syl5eq 2517 . . . . . . . . 9
114113oveq2d 6324 . . . . . . . 8
11563, 114eqtrd 2505 . . . . . . 7
11661, 115oveq12d 6326 . . . . . 6 Λ Λ
11760, 116eqtrd 2505 . . . . 5 Λ Λ
118117sumeq2dv 13846 . . . 4 Λ Λ
119 fzfid 12224 . . . . . . . . 9
120 inss1 3643 . . . . . . . . 9
121 ssfi 7810 . . . . . . . . 9
122119, 120, 121sylancl 675 . . . . . . . 8
1232phicld 14799 . . . . . . . . 9
124123nncnd 10647 . . . . . . . 8
125120a1i 11 . . . . . . . . . 10
126125sselda 3418 . . . . . . . . 9
127126, 40syldan 478 . . . . . . . 8 Λ
128122, 124, 127fsummulc2 13922 . . . . . . 7 Λ Λ
129124adantr 472 . . . . . . . . . . 11
130129, 40mulcld 9681 . . . . . . . . . 10 Λ
131126, 130syldan 478 . . . . . . . . 9 Λ
132131ralrimiva 2809 . . . . . . . 8 Λ
133119olcd 400 . . . . . . . 8
134 sumss2 13869 . . . . . . . 8 Λ Λ Λ
135125, 132, 133, 134syl21anc 1291 . . . . . . 7 Λ Λ
136 elin 3608 . . . . . . . . . . . . 13
137136baib 919 . . . . . . . . . . . 12
138137adantl 473 . . . . . . . . . . 11
139 rpvmasum2.t . . . . . . . . . . . . 13
140139eleq2i 2541 . . . . . . . . . . . 12
141 ffn 5739 . . . . . . . . . . . . . 14
14228, 141syl 17 . . . . . . . . . . . . 13
143 fniniseg 6018 . . . . . . . . . . . . . 14
144143baibd 923 . . . . . . . . . . . . 13
145142, 29, 144syl2an 485 . . . . . . . . . . . 12
146140, 145syl5bb 265 . . . . . . . . . . 11
147138, 146bitr2d 262 . . . . . . . . . 10
14840mul02d 9849 . . . . . . . . . 10 Λ
149147, 148ifbieq2d 3897 . . . . . . . . 9 Λ Λ Λ
150 ovif 6392 . . . . . . . . . 10 Λ Λ Λ
1511ad2antrr 740 . . . . . . . . . . . . 13
152151, 5syl 17 . . . . . . . . . . . 12
15319adantlr 729 . . . . . . . . . . . . 13
15433, 153mulcld 9681 . . . . . . . . . . . 12
155152, 40, 154fsummulc1 13923 . . . . . . . . . . 11 Λ Λ
15614ad2antrr 740 . . . . . . . . . . . . 13
1573, 4, 8, 9, 12, 151, 31, 156sum2dchr 24281 . . . . . . . . . . . 12
158157oveq1d 6323 . . . . . . . . . . 11 Λ Λ
15940adantr 472 . . . . . . . . . . . . 13 Λ
160 mulass 9645 . . . . . . . . . . . . . 14 Λ Λ Λ
161 mul12 9817 . . . . . . . . . . . . . 14 Λ Λ Λ
162160, 161eqtrd 2505 . . . . . . . . . . . . 13 Λ Λ Λ
16333, 153, 159, 162syl3anc 1292 . . . . . . . . . . . 12 Λ Λ
164163sumeq2dv 13846 . . . . . . . . . . 11 Λ Λ
165155, 158, 1643eqtr3d 2513 . . . . . . . . . 10 Λ Λ
166150, 165syl5eqr 2519 . . . . . . . . 9 Λ Λ Λ
167149, 166eqtr3d 2507 . . . . . . . 8 Λ Λ
168167sumeq2dv 13846 . . . . . . 7 Λ Λ
169128, 135, 1683eqtrd 2509 . . . . . 6 Λ Λ
170119, 6, 43fsumcom 13913 . . . . . 6 Λ Λ
171169, 170eqtrd 2505 . . . . 5 Λ Λ
1723dchrabl 24261 . . . . . . . . . 10
173 ablgrp 17513 . . . . . . . . . 10
1744, 66grpidcl 16772 . . . . . . . . . 10
1752, 172, 173, 1744syl 19 . . . . . . . . 9
17648mulid1d 9678 . . . . . . . . . 10
177176, 48eqeltrd 2549 . . . . . . . . 9
178 iftrue 3878 . . . . . . . . . . 11
179178oveq2d 6324 . . . . . . . . . 10
180179sumsn 13884 . . . . . . . . 9
181175, 177, 180syl2anc 673 . . . . . . . 8
182 eldifsn 4088 . . . . . . . . . . 11
183 ifnefalse 3884 . . . . . . . . . . . . . . 15
184183ad2antll 743 . . . . . . . . . . . . . 14
185 negeq 9887 . . . . . . . . . . . . . . 15
186 negeq 9887 . . . . . . . . . . . . . . . 16
187 neg0 9940 . . . . . . . . . . . . . . . 16
188186, 187syl6eq 2521 . . . . . . . . . . . . . . 15
189185, 188ifsb 3885 . . . . . . . . . . . . . 14
190184, 189syl6eqr 2523 . . . . . . . . . . . . 13
191190oveq2d 6324 . . . . . . . . . . . 12
19248adantr 472 . . . . . . . . . . . . 13
19350, 52keepel 3939 . . . . . . . . . . . . 13
194 mulneg2 10077 . . . . . . . . . . . . 13
195192, 193, 194sylancl 675 . . . . . . . . . . . 12
196191, 195eqtrd 2505 . . . . . . . . . . 11
197182, 196sylan2b 483 . . . . . . . . . 10
198197sumeq2dv 13846 . . . . . . . . 9
199 diffi 7821 . . . . . . . . . . 11
2006, 199syl 17 . . . . . . . . . 10
20148adantr 472 . . . . . . . . . . 11
202 mulcl 9641 . . . . . . . . . . 11
203201, 193, 202sylancl 675 . . . . . . . . . 10
204200, 203fsumneg 13925 . . . . . . . . 9
205193a1i 11 . . . . . . . . . . . 12
206200, 48, 205fsummulc2 13922 . . . . . . . . . . 11
207 rpvmasum2.w . . . . . . . . . . . . . . . . 17
208 ssrab2 3500 . . . . . . . . . . . . . . . . 17
209207, 208eqsstri 3448 . . . . . . . . . . . . . . . 16
210 difss 3549 . . . . . . . . . . . . . . . 16
211209, 210sstri 3427 . . . . . . . . . . . . . . 15
212 ssfi 7810 . . . . . . . . . . . . . . 15
2136, 211, 212sylancl 675 . . . . . . . . . . . . . 14
214 fsumconst 13928 . . . . . . . . . . . . . 14
215213, 50, 214sylancl 675 . . . . . . . . . . . . 13
216209a1i 11 . . . . . . . . . . . . . 14
21750a1i 11 . . . . . . . . . . . . . . 15
218217ralrimivw 2810 . . . . . . . . . . . . . 14
219200olcd 400 . . . . . . . . . . . . . 14
220 sumss2 13869 . . . . . . . . . . . . . 14
221216, 218, 219, 220syl21anc 1291 . . . . . . . . . . . . 13
222 hashcl 12576 . . . . . . . . . . . . . . . 16
223213, 222syl 17 . . . . . . . . . . . . . . 15
224223nn0cnd 10951 . . . . . . . . . . . . . 14
225224mulid1d 9678 . . . . . . . . . . . . 13
226215, 221, 2253eqtr3d 2513 . . . . . . . . . . . 12
227226oveq2d 6324 . . . . . . . . . . 11
228206, 227eqtr3d 2507 . . . . . . . . . 10
229228negeqd 9889 . . . . . . . . 9
230198, 204, 2293eqtrd 2509 . . . . . . . 8
231181, 230oveq12d 6326 . . . . . . 7
23248, 224mulcld 9681 . . . . . . . 8
233177, 232negsubd 10011 . . . . . . 7
234231, 233eqtrd 2505 . . . . . 6
235 disjdif 3830 . . . . . . . 8
236235a1i 11 . . . . . . 7
237 undif2 3834 . . . . . . . 8
238175snssd 4108 . . . . . . . . 9
239 ssequn1 3595 . . . . . . . . 9
240238, 239sylib 201 . . . . . . . 8
241237, 240syl5req 2518 . . . . . . 7
242236, 241, 6, 56fsumsplit 13883 . . . . . 6
24348, 217, 224subdid 10095 . . . . . 6
244234, 242, 2433eqtr4rd 2516 . . . . 5
245171, 244oveq12d 6326 . . . 4 Λ Λ
24657, 118, 2453eqtr4d 2515 . . 3 Λ Λ
247246mpteq2dva 4482 . 2 Λ Λ
248 rpssre 11335 . . . 4
249248a1i 11 . . 3
2501, 5syl 17 . . 3
25117adantlr 729 . . . . . 6
252251cjcld 13336 . . . . 5
25359, 56subcld 10005 . . . . 5 Λ
254252, 253mulcld 9681 . . . 4 Λ
255254anasss 659 . . 3 Λ
25618adantr 472 . . . 4
257253an32s 821 . . . 4 Λ
258 o1const 13760 . . . . 5
259248, 18, 258sylancr 676 . . . 4
260 fveq1 5878 . . . . . . . . . . . 12
261260oveq1d 6323 . . . . . . . . . . 11 Λ Λ
262261sumeq2sdv 13847 . . . . . . . . . 10 Λ Λ
263262, 179oveq12d 6326 . . . . . . . . 9 Λ Λ
264263adantl 473 . . . . . . . 8 Λ Λ
26546recnd 9687 . . . . . . . . . 10
266265mulid1d 9678 . . . . . . . . 9
267266oveq2d 6324 . . . . . . . 8 Λ Λ
268264, 267sylan9eq 2525 . . . . . . 7 Λ Λ
269268mpteq2dva 4482 . . . . . 6 Λ Λ
2708, 24, 1, 3, 4, 66rpvmasumlem 24404 . . . . . . 7 Λ
271270ad2antrr 740 . . . . . 6 Λ
272269, 271eqeltrd 2549 . . . . 5 Λ
273183oveq2d 6324 . . . . . . . . . 10
274273oveq2d 6324 . . . . . . . . 9 Λ Λ
27548adantlr 729 . . . . . . . . . . . . . . 15
276 mulcom 9643 . . . . . . . . . . . . . . 15
277275, 51, 276sylancl 675 . . . . . . . . . . . . . 14
278275mulm1d 10091 . . . . . . . . . . . . . 14
279277, 278eqtrd 2505 . . . . . . . . . . . . 13
280275mul01d 9850 . . . . . . . . . . . . 13
281279, 280ifeq12d 3892 . . . . . . . . . . . 12
282 ovif2 6393 . . . . . . . . . . . 12
283 negeq 9887 . . . . . . . . . . . . 13
284 negeq 9887 . . . . . . . . . . . . . 14
285284, 187syl6eq 2521 . . . . . . . . . . . . 13
286283, 285ifsb 3885 . . . . . . . . . . . 12
287281, 282, 2863eqtr4g 2530 . . . . . . . . . . 11
288287oveq2d 6324 . . . . . . . . . 10 Λ Λ
28959an32s 821 . . . . . . . . . . 11 Λ
290 ifcl 3914 . . . . . . . . . . . 12
291275, 52, 290sylancl 675 . . . . . . . . . . 11
292289, 291subnegd 10012 . . . . . . . . . 10 Λ Λ
293288, 292eqtrd 2505 . . . . . . . . 9 Λ Λ
294274, 293sylan9eqr 2527 . . . . . . . 8 Λ Λ
295294an32s 821 . . . . . . 7 Λ Λ
296295mpteq2dva 4482 . . . . . 6 Λ Λ
2971ad2antrr 740 . . . . . . . 8
298 simplr 770 . . . . . . . 8
299 simpr 468 . . . . . . . 8
300 eqid 2471 . . . . . . . 8
3018, 24, 297, 3, 4, 66, 298, 299, 300dchrmusumlema 24410 . . . . . . 7
3021adantr 472 . . . . . . . . . . . . 13
303302ad2antrr 740 . . . . . . . . . . . 12
304298adantr 472 . . . . . . . . . . . 12
305 simplr 770 . . . . . . . . . . . 12
306 simprl 772 . . . . . . . . . . . 12
307 simprrl 782 . . . . . . . . . . . 12
308 simprrr 783 . . . . . . . . . . . 12
3098, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308, 207dchrvmaeq0 24421 . . . . . . . . . . 11
310 ifbi 3893 . . . . . . . . . . . . 13
311310oveq2d 6324 . . . . . . . . . . . 12 Λ Λ
312311mpteq2dv 4483 . . . . . . . . . . 11 Λ Λ
313309, 312syl 17 . . . . . . . . . 10 Λ Λ
3148, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308dchrvmasumif 24420 . . . . . . . . . 10 Λ
315313, 314eqeltrd 2549 . . . . . . . . 9 Λ
316315rexlimdvaa 2872 . . . . . . . 8