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