P. 280 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27901-28000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pntsf 27901*	Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    ⇒   ⊢ 𝑆:ℝ⟶ℝ
Theorem	selbergs 27902*	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 27903*	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 27904*	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 27905*	The sum of selberg3r 27897 and selberg4r 27898. (Contributed by Mario Carneiro, 31-May-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    ⇒   ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)
Theorem	pntrlog2bndlem2 27906*	Lemma for pntrlog2bnd 27912. 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 27907*	Lemma for pntrlog2bnd 27912. 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 27908*	Lemma for pntrlog2bnd 27912. 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 27909*	Lemma for pntrlog2bnd 27912. 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 27910*	Lemma for pntrlog2bndlem6 27911. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖)))))    &   ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 1 ≤ 𝐴)    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = ((1...(⌊‘(𝑥 / 𝐴))) ∪ (((⌊‘(𝑥 / 𝐴)) + 1)...(⌊‘𝑥))))
Theorem	pntrlog2bndlem6 27911*	Lemma for pntrlog2bnd 27912. 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 27912*	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 27913*	Lemma for pntpbnd 27916. (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 27914*	Lemma for pntpbnd 27916. (Contributed by Mario Carneiro, 11-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ 𝑋 = (exp‘(2 / 𝐸))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)    &   ⊢ 𝐶 = (𝐴 + 2)    &   ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))    ⇒   ⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴)
Theorem	pntpbnd2 27915*	Lemma for pntpbnd 27916. (Contributed by Mario Carneiro, 11-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ 𝑋 = (exp‘(2 / 𝐸))    &   ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴)    &   ⊢ 𝐶 = (𝐴 + 2)    &   ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞))    &   ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸))    ⇒   ⊢ ¬ 𝜑
Theorem	pntpbnd 27916*	Lemma for pnt 27942. 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 27917	Lemma for pntibnd 27921. (Contributed by Mario Carneiro, 10-Apr-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3))    ⇒   ⊢ (𝜑 → 𝐿 ∈ (0(,)1))
Theorem	pntibndlem2a 27918*	Lemma for pntibndlem2 27919. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))    &   ⊢ 𝐶 = ((2 · 𝐵) + (log‘2))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ (𝜑 → 𝑍 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
Theorem	pntibndlem2 27919*	Lemma for pntibnd 27921. 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 27920*	Lemma for pntibnd 27921. Package up pntibndlem2 27919 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 27921*	Lemma for pnt 27942. 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 27922	Lemma for pnt 27942. 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 27923*	Lemma for pnt 27942. 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 27924*	Lemma for pnt 27942. 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 27925*	Lemma for pnt 27942. 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 27926*	Lemma for pnt 27942. 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 27927*	Lemma for pnt 27942. 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 27928*	Lemma for pnt 27942. 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 27929*	Lemma for pntlemj 27931. (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 27930*	Lemma for pntlemj 27931. (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 27931*	Lemma for pnt 27942. The induction step. Using pntibnd 27921, 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 27932*	Lemma for pnt 27942. Eliminate some assumptions from pntlemj 27931. (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 27933*	Lemma for pnt 27942. Add up the pieces in pntlemi 27932 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 27934*	Lemma for pnt 27942. 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 27935*	Lemma for pnt 27942. 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 27936*	Lemma for pnt 27942. Package up pntlemo 27935 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 27937*	Lemma for pnt 27942. 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 27938*	Lemma for pnt 27942. 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 27939*	Lemma for pnt 27942. 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 27940	The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1
Theorem	pnt2 27941	The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1
Theorem	pnt 27942	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 27943*	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 27944*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑ -(𝑞 pCnt 𝑥)))))    ⇒   ⊢ (𝑃 ∈ ℙ → (𝐽‘𝑃) = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑃↑ -(𝑃 pCnt 𝑥)))))
Theorem	padicval 27945*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑ -(𝑞 pCnt 𝑥)))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽‘𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑ -(𝑃 pCnt 𝑋))))
Theorem	ostth2lem1 27946*	Lemma for ostth2 27965, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 27965. 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 27947	The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ℚ = (Base‘𝑄)
Theorem	qdrng 27948	The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 𝑄 ∈ DivRing
Theorem	qrng0 27949	The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 0 = (0g‘𝑄)
Theorem	qrng1 27950	The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 1 = (1r‘𝑄)
Theorem	qrngneg 27951	The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋)
Theorem	qrngdiv 27952	The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌))
Theorem	qabvle 27953	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 27954	Induct the product rule abvmul 21079 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))
Theorem	ostthlem1 27955*	Lemma for ostth 27967. 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 27956*	Lemma for ostth 27967. Refine ostthlem1 27955 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 27957	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 27958*	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 27959*	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 27960*	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 27961*	- Lemma for ostth 27967: 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 21079 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 27955 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 27962*	Lemma for ostth2 27965. (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 27963*	Lemma for ostth2 27965. (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 27964*	Lemma for ostth2 27965. (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 27965*	- Lemma for ostth 27967: 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 27966*	- Lemma for ostth 27967: 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 27967*	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 𝐽 𝐹 = (𝑦 ∈ ℚ ↦ ((𝑔‘𝑦)↑𝑐𝑎))))
14.4.15  Fermat's Last Theorem
14.4.15.1  Basic reductions for Fermat's Last Theorem
Theorem	infdesc 27968*	Infinite descent. The hypotheses say that 𝑆 is lower bounded, and that if 𝜓 holds for an integer in 𝑆, it holds for a smaller integer in 𝑆. By infinite descent, eventually we cannot go any smaller, therefore 𝜓 holds for no integer in 𝑆. (Contributed by SN, 20-Aug-2024.)
⊢ (𝑦 = 𝑥 → (𝜓 ↔ 𝜒))    &   ⊢ (𝑦 = 𝑧 → (𝜓 ↔ 𝜃))    &   ⊢ (𝜑 → 𝑆 ⊆ (ℤ≥‘𝑀))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑆 ∧ 𝜒)) → ∃𝑧 ∈ 𝑆 (𝜃 ∧ 𝑧 < 𝑥))    ⇒   ⊢ (𝜑 → {𝑦 ∈ 𝑆 ∣ 𝜓} = ∅)
Theorem	fltdiv 27969	A counterexample to FLT stays valid when scaled. The hypotheses are more general than they need to be for convenience. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝑆 ∈ ℂ)    &   ⊢ (𝜑 → 𝑆 ≠ 0)    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / 𝑆)↑𝑁) + ((𝐵 / 𝑆)↑𝑁)) = ((𝐶 / 𝑆)↑𝑁))
Theorem	flt0 27970	A counterexample for FLT does not exist for 𝑁 = 0. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝑁 ∈ ℕ)
Theorem	fltdvdsabdvdsc 27971	Any factor of both 𝐴 and 𝐵 also divides 𝐶. This establishes the validity of fltabcoprmex 27972. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) ∥ 𝐶)
Theorem	fltabcoprmex 27972	A counterexample to FLT implies a counterexample to FLT with 𝐴, 𝐵 (assigned to 𝐴 / (𝐴 gcd 𝐵) and 𝐵 / (𝐴 gcd 𝐵)) coprime (by divgcdcoprm0 16841). (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵))↑𝑁) + ((𝐵 / (𝐴 gcd 𝐵))↑𝑁)) = ((𝐶 / (𝐴 gcd 𝐵))↑𝑁))
Theorem	fltaccoprm 27973	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐴, 𝐶 coprime. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)
Theorem	fltbccoprm 27974	A counterexample to FLT with 𝐴, 𝐵 coprime also has 𝐵, 𝐶 coprime. Proven from fltaccoprm 27973 using commutativity of addition. (Contributed by SN, 20-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ0)    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → (𝐵 gcd 𝐶) = 1)
Theorem	fltabcoprm 27975	A counterexample to FLT with 𝐴, 𝐶 coprime also has 𝐴, 𝐵 coprime. Converse of fltaccoprm 27973. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐶) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)
Theorem	fltne 27976	If a counterexample to FLT exists, its addends are not equal. (Contributed by SN, 1-Jun-2023.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘2))    &   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) = (𝐶↑𝑁))    ⇒   ⊢ (𝜑 → 𝐴 ≠ 𝐵)
Theorem	flt4lem1 27977	Satisfy the antecedent used in several pythagtrip 17013 lemmas. (Contributed by SN, 21-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)))
Theorem	flt4lem2 27978	If 𝐴 is even, 𝐵 is odd. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    ⇒   ⊢ (𝜑 → ¬ 2 ∥ 𝐵)
Theorem	flt4lem3 27979	Equivalent to pythagtriplem4 16998. Show that 𝐶 + 𝐴 and 𝐶 − 𝐴 are coprime. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐶 + 𝐴) gcd (𝐶 − 𝐴)) = 1)
Theorem	flt4lem4 27980	If the product of two coprime factors is a perfect square, the factors are perfect squares. (Contributed by SN, 22-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → (𝐴 · 𝐵) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (𝐴 = ((𝐴 gcd 𝐶)↑2) ∧ 𝐵 = ((𝐵 gcd 𝐶)↑2)))
Theorem	flt4lem5 27981	In the context of the lemmas of pythagtrip 17013, 𝑀 and 𝑁 are coprime. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + 𝐵)) + (√‘(𝐶 − 𝐵))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + 𝐵)) − (√‘(𝐶 − 𝐵))) / 2)    ⇒   ⊢ (((𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ ∧ 𝐶 ∈ ℕ) ∧ ((𝐴↑2) + (𝐵↑2)) = (𝐶↑2) ∧ ((𝐴 gcd 𝐵) = 1 ∧ ¬ 2 ∥ 𝐴)) → (𝑀 gcd 𝑁) = 1)
Theorem	flt4lem5elem 27982	Version of fltaccoprm 27973 and fltbccoprm 27974 where 𝑀 is not squared. This can be proved in general for any polynomial in three variables: using prmdvdsncoprmbd 16904, dvds2addd 16463, and prmdvdsexp 16892, we can show that if two variables are coprime, the third is also coprime to the two. (Contributed by SN, 24-Aug-2024.)
⊢ (𝜑 → 𝑀 ∈ ℕ)    &   ⊢ (𝜑 → 𝑅 ∈ ℕ)    &   ⊢ (𝜑 → 𝑆 ∈ ℕ)    &   ⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2)))    &   ⊢ (𝜑 → (𝑅 gcd 𝑆) = 1)    ⇒   ⊢ (𝜑 → ((𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1))
Theorem	flt4lem5a 27983	Part 1 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝐴↑2) + (𝑁↑2)) = (𝑀↑2))
Theorem	flt4lem5b 27984	Part 2 of Equation 1 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (2 · (𝑀 · 𝑁)) = (𝐵↑2))
Theorem	flt4lem5c 27985	Part 2 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 22-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑁 = (2 · (𝑅 · 𝑆)))
Theorem	flt4lem5d 27986	Part 3 of Equation 2 of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → 𝑀 = ((𝑅↑2) + (𝑆↑2)))
Theorem	flt4lem5e 27987	Satisfy the hypotheses of flt4lem4 27980. (Contributed by SN, 23-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (((𝑅 gcd 𝑆) = 1 ∧ (𝑅 gcd 𝑀) = 1 ∧ (𝑆 gcd 𝑀) = 1) ∧ (𝑅 ∈ ℕ ∧ 𝑆 ∈ ℕ ∧ 𝑀 ∈ ℕ) ∧ ((𝑀 · (𝑅 · 𝑆)) = ((𝐵 / 2)↑2) ∧ (𝐵 / 2) ∈ ℕ)))
Theorem	flt4lem5f 27988	Final equation of https://crypto.stanford.edu/pbc/notes/numberfield/fermatn4.html. Given 𝐴↑4 + 𝐵↑4 = 𝐶↑2, provide a smaller solution. This satisfies the infinite descent condition. (Contributed by SN, 24-Aug-2024.)
⊢ 𝑀 = (((√‘(𝐶 + (𝐵↑2))) + (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑁 = (((√‘(𝐶 + (𝐵↑2))) − (√‘(𝐶 − (𝐵↑2)))) / 2)    &   ⊢ 𝑅 = (((√‘(𝑀 + 𝑁)) + (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ 𝑆 = (((√‘(𝑀 + 𝑁)) − (√‘(𝑀 − 𝑁))) / 2)    &   ⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ((𝑀 gcd (𝐵 / 2))↑2) = (((𝑅 gcd (𝐵 / 2))↑4) + ((𝑆 gcd (𝐵 / 2))↑4)))
Theorem	flt4lem6 27989	Remove shared factors in a solution to 𝐴↑4 + 𝐵↑4 = 𝐶↑2. (Contributed by SN, 24-Jul-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → (((𝐴 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐵 / (𝐴 gcd 𝐵)) ∈ ℕ ∧ (𝐶 / ((𝐴 gcd 𝐵)↑2)) ∈ ℕ) ∧ (((𝐴 / (𝐴 gcd 𝐵))↑4) + ((𝐵 / (𝐴 gcd 𝐵))↑4)) = ((𝐶 / ((𝐴 gcd 𝐵)↑2))↑2)))
Theorem	flt4lem7 27990*	Convert flt4lem5f 27988 into a convenient form for nna4b4nsq 27991. (Contributed by SN, 25-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ¬ 2 ∥ 𝐴)    &   ⊢ (𝜑 → (𝐴 gcd 𝐵) = 1)    &   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) = (𝐶↑2))    ⇒   ⊢ (𝜑 → ∃𝑙 ∈ ℕ (∃𝑔 ∈ ℕ ∃ℎ ∈ ℕ (¬ 2 ∥ 𝑔 ∧ ((𝑔 gcd ℎ) = 1 ∧ ((𝑔↑4) + (ℎ↑4)) = (𝑙↑2))) ∧ 𝑙 < 𝐶))
Theorem	nna4b4nsq 27991	Strengthening of Fermat's last theorem for exponent 4, where the sum is only assumed to be a square. (Contributed by SN, 23-Aug-2024.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑2))
Theorem	flt4 27992	Fermat's last theorem for the exponent four. (Contributed by AV, 15-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    ⇒   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑4))
Theorem	flt4ALT 27993*	Fermat's last theorem for the exponent four, derived from Fermat's right triangle theorem (which is not proved yet, see fermrtt: after a proof is available, the hypothesis flt4ALT.r can be removed - TODO-AV). (Contributed by AV, 15-Sep-2026.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ((𝑎↑4) − (𝑏↑4)) ≠ (𝑐↑2))    ⇒   ⊢ (𝜑 → ((𝐴↑4) + (𝐵↑4)) ≠ (𝐶↑4))
14.4.15.2  Proof of Fermat's Last Theorem (work in progress) On September 4th, 2026 Anthropic published that their AI "Claude" created a complete and machine-verified formal proof for Fermat's Last Theorem: it consists of about 13 million lines of code, and about 30.000 verified theorems, created within about 11 days, built on Lean's library "mathlib" as well as preliminary work of the Buzzard community (in 2024, Kevin Buzzard started a project at Imperial College to formalize a complete proof in Lean, planned for many years and founded up to 2029). For more details see https://www.anthropic.com/research/formalizing-fermats-last-theorem. Asking Claude (Opus 5) itself if it is possible to prove Fermat's last theorem also with Metamath, it answered: "Short version: in principle yes, in practice no. Foundations aren't the problem. set.mm is built on ZFC, and in the Grothendieck extension (ax-groth 10909, Tarski's axiom) universes are available too - exactly what Wiles's proof appeared to need beyond ZFC. (Colin McLarty has shown in any case that this can be pushed down into far weaker systems.) So there is no logical obstacle, only a labor one. What has been proved so far is the case n = 4 (see flt4 27992). ... Why it's nevertheless a size too big: Metamath has no tactics; every step stands there fully expanded. More serious is that set.mm simply lacks the necessary infrastructure: no schemes, no modular forms, no Galois representations, no class field theory. That is the actual proof - the number theory of FLT is only the last line. Mathlib had a large part of it after years of community work, and even building on that, the Lean formalization comprised some 30,000 additional theorems; set.mm in total holds only an order of magnitude more than that. ... So it would be feasible - but it would be a project on the same scale as everything assembled in set.mm since 1993." Nevertheless, this and the previous subsections provide some starting points for a formal proof by Metamath: According to the blueprint provided by Kevin Buzzard, see https://imperialcollegelondon.github.io/FLT/blueprint/ 27992, Lemma 2.1 is already proven (see fltoprm 27996). The next step would be to prove Lemma 2.2 (FLT for n = 3, see flt3 above). Corollary 2.3 follows immediately from Lemmas 2.1 and 2.2 (see fltoprmgt3 27997). Finally, asking Claude if it makes sense to translate the Lean proof into the Metamath language, it says: "Possible in principle - sensible, not really. Foundationally there's no obstacle. Mario Carneiro showed that Lean's type theory is consistent relative to ZFC with n inaccessible cardinals for all n < ω. set.mm, via Tarski's axiom (ax-groth 10909), supplies arbitrarily large inaccessibles - so the required model is within reach. And there's precedent: in 2014/16 Carneiro translated proofs from the OpenTheory format (HOL Light, HOL4, Isabelle) into Metamath, first into a HOL formalization hol.mm, then embedded into set.mm. The exercise has been done once already. But Lean is a different league from HOL. Three problems: * The translation isn't a rewrite. ... * The transfer problem. ... * The scale. Lean's elaborator performs an enormous amount of invisible work: instance resolution, implicit arguments, universe unification, definitional unfolding. Metamath has none of it. 13 million lines of Lean on top of over a million lines of mathlib plausibly expand into the billions of steps - against the few tens of thousands of statements that make up all of set.mm. The real objection, though, isn't feasibility but payoff. ... Nothing for set.mm. The database is curated and maintained for readability; a generated dump would contradict its purpose and wouldn't be admitted into the main database anyway. What does transfer is the blueprint. The lemma decomposition, the definitional choices, the proof strategy - that's language-independent, and it's precisely the part that took years of work to produce. Buzzard's blueprint for the FLT project is literally that document. A native Metamath development following it would be the sensible path, and it would reasonably start at n = 3.". The last sentence is actually the way we want to continue (as described above)...
Theorem	fltoprmlem1 27994*	Lemma 1 for fltoprm 27996: Every positive integer is either a power of 2 or has an odd prime factor. (Contributed by AV, 15-Sep-2026.)
⊢ (𝑁 ∈ ℕ → (∃𝑝 ∈ ℙ (2 < 𝑝 ∧ 𝑝 ∥ 𝑁) ∨ ∃𝑛 ∈ ℕ0 𝑁 = (2↑𝑛)))
Theorem	fltoprmlem2 27995	Lemma 2 for fltoprm 27996: If an integer greater than or equal to 3 is a power of 2, it is a multiple of 4. (Contributed by AV, 15-Sep-2026.)
⊢ ((𝑁 ∈ (ℤ≥‘3) ∧ 𝐾 ∈ ℕ0 ∧ 𝑁 = (2↑𝐾)) → 4 ∥ 𝑁)
Theorem	fltoprm 27996*	Fermat's last theorem holds for any exponent greater than 2 if it holds for odd prime exponents. (Contributed by AV, 15-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (2 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))
Theorem	fltoprmgt3 27997*	Fermat's last theorem holds for any exponent greater than 2 if it holds for all odd prime exponents greater than 3. (TODO-AV: after a proof is available for 𝑁 = 3, see flt3, the hypothesis fltoprmgt3.3 can be removed.) (Contributed by AV, 15-Sep-2026.)
⊢ (𝜑 → 𝐴 ∈ ℕ)    &   ⊢ (𝜑 → 𝐵 ∈ ℕ)    &   ⊢ (𝜑 → 𝐶 ∈ ℕ)    &   ⊢ (𝜑 → 𝑁 ∈ (ℤ≥‘3))    &   ⊢ (𝜑 → ∀𝑎 ∈ ℕ ∀𝑏 ∈ ℕ ∀𝑐 ∈ ℕ ∀𝑝 ∈ ℙ (3 < 𝑝 → ((𝑎↑𝑝) + (𝑏↑𝑝)) ≠ (𝑐↑𝑝)))    &   ⊢ (𝜑 → ((𝑎↑3) + (𝑏↑3)) ≠ (𝑐↑3))    ⇒   ⊢ (𝜑 → ((𝐴↑𝑁) + (𝐵↑𝑁)) ≠ (𝐶↑𝑁))
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 27998	Declare the class of all surreal numbers (see df-no 28001).
class No
Syntax	clts 27999	Declare the less-than relation over surreal numbers (see df-lts 28002).
class <s
Syntax	cbday 28000	Declare the birthday function for surreal numbers (see df-bday 28003).
class bday