P. 279 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27801-27900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	selberg3lem1 27801*	Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27795 (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 27802*	Lemma for selberg3 27803. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.)
⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)
Theorem	selberg3 27803*	Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27795 (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 27804*	Lemma for selberg4 27805. 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 27805*	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 27806*	Define the residual of the second Chebyshev function. The goal is to have 𝑅(𝑥) ∈ 𝑜(𝑥), or 𝑅(𝑥) / 𝑥 ⇝𝑟 0. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝐴 ∈ ℝ+ → (𝑅‘𝐴) = ((ψ‘𝐴) − 𝐴))
Theorem	pntrf 27807	Functionality of the residual. Lemma for pnt 27858. (Contributed by Mario Carneiro, 8-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ 𝑅:ℝ+⟶ℝ
Theorem	pntrmax 27808*	There is a bound on the residual valid for all 𝑥. (Contributed by Mario Carneiro, 9-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑐
Theorem	pntrsumo1 27809*	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 27810*	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 27811*	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 27812*	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 27813*	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 27814*	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 27815*	The sum of selberg3r 27813 and selberg4r 27814. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1)
Theorem	pntsval 27816*	Define the "Selberg function", whose asymptotic behavior is the content of selberg 27792. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ (𝐴 ∈ ℝ → (𝑆‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝐴 / 𝑛)))))
Theorem	pntsf 27817*	Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ 𝑆:ℝ⟶ℝ
Theorem	selbergs 27818*	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 27819*	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 27820*	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 27821*	The sum of selberg3r 27813 and selberg4r 27814. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)
Theorem	pntrlog2bndlem2 27822*	Lemma for pntrlog2bnd 27828. 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 27823*	Lemma for pntrlog2bnd 27828. 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 27824*	Lemma for pntrlog2bnd 27828. 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 27825*	Lemma for pntrlog2bnd 27828. 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 27826*	Lemma for pntrlog2bndlem6 27827. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = ((1...(⌊‘(𝑥 / 𝐴))) ∪ (((⌊‘(𝑥 / 𝐴)) + 1)...(⌊‘𝑥))))
Theorem	pntrlog2bndlem6 27827*	Lemma for pntrlog2bnd 27828. 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))
Theorem	pntrlog2bnd 27828*	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‘𝑛)))) / 𝑥) ≤ 𝑐)
Theorem	pntpbnd1a 27829*	Lemma for pntpbnd 27832. (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‘((𝑅‘𝑁) / 𝑁)) ≤ 𝐸)
Theorem	pntpbnd1 27830*	Lemma for pntpbnd 27832. (Contributed by Mario Carneiro, 11-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ 𝑋 = (exp‘(2 / 𝐸))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)    &   ⊢ 𝐶 = (𝐴 + 2)    &   ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)
Theorem	pntpbnd2 27831*	Lemma for pntpbnd 27832. (Contributed by Mario Carneiro, 11-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ 𝑋 = (exp‘(2 / 𝐸))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)    &   ⊢ 𝐶 = (𝐴 + 2)    &   ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))    ⇒   ⊢ ¬ 𝜑
Theorem	pntpbnd 27832*	Lemma for pnt 27858. 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‘((𝑅‘𝑛) / 𝑛)) ≤ 𝑒)
Theorem	pntibndlem1 27833	Lemma for pntibnd 27837. (Contributed by Mario Carneiro, 10-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3))    ⇒   ⊢ (𝜑 → 𝐿 ∈ (0(,)1))
Theorem	pntibndlem2a 27834*	Lemma for pntibndlem2 27835. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))    &   ⊢ 𝐶 = ((2 · 𝐵) + (log‘2))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ (𝜑 → 𝑍 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
Theorem	pntibndlem2 27835*	Lemma for pntibnd 27837. 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‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
Theorem	pntibndlem3 27836*	Lemma for pntibnd 27837. Package up pntibndlem2 27835 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‘((𝑅‘𝑢) / 𝑢)) ≤ 𝐸))
Theorem	pntibnd 27837*	Lemma for pnt 27858. 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‘((𝑅‘𝑢) / 𝑢)) ≤ 𝑒)
Theorem	pntlemd 27838	Lemma for pnt 27858. 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)))    ⇒   ⊢ (𝜑 → (𝐿 ∈ ℝ+ ∧ 𝐷 ∈ ℝ+ ∧ 𝐹 ∈ ℝ+))
Theorem	pntlemc 27839*	Lemma for pnt 27858. 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 < 𝐾 ∧ (𝑈 − 𝐸) ∈ ℝ+)))
Theorem	pntlema 27840*	Lemma for pnt 27858. 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) + 𝐶)))))    ⇒   ⊢ (𝜑 → 𝑊 ∈ ℝ+)
Theorem	pntlemb 27841*	Lemma for pnt 27858. 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‘𝑍)))))
Theorem	pntlemg 27842*	Lemma for pnt 27858. 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) ≤ (𝑁 − 𝑀)))
Theorem	pntlemh 27843*	Lemma for pnt 27858. 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))    ⇒   ⊢ ((𝜑 ∧ 𝐽 ∈ (𝑀...𝑁)) → (𝑋 < (𝐾↑𝐽) ∧ (𝐾↑𝐽) ≤ (√‘𝑍)))
Theorem	pntlemn 27844*	Lemma for pnt 27858. 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‘𝐽)))
Theorem	pntlemq 27845*	Lemma for pntlemj 27847. (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)...(⌊‘(𝑍 / 𝑉)))    ⇒   ⊢ (𝜑 → 𝐼 ⊆ 𝑂)
Theorem	pntlemr 27846*	Lemma for pntlemj 27847. (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‘(𝑍 / 𝑉)) / (𝑍 / 𝑉)))))
Theorem	pntlemj 27847*	Lemma for pnt 27858. The induction step. Using pntibnd 27837, 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‘𝑛)))
Theorem	pntlemi 27848*	Lemma for pnt 27858. Eliminate some assumptions from pntlemj 27847. (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‘𝑛)))
Theorem	pntlemf 27849*	Lemma for pnt 27858. Add up the pieces in pntlemi 27848 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‘𝑛)))
Theorem	pntlemk 27850*	Lemma for pnt 27858. 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‘𝑍)))
Theorem	pntlemo 27851*	Lemma for pnt 27858. 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))))
Theorem	pntleme 27852*	Lemma for pnt 27858. Package up pntlemo 27851 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))))
Theorem	pntlem3 27853*	Lemma for pnt 27858. 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)
Theorem	pntlemp 27854*	Lemma for pnt 27858. 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))))
Theorem	pntleml 27855*	Lemma for pnt 27858. 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)
Theorem	pnt3 27856	The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1
Theorem	pnt2 27857	The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1
Theorem	pnt 27858	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
Theorem	abvcxp 27859*	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)) → 𝐺 ∈ 𝐴)
Theorem	padicfval 27860*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ (𝑃 ∈ ℙ → (𝐽‘𝑃) = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑥)))))
Theorem	padicval 27861*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽‘𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑋))))
Theorem	ostth2lem1 27862*	Lemma for ostth2 27881, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 27881. 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)
Theorem	qrngbas 27863	The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ℚ = (Base‘𝑄)
Theorem	qdrng 27864	The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 𝑄 ∈ DivRing
Theorem	qrng0 27865	The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 0 = (0g‘𝑄)
Theorem	qrng1 27866	The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 1 = (1r‘𝑄)
Theorem	qrngneg 27867	The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋)
Theorem	qrngdiv 27868	The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌))
Theorem	qabvle 27869	By using induction on 𝑁, we show a long-range inequality coming from the triangle inequality. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑁 ∈ ℕ0) → (𝐹‘𝑁) ≤ 𝑁)
Theorem	qabvexp 27870	Induct the product rule abvmul 20993 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))
Theorem	ostthlem1 27871*	Lemma for ostth 27883. If two absolute values agree on the positive integers greater than one, then they agree for all rational numbers and thus are equal as functions. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ≥‘2)) → (𝐹‘𝑛) = (𝐺‘𝑛))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	ostthlem2 27872*	Lemma for ostth 27883. Refine ostthlem1 27871 so that it is sufficient to only show equality on the primes. (Contributed by Mario Carneiro, 9-Sep-2014.) (Revised by Mario Carneiro, 20-Jun-2015.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝐺 ∈ 𝐴)    &   ⊢ ((𝜑 ∧ 𝑝 ∈ ℙ) → (𝐹‘𝑝) = (𝐺‘𝑝))    ⇒   ⊢ (𝜑 → 𝐹 = 𝐺)
Theorem	qabsabv 27873	The regular absolute value function on the rationals is in fact an absolute value under our definition. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ (abs ↾ ℚ) ∈ 𝐴
Theorem	padicabv 27874*	The p-adic absolute value (with arbitrary base) is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐹 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑁↑(𝑃 pCnt 𝑥))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑁 ∈ (0(,)1)) → 𝐹 ∈ 𝐴)
Theorem	padicabvf 27875*	The p-adic absolute value is an absolute value. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ 𝐽:ℙ⟶𝐴
Theorem	padicabvcxp 27876*	All positive powers of the p-adic absolute value are absolute values. (Contributed by Mario Carneiro, 9-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑅 ∈ ℝ+) → (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑅)) ∈ 𝐴)
Theorem	ostth1 27877*	- Lemma for ostth 27883: trivial case. (Not that the proof is trivial, but that we are proving that the function is trivial.) If 𝐹 is equal to 1 on the primes, then by complete induction and the multiplicative property abvmul 20993 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 27871 extends this to the other rational numbers. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℙ ¬ (𝐹‘𝑛) < 1)    ⇒   ⊢ (𝜑 → 𝐹 = 𝐾)
Theorem	ostth2lem2 27878*	Lemma for ostth2 27881. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀))    &   ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ (0...((𝑀↑𝑋) − 1))) → (𝐹‘𝑌) ≤ ((𝑀 · 𝑋) · (𝑇↑𝑋)))
Theorem	ostth2lem3 27879*	Lemma for ostth2 27881. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀))    &   ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))    &   ⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀))    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ ℕ) → (((𝐹‘𝑁) / (𝑇↑𝑐𝑈))↑𝑋) ≤ (𝑋 · ((𝑀 · 𝑇) · (𝑈 + 1))))
Theorem	ostth2lem4 27880*	Lemma for ostth2 27881. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    &   ⊢ (𝜑 → 𝑀 ∈ (ℤ≥‘2))    &   ⊢ 𝑆 = ((log‘(𝐹‘𝑀)) / (log‘𝑀))    &   ⊢ 𝑇 = if((𝐹‘𝑀) ≤ 1, 1, (𝐹‘𝑀))    &   ⊢ 𝑈 = ((log‘𝑁) / (log‘𝑀))    ⇒   ⊢ (𝜑 → (1 < (𝐹‘𝑀) ∧ 𝑅 ≤ 𝑆))
Theorem	ostth2 27881*	- Lemma for ostth 27883: regular case. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → 1 < (𝐹‘𝑁))    &   ⊢ 𝑅 = ((log‘(𝐹‘𝑁)) / (log‘𝑁))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎)))
Theorem	ostth3 27882*	- Lemma for ostth 27883: p-adic case. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    &   ⊢ (𝜑 → 𝐹 ∈ 𝐴)    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ¬ 1 < (𝐹‘𝑛))    &   ⊢ (𝜑 → 𝑃 ∈ ℙ)    &   ⊢ (𝜑 → (𝐹‘𝑃) < 1)    &   ⊢ 𝑅 = -((log‘(𝐹‘𝑃)) / (log‘𝑃))    &   ⊢ 𝑆 = if((𝐹‘𝑃) ≤ (𝐹‘𝑝), (𝐹‘𝑝), (𝐹‘𝑃))    ⇒   ⊢ (𝜑 → ∃𝑎 ∈ ℝ+ 𝐹 = (𝑦 ∈ ℚ ↦ (((𝐽‘𝑃)‘𝑦)↑𝑐𝑎)))
Theorem	ostth 27883*	Ostrowski's theorem, which classifies all absolute values on ℚ. Any such absolute value must either be the trivial absolute value 𝐾, a constant exponent 0 < 𝑎 ≤ 1 times the regular absolute value, or a positive exponent times the p-adic absolute value. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    &   ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    &   ⊢ 𝐾 = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, 1))    ⇒   ⊢ (𝐹 ∈ 𝐴 ↔ (𝐹 = 𝐾 ∨ ∃𝑎 ∈ (0(,]1)𝐹 = (𝑦 ∈ ℚ ↦ ((abs‘𝑦)↑𝑐𝑎)) ∨ ∃𝑎 ∈ ℝ+ ∃𝑔 ∈ ran 𝐽 𝐹 = (𝑦 ∈ ℚ ↦ ((𝑔‘𝑦)↑𝑐𝑎))))
PART 15  SURREAL NUMBERS
15.1  Sign sequence representation and Alling's axioms The surreal numbers can be represented in several equivalent ways. In [Alling], Norman Alling made this notion explicit by giving a set of axioms that all representations admit, then proving that there is an order and birthday preserving bijection between any systems that satisfy these axioms. In this section, we start with the definition of surreal numbers given in [Gonshor] and derive Alling's axioms. After deriving them we no longer refer to the explicit definition of surreals. In particular, we never take advantage of the fact that the empty set is a surreal number under our definition.
15.1.1  Definitions and initial properties
Syntax	csur 27884	Declare the class of all surreal numbers (see df-no 27887).
class No
Syntax	clts 27885	Declare the less-than relation over surreal numbers (see df-lts 27888).
class <s
Syntax	cbday 27886	Declare the birthday function for surreal numbers (see df-bday 27889).
class bday
Definition	df-no 27887*	Define the class of surreal numbers. The surreal numbers are a proper class of numbers developed by John H. Conway and introduced by Donald Knuth in 1975. They form a proper class into which all ordered fields can be embedded. The approach we take to defining them was first introduced by Hary Gonshor, and is based on the conception of a "sign expansion" of a surreal number. We define the surreals as ordinal-indexed sequences of 1o and 2o, analogous to Gonshor's ( − ) and ( + ). After introducing this definition, we will abstract away from it using axioms that Norman Alling developed in "Foundations of Analysis over Surreal Number Fields." This is done in an effort to be agnostic towards the exact implementation of surreals. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ No = {𝑓 ∣ ∃𝑎 ∈ On 𝑓:𝑎⟶{1o, 2o}}
Definition	df-lts 27888*	Next, we introduce surreal less-than, a comparison relation over the surreals by lexicographically ordering them. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ <s = {⟨𝑓, 𝑔⟩ ∣ ((𝑓 ∈ No ∧ 𝑔 ∈ No ) ∧ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝑔‘𝑦) ∧ (𝑓‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝑔‘𝑥)))}
Definition	df-bday 27889	Finally, we introduce the birthday function. This function maps each surreal to an ordinal. In our implementation, this is the domain of the sign function. The important properties of this function are established later. (Contributed by Scott Fenton, 11-Jun-2011.)
⊢ bday = (𝑥 ∈ No ↦ dom 𝑥)
Theorem	elno 27890*	Membership in the surreals. (Contributed by Scott Fenton, 11-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) Avoid ax-rep 5236. (Revised by SN, 5-Jun-2025.)
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
Theorem	ltsval 27891*	The value of the surreal less-than relation. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ ∃𝑥 ∈ On (∀𝑦 ∈ 𝑥 (𝐴‘𝑦) = (𝐵‘𝑦) ∧ (𝐴‘𝑥){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘𝑥))))
Theorem	bdayval 27892	The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴)
Theorem	nofun 27893	A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → Fun 𝐴)
Theorem	nodmon 27894	The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)
Theorem	norn 27895	The range of a surreal is a subset of the surreal signs. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → ran 𝐴 ⊆ {1o, 2o})
Theorem	nofnbday 27896	A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴))
Theorem	nodmord 27897	The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → Ord dom 𝐴)
Theorem	elno2 27898	An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o}))
Theorem	elno3 27899	Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On))
Theorem	ltsval2 27900*	Alternate expression for surreal less-than. Two surreals obey surreal less-than iff they obey the sign ordering at the first place they differ. (Contributed by Scott Fenton, 17-Jun-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 ↔ (𝐴‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)}){⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} (𝐵‘∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))