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 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
dchrmusum.g 𝐺 = ( DChr ‘ 𝑁 )
dchrmusum.d 𝐷 = ( Base ‘ 𝐺 )
dchrmusum.1 1 = ( 0g𝐺 )
dchrmusum.b ( 𝜑𝑋𝐷 )
dchrmusum.n1 ( 𝜑𝑋1 )
dchrmusum.f 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) )
dchrmusum.c ( 𝜑𝐶 ∈ ( 0 [,) +∞ ) )
dchrmusum.t ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
dchrmusum.2 ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
Assertion dchrmusumlem ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
4 dchrmusum.g 𝐺 = ( DChr ‘ 𝑁 )
5 dchrmusum.d 𝐷 = ( Base ‘ 𝐺 )
6 dchrmusum.1 1 = ( 0g𝐺 )
7 dchrmusum.b ( 𝜑𝑋𝐷 )
8 dchrmusum.n1 ( 𝜑𝑋1 )
9 dchrmusum.f 𝐹 = ( 𝑎 ∈ ℕ ↦ ( ( 𝑋 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) )
10 dchrmusum.c ( 𝜑𝐶 ∈ ( 0 [,) +∞ ) )
11 dchrmusum.t ( 𝜑 → seq 1 ( + , 𝐹 ) ⇝ 𝑇 )
12 dchrmusum.2 ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , 𝐹 ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑇 ) ) ≤ ( 𝐶 / 𝑦 ) )
13 fzfid ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
14 7 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋𝐷 )
15 elfzelz ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
16 15 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
17 4 1 5 2 14 16 dchrzrhcl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿𝑛 ) ) ∈ ℂ )
18 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
19 18 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
20 mucl ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
21 19 20 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
22 21 zred ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
23 22 19 nndivred ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
24 23 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
25 17 24 mulcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
26 13 25 fsumcl ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
27 climcl ( seq 1 ( + , 𝐹 ) ⇝ 𝑇𝑇 ∈ ℂ )
28 11 27 syl ( 𝜑𝑇 ∈ ℂ )
29 28 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑇 ∈ ℂ )
30 26 29 mulcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) ∈ ℂ )
31 1 2 3 4 5 6 7 8 9 10 11 12 dchrisumn0 ( 𝜑𝑇 ≠ 0 )
32 31 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑇 ≠ 0 )
33 30 29 32 divrecd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) / 𝑇 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) )
34 26 29 32 divcan4d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) / 𝑇 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
35 33 34 eqtr3d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) )
36 35 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) )
37 28 31 reccld ( 𝜑 → ( 1 / 𝑇 ) ∈ ℂ )
38 37 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 / 𝑇 ) ∈ ℂ )
39 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) ) ∈ 𝑂(1) )
40 rpssre + ⊆ ℝ
41 o1const ( ( ℝ+ ⊆ ℝ ∧ ( 1 / 𝑇 ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑇 ) ) ∈ 𝑂(1) )
42 40 37 41 sylancr ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑇 ) ) ∈ 𝑂(1) )
43 30 38 39 42 o1mul2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) · 𝑇 ) · ( 1 / 𝑇 ) ) ) ∈ 𝑂(1) )
44 36 43 eqeltrrd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) · ( ( μ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )