Home Metamath Proof ExplorerTheorem List (p. 250 of 425) < Previous  Next > Bad symbols? Try the GIF version. Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

 Color key: Metamath Proof Explorer (1-26947) Hilbert Space Explorer (26948-28472) Users' Mathboxes (28473-42426)

Theorem List for Metamath Proof Explorer - 24901-25000   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremdchrvmasumlem 24901* 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))

Theoremdchrmusum 24902* 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))

Theoremdchrvmasum 24903* 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))

Theoremrpvmasum 24904* 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))

Theoremrplogsum 24905* 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))

Theoremdirith2 24906 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‘𝑍)    &   (𝜑𝐴𝑈)    &   𝑇 = (𝐿 “ {𝐴})       (𝜑 → (ℙ ∩ 𝑇) ≈ ℕ)

Theoremdirith 24907* Dirichlet's theorem: there are infinitely many primes in any arithmetic progression coprime to 𝑁. Theorem 9.4.1 of [Shapiro], p. 375. See http://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

Theoremmudivsum 24908* Asymptotic formula for Σ𝑛𝑥, μ(𝑛) / 𝑛 = 𝑂(1). Equation 10.2.1 of [Shapiro], p. 405. (Contributed by Mario Carneiro, 14-May-2016.)
(𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) / 𝑛)) ∈ 𝑂(1)

Theoremmulogsumlem 24909* Lemma for mulogsum 24910. (Contributed by Mario Carneiro, 14-May-2016.)
(𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(1 / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ 𝑂(1)

Theoremmulogsum 24910* Asymptotic formula for Σ𝑛𝑥, (μ(𝑛) / 𝑛)log(𝑥 / 𝑛) = 𝑂(1). Equation 10.2.6 of [Shapiro], p. 406. (Contributed by Mario Carneiro, 14-May-2016.)
(𝑥 ∈ ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) ∈ 𝑂(1)

Theoremlogdivsum 24911* Asymptotic analysis of Σ𝑛𝑥, log𝑛 / 𝑛 = (log𝑥)↑2 / 2 + 𝐿 + 𝑂(log𝑥 / 𝑥). (Contributed by Mario Carneiro, 18-May-2016.)
𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))       (𝐹:ℝ+⟶ℝ ∧ 𝐹 ∈ dom ⇝𝑟 ∧ ((𝐹𝑟 𝐿𝐴 ∈ ℝ+ ∧ e ≤ 𝐴) → (abs‘((𝐹𝐴) − 𝐿)) ≤ ((log‘𝐴) / 𝐴)))

Theoremmulog2sumlem1 24912* 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‘𝐴) / 𝐴)))

Theoremmulog2sumlem2 24913* Lemma for mulog2sum 24915. (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))

Theoremmulog2sumlem3 24914* Lemma for mulog2sum 24915. (Contributed by Mario Carneiro, 13-May-2016.)
𝐹 = (𝑦 ∈ ℝ+ ↦ (Σ𝑖 ∈ (1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2)))    &   (𝜑𝐹𝑟 𝐿)       (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · ((log‘(𝑥 / 𝑛))↑2)) − (2 · (log‘𝑥)))) ∈ 𝑂(1))

Theoremmulog2sum 24915* 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)

Theoremvmalogdivsum2 24916* 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)

Theoremvmalogdivsum 24917* 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)

(𝜑𝐴 ∈ ℝ+)    &   (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴)       (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1))

Theorem2vmadivsum 24919* The sum Σ𝑚𝑛𝑥, Λ(𝑚)Λ(𝑛) / 𝑚𝑛 is asymptotic to log↑2(𝑥) / 2 + 𝑂(log𝑥). (Contributed by Mario Carneiro, 30-May-2016.)
(𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1)

Theoremlogsqvma 24920* 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))

Theoremlogsqvma2 24921* The Möbius inverse of logsqvma 24920. Equation 10.4.8 of [Shapiro], p. 418. (Contributed by Mario Carneiro, 13-May-2016.)
(𝑁 ∈ ℕ → Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ((μ‘𝑑) · ((log‘(𝑁 / 𝑑))↑2)) = (Σ𝑑 ∈ {𝑥 ∈ ℕ ∣ 𝑥𝑁} ((Λ‘𝑑) · (Λ‘(𝑁 / 𝑑))) + ((Λ‘𝑁) · (log‘𝑁))))

Theoremlog2sumbnd 24922* 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))

Theoremselberglem1 24923* Lemma for selberg 24926. Estimation of the asymptotic part of selberglem3 24925. (Contributed by Mario Carneiro, 20-May-2016.)
𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)       (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Theoremselberglem2 24924* Lemma for selberg 24926. (Contributed by Mario Carneiro, 23-May-2016.)
𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 · (log‘(𝑥 / 𝑛))))) / 𝑛)       (𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Theoremselberglem3 24925* Lemma for selberg 24926. Estimation of the left-hand side of logsqvma2 24921. (Contributed by Mario Carneiro, 23-May-2016.)
(𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑑 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((μ‘𝑑) · ((log‘(𝑛 / 𝑑))↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Theoremselberg 24926* 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)

Theoremselbergb 24927* Convert eventual boundedness in selberg 24926 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‘𝑥)))) ≤ 𝑐

Theoremselberg2lem 24928* Lemma for selberg2 24929. Equation 10.4.12 of [Shapiro], p. 420. (Contributed by Mario Carneiro, 23-May-2016.)
(𝑥 ∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (log‘𝑛)) − ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)

Theoremselberg2 24929* 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)

Theoremselberg2b 24930* Convert eventual boundedness in selberg2 24929 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‘𝑥)))) ≤ 𝑐

Theoremchpdifbndlem1 24931* Lemma for chpdifbnd 24933. (Contributed by Mario Carneiro, 25-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑 → 1 ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)    &   𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))    &   (𝜑𝑋 ∈ (1(,)+∞))    &   (𝜑𝑌 ∈ (𝑋[,](𝐴 · 𝑋)))       (𝜑 → ((ψ‘𝑌) − (ψ‘𝑋)) ≤ ((2 · (𝑌𝑋)) + (𝐶 · (𝑋 / (log‘𝑋)))))

Theoremchpdifbndlem2 24932* Lemma for chpdifbnd 24933. (Contributed by Mario Carneiro, 25-May-2016.)
(𝜑𝐴 ∈ ℝ+)    &   (𝜑 → 1 ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘(((((ψ‘𝑧) · (log‘𝑧)) + Σ𝑚 ∈ (1...(⌊‘𝑧))((Λ‘𝑚) · (ψ‘(𝑧 / 𝑚)))) / 𝑧) − (2 · (log‘𝑧)))) ≤ 𝐵)    &   𝐶 = ((𝐵 · (𝐴 + 1)) + ((2 · 𝐴) · (log‘𝐴)))       (𝜑 → ∃𝑐 ∈ ℝ+𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](𝐴 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑐 · (𝑥 / (log‘𝑥)))))

Theoremchpdifbnd 24933* 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‘𝑥)))))

Theoremlogdivbnd 24934* A bound on a sum of logs, used in pntlemk 24984. This is not as precise as logdivsum 24911 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))

Theoremselberg3lem1 24935* Introduce a log weighting on the summands of Σ𝑚 · 𝑛𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 24929 (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))

Theoremselberg3lem2 24936* Lemma for selberg3 24937. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
(𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)

Theoremselberg3 24937* Introduce a log weighting on the summands of Σ𝑚 · 𝑛𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 24929 (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)

Theoremselberg4lem1 24938* Lemma for selberg4 24939. 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))

Theoremselberg4 24939* 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(𝑥) = 𝑖𝑗𝑘𝑥, Λ(𝑖)Λ(𝑗)Λ(𝑘) + 𝑂(𝑥log𝑥). Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
(𝑥 ∈ (1(,)+∞) ↦ ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)

Theorempntrval 24940* Define the residual of the second Chebyshev function. The goal is to have 𝑅(𝑥) ∈ 𝑜(𝑥), or 𝑅(𝑥) / 𝑥𝑟 0. (Contributed by Mario Carneiro, 8-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       (𝐴 ∈ ℝ+ → (𝑅𝐴) = ((ψ‘𝐴) − 𝐴))

Theorempntrf 24941 Functionality of the residual. Lemma for pnt 24992. (Contributed by Mario Carneiro, 8-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       𝑅:ℝ+⟶ℝ

Theorempntrmax 24942* There is a bound on the residual valid for all 𝑥. (Contributed by Mario Carneiro, 9-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       𝑐 ∈ ℝ+𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝑐

Theorempntrsumo1 24943* A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1)

Theorempntrsumbnd 24944* A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       𝑐 ∈ ℝ+𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐

Theorempntrsumbnd2 24945* A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 14-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       𝑐 ∈ ℝ+𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐

Theoremselbergr 24946* 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)

Theoremselberg3r 24947* 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)

Theoremselberg4r 24948* 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)

Theoremselberg34r 24949* The sum of selberg3r 24947 and selberg4r 24948. (Contributed by Mario Carneiro, 31-May-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)

Theorempntsval 24950* Define the "Selberg function", whose asymptotic behavior is the content of selberg 24926. (Contributed by Mario Carneiro, 31-May-2016.)
𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))       (𝐴 ∈ ℝ → (𝑆𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝐴 / 𝑛)))))

Theorempntsf 24951* Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))       𝑆:ℝ⟶ℝ

Theoremselbergs 24952* Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))       (𝑥 ∈ ℝ+ ↦ (((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1)

Theoremselbergsb 24953* Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))       𝑐 ∈ ℝ+𝑥 ∈ (1[,)+∞)(abs‘(((𝑆𝑥) / 𝑥) − (2 · (log‘𝑥)))) ≤ 𝑐

Theorempntsval2 24954* 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‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))

Theorempntrlog2bndlem1 24955* The sum of selberg3r 24947 and selberg4r 24948. (Contributed by Mario Carneiro, 31-May-2016.)
𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)

Theorempntrlog2bndlem2 24956* Lemma for pntrlog2bnd 24962. 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))

Theorempntrlog2bndlem3 24957* Lemma for pntrlog2bnd 24962. 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))

Theorempntrlog2bndlem4 24958* Lemma for pntrlog2bnd 24962. 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)

Theorempntrlog2bndlem5 24959* Lemma for pntrlog2bnd 24962. 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))

Theorempntrlog2bndlem6a 24960* Lemma for pntrlog2bndlem6 24961. (Contributed by Mario Carneiro, 7-Jun-2016.)
𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐵)    &   (𝜑𝐴 ∈ ℝ)    &   (𝜑 → 1 ≤ 𝐴)       ((𝜑𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = ((1...(⌊‘(𝑥 / 𝐴))) ∪ (((⌊‘(𝑥 / 𝐴)) + 1)...(⌊‘𝑥))))

Theorempntrlog2bndlem6 24961* Lemma for pntrlog2bnd 24962. 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 ≤ 𝐴)       (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ ≤𝑂(1))

Theorempntrlog2bnd 24962* A bound on 𝑅(𝑥)log↑2(𝑥). Equation 10.6.15 of [Shapiro], p. 431. (Contributed by Mario Carneiro, 1-Jun-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       ((𝐴 ∈ ℝ ∧ 1 ≤ 𝐴) → ∃𝑐 ∈ ℝ+𝑥 ∈ (1(,)+∞)((((abs‘(𝑅𝑥)) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝐴)))((abs‘(𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) ≤ 𝑐)

Theorempntpbnd1a 24963* Lemma for pntpbnd 24966. (Contributed by Mario Carneiro, 11-Apr-2016.) Replace reference to OLD theorem. (Revised by Wolf Lammen, 8-Sep-2020.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐸 ∈ (0(,)1))    &   𝑋 = (exp‘(2 / 𝐸))    &   (𝜑𝑌 ∈ (𝑋(,)+∞))    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑 → (𝑌 < 𝑁𝑁 ≤ (𝐾 · 𝑌)))    &   (𝜑 → (abs‘(𝑅𝑁)) ≤ (abs‘((𝑅‘(𝑁 + 1)) − (𝑅𝑁))))       (𝜑 → (abs‘((𝑅𝑁) / 𝑁)) ≤ 𝐸)

Theorempntpbnd1 24964* Lemma for pntpbnd 24966. (Contributed by Mario Carneiro, 11-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐸 ∈ (0(,)1))    &   𝑋 = (exp‘(2 / 𝐸))    &   (𝜑𝑌 ∈ (𝑋(,)+∞))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)    &   𝐶 = (𝐴 + 2)    &   (𝜑𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))       (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)

Theorempntpbnd2 24965* Lemma for pntpbnd 24966. (Contributed by Mario Carneiro, 11-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐸 ∈ (0(,)1))    &   𝑋 = (exp‘(2 / 𝐸))    &   (𝜑𝑌 ∈ (𝑋(,)+∞))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)    &   𝐶 = (𝐴 + 2)    &   (𝜑𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅𝑦) / 𝑦)) ≤ 𝐸))        ¬ 𝜑

Theorempntpbnd 24966* Lemma for pnt 24992. Establish smallness of 𝑅 at a point. Lemma 10.6.1 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       𝑐 ∈ ℝ+𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑛 ∈ ℕ ((𝑦 < 𝑛𝑛 ≤ (𝑘 · 𝑦)) ∧ (abs‘((𝑅𝑛) / 𝑛)) ≤ 𝑒)

Theorempntibndlem1 24967 Lemma for pntibnd 24971. (Contributed by Mario Carneiro, 10-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   𝐿 = ((1 / 4) / (𝐴 + 3))       (𝜑𝐿 ∈ (0(,)1))

Theorempntibndlem2a 24968* Lemma for pntibndlem2 24969. (Contributed by Mario Carneiro, 7-Jun-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   𝐿 = ((1 / 4) / (𝐴 + 3))    &   (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   𝐾 = (exp‘(𝐵 / (𝐸 / 2)))    &   𝐶 = ((2 · 𝐵) + (log‘2))    &   (𝜑𝐸 ∈ (0(,)1))    &   (𝜑𝑍 ∈ ℝ+)    &   (𝜑𝑁 ∈ ℕ)       ((𝜑𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁𝑢𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))

Theorempntibndlem2 24969* Lemma for pntibnd 24971. The main work, after eliminating all the quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   𝐿 = ((1 / 4) / (𝐴 + 3))    &   (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   𝐾 = (exp‘(𝐵 / (𝐸 / 2)))    &   𝐶 = ((2 · 𝐵) + (log‘2))    &   (𝜑𝐸 ∈ (0(,)1))    &   (𝜑𝑍 ∈ ℝ+)    &   (𝜑𝑁 ∈ ℕ)    &   (𝜑𝑇 ∈ ℝ+)    &   (𝜑 → ∀𝑥 ∈ (1(,)+∞)∀𝑦 ∈ (𝑥[,](2 · 𝑥))((ψ‘𝑦) − (ψ‘𝑥)) ≤ ((2 · (𝑦𝑥)) + (𝑇 · (𝑥 / (log‘𝑥)))))    &   𝑋 = ((exp‘(𝑇 / (𝐸 / 4))) + 𝑍)    &   (𝜑𝑀 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   (𝜑𝑌 ∈ (𝑋(,)+∞))    &   (𝜑 → ((𝑌 < 𝑁𝑁 ≤ ((𝑀 / 2) · 𝑌)) ∧ (abs‘((𝑅𝑁) / 𝑁)) ≤ (𝐸 / 2)))       (𝜑 → ∃𝑧 ∈ ℝ+ ((𝑌 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑀 · 𝑌)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))

Theorempntibndlem3 24970* Lemma for pntibnd 24971. Package up pntibndlem2 24969 in quantifiers. (Contributed by Mario Carneiro, 10-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   𝐿 = ((1 / 4) / (𝐴 + 3))    &   (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   𝐾 = (exp‘(𝐵 / (𝐸 / 2)))    &   𝐶 = ((2 · 𝐵) + (log‘2))    &   (𝜑𝐸 ∈ (0(,)1))    &   (𝜑𝑍 ∈ ℝ+)    &   (𝜑 → ∀𝑚 ∈ (𝐾[,)+∞)∀𝑣 ∈ (𝑍(,)+∞)∃𝑖 ∈ ℕ ((𝑣 < 𝑖𝑖 ≤ (𝑚 · 𝑣)) ∧ (abs‘((𝑅𝑖) / 𝑖)) ≤ (𝐸 / 2)))       (𝜑 → ∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))

Theorempntibnd 24971* Lemma for pnt 24992. Establish smallness of 𝑅 on an interval. Lemma 10.6.2 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 10-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))       𝑐 ∈ ℝ+𝑙 ∈ (0(,)1)∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝑐 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝑙 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝑙 · 𝑒)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝑒)

Theorempntlemd 24972 Lemma for pnt 24992. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, 𝐴 is C^*, 𝐵 is c1, 𝐿 is λ, 𝐷 is c2, and 𝐹 is c3. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))       (𝜑 → (𝐿 ∈ ℝ+𝐷 ∈ ℝ+𝐹 ∈ ℝ+))

Theorempntlemc 24973* Lemma for pnt 24992. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, 𝑈 is α, 𝐸 is ε, and 𝐾 is K. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))       (𝜑 → (𝐸 ∈ ℝ+𝐾 ∈ ℝ+ ∧ (𝐸 ∈ (0(,)1) ∧ 1 < 𝐾 ∧ (𝑈𝐸) ∈ ℝ+)))

Theorempntlema 24974* Lemma for pnt 24992. Closure for the constants used in the proof. The mammoth expression 𝑊 is a number large enough to satisfy all the lower bounds needed for 𝑍. For comparison with Equation 10.6.27 of [Shapiro], p. 434, 𝑌 is x2, 𝑋 is x1, 𝐶 is the big-O constant in Equation 10.6.29 of [Shapiro], p. 435, and 𝑊 is the unnamed lower bound of "for sufficiently large x" in Equation 10.6.34 of [Shapiro], p. 436. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))       (𝜑𝑊 ∈ ℝ+)

Theorempntlemb 24975* Lemma for pnt 24992. Unpack all the lower bounds contained in 𝑊, in the form they will be used. For comparison with Equation 10.6.27 of [Shapiro], p. 434, 𝑍 is x. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))       (𝜑 → (𝑍 ∈ ℝ+ ∧ (1 < 𝑍 ∧ e ≤ (√‘𝑍) ∧ (√‘𝑍) ≤ (𝑍 / 𝑌)) ∧ ((4 / (𝐿 · 𝐸)) ≤ (√‘𝑍) ∧ (((log‘𝑋) / (log‘𝐾)) + 2) ≤ (((log‘𝑍) / (log‘𝐾)) / 4) ∧ ((𝑈 · 3) + 𝐶) ≤ (((𝑈𝐸) · ((𝐿 · (𝐸↑2)) / (32 · 𝐵))) · (log‘𝑍)))))

Theorempntlemg 24976* Lemma for pnt 24992. Closure for the constants used in the proof. For comparison with Equation 10.6.27 of [Shapiro], p. 434, 𝑀 is j^* and 𝑁 is ĵ. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))       (𝜑 → (𝑀 ∈ ℕ ∧ 𝑁 ∈ (ℤ𝑀) ∧ (((log‘𝑍) / (log‘𝐾)) / 4) ≤ (𝑁𝑀)))

Theorempntlemh 24977* Lemma for pnt 24992. Bounds on the subintervals in the induction. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))       ((𝜑𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾𝐽) ∧ (𝐾𝐽) ≤ (√‘𝑍)))

Theorempntlemn 24978* Lemma for pnt 24992. The "naive" base bound, which we will slightly improve. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)       ((𝜑 ∧ (𝐽 ∈ ℕ ∧ 𝐽 ≤ (𝑍 / 𝑌))) → 0 ≤ (((𝑈 / 𝐽) − (abs‘((𝑅‘(𝑍 / 𝐽)) / 𝑍))) · (log‘𝐽)))

Theorempntlemq 24979* Lemma for pntlemj 24981. (Contributed by Mario Carneiro, 7-Jun-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))    &   (𝜑𝑉 ∈ ℝ+)    &   (𝜑 → (((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   (𝜑𝐽 ∈ (𝑀..^𝑁))    &   𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))       (𝜑𝐼𝑂)

Theorempntlemr 24980* Lemma for pntlemj 24981. (Contributed by Mario Carneiro, 7-Jun-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))    &   (𝜑𝑉 ∈ ℝ+)    &   (𝜑 → (((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   (𝜑𝐽 ∈ (𝑀..^𝑁))    &   𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))       (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ ((#‘𝐼) · ((𝑈𝐸) · ((log‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))

Theorempntlemj 24981* Lemma for pnt 24992. The induction step. Using pntibnd 24971, we find an interval in 𝐾𝐽...𝐾↑(𝐽 + 1) which is sufficiently large and has a much smaller value, 𝑅(𝑧) / 𝑧𝐸 (instead of our original bound 𝑅(𝑧) / 𝑧𝑈). (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))    &   (𝜑𝑉 ∈ ℝ+)    &   (𝜑 → (((𝐾𝐽) < 𝑉 ∧ ((1 + (𝐿 · 𝐸)) · 𝑉) < (𝐾 · (𝐾𝐽))) ∧ ∀𝑢 ∈ (𝑉[,]((1 + (𝐿 · 𝐸)) · 𝑉))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   (𝜑𝐽 ∈ (𝑀..^𝑁))    &   𝐼 = (((⌊‘(𝑍 / ((1 + (𝐿 · 𝐸)) · 𝑉))) + 1)...(⌊‘(𝑍 / 𝑉)))       (𝜑 → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))

Theorempntlemi 24982* Lemma for pnt 24992. Eliminate some assumptions from pntlemj 24981. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   𝑂 = (((⌊‘(𝑍 / (𝐾↑(𝐽 + 1)))) + 1)...(⌊‘(𝑍 / (𝐾𝐽))))       ((𝜑𝐽 ∈ (𝑀..^𝑁)) → ((𝑈𝐸) · (((𝐿 · 𝐸) / 8) · (log‘𝑍))) ≤ Σ𝑛𝑂 (((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))

Theorempntlemf 24983* Lemma for pnt 24992. Add up the pieces in pntlemi 24982 to get an estimate slightly better than the naive lower bound 0. (Contributed by Mario Carneiro, 13-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))       (𝜑 → ((𝑈𝐸) · (((𝐿 · (𝐸↑2)) / (32 · 𝐵)) · ((log‘𝑍)↑2))) ≤ Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))(((𝑈 / 𝑛) − (abs‘((𝑅‘(𝑍 / 𝑛)) / 𝑍))) · (log‘𝑛)))

Theorempntlemk 24984* Lemma for pnt 24992. Evaluate the naive part of the estimate. (Contributed by Mario Carneiro, 14-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))       (𝜑 → (2 · Σ𝑛 ∈ (1...(⌊‘(𝑍 / 𝑌)))((𝑈 / 𝑛) · (log‘𝑛))) ≤ ((𝑈 · ((log‘𝑍) + 3)) · (log‘𝑍)))

Theorempntlemo 24985* Lemma for pnt 24992. Combine all the estimates to establish a smaller eventual bound on 𝑅(𝑍) / 𝑍. (Contributed by Mario Carneiro, 14-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑𝑍 ∈ (𝑊[,)+∞))    &   𝑀 = ((⌊‘((log‘𝑋) / (log‘𝐾))) + 1)    &   𝑁 = (⌊‘(((log‘𝑍) / (log‘𝐾)) / 2))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝐾 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   (𝜑 → ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶)       (𝜑 → (abs‘((𝑅𝑍) / 𝑍)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))

Theorempntleme 24986* Lemma for pnt 24992. Package up pntlemo 24985 in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → (𝑋 ∈ ℝ+𝑌 < 𝑋))    &   (𝜑𝐶 ∈ ℝ+)    &   𝑊 = (((𝑌 + (4 / (𝐿 · 𝐸)))↑2) + (((𝑋 · (𝐾↑2))↑4) + (exp‘(((32 · 𝐵) / ((𝑈𝐸) · (𝐿 · (𝐸↑2)))) · ((𝑈 · 3) + 𝐶)))))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)    &   (𝜑 → ∀𝑘 ∈ (𝐾[,)+∞)∀𝑦 ∈ (𝑋(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝐸)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝐸)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝐸))    &   (𝜑 → ∀𝑧 ∈ (1(,)+∞)((((abs‘(𝑅𝑧)) · (log‘𝑧)) − ((2 / (log‘𝑧)) · Σ𝑖 ∈ (1...(⌊‘(𝑧 / 𝑌)))((abs‘(𝑅‘(𝑧 / 𝑖))) · (log‘𝑖)))) / 𝑧) ≤ 𝐶)       (𝜑 → ∃𝑤 ∈ ℝ+𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))

Theorempntlem3 24987* Lemma for pnt 24992. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 8-Apr-2016.) (Proof shortened by AV, 27-Sep-2020.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)    &   𝑇 = {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑡}    &   (𝜑𝐶 ∈ ℝ+)    &   ((𝜑𝑢𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇)       (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1)

Theorempntlemp 24988* Lemma for pnt 24992. Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑 → ∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐵 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝑒))    &   (𝜑𝑈 ∈ ℝ+)    &   (𝜑𝑈𝐴)    &   𝐸 = (𝑈 / 𝐷)    &   𝐾 = (exp‘(𝐵 / 𝐸))    &   (𝜑 → (𝑌 ∈ ℝ+ ∧ 1 ≤ 𝑌))    &   (𝜑 → ∀𝑧 ∈ (𝑌[,)+∞)(abs‘((𝑅𝑧) / 𝑧)) ≤ 𝑈)       (𝜑 → ∃𝑤 ∈ ℝ+𝑣 ∈ (𝑤[,)+∞)(abs‘((𝑅𝑣) / 𝑣)) ≤ (𝑈 − (𝐹 · (𝑈↑3))))

Theorempntleml 24989* Lemma for pnt 24992. Equation 10.6.35 in [Shapiro], p. 436. (Contributed by Mario Carneiro, 14-Apr-2016.)
𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   (𝜑𝐴 ∈ ℝ+)    &   (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅𝑥) / 𝑥)) ≤ 𝐴)    &   (𝜑𝐵 ∈ ℝ+)    &   (𝜑𝐿 ∈ (0(,)1))    &   𝐷 = (𝐴 + 1)    &   𝐹 = ((1 − (1 / 𝐷)) · ((𝐿 / (32 · 𝐵)) / (𝐷↑2)))    &   (𝜑 → ∀𝑒 ∈ (0(,)1)∃𝑥 ∈ ℝ+𝑘 ∈ ((exp‘(𝐵 / 𝑒))[,)+∞)∀𝑦 ∈ (𝑥(,)+∞)∃𝑧 ∈ ℝ+ ((𝑦 < 𝑧 ∧ ((1 + (𝐿 · 𝑒)) · 𝑧) < (𝑘 · 𝑦)) ∧ ∀𝑢 ∈ (𝑧[,]((1 + (𝐿 · 𝑒)) · 𝑧))(abs‘((𝑅𝑢) / 𝑢)) ≤ 𝑒))       (𝜑 → (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1)

Theorempnt3 24990 The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
(𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1

Theorempnt2 24991 The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
(𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1

Theorempnt 24992 The Prime Number Theorem: the number of prime numbers less than 𝑥 tends asymptotically to 𝑥 / log(𝑥) as 𝑥 goes to infinity. This is Metamath 100 proof #5. (Contributed by Mario Carneiro, 1-Jun-2016.)
(𝑥 ∈ (1(,)+∞) ↦ ((π𝑥) / (𝑥 / (log‘𝑥)))) ⇝𝑟 1

14.4.14  Ostrowski's theorem

Theoremabvcxp 24993* Raising an absolute value to a power less than one yields another absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝐴 = (AbsVal‘𝑅)    &   𝐵 = (Base‘𝑅)    &   𝐺 = (𝑥𝐵 ↦ ((𝐹𝑥)↑𝑐𝑆))       ((𝐹𝐴𝑆 ∈ (0(,]1)) → 𝐺𝐴)

Theorempadicfval 24994* Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))       (𝑃 ∈ ℙ → (𝐽𝑃) = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑥)))))

Theorempadicval 24995* Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))       ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑋))))

Theoremostth2lem1 24996* Lemma for ostth2 25015, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 25015. If a power is upper bounded by a linear term, the exponent must be less than one. Or in big-O notation, 𝑛𝑜(𝐴𝑛) for any 1 < 𝐴. (Contributed by Mario Carneiro, 10-Sep-2014.)
(𝜑𝐴 ∈ ℝ)    &   (𝜑𝐵 ∈ ℝ)    &   ((𝜑𝑛 ∈ ℕ) → (𝐴𝑛) ≤ (𝑛 · 𝐵))       (𝜑𝐴 ≤ 1)

Theoremqrngbas 24997 The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝑄 = (ℂflds ℚ)       ℚ = (Base‘𝑄)

Theoremqdrng 24998 The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝑄 = (ℂflds ℚ)       𝑄 ∈ DivRing

Theoremqrng0 24999 The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝑄 = (ℂflds ℚ)       0 = (0g𝑄)

Theoremqrng1 25000 The unit element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
𝑄 = (ℂflds ℚ)       1 = (1r𝑄)

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13200 133 13201-13300 134 13301-13400 135 13401-13500 136 13501-13600 137 13601-13700 138 13701-13800 139 13801-13900 140 13901-14000 141 14001-14100 142 14101-14200 143 14201-14300 144 14301-14400 145 14401-14500 146 14501-14600 147 14601-14700 148 14701-14800 149 14801-14900 150 14901-15000 151 15001-15100 152 15101-15200 153 15201-15300 154 15301-15400 155 15401-15500 156 15501-15600 157 15601-15700 158 15701-15800 159 15801-15900 160 15901-16000 161 16001-16100 162 16101-16200 163 16201-16300 164 16301-16400 165 16401-16500 166 16501-16600 167 16601-16700 168 16701-16800 169 16801-16900 170 16901-17000 171 17001-17100 172 17101-17200 173 17201-17300 174 17301-17400 175 17401-17500 176 17501-17600 177 17601-17700 178 17701-17800 179 17801-17900 180 17901-18000 181 18001-18100 182 18101-18200 183 18201-18300 184 18301-18400 185 18401-18500 186 18501-18600 187 18601-18700 188 18701-18800 189 18801-18900 190 18901-19000 191 19001-19100 192 19101-19200 193 19201-19300 194 19301-19400 195 19401-19500 196 19501-19600 197 19601-19700 198 19701-19800 199 19801-19900 200 19901-20000 201 20001-20100 202 20101-20200 203 20201-20300 204 20301-20400 205 20401-20500 206 20501-20600 207 20601-20700 208 20701-20800 209 20801-20900 210 20901-21000 211 21001-21100 212 21101-21200 213 21201-21300 214 21301-21400 215 21401-21500 216 21501-21600 217 21601-21700 218 21701-21800 219 21801-21900 220 21901-22000 221 22001-22100 222 22101-22200 223 22201-22300 224 22301-22400 225 22401-22500 226 22501-22600 227 22601-22700 228 22701-22800 229 22801-22900 230 22901-23000 231 23001-23100 232 23101-23200 233 23201-23300 234 23301-23400 235 23401-23500 236 23501-23600 237 23601-23700 238 23701-23800 239 23801-23900 240 23901-24000 241 24001-24100 242 24101-24200 243 24201-24300 244 24301-24400 245 24401-24500 246 24501-24600 247 24601-24700 248 24701-24800 249 24801-24900 250 24901-25000 251 25001-25100 252 25101-25200 253 25201-25300 254 25301-25400 255 25401-25500 256 25501-25600 257 25601-25700 258 25701-25800 259 25801-25900 260 25901-26000 261 26001-26100 262 26101-26200 263 26201-26300 264 26301-26400 265 26401-26500 266 26501-26600 267 26601-26700 268 26701-26800 269 26801-26900 270 26901-27000 271 27001-27100 272 27101-27200 273 27201-27300 274 27301-27400 275 27401-27500 276 27501-27600 277 27601-27700 278 27701-27800 279 27801-27900 280 27901-28000 281 28001-28100 282 28101-28200 283 28201-28300 284 28301-28400 285 28401-28500 286 28501-28600 287 28601-28700 288 28701-28800 289 28801-28900 290 28901-29000 291 29001-29100 292 29101-29200 293 29201-29300 294 29301-29400 295 29401-29500 296 29501-29600 297 29601-29700 298 29701-29800 299 29801-29900 300 29901-30000 301 30001-30100 302 30101-30200 303 30201-30300 304 30301-30400 305 30401-30500 306 30501-30600 307 30601-30700 308 30701-30800 309 30801-30900 310 30901-31000 311 31001-31100 312 31101-31200 313 31201-31300 314 31301-31400 315 31401-31500 316 31501-31600 317 31601-31700 318 31701-31800 319 31801-31900 320 31901-32000 321 32001-32100 322 32101-32200 323 32201-32300 324 32301-32400 325 32401-32500 326 32501-32600 327 32601-32700 328 32701-32800 329 32801-32900 330 32901-33000 331 33001-33100 332 33101-33200 333 33201-33300 334 33301-33400 335 33401-33500 336 33501-33600 337 33601-33700 338 33701-33800 339 33801-33900 340 33901-34000 341 34001-34100 342 34101-34200 343 34201-34300 344 34301-34400 345 34401-34500 346 34501-34600 347 34601-34700 348 34701-34800 349 34801-34900 350 34901-35000 351 35001-35100 352 35101-35200 353 35201-35300 354 35301-35400 355 35401-35500 356 35501-35600 357 35601-35700 358 35701-35800 359 35801-35900 360 35901-36000 361 36001-36100 362 36101-36200 363 36201-36300 364 36301-36400 365 36401-36500 366 36501-36600 367 36601-36700 368 36701-36800 369 36801-36900 370 36901-37000 371 37001-37100 372 37101-37200 373 37201-37300 374 37301-37400 375 37401-37500 376 37501-37600 377 37601-37700 378 37701-37800 379 37801-37900 380 37901-38000 381 38001-38100 382 38101-38200 383 38201-38300 384 38301-38400 385 38401-38500 386 38501-38600 387 38601-38700 388 38701-38800 389 38801-38900 390 38901-39000 391 39001-39100 392 39101-39200 393 39201-39300 394 39301-39400 395 39401-39500 396 39501-39600 397 39601-39700 398 39701-39800 399 39801-39900 400 39901-40000 401 40001-40100 402 40101-40200 403 40201-40300 404 40301-40400 405 40401-40500 406 40501-40600 407 40601-40700 408 40701-40800 409 40801-40900 410 40901-41000 411 41001-41100 412 41101-41200 413 41201-41300 414 41301-41400 415 41401-41500 416 41501-41600 417 41601-41700 418 41701-41800 419 41801-41900 420 41901-42000 421 42001-42100 422 42101-42200 423 42201-42300 424 42301-42400 425 42401-42426
 Copyright terms: Public domain < Previous  Next >