Metamath Proof Explorer


Theorem dchrmusum

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˙
Assertion dchrmusum φ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 eqid aXLaa=aXLaa
10 1 2 3 4 5 6 7 8 9 dchrmusumlema φtc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcy
11 3 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyN
12 7 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyXD
13 8 adantr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyX1˙
14 simprl φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyc0+∞
15 simprrl φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyseq1+aXLaat
16 simprrr φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyy1+∞seq1+aXLaaytcy
17 1 2 11 4 5 6 12 13 9 14 15 16 dchrmusumlem φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyx+n=1xXLnμnn𝑂1
18 17 rexlimdvaa φc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyx+n=1xXLnμnn𝑂1
19 18 exlimdv φtc0+∞seq1+aXLaaty1+∞seq1+aXLaaytcyx+n=1xXLnμnn𝑂1
20 10 19 mpd φx+n=1xXLnμnn𝑂1