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 = ℤRHom Z
rpvmasum.a φ N
dchrmusum.g G = DChr N
dchrmusum.d D = Base G
dchrmusum.1 1 ˙ = 0 G
dchrmusum.b φ X D
dchrmusum.n1 φ X 1 ˙
Assertion dchrmusum φ x + n = 1 x X L n μ n n 𝑂1

Proof

Step Hyp Ref Expression
1 rpvmasum.z Z = /N
2 rpvmasum.l L = ℤRHom Z
3 rpvmasum.a φ N
4 dchrmusum.g G = DChr N
5 dchrmusum.d D = Base G
6 dchrmusum.1 1 ˙ = 0 G
7 dchrmusum.b φ X D
8 dchrmusum.n1 φ X 1 ˙
9 eqid a X L a a = a X L a a
10 1 2 3 4 5 6 7 8 9 dchrmusumlema φ t c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y
11 3 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y N
12 7 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X D
13 8 adantr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y X 1 ˙
14 simprl φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y c 0 +∞
15 simprrl φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y seq 1 + a X L a a t
16 simprrr φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y y 1 +∞ seq 1 + a X L a a y t c y
17 1 2 11 4 5 6 12 13 9 14 15 16 dchrmusumlem φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y x + n = 1 x X L n μ n n 𝑂1
18 17 rexlimdvaa φ c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y x + n = 1 x X L n μ n n 𝑂1
19 18 exlimdv φ t c 0 +∞ seq 1 + a X L a a t y 1 +∞ seq 1 + a X L a a y t c y x + n = 1 x X L n μ n n 𝑂1
20 10 19 mpd φ x + n = 1 x X L n μ n n 𝑂1