Metamath Proof Explorer


Theorem dchrmusumlem

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded. Equation 9.4.16 of Shapiro, p. 379. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z Z=/N
rpvmasum.l L=ℤRHomZ
rpvmasum.a φN
dchrmusum.g G=DChrN
dchrmusum.d D=BaseG
dchrmusum.1 1˙=0G
dchrmusum.b φXD
dchrmusum.n1 φX1˙
dchrmusum.f F=aXLaa
dchrmusum.c φC0+∞
dchrmusum.t φseq1+FT
dchrmusum.2 φy1+∞seq1+FyTCy
Assertion dchrmusumlem φx+n=1xXLnμnn𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z=/N
2 rpvmasum.l L=ℤRHomZ
3 rpvmasum.a φN
4 dchrmusum.g G=DChrN
5 dchrmusum.d D=BaseG
6 dchrmusum.1 1˙=0G
7 dchrmusum.b φXD
8 dchrmusum.n1 φX1˙
9 dchrmusum.f F=aXLaa
10 dchrmusum.c φC0+∞
11 dchrmusum.t φseq1+FT
12 dchrmusum.2 φy1+∞seq1+FyTCy
13 fzfid φx+1xFin
14 7 ad2antrr φx+n1xXD
15 elfzelz n1xn
16 15 adantl φx+n1xn
17 4 1 5 2 14 16 dchrzrhcl φx+n1xXLn
18 elfznn n1xn
19 18 adantl φx+n1xn
20 mucl nμn
21 19 20 syl φx+n1xμn
22 21 zred φx+n1xμn
23 22 19 nndivred φx+n1xμnn
24 23 recnd φx+n1xμnn
25 17 24 mulcld φx+n1xXLnμnn
26 13 25 fsumcl φx+n=1xXLnμnn
27 climcl seq1+FTT
28 11 27 syl φT
29 28 adantr φx+T
30 26 29 mulcld φx+n=1xXLnμnnT
31 1 2 3 4 5 6 7 8 9 10 11 12 dchrisumn0 φT0
32 31 adantr φx+T0
33 30 29 32 divrecd φx+n=1xXLnμnnTT=n=1xXLnμnnT1T
34 26 29 32 divcan4d φx+n=1xXLnμnnTT=n=1xXLnμnn
35 33 34 eqtr3d φx+n=1xXLnμnnT1T=n=1xXLnμnn
36 35 mpteq2dva φx+n=1xXLnμnnT1T=x+n=1xXLnμnn
37 28 31 reccld φ1T
38 37 adantr φx+1T
39 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 φx+n=1xXLnμnnT𝑂1
40 rpssre +
41 o1const +1Tx+1T𝑂1
42 40 37 41 sylancr φx+1T𝑂1
43 30 38 39 42 o1mul2 φx+n=1xXLnμnnT1T𝑂1
44 36 43 eqeltrrd φx+n=1xXLnμnn𝑂1