Metamath Proof Explorer

Theorem dchrvmasumlem

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 dchrvmasumlem ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 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 1 2 3 4 5 6 7 8 9 10 11 12 dchrisumn0 ⊢ ( 𝜑 → 𝑇 ≠ 0 )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝑇 ≠ 0 )
15 ifnefalse ⊢ ( 𝑇 ≠ 0 → if ( 𝑇 = 0 , ( log ‘ 𝑥 ) , 0 ) = 0 )
16 14 15 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑇 = 0 , ( log ‘ 𝑥 ) , 0 ) = 0 )
17 16 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑇 = 0 , ( log ‘ 𝑥 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + 0 ) )
18 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
19 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑋 ∈ 𝐷 )
20 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
21 20 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
22 4 1 5 2 19 21 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
23 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
24 23 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
25 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
26 nndivre ⊢ ( ( ( Λ ‘ 𝑛 ) ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
27 25 26 mpancom ⊢ ( 𝑛 ∈ ℕ → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
28 24 27 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
29 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
30 22 29 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
31 18 30 fsumcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
32 31 addridd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + 0 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
33 17 32 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑇 = 0 , ( log ‘ 𝑥 ) , 0 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
34 33 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑇 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 dchrvmasumif ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑇 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )
36 34 35 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ 𝑂(1) )