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	2sqreuop 27401*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two nonnegative integers. Ordered pair variant of 2sqreu 27395. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuopnn 27402*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two positive integers. Ordered pair variant of 2sqreunn 27396. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) ≤ (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuoplt 27403*	There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers. Ordered pair variant of 2sqreult 27397. (Contributed by AV, 2-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuopltb 27404*	There exists a unique decomposition of a prime as a sum of squares of two different nonnegative integers iff 𝑃≡1 (mod 4). Ordered pair variant of 2sqreultb 27398. (Contributed by AV, 3-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ0 × ℕ0)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)))
Theorem	2sqreuopnnlt 27405*	There exists a unique decomposition of a prime of the form 4𝑘 + 1 as a sum of squares of two different positive integers. Ordered pair variant of 2sqreunnlt 27399. (Contributed by AV, 3-Jul-2023.)
⊢ ((𝑃 ∈ ℙ ∧ (𝑃 mod 4) = 1) → ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃))
Theorem	2sqreuopnnltb 27406*	There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Ordered pair variant of 2sqreunnltb 27400. (Contributed by AV, 3-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)((1st ‘𝑝) < (2nd ‘𝑝) ∧ (((1st ‘𝑝)↑2) + ((2nd ‘𝑝)↑2)) = 𝑃)))
Theorem	2sqreuopb 27407*	There exists a unique decomposition of a prime as a sum of squares of two different positive integers iff the prime is of the form 4𝑘 + 1. Alternate ordered pair variant of 2sqreunnltb 27400. (Contributed by AV, 3-Jul-2023.)
⊢ (𝑃 ∈ ℙ → ((𝑃 mod 4) = 1 ↔ ∃!𝑝 ∈ (ℕ × ℕ)∃𝑎∃𝑏(𝑝 = ⟨𝑎, 𝑏⟩ ∧ (𝑎 < 𝑏 ∧ ((𝑎↑2) + (𝑏↑2)) = 𝑃))))
14.4.12  Chebyshev's Weak Prime Number Theorem, Dirichlet's Theorem
Theorem	chebbnd1lem1 27408	Lemma for chebbnd1 27411: show a lower bound on π(𝑥) at even integers using similar techniques to those used to prove bpos 27232. (Note that the expression 𝐾 is actually equal to 2 · 𝑁, but proving that is not necessary for the proof, and it's too much work.) The key to the proof is bposlem1 27223, which shows that each term in the expansion ((2 · 𝑁)C𝑁) = ∏𝑝 ∈ ℙ (𝑝↑(𝑝 pCnt ((2 · 𝑁)C𝑁))) is at most 2 · 𝑁, so that the sum really only has nonzero elements up to 2 · 𝑁, and since each term is at most 2 · 𝑁, after taking logs we get the inequality π(2 · 𝑁) · log(2 · 𝑁) ≤ log((2 · 𝑁)C𝑁), and bclbnd 27219 finishes the proof. (Contributed by Mario Carneiro, 22-Sep-2014.) (Revised by Mario Carneiro, 15-Apr-2016.)
⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁))    ⇒   ⊢ (𝑁 ∈ (ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 · 𝑁)) · (log‘(2 · 𝑁))))
Theorem	chebbnd1lem2 27409	Lemma for chebbnd1 27411: Show that log(𝑁) / 𝑁 does not change too much between 𝑁 and 𝑀 = ⌊(𝑁 / 2). (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ 𝑀 = (⌊‘(𝑁 / 2))    ⇒   ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → ((log‘(2 · 𝑀)) / (2 · 𝑀)) < (2 · ((log‘𝑁) / 𝑁)))
Theorem	chebbnd1lem3 27410	Lemma for chebbnd1 27411: get a lower bound on π(𝑁) / (𝑁 / log(𝑁)) that is independent of 𝑁. (Contributed by Mario Carneiro, 21-Sep-2014.)
⊢ 𝑀 = (⌊‘(𝑁 / 2))    ⇒   ⊢ ((𝑁 ∈ ℝ ∧ 8 ≤ 𝑁) → (((log‘2) − (1 / (2 · e))) / 2) < ((π‘𝑁) · ((log‘𝑁) / 𝑁)))
Theorem	chebbnd1 27411	The Chebyshev bound: The function π(𝑥) is eventually lower bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function (𝑥 / log(𝑥)) / π(𝑥) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1)
Theorem	chtppilimlem1 27412	Lemma for chtppilim 27414. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 1)    &   ⊢ (𝜑 → 𝑁 ∈ (2[,)+∞))    &   ⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴))    ⇒   ⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁))
Theorem	chtppilimlem2 27413*	Lemma for chtppilim 27414. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐴 < 1)    ⇒   ⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))
Theorem	chtppilim 27414	The θ function is asymptotic to π(𝑥)log(𝑥), so it is sufficient to prove θ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟 1
Theorem	chto1ub 27415	The θ function is upper bounded by a linear term. Corollary of chtub 27151. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1)
Theorem	chebbnd2 27416	The Chebyshev bound, part 2: The function π(𝑥) is eventually upper bounded by a positive constant times 𝑥 / log(𝑥). Alternatively stated, the function π(𝑥) / (𝑥 / log(𝑥)) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014.)
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((π‘𝑥) / (𝑥 / (log‘𝑥)))) ∈ 𝑂(1)
Theorem	chto1lb 27417	The θ function is lower bounded by a linear term. Corollary of chebbnd1 27411. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) ∈ 𝑂(1)
Theorem	chpchtlim 27418	The ψ and θ functions are asymptotic to each other, so is sufficient to prove either θ(𝑥) / 𝑥 ⇝𝑟 1 or ψ(𝑥) / 𝑥 ⇝𝑟 1 to establish the PNT. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ (𝑥 ∈ (2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟 1
Theorem	chpo1ub 27419	The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ∈ 𝑂(1)
Theorem	chpo1ubb 27420*	The ψ function is upper bounded by a linear term. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (ψ‘𝑥) ≤ (𝑐 · 𝑥)
Theorem	vmadivsum 27421*	The sum of the von Mangoldt function over 𝑛 is asymptotic to log𝑥 + 𝑂(1). Equation 9.2.13 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 16-Apr-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)
Theorem	vmadivsumb 27422*	Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1[,)+∞)(abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ≤ 𝑐
Theorem	rplogsumlem1 27423*	Lemma for rplogsum 27466. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝐴 ∈ ℕ → Σ𝑛 ∈ (2...𝐴)((log‘𝑛) / (𝑛 · (𝑛 − 1))) ≤ 2)
Theorem	rplogsumlem2 27424*	Lemma for rplogsum 27466. Equation 9.2.14 of [Shapiro], p. 331. (Contributed by Mario Carneiro, 2-May-2016.)
⊢ (𝐴 ∈ ℤ → Σ𝑛 ∈ (1...𝐴)(((Λ‘𝑛) − if(𝑛 ∈ ℙ, (log‘𝑛), 0)) / 𝑛) ≤ 2)
Theorem	dchrisum0lem1a 27425	Lemma for dchrisum0lem1 27455. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ (((𝜑 ∧ 𝑋 ∈ ℝ+) ∧ 𝐷 ∈ (1...(⌊‘𝑋))) → (𝑋 ≤ ((𝑋↑2) / 𝐷) ∧ (⌊‘((𝑋↑2) / 𝐷)) ∈ (ℤ≥‘(⌊‘𝑋))))
Theorem	rpvmasumlem 27426*	Lemma for rpvmasum 27465. 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 27427*	Lemma for dchrisum 27431. 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 27428*	Lemma for dchrisum 27431. 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 27429*	Lemma for dchrisum 27431. 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 27430*	Lemma for dchrisum 27431. 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 27431*	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 27432*	Lemma for dchrmusum 27463 and dchrisumn0 27460. Apply dchrisum 27431 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 27433*	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 27434*	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 27435*	Give an expression for log𝑥 remarkably similar to Σ𝑛 ≤ 𝑥(𝑋(𝑛)Λ(𝑛) / 𝑛) given in dchrvmasumlem1 27434. 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 27436*	Combine the results of dchrvmasumlem1 27434 and dchrvmasum2lem 27435 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 27437*	Lemma for dchrvmasum 27464. (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 27438*	Lemma for dchrvmasum 27464. (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 27439*	Lemma for dchrvmasum 27464 and dchrvmasumif 27442. Apply dchrisum 27431 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 27440*	Lemma for dchrvmasumif 27442. (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 27441*	Lemma for dchrvmasum 27464. (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 27442*	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 27464.) (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 27443*	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 27444*	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 27445*	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 27446*	The function 𝐹 is a real function. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    ⇒   ⊢ (𝜑 → 𝐹:ℕ⟶ℝ)
Theorem	dchrisum0flblem1 27447*	Lemma for dchrisum0flb 27449. Base case, prime power. (Contributed by Mario Carneiro, 5-May-2016.)
⊢ 𝑍 = (ℤ/nℤ‘𝑁)    &   ⊢ 𝐿 = (ℤRHom‘𝑍)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ 𝐺 = (DChr‘𝑁)    &   ⊢ 𝐷 = (Base‘𝐺)    &   ⊢ 1 = (0g‘𝐺)    &   ⊢ 𝐹 = (𝑏 ∈ ℕ ↦ Σ𝑣 ∈ {𝑞 ∈ ℕ ∣ 𝑞 ∥ 𝑏} (𝑋‘(𝐿‘𝑣)))    &   ⊢ (𝜑 → 𝑋 ∈ 𝐷)    &   ⊢ (𝜑 → 𝑋:(Base‘𝑍)⟶ℝ)    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ0)    ⇒   ⊢ (𝜑 → if((√‘(𝑃↑𝐴)) ∈ ℕ, 1, 0) ≤ (𝐹‘(𝑃↑𝐴)))
Theorem	dchrisum0flblem2 27448*	Lemma for dchrisum0flb 27449. 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 27449*	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 27450*	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 27451*	A partial result along the lines of rpvmasum 27465. 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 27452*	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 27453*	Lemma for dchrisum0 27459. Apply dchrisum 27431 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 27454*	Lemma for dchrisum0lem1 27455. (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 27455*	Lemma for dchrisum0 27459. (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 27456*	Lemma for dchrisum0 27459. (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 27457*	Lemma for dchrisum0 27459. (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 27458*	Lemma for dchrisum0 27459. (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 27459*	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 27433 and dchrvmasumif 27442. 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 27460*	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 27433 and dchrvmasumif 27442. 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 27461*	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 27462*	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 27463*	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 27464*	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 27465*	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 27466*	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 27467	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 27468*	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 27469*	Asymptotic formula for Σ𝑛 ≤ 𝑥, μ(𝑛) / 𝑛 = 𝑂(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)
Theorem	mulogsumlem 27470*	Lemma for mulogsum 27471. (Contributed by Mario Carneiro, 14-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)
Theorem	mulogsum 27471*	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 27472*	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 27473*	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 27474*	Lemma for mulog2sum 27476. (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 27475*	Lemma for mulog2sum 27476. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))    &   ⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿)    ⇒   ⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 · (log‘𝑥)))) ∈ 𝑂(1))
Theorem	mulog2sum 27476*	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 27477*	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 27478*	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 27479*	Lemma for 2vmadivsum 27480. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)    ⇒   ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))
Theorem	2vmadivsum 27480*	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 27481*	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 27482*	The Möbius inverse of logsqvma 27481. Equation 10.4.8 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
⊢ (𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁))))
Theorem	log2sumbnd 27483*	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 27484*	Lemma for selberg 27487. Estimation of the asymptotic part of selberglem3 27486. (Contributed by Mario Carneiro, 20-May-2016.)
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)    ⇒   ⊢ (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberglem2 27485*	Lemma for selberg 27487. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)    ⇒   ⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberglem3 27486*	Lemma for selberg 27487. Estimation of the left-hand side of logsqvma2 27482. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)
Theorem	selberg 27487*	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 27488*	Convert eventual boundedness in selberg 27487 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 27489*	Lemma for selberg2 27490. Equation 10.4.12 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg2 27490*	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 27491*	Convert eventual boundedness in selberg2 27490 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 27492*	Lemma for chpdifbnd 27494. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)    &   ⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))    &   ⊢ (𝜑 → 𝑋 ∈ (1(,)+∞))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋[,](𝐴 · 𝑋)))    ⇒   ⊢ (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌 − 𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))))
Theorem	chpdifbndlem2 27493*	Lemma for chpdifbnd 27494. (Contributed by Mario Carneiro, 25-May-2016.)
⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)    &   ⊢ 𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))    ⇒   ⊢ (𝜑 → ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](𝐴 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦 − 𝑥)) + (𝑐 · (𝑥 / (log‘𝑥)))))
Theorem	chpdifbnd 27494*	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 27495*	A bound on a sum of logs, used in pntlemk 27545. This is not as precise as logdivsum 27472 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 27496*	Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27490 (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 27497*	Lemma for selberg3 27498. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg3 27498*	Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27490 (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 27499*	Lemma for selberg4 27500. 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 27500*	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)