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

Theorem rpvmasum2 21198
 Description: A partial result along the lines of rpvmasum 21212. 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 452 . . . . . 6
3 rpvmasum2.g . . . . . . 7 DChr
4 rpvmasum2.d . . . . . . 7
53, 4dchrfi 21031 . . . . . 6
62, 5syl 16 . . . . 5
7 fzfid 11304 . . . . . 6
8 rpvmasum.z . . . . . . . . . . . . 13 ℤ/n
9 eqid 2435 . . . . . . . . . . . . 13
10 simpr 448 . . . . . . . . . . . . 13
113, 8, 4, 9, 10dchrf 21018 . . . . . . . . . . . 12
12 rpvmasum2.u . . . . . . . . . . . . . . 15 Unit
139, 12unitss 15757 . . . . . . . . . . . . . 14
14 rpvmasum2.b . . . . . . . . . . . . . 14
1513, 14sseldi 3338 . . . . . . . . . . . . 13
1615adantr 452 . . . . . . . . . . . 12
1711, 16ffvelrnd 5863 . . . . . . . . . . 11
1817cjcld 11993 . . . . . . . . . 10
1918adantlr 696 . . . . . . . . 9
2019adantrl 697 . . . . . . . 8
2111adantlr 696 . . . . . . . . . . . 12
2221adantlr 696 . . . . . . . . . . 11
231nnnn0d 10266 . . . . . . . . . . . . . . 15
24 rpvmasum.l . . . . . . . . . . . . . . . 16 RHom
258, 9, 24znzrhfo 16820 . . . . . . . . . . . . . . 15
26 fof 5645 . . . . . . . . . . . . . . 15
2723, 25, 263syl 19 . . . . . . . . . . . . . 14
2827adantr 452 . . . . . . . . . . . . 13
29 elfzelz 11051 . . . . . . . . . . . . 13
30 ffvelrn 5860 . . . . . . . . . . . . 13
3128, 29, 30syl2an 464 . . . . . . . . . . . 12
3231adantr 452 . . . . . . . . . . 11
3322, 32ffvelrnd 5863 . . . . . . . . . 10
3433anasss 629 . . . . . . . . 9
35 elfznn 11072 . . . . . . . . . . . . . 14
3635adantl 453 . . . . . . . . . . . . 13
37 vmacl 20893 . . . . . . . . . . . . 13 Λ
3836, 37syl 16 . . . . . . . . . . . 12 Λ
3938, 36nndivred 10040 . . . . . . . . . . 11 Λ
4039recnd 9106 . . . . . . . . . 10 Λ
4140adantrr 698 . . . . . . . . 9 Λ
4234, 41mulcld 9100 . . . . . . . 8 Λ
4320, 42mulcld 9100 . . . . . . 7 Λ
4443anass1rs 783 . . . . . 6 Λ
457, 44fsumcl 12519 . . . . 5 Λ
46 relogcl 20465 . . . . . . . . 9
4746adantl 453 . . . . . . . 8
4847recnd 9106 . . . . . . 7
4948adantr 452 . . . . . 6
50 ax-1cn 9040 . . . . . . 7
51 neg1cn 10059 . . . . . . . 8
52 0cn 9076 . . . . . . . 8
5351, 52keepel 3788 . . . . . . 7
5450, 53keepel 3788 . . . . . 6
55 mulcl 9066 . . . . . 6
5649, 54, 55sylancl 644 . . . . 5
576, 45, 56fsumsub 12563 . . . 4 Λ Λ
5842anass1rs 783 . . . . . . . 8 Λ
597, 58fsumcl 12519 . . . . . . 7 Λ
6019, 59, 56subdid 9481 . . . . . 6 Λ Λ
617, 19, 58fsummulc2 12559 . . . . . . 7 Λ Λ
6254a1i 11 . . . . . . . . 9
6319, 49, 62mul12d 9267 . . . . . . . 8
64 oveq2 6081 . . . . . . . . . . 11
65 oveq2 6081 . . . . . . . . . . 11
6664, 65ifsb 3740 . . . . . . . . . 10
67 fveq1 5719 . . . . . . . . . . . . . . . . 17
68 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18
691ad2antrr 707 . . . . . . . . . . . . . . . . . 18
7014ad2antrr 707 . . . . . . . . . . . . . . . . . 18
713, 8, 68, 12, 69, 70dchr1 21033 . . . . . . . . . . . . . . . . 17
7267, 71sylan9eqr 2489 . . . . . . . . . . . . . . . 16
7372fveq2d 5724 . . . . . . . . . . . . . . 15
74 1re 9082 . . . . . . . . . . . . . . . 16
75 cjre 11936 . . . . . . . . . . . . . . . 16
7674, 75ax-mp 8 . . . . . . . . . . . . . . 15
7773, 76syl6eq 2483 . . . . . . . . . . . . . 14
7877oveq1d 6088 . . . . . . . . . . . . 13
79 1t1e1 10118 . . . . . . . . . . . . 13
8078, 79syl6eq 2483 . . . . . . . . . . . 12
8180ifeq1da 3756 . . . . . . . . . . 11
82 df-ne 2600 . . . . . . . . . . . . 13
83 oveq2 6081 . . . . . . . . . . . . . . 15
84 oveq2 6081 . . . . . . . . . . . . . . 15
8583, 84ifsb 3740 . . . . . . . . . . . . . 14
86 simplll 735 . . . . . . . . . . . . . . . . . . . . . 22
87 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23
8887fveq2d 5724 . . . . . . . . . . . . . . . . . . . . . 22
8986, 88sylan 458 . . . . . . . . . . . . . . . . . . . . 21
903, 8, 4dchrmhm 21017 . . . . . . . . . . . . . . . . . . . . . . . 24 mulGrp MndHom mulGrpfld
91 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . 24
9290, 91sseldi 3338 . . . . . . . . . . . . . . . . . . . . . . 23 mulGrp MndHom mulGrpfld
93 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . 25 mulGrp mulGrp
94 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . 25
9593, 94rngidval 15658 . . . . . . . . . . . . . . . . . . . . . . . 24 mulGrp
96 eqid 2435 . . . . . . . . . . . . . . . . . . . . . . . . 25 mulGrpfld mulGrpfld
97 cnfld1 16718 . . . . . . . . . . . . . . . . . . . . . . . . 25 fld
9896, 97rngidval 15658 . . . . . . . . . . . . . . . . . . . . . . . 24 mulGrpfld
9995, 98mhm0 14738 . . . . . . . . . . . . . . . . . . . . . . 23 mulGrp MndHom mulGrpfld
10092, 99syl 16 . . . . . . . . . . . . . . . . . . . . . 22
101100ad2antrr 707 . . . . . . . . . . . . . . . . . . . . 21
10289, 101eqtrd 2467 . . . . . . . . . . . . . . . . . . . 20
103102fveq2d 5724 . . . . . . . . . . . . . . . . . . 19
104103, 76syl6eq 2483 . . . . . . . . . . . . . . . . . 18
105104oveq1d 6088 . . . . . . . . . . . . . . . . 17
10651mulid2i 9085 . . . . . . . . . . . . . . . . 17
107105, 106syl6eq 2483 . . . . . . . . . . . . . . . 16
108107ifeq1da 3756 . . . . . . . . . . . . . . 15
10919adantr 452 . . . . . . . . . . . . . . . . 17
110109mul01d 9257 . . . . . . . . . . . . . . . 16
111110ifeq2d 3746 . . . . . . . . . . . . . . 15
112108, 111eqtrd 2467 . . . . . . . . . . . . . 14
11385, 112syl5eq 2479 . . . . . . . . . . . . 13
11482, 113sylan2br 463 . . . . . . . . . . . 12
115114ifeq2da 3757 . . . . . . . . . . 11
11681, 115eqtrd 2467 . . . . . . . . . 10
11766, 116syl5eq 2479 . . . . . . . . 9
118117oveq2d 6089 . . . . . . . 8
11963, 118eqtrd 2467 . . . . . . 7
12061, 119oveq12d 6091 . . . . . 6 Λ Λ
12160, 120eqtrd 2467 . . . . 5 Λ Λ
122121sumeq2dv 12489 . . . 4 Λ Λ
123 fzfid 11304 . . . . . . . . 9
124 inss1 3553 . . . . . . . . 9
125 ssfi 7321 . . . . . . . . 9
126123, 124, 125sylancl 644 . . . . . . . 8
1272phicld 13153 . . . . . . . . 9
128127nncnd 10008 . . . . . . . 8
129124a1i 11 . . . . . . . . . 10
130129sselda 3340 . . . . . . . . 9
131130, 40syldan 457 . . . . . . . 8 Λ
132126, 128, 131fsummulc2 12559 . . . . . . 7 Λ Λ
133128adantr 452 . . . . . . . . . . 11
134133, 40mulcld 9100 . . . . . . . . . 10 Λ
135130, 134syldan 457 . . . . . . . . 9 Λ
136135ralrimiva 2781 . . . . . . . 8 Λ
137123olcd 383 . . . . . . . 8
138 sumss2 12512 . . . . . . . 8 Λ Λ Λ
139129, 136, 137, 138syl21anc 1183 . . . . . . 7 Λ Λ
140 elin 3522 . . . . . . . . . . . . 13
141140baib 872 . . . . . . . . . . . 12
142141adantl 453 . . . . . . . . . . 11
143 rpvmasum2.t . . . . . . . . . . . . 13
144143eleq2i 2499 . . . . . . . . . . . 12
145 ffn 5583 . . . . . . . . . . . . . 14
14628, 145syl 16 . . . . . . . . . . . . 13
147 fniniseg 5843 . . . . . . . . . . . . . 14
148147baibd 876 . . . . . . . . . . . . 13
149146, 29, 148syl2an 464 . . . . . . . . . . . 12
150144, 149syl5bb 249 . . . . . . . . . . 11
151142, 150bitr2d 246 . . . . . . . . . 10
15240mul02d 9256 . . . . . . . . . 10 Λ
153151, 152ifbieq2d 3751 . . . . . . . . 9 Λ Λ Λ
154 oveq1 6080 . . . . . . . . . . 11 Λ Λ
155 oveq1 6080 . . . . . . . . . . 11 Λ Λ
156154, 155ifsb 3740 . . . . . . . . . 10 Λ Λ Λ
1571ad2antrr 707 . . . . . . . . . . . . 13
158157, 5syl 16 . . . . . . . . . . . 12
15919adantlr 696 . . . . . . . . . . . . 13
16033, 159mulcld 9100 . . . . . . . . . . . 12
161158, 40, 160fsummulc1 12560 . . . . . . . . . . 11 Λ Λ
16214ad2antrr 707 . . . . . . . . . . . . 13
1633, 4, 8, 9, 12, 157, 31, 162sum2dchr 21050 . . . . . . . . . . . 12
164163oveq1d 6088 . . . . . . . . . . 11 Λ Λ
16540adantr 452 . . . . . . . . . . . . 13 Λ
166 mulass 9070 . . . . . . . . . . . . . 14 Λ Λ Λ
167 mul12 9224 . . . . . . . . . . . . . 14 Λ Λ Λ
168166, 167eqtrd 2467 . . . . . . . . . . . . 13 Λ Λ Λ
16933, 159, 165, 168syl3anc 1184 . . . . . . . . . . . 12 Λ Λ
170169sumeq2dv 12489 . . . . . . . . . . 11 Λ Λ
171161, 164, 1703eqtr3d 2475 . . . . . . . . . 10 Λ Λ
172156, 171syl5eqr 2481 . . . . . . . . 9 Λ Λ Λ
173153, 172eqtr3d 2469 . . . . . . . 8 Λ Λ
174173sumeq2dv 12489 . . . . . . 7 Λ Λ
175132, 139, 1743eqtrd 2471 . . . . . 6 Λ Λ
176123, 6, 43fsumcom 12551 . . . . . 6 Λ Λ
177175, 176eqtrd 2467 . . . . 5 Λ Λ
1783dchrabl 21030 . . . . . . . . . . 11
179 ablgrp 15409 . . . . . . . . . . 11
1802, 178, 1793syl 19 . . . . . . . . . 10
1814, 68grpidcl 14825 . . . . . . . . . 10
182180, 181syl 16 . . . . . . . . 9
18348mulid1d 9097 . . . . . . . . . 10
184183, 48eqeltrd 2509 . . . . . . . . 9
185 iftrue 3737 . . . . . . . . . . 11
186185oveq2d 6089 . . . . . . . . . 10
187186sumsn 12526 . . . . . . . . 9
188182, 184, 187syl2anc 643 . . . . . . . 8
189 eldifsn 3919 . . . . . . . . . . 11
190 ifnefalse 3739 . . . . . . . . . . . . . . 15
191190ad2antll 710 . . . . . . . . . . . . . 14
192 negeq 9290 . . . . . . . . . . . . . . 15
193 negeq 9290 . . . . . . . . . . . . . . . 16
194 neg0 9339 . . . . . . . . . . . . . . . 16
195193, 194syl6eq 2483 . . . . . . . . . . . . . . 15
196192, 195ifsb 3740 . . . . . . . . . . . . . 14
197191, 196syl6eqr 2485 . . . . . . . . . . . . 13
198197oveq2d 6089 . . . . . . . . . . . 12
19948adantr 452 . . . . . . . . . . . . 13
20050, 52keepel 3788 . . . . . . . . . . . . 13
201 mulneg2 9463 . . . . . . . . . . . . 13
202199, 200, 201sylancl 644 . . . . . . . . . . . 12
203198, 202eqtrd 2467 . . . . . . . . . . 11
204189, 203sylan2b 462 . . . . . . . . . 10
205204sumeq2dv 12489 . . . . . . . . 9
206 diffi 7331 . . . . . . . . . . 11
2076, 206syl 16 . . . . . . . . . 10
20848adantr 452 . . . . . . . . . . 11
209 mulcl 9066 . . . . . . . . . . 11
210208, 200, 209sylancl 644 . . . . . . . . . 10
211207, 210fsumneg 12562 . . . . . . . . 9
212200a1i 11 . . . . . . . . . . . 12
213207, 48, 212fsummulc2 12559 . . . . . . . . . . 11
214 rpvmasum2.w . . . . . . . . . . . . . . . . 17
215 ssrab2 3420 . . . . . . . . . . . . . . . . 17
216214, 215eqsstri 3370 . . . . . . . . . . . . . . . 16
217 difss 3466 . . . . . . . . . . . . . . . 16
218216, 217sstri 3349 . . . . . . . . . . . . . . 15
219 ssfi 7321 . . . . . . . . . . . . . . 15
2206, 218, 219sylancl 644 . . . . . . . . . . . . . 14
221 fsumconst 12565 . . . . . . . . . . . . . 14
222220, 50, 221sylancl 644 . . . . . . . . . . . . 13
223216a1i 11 . . . . . . . . . . . . . 14
22450a1i 11 . . . . . . . . . . . . . . 15
225224ralrimivw 2782 . . . . . . . . . . . . . 14
226207olcd 383 . . . . . . . . . . . . . 14
227 sumss2 12512 . . . . . . . . . . . . . 14
228223, 225, 226, 227syl21anc 1183 . . . . . . . . . . . . 13
229 hashcl 11631 . . . . . . . . . . . . . . . 16
230220, 229syl 16 . . . . . . . . . . . . . . 15
231230nn0cnd 10268 . . . . . . . . . . . . . 14
232231mulid1d 9097 . . . . . . . . . . . . 13
233222, 228, 2323eqtr3d 2475 . . . . . . . . . . . 12
234233oveq2d 6089 . . . . . . . . . . 11
235213, 234eqtr3d 2469 . . . . . . . . . 10
236235negeqd 9292 . . . . . . . . 9
237205, 211, 2363eqtrd 2471 . . . . . . . 8
238188, 237oveq12d 6091 . . . . . . 7
23948, 231mulcld 9100 . . . . . . . 8
240184, 239negsubd 9409 . . . . . . 7
241238, 240eqtrd 2467 . . . . . 6
242 disjdif 3692 . . . . . . . 8
243242a1i 11 . . . . . . 7
244 undif2 3696 . . . . . . . 8
245182snssd 3935 . . . . . . . . 9
246 ssequn1 3509 . . . . . . . . 9
247245, 246sylib 189 . . . . . . . 8
248244, 247syl5req 2480 . . . . . . 7
249243, 248, 6, 56fsumsplit 12525 . . . . . 6
25048, 224, 231subdid 9481 . . . . . 6
251241, 249, 2503eqtr4rd 2478 . . . . 5
252177, 251oveq12d 6091 . . . 4 Λ Λ
25357, 122, 2523eqtr4d 2477 . . 3 Λ Λ
254253mpteq2dva 4287 . 2 Λ Λ
255 rpssre 10614 . . . 4
256255a1i 11 . . 3
2571, 5syl 16 . . 3
25817adantlr 696 . . . . . 6
259258cjcld 11993 . . . . 5
26059, 56subcld 9403 . . . . 5 Λ
261259, 260mulcld 9100 . . . 4 Λ
262261anasss 629 . . 3 Λ
26318adantr 452 . . . 4
264260an32s 780 . . . 4 Λ
265 o1const 12405 . . . . 5
266255, 18, 265sylancr 645 . . . 4
267 fveq1 5719 . . . . . . . . . . . 12
268267oveq1d 6088 . . . . . . . . . . 11 Λ Λ
269268sumeq2sdv 12490 . . . . . . . . . 10 Λ Λ
270269, 186oveq12d 6091 . . . . . . . . 9 Λ Λ
271270adantl 453 . . . . . . . 8 Λ Λ
27246recnd 9106 . . . . . . . . . 10
273272mulid1d 9097 . . . . . . . . 9
274273oveq2d 6089 . . . . . . . 8 Λ Λ
275271, 274sylan9eq 2487 . . . . . . 7 Λ Λ
276275mpteq2dva 4287 . . . . . 6 Λ Λ
2778, 24, 1, 3, 4, 68rpvmasumlem 21173 . . . . . . 7 Λ
278277ad2antrr 707 . . . . . 6 Λ
279276, 278eqeltrd 2509 . . . . 5 Λ
280190oveq2d 6089 . . . . . . . . . 10
281280oveq2d 6089 . . . . . . . . 9 Λ Λ
28248adantlr 696 . . . . . . . . . . . . . . 15
283 mulcom 9068 . . . . . . . . . . . . . . 15
284282, 51, 283sylancl 644 . . . . . . . . . . . . . 14
285282mulm1d 9477 . . . . . . . . . . . . . 14
286284, 285eqtrd 2467 . . . . . . . . . . . . 13
287282mul01d 9257 . . . . . . . . . . . . 13
288286, 287ifeq12d 3747 . . . . . . . . . . . 12
289 oveq2 6081 . . . . . . . . . . . . 13
290 oveq2 6081 . . . . . . . . . . . . 13
291289, 290ifsb 3740 . . . . . . . . . . . 12
292 negeq 9290 . . . . . . . . . . . . 13
293 negeq 9290 . . . . . . . . . . . . . 14
294293, 194syl6eq 2483 . . . . . . . . . . . . 13
295292, 294ifsb 3740 . . . . . . . . . . . 12
296288, 291, 2953eqtr4g 2492 . . . . . . . . . . 11
297296oveq2d 6089 . . . . . . . . . 10 Λ Λ
29859an32s 780 . . . . . . . . . . 11 Λ
299 ifcl 3767 . . . . . . . . . . . 12
300282, 52, 299sylancl 644 . . . . . . . . . . 11
301298, 300subnegd 9410 . . . . . . . . . 10 Λ Λ
302297, 301eqtrd 2467 . . . . . . . . 9 Λ Λ
303281, 302sylan9eqr 2489 . . . . . . . 8 Λ Λ
304303an32s 780 . . . . . . 7 Λ Λ
305304mpteq2dva 4287 . . . . . 6 Λ Λ
3061ad2antrr 707 . . . . . . . 8
307 simplr 732 . . . . . . . 8
308 simpr 448 . . . . . . . 8
309 eqid 2435 . . . . . . . 8
3108, 24, 306, 3, 4, 68, 307, 308, 309dchrmusumlema 21179 . . . . . . 7
3111adantr 452 . . . . . . . . . . . . 13
312311ad2antrr 707 . . . . . . . . . . . 12
313307adantr 452 . . . . . . . . . . . 12
314 simplr 732 . . . . . . . . . . . 12
315 simprl 733 . . . . . . . . . . . 12
316 simprrl 741 . . . . . . . . . . . 12
317 simprrr 742 . . . . . . . . . . . 12
3188, 24, 312, 3, 4, 68, 313, 314, 309, 315, 316, 317, 214dchrvmaeq0 21190 . . . . . . . . . . 11
319 ifbi 3748 . . . . . . . . . . . . 13
320319oveq2d 6089 . . . . . . . . . . . 12 Λ Λ
321320mpteq2dv 4288 . . . . . . . . . . 11 Λ Λ
322318, 321syl 16 . . . . . . . . . 10