P. 275 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27401-27500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	vmadivsumb 27401*	Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐
Theorem	rplogsumlem1 27402*	Lemma for rplogsum 27445. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2)
Theorem	rplogsumlem2 27403*	Lemma for rplogsum 27445. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
Theorem	dchrisum0lem1a 27404	Lemma for dchrisum0lem1 27434. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ (((𝜑 ∧ 𝑋 ∈ ℝ+) ∧ 𝐷 ∈ (1...(⌊‘𝑋))) → (𝑋 ≤ ((𝑋↑2) / 𝐷) ∧ (⌊‘((𝑋↑2) / 𝐷)) ∈ (ℤ≥‘(⌊‘𝑋))))
Theorem	rpvmasumlem 27405*	Lemma for rpvmasum 27444. Calculate the "trivial case" estimate Σ𝑛 ≤ 𝑥( 1 (𝑛)Λ(𝑛) / 𝑛) = log𝑥 + 𝑂(1), where 1 (𝑥) is the principal Dirichlet character. Equation 9.4.7 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
Theorem	dchrisumlema 27406*	Lemma for dchrisum 27410. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))    ⇒   ⊢ (𝜑 → ((𝐼 ∈ ℝ+ → ⦋𝐼 / 𝑛⦌𝐴 ∈ ℝ) ∧ (𝐼 ∈ (𝑀[,)+∞) → 0 ≤ ⦋𝐼 / 𝑛⦌𝐴)))
Theorem	dchrisumlem1 27407*	Lemma for dchrisum 27410. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)    ⇒   ⊢ ((𝜑 ∧ 𝑈 ∈ ℕ0) → (abs‘Σ𝑛 ∈ (0..^𝑈)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)
Theorem	dchrisumlem2 27408*	Lemma for dchrisum 27410. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)    &   ⊢ (𝜑 → 𝑈 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑀 ≤ 𝑈)    &   ⊢ (𝜑 → 𝑈 ≤ (𝐼 + 1))    &   ⊢ (𝜑 → 𝐼 ∈ ℕ)    &   ⊢ (𝜑 → 𝐽 ∈ (ℤ≥‘𝐼))    ⇒   ⊢ (𝜑 → (abs‘((seq1( + , 𝐹)‘𝐽) − (seq1( + , 𝐹)‘𝐼))) ≤ ((2 · 𝑅) · ⦋𝑈 / 𝑛⦌𝐴))
Theorem	dchrisumlem3 27409*	Lemma for dchrisum 27410. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑢 ∈ (0..^𝑁)(abs‘Σ𝑛 ∈ (0..^𝑢)(𝑋‘(𝐿‘𝑛))) ≤ 𝑅)    ⇒   ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
Theorem	dchrisum 27410*	If 𝑛 ∈ [𝑀, +∞) ↦ 𝐴(𝑛) is a positive decreasing function approaching zero, then the infinite sum Σ𝑛, 𝑋(𝑛)𝐴(𝑛) is convergent, with the partial sum Σ𝑛 ≤ 𝑥, 𝑋(𝑛)𝐴(𝑛) within 𝑂(𝐴(𝑀)) of the limit 𝑇. Lemma 9.4.1 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝑛 = 𝑥 → 𝐴 = 𝐵)    &   ⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ ℝ+) → 𝐴 ∈ ℝ)    &   ⊢ ((𝜑 ∧ (𝑛 ∈ ℝ+ ∧ 𝑥 ∈ ℝ+) ∧ (𝑀 ≤ 𝑛 ∧ 𝑛 ≤ 𝑥)) → 𝐵 ≤ 𝐴)    &   ⊢ (𝜑 → (𝑛 ∈ ℝ+ ↦ 𝐴) ⇝𝑟 0)    &   ⊢ 𝐹 = (𝑛 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑛)) · 𝐴))    ⇒   ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑥 ∈ (𝑀[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑥)) − 𝑡)) ≤ (𝑐 · 𝐵)))
Theorem	dchrmusumlema 27411*	Lemma for dchrmusum 27442 and dchrisumn0 27439. Apply dchrisum 27410 for the function 1 / 𝑦. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    ⇒   ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))
Theorem	dchrmusum2 27412*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded, provided that 𝑇 ≠ 0. Lemma 9.4.2 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · 𝑇)) ∈ 𝑂(1))
Theorem	dchrvmasumlem1 27413*	An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of [Shapiro], p. 377. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘𝑚) / 𝑚))))
Theorem	dchrvmasum2lem 27414*	Give an expression for log𝑥 remarkably similar to Σ𝑛 ≤ 𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 27413. Part of Lemma 9.4.3 of [Shapiro], p. 380. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (log‘𝐴) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘((𝐴 / 𝑑) / 𝑚)) / 𝑚))))
Theorem	dchrvmasum2if 27415*	Combine the results of dchrvmasumlem1 27413 and dchrvmasum2lem 27414 inside a conditional. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ (𝜑 → (Σ𝑛 ∈ (1...(⌊‘𝐴))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝜓, (log‘𝐴), 0)) = Σ𝑑 ∈ (1...(⌊‘𝐴))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · Σ𝑚 ∈ (1...(⌊‘(𝐴 / 𝑑)))((𝑋‘(𝐿‘𝑚)) · ((log‘if(𝜓, (𝐴 / 𝑑), 𝑚)) / 𝑚))))
Theorem	dchrvmasumlem2 27416*	Lemma for dchrvmasum 27443. (Contributed by Mario Carneiro, 4-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈ ℂ)    &   ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1))
Theorem	dchrvmasumlem3 27417*	Lemma for dchrvmasum 27443. (Contributed by Mario Carneiro, 3-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈ ℂ)    &   ⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾)    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → 𝑇 ∈ ℂ)    &   ⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚)))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ)    &   ⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1))
Theorem	dchrvmasumlema 27418*	Lemma for dchrvmasum 27443 and dchrvmasumif 27421. Apply dchrisum 27410 for the function log(𝑦) / 𝑦, which is decreasing above e (or above 3, the nearest integer bound). (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎)))    ⇒   ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 · ((log‘𝑦) / 𝑦))))
Theorem	dchrvmasumiflem1 27419*	Lemma for dchrvmasumif 27421. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))    &   ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎)))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑑 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1))
Theorem	dchrvmasumiflem2 27420*	Lemma for dchrvmasum 27443. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))    &   ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎)))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑆 = 0, (log‘𝑥), 0))) ∈ 𝑂(1))
Theorem	dchrvmasumif 27421*	An asymptotic approximation for the sum of 𝑋(𝑛)Λ(𝑛) / 𝑛 conditional on the value of the infinite sum 𝑆. (We will later show that the case 𝑆 = 0 is impossible, and hence establish dchrvmasum 27443.) (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑆 = 0, (log‘𝑥), 0))) ∈ 𝑂(1))
Theorem	dchrvmaeq0 27422*	The set 𝑊 is the collection of all non-principal Dirichlet characters such that the sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is equal to zero. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦))    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    ⇒   ⊢ (𝜑 → (𝑋 ∈ 𝑊 ↔ 𝑆 = 0))
Theorem	dchrisum0fval 27423*	Value of the function 𝐹, the divisor sum of a Dirichlet character. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    ⇒   ⊢ (𝐴 ∈ ℕ → (𝐹‘𝐴) = Σ𝑡 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝐴} (𝑋‘(𝐿‘𝑡)))
Theorem	dchrisum0fmul 27424*	The function 𝐹, the divisor sum of a Dirichlet character, is a multiplicative function (but not completely multiplicative). Equation 9.4.27 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐹‘(𝐴 · 𝐵)) = ((𝐹‘𝐴) · (𝐹‘𝐵)))
Theorem	dchrisum0ff 27425*	The function 𝐹 is a real function. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶ℝ)
Theorem	dchrisum0flblem1 27426*	Lemma for dchrisum0flb 27428. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑𝐴)))
Theorem	dchrisum0flblem2 27427*	Lemma for dchrisum0flb 27428. Induction over relatively prime factors, with the prime power case handled in dchrisum0flblem1 . (Contributed by Mario Carneiro, 5-May-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝑃 ∥ 𝐴)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1..^𝐴)if((√‘𝑦) ∈ ℕ, 1, 0) ≤ (𝐹‘𝑦))    ⇒   ⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤ (𝐹‘𝐴))
Theorem	dchrisum0flb 27428*	The divisor sum of a real Dirichlet character, is lower bounded by zero everywhere and one at the squares. Equation 9.4.29 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    ⇒   ⊢ (𝜑 → if((√‘𝐴) ∈ ℕ, 1, 0) ≤ (𝐹‘𝐴))
Theorem	dchrisum0fno1 27429*	The sum Σ𝑘 ≤ 𝑥, 𝐹(𝑥) / √𝑘 is divergent (i.e. not eventually bounded). Equation 9.4.30 of [Shapiro], p. 383. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    &   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑘 ∈ (1...(⌊‘𝑥))((𝐹‘𝑘) / (√‘𝑘))) ∈ 𝑂(1))    ⇒   ⊢ ¬ 𝜑
Theorem	rpvmasum2 27430*	A partial result along the lines of rpvmasum 27444. The sum of the von Mangoldt function over those integers 𝑛≡𝐴 (mod 𝑁) is asymptotic to (1 − 𝑀)(log𝑥 / ϕ(𝑥)) + 𝑂(1), where 𝑀 is the number of non-principal Dirichlet characters with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Our goal is to show this set is empty. Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ 𝑇 = (◡𝐿 “ {𝐴})    &   ⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → 𝐴 = (1r‘𝑍))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1))
Theorem	dchrisum0re 27431*	Suppose 𝑋 is a non-principal Dirichlet character with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Then 𝑋 is a real character. Part of Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    ⇒   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)
Theorem	dchrisum0lema 27432*	Lemma for dchrisum0 27438. Apply dchrisum 27410 for the function 1 / √𝑦. (Contributed by Mario Carneiro, 10-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))    ⇒   ⊢ (𝜑 → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , 𝐹) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / (√‘𝑦))))
Theorem	dchrisum0lem1b 27433*	Lemma for dchrisum0lem1 27434. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))    ⇒   ⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈ (1...(⌊‘𝑥))) → (abs‘Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘((𝑥↑2) / 𝑑)))((𝑋‘(𝐿‘𝑚)) / (√‘𝑚))) ≤ ((2 · 𝐶) / (√‘𝑥)))
Theorem	dchrisum0lem1 27434*	Lemma for dchrisum0 27438. (Contributed by Mario Carneiro, 12-May-2016.) (Revised by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (((⌊‘𝑥) + 1)...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))
Theorem	dchrisum0lem2a 27435*	Lemma for dchrisum0 27438. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))    &   ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) · (𝐻‘((𝑥↑2) / 𝑚)))) ∈ 𝑂(1))
Theorem	dchrisum0lem2 27436*	Lemma for dchrisum0 27438. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))    &   ⊢ 𝐻 = (𝑦 ∈ ℝ+ ↦ (Σ𝑑 ∈ (1...(⌊‘𝑦))(1 / (√‘𝑑)) − (2 · (√‘𝑦))))    &   ⊢ (𝜑 → 𝐻 ⇝𝑟 𝑈)    &   ⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 / 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))(((𝑋‘(𝐿‘𝑚)) / (√‘𝑚)) / (√‘𝑑))) ∈ 𝑂(1))
Theorem	dchrisum0lem3 27437*	Lemma for dchrisum0 27438. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / (√‘𝑎)))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑆)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / (√‘𝑦)))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑚 ∈ (1...(⌊‘(𝑥↑2)))Σ𝑑 ∈ (1...(⌊‘((𝑥↑2) / 𝑚)))((𝑋‘(𝐿‘𝑚)) / (√‘(𝑚 · 𝑑)))) ∈ 𝑂(1))
Theorem	dchrisum0 27438*	The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows to eliminate the conditionals from dchrmusum2 27412 and dchrvmasumif 27421. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0}    &   ⊢ (𝜑 → 𝑋 ∈ 𝑊)    ⇒   ⊢ ¬ 𝜑
Theorem	dchrisumn0 27439*	The sum Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 is nonzero for all non-principal Dirichlet characters (i.e. the assumption 𝑋 ∈ 𝑊 is contradictory). This is the key result that allows to eliminate the conditionals from dchrmusum2 27412 and dchrvmasumif 27421. Lemma 9.4.4 of [Shapiro], p. 382. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦))    ⇒   ⊢ (𝜑 → 𝑇 ≠ 0)
Theorem	dchrmusumlem 27440*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((μ‘𝑛) / 𝑛))) ∈ 𝑂(1))
Theorem	dchrvmasumlem 27441*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    &   ⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎))    &   ⊢ (𝜑 → 𝐶 ∈ (0[,)+∞))    &   ⊢ (𝜑 → seq1( + , 𝐹) ⇝ 𝑇)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐶 / 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1))
Theorem	dchrmusum 27442*	The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((μ‘𝑛) / 𝑛))) ∈ 𝑂(1))
Theorem	dchrvmasum 27443*	The sum of the von Mangoldt function multiplied by a non-principal Dirichlet character, divided by 𝑛, is bounded. Equation 9.4.8 of [Shapiro], p. 376. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋 ≠ 1 )    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑋‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ 𝑂(1))
Theorem	rpvmasum 27444*	The sum of the von Mangoldt function over those integers 𝑛≡𝐴 (mod 𝑁) is asymptotic to log𝑥 / ϕ(𝑥) + 𝑂(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 2-May-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ 𝑇 = (◡𝐿 “ {𝐴})    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
Theorem	rplogsum 27445*	The sum of log𝑝 / 𝑝 over the primes 𝑝≡𝐴 (mod 𝑁) is asymptotic to log𝑥 / ϕ(𝑥) + 𝑂(1). Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ 𝑇 = (◡𝐿 “ {𝐴})    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑝 ∈ ((1...(⌊‘𝑥)) ∩ (ℙ ∩ 𝑇))((log‘𝑝) / 𝑝)) − (log‘𝑥))) ∈ 𝑂(1))
Theorem	dirith2 27446	Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to 𝑁. Theorem 9.4.1 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 30-Apr-2016.) (Proof shortened by Mario Carneiro, 26-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝑈 = (Unit‘𝑍)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑈)    &   ⊢ 𝑇 = (◡𝐿 “ {𝐴})    ⇒   ⊢ (𝜑 → (ℙ ∩ 𝑇) ≈ ℕ)
Theorem	dirith 27447*	Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to 𝑁. Theorem 9.4.1 of [Shapiro], p. 375. See https://metamath-blog.blogspot.com/2016/05/dirichlets-theorem.html for an informal exposition. This is Metamath 100 proof #48. (Contributed by Mario Carneiro, 12-May-2016.)
⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ ℤ ∧ (𝐴 gcd 𝑁) = 1) → {𝑝 ∈ ℙ ∣ 𝑁 ∥ (𝑝 − 𝐴)} ≈ ℕ)
14.4.13  The Prime Number Theorem
Theorem	mudivsum 27448*	Asymptotic formula for Σ𝑛 ≤ 𝑥, μ(𝑛) / 𝑛 = 𝑂(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)
Theorem	mulogsumlem 27449*	Lemma for mulogsum 27450. (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)
Theorem	mulogsum 27450*	Asymptotic formula for Σ𝑛 ≤ 𝑥, (μ(𝑛) / 𝑛)log(𝑥 / 𝑛) = 𝑂(1). Equation 10.2.6 of [Shapiro], p. 406. (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1)
Theorem	logdivsum 27451*	Asymptotic analysis of Σ𝑛 ≤ 𝑥, log𝑛 / 𝑛 = (log𝑥)↑2 / 2 + 𝐿 + 𝑂(log𝑥 / 𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))    ⇒   ⊢ (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹 ⇝𝑟 𝐿 ∧ 𝐴 ∈ ℝ+ ∧ e ≤ 𝐴) → (abs‘((𝐹‘𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)))
Theorem	mulog2sumlem1 27452*	Asymptotic formula for Σ𝑛 ≤ 𝑥, log(𝑥 / 𝑛) / 𝑛 = (1 / 2)log↑2(𝑥) + γ · log𝑥 − 𝐿 + 𝑂(log𝑥 / 𝑥), with explicit constants. Equation 10.2.7 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 18-May-2016.)
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → e ≤ 𝐴)    ⇒   ⊢ (𝜑 → (abs‘(Σ𝑚 ∈ (1...(⌊‘𝐴))((log‘(𝐴 / 𝑚)) / 𝑚) − ((((log‘𝐴)↑2) / 2) + ((γ · (log‘𝐴)) − 𝐿)))) ≤ (2 · ((log‘𝐴) / 𝐴)))
Theorem	mulog2sumlem2 27453*	Lemma for mulog2sum 27455. (Contributed by Mario Carneiro, 19-May-2016.)
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)    &   ⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ · (log‘(𝑥 / 𝑛))) − 𝐿))    &   ⊢ 𝑅 = (((1 / 2) + (γ + (abs‘𝐿))) + Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚))    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1))
Theorem	mulog2sumlem3 27454*	Lemma for mulog2sum 27455. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
Theorem	mulog2sum 27455*	Asymptotic formula for Σ𝑛 ≤ 𝑥, (μ(𝑛) / 𝑛)log↑2(𝑥 / 𝑛) = 2log𝑥 + 𝑂(1). Equation 10.2.8 of [Shapiro], p. 407. (Contributed by Mario Carneiro, 19-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	vmalogdivsum2 27456*	The sum Σ𝑛 ≤ 𝑥, Λ(𝑛)log(𝑥 / 𝑛) / 𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
Theorem	vmalogdivsum 27457*	The sum Σ𝑛 ≤ 𝑥, Λ(𝑛)log𝑛 / 𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). Exercise 9.1.7 of [Shapiro], p. 336. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘𝑛)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
Theorem	2vmadivsumlem 27458*	Lemma for 2vmadivsum 27459. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
Theorem	2vmadivsum 27459*	The sum Σ𝑚𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛) / 𝑚𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)
Theorem	logsqvma 27460*	A formula for log↑2(𝑁) in terms of the primes. Equation 10.4.6 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} (Σ𝑢 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑑} ((Λ‘𝑢) · (Λ‘(𝑑 / 𝑢))) + ((Λ‘𝑑) · (log‘𝑑))) = ((log‘𝑁)↑2))
Theorem	logsqvma2 27461*	The Möbius inverse of logsqvma 27460. Equation 10.4.8 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁))))
Theorem	log2sumbnd 27462*	Bound on the difference between Σ𝑛 ≤ 𝐴, log↑2(𝑛) and the equivalent integral. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ ((𝐴 ∈ ℝ+ ∧ 1 ≤ 𝐴) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝐴))((log‘𝑛)↑2) − (𝐴 · (((log‘𝐴)↑2) + (2 − (2 · (log‘𝐴))))))) ≤ (((log‘𝐴)↑2) + 2))
Theorem	selberglem1 27463*	Lemma for selberg 27466. Estimation of the asymptotic part of selberglem3 27465. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)    ⇒   ⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberglem2 27464*	Lemma for selberg 27466. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)    ⇒   ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberglem3 27465*	Lemma for selberg 27466. Estimation of the left-hand side of logsqvma2 27461. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberg 27466*	Selberg's symmetry formula. The statement has many forms, and this one is equivalent to the statement that Σ𝑛 ≤ 𝑥, Λ(𝑛)log𝑛 + Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛) = 2𝑥log𝑥 + 𝑂(𝑥). Equation 10.4.10 of [Shapiro], p. 419. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selbergb 27467*	Convert eventual boundedness in selberg 27466 to boundedness on [1, +∞). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐
Theorem	selberg2lem 27468*	Lemma for selberg2 27469. Equation 10.4.12 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg2 27469*	Selberg's symmetry formula, using the second Chebyshev function. Equation 10.4.14 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberg2b 27470*	Convert eventual boundedness in selberg2 27469 to boundedness on any interval [𝐴, +∞). (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 25-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐
Theorem	chpdifbndlem1 27471*	Lemma for chpdifbnd 27473. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)    &   ⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ (1(,)+∞))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋[,](𝐴 · 𝑋)))    ⇒   ⊢ (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))))
Theorem	chpdifbndlem2 27472*	Lemma for chpdifbnd 27473. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)    &   ⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](𝐴 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑐 · (𝑥 / (log‘𝑥)))))
Theorem	chpdifbnd 27473*	A bound on the difference of nearby ψ values. Theorem 10.5.2 of [Shapiro], p. 427. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](𝐴 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑐 · (𝑥 / (log‘𝑥)))))
Theorem	logdivbnd 27474*	A bound on a sum of logs, used in pntlemk 27524. This is not as precise as logdivsum 27451 in its asymptotic behavior, but it is valid for all 𝑁 and does not require a limit value. (Contributed by Mario Carneiro, 13-Apr-2016.)
⊢ (𝑁 ∈ ℕ → Σ𝑛 ∈ (1...𝑁)((log‘𝑛) / 𝑛) ≤ ((((log‘𝑁) + 1)↑2) / 2))
Theorem	selberg3lem1 27475*	Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27469 (written here as Σ𝑛 ≤ 𝑥, Λ(𝑛)ψ(𝑥 / 𝑛)). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1))
Theorem	selberg3lem2 27476*	Lemma for selberg3 27477. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg3 27477*	Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27469 (written here as Σ𝑛 ≤ 𝑥, Λ(𝑛)ψ(𝑥 / 𝑛)). Equation 10.6.7 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ (((((ψ‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberg4lem1 27478*	Lemma for selberg4 27479. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1))
Theorem	selberg4 27479*	The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form Σ𝑖𝑗𝑘 ≤ 𝑥, Λ(𝑖)Λ(𝑗)Λ(𝑘); we eliminate one of the nested sums by using the definition of ψ(𝑥) = Σ𝑘 ≤ 𝑥, Λ(𝑘). This statement can thus equivalently be written ψ(𝑥)log↑2(𝑥) = 2Σ𝑖𝑗𝑘 ≤ 𝑥, Λ(𝑖)Λ(𝑗)Λ(𝑘) + 𝑂(𝑥log𝑥). Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)
Theorem	pntrval 27480*	Define the residual of the second Chebyshev function. The goal is to have 𝑅(𝑥) ∈ 𝑜(𝑥), or 𝑅(𝑥) / 𝑥 ⇝𝑟 0. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝐴 ∈ ℝ+ → (𝑅‘𝐴) = ((ψ‘𝐴) − 𝐴))
Theorem	pntrf 27481	Functionality of the residual. Lemma for pnt 27532. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ 𝑅:ℝ+⟶ℝ
Theorem	pntrmax 27482*	There is a bound on the residual valid for all 𝑥. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑐
Theorem	pntrsumo1 27483*	A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)
Theorem	pntrsumbnd 27484*	A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐
Theorem	pntrsumbnd2 27485*	A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 14-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐
Theorem	selbergr 27486*	Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ ℝ+ ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg3r 27487*	Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg4r 27488*	Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg34r 27489*	The sum of selberg3r 27487 and selberg4r 27488. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)
Theorem	pntsval 27490*	Define the "Selberg function", whose asymptotic behavior is the content of selberg 27466. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑆‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝐴 / 𝑛)))))
Theorem	pntsf 27491*	Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ 𝑆:ℝ⟶ℝ
Theorem	selbergs 27492*	Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ (𝑥 ∈ ℝ+ ↦ (((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selbergsb 27493*	Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑥) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐
Theorem	pntsval2 27494*	The Selberg function can be expressed using the convolution product of the von Mangoldt function with itself. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑆‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))(((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))
Theorem	pntrlog2bndlem1 27495*	The sum of selberg3r 27487 and selberg4r 27488. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)
Theorem	pntrlog2bndlem2 27496*	Lemma for pntrlog2bnd 27502. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (ψ‘𝑦) ≤ (𝐴 · 𝑦))    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(𝑛 · (abs‘((𝑅‘(𝑥 / (𝑛 + 1))) − (𝑅‘(𝑥 / 𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
Theorem	pntrlog2bndlem3 27497*	Lemma for pntrlog2bnd 27502. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(((𝑆‘𝑦) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((abs‘(𝑅‘(𝑥 / 𝑛))) − (abs‘(𝑅‘(𝑥 / (𝑛 + 1))))) · ((𝑆‘𝑛) − (2 · (𝑛 · (log‘𝑛))))) / (𝑥 · (log‘𝑥)))) ∈ 𝑂(1))
Theorem	pntrlog2bndlem4 27498*	Lemma for pntrlog2bnd 27502. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑇‘𝑛) − (𝑇‘(𝑛 − 1)))))) / 𝑥)) ∈ ≤𝑂(1)
Theorem	pntrlog2bndlem5 27499*	Lemma for pntrlog2bnd 27502. Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1))
Theorem	pntrlog2bndlem6a 27500*	Lemma for pntrlog2bndlem6 27501. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = ((1...(⌊‘(𝑥 / 𝐴))) ∪ (((⌊‘(𝑥 / 𝐴)) + 1)...(⌊‘𝑥))))