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 | |
|
rpvmasum.l | |
||
rpvmasum.a | |
||
dchrmusum.g | |
||
dchrmusum.d | |
||
dchrmusum.1 | |
||
dchrmusum.b | |
||
dchrmusum.n1 | |
||
Assertion | dchrmusum | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rpvmasum.z | |
|
2 | rpvmasum.l | |
|
3 | rpvmasum.a | |
|
4 | dchrmusum.g | |
|
5 | dchrmusum.d | |
|
6 | dchrmusum.1 | |
|
7 | dchrmusum.b | |
|
8 | dchrmusum.n1 | |
|
9 | eqid | |
|
10 | 1 2 3 4 5 6 7 8 9 | dchrmusumlema | |
11 | 3 | adantr | |
12 | 7 | adantr | |
13 | 8 | adantr | |
14 | simprl | |
|
15 | simprrl | |
|
16 | simprrr | |
|
17 | 1 2 11 4 5 6 12 13 9 14 15 16 | dchrmusumlem | |
18 | 17 | rexlimdvaa | |
19 | 18 | exlimdv | |
20 | 10 19 | mpd | |