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 | |
||
dchrmusum.f | |
||
dchrmusum.c | |
||
dchrmusum.t | |
||
dchrmusum.2 | |
||
Assertion | dchrmusumlem | |
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 | dchrmusum.f | |
|
10 | dchrmusum.c | |
|
11 | dchrmusum.t | |
|
12 | dchrmusum.2 | |
|
13 | fzfid | |
|
14 | 7 | ad2antrr | |
15 | elfzelz | |
|
16 | 15 | adantl | |
17 | 4 1 5 2 14 16 | dchrzrhcl | |
18 | elfznn | |
|
19 | 18 | adantl | |
20 | mucl | |
|
21 | 19 20 | syl | |
22 | 21 | zred | |
23 | 22 19 | nndivred | |
24 | 23 | recnd | |
25 | 17 24 | mulcld | |
26 | 13 25 | fsumcl | |
27 | climcl | |
|
28 | 11 27 | syl | |
29 | 28 | adantr | |
30 | 26 29 | mulcld | |
31 | 1 2 3 4 5 6 7 8 9 10 11 12 | dchrisumn0 | |
32 | 31 | adantr | |
33 | 30 29 32 | divrecd | |
34 | 26 29 32 | divcan4d | |
35 | 33 34 | eqtr3d | |
36 | 35 | mpteq2dva | |
37 | 28 31 | reccld | |
38 | 37 | adantr | |
39 | 1 2 3 4 5 6 7 8 9 10 11 12 | dchrmusum2 | |
40 | rpssre | |
|
41 | o1const | |
|
42 | 40 37 41 | sylancr | |
43 | 30 38 39 42 | o1mul2 | |
44 | 36 43 | eqeltrrd | |