P. 276 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 27501-27600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pntibndlem2a 27501*	Lemma for pntibndlem2 27502. (Contributed by Mario Carneiro, 7-Jun-2016.)
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎))    &   ⊢ (𝜑 → 𝐴 ∈ ℝ+)    &   ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3))    &   ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴)    &   ⊢ (𝜑 → 𝐵 ∈ ℝ+)    &   ⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2)))    &   ⊢ 𝐶 = ((2 · 𝐵) + (log‘2))    &   ⊢ (𝜑 → 𝐸 ∈ (0(,)1))    &   ⊢ (𝜑 → 𝑍 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑁 ∈ ℕ)    ⇒   ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁)))
Theorem	pntibndlem2 27502*	Lemma for pntibnd 27504. 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 27503*	Lemma for pntibnd 27504. Package up pntibndlem2 27502 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 27504*	Lemma for pnt 27525. 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 27505	Lemma for pnt 27525. 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 27506*	Lemma for pnt 27525. 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 27507*	Lemma for pnt 27525. 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 27508*	Lemma for pnt 27525. 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 27509*	Lemma for pnt 27525. 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 27510*	Lemma for pnt 27525. 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 27511*	Lemma for pnt 27525. 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 27512*	Lemma for pntlemj 27514. (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 27513*	Lemma for pntlemj 27514. (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 27514*	Lemma for pnt 27525. The induction step. Using pntibnd 27504, 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 27515*	Lemma for pnt 27525. Eliminate some assumptions from pntlemj 27514. (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 27516*	Lemma for pnt 27525. Add up the pieces in pntlemi 27515 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 27517*	Lemma for pnt 27525. 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 27518*	Lemma for pnt 27525. 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 27519*	Lemma for pnt 27525. Package up pntlemo 27518 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 27520*	Lemma for pnt 27525. 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 27521*	Lemma for pnt 27525. 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 27522*	Lemma for pnt 27525. 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 27523	The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1
Theorem	pnt2 27524	The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.)
⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1
Theorem	pnt 27525	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 27526*	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 27527*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ (𝑃 ∈ ℙ → (𝐽‘𝑃) = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑥)))))
Theorem	padicval 27528*	Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥)))))    ⇒   ⊢ ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽‘𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑋))))
Theorem	ostth2lem1 27529*	Lemma for ostth2 27548, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 27548. 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 27530	The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ℚ = (Base‘𝑄)
Theorem	qdrng 27531	The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 𝑄 ∈ DivRing
Theorem	qrng0 27532	The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 0 = (0g‘𝑄)
Theorem	qrng1 27533	The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ 1 = (1r‘𝑄)
Theorem	qrngneg 27534	The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋)
Theorem	qrngdiv 27535	The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    ⇒   ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌))
Theorem	qabvle 27536	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 27537	Induct the product rule abvmul 20730 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.)
⊢ 𝑄 = (ℂfld ↾s ℚ)    &   ⊢ 𝐴 = (AbsVal‘𝑄)    ⇒   ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁))
Theorem	ostthlem1 27538*	Lemma for ostth 27550. 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 27539*	Lemma for ostth 27550. Refine ostthlem1 27538 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 27540	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 27541*	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 27542*	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 27543*	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 27544*	- Lemma for ostth 27550: 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 20730 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 27538 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 27545*	Lemma for ostth2 27548. (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 27546*	Lemma for ostth2 27548. (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 27547*	Lemma for ostth2 27548. (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 27548*	- Lemma for ostth 27550: 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 27549*	- Lemma for ostth 27550: 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 27550*	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 27551	Declare the class of all surreal numbers (see df-no 27554).
class No
Syntax	cslt 27552	Declare the less-than relation over surreal numbers (see df-slt 27555).
class <s
Syntax	cbday 27553	Declare the birthday function for surreal numbers (see df-bday 27556).
class bday
Definition	df-no 27554*	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-slt 27555*	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 27556	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 27557*	Membership in the surreals. (Contributed by Scott Fenton, 11-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) Avoid ax-rep 5234. (Revised by SN, 5-Jun-2025.)
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
Theorem	elnoOLD 27558*	Obsolete version of elno 27557 as of 5-Jun-2025. (Contributed by Scott Fenton, 11-Jun-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o})
Theorem	sltval 27559*	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 27560	The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.)
⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴)
Theorem	nofun 27561	A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → Fun 𝐴)
Theorem	nodmon 27562	The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → dom 𝐴 ∈ On)
Theorem	norn 27563	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 27564	A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴))
Theorem	nodmord 27565	The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (𝐴 ∈ No → Ord dom 𝐴)
Theorem	elno2 27566	An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.)
⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o}))
Theorem	elno3 27567	Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.)
⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On))
Theorem	sltval2 27568*	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 ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)})))
Theorem	nofv 27569	The function value of a surreal is either a sign or the empty set. (Contributed by Scott Fenton, 22-Jun-2011.)
⊢ (𝐴 ∈ No → ((𝐴‘𝑋) = ∅ ∨ (𝐴‘𝑋) = 1o ∨ (𝐴‘𝑋) = 2o))
Theorem	nosgnn0 27570	∅ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ ¬ ∅ ∈ {1o, 2o}
Theorem	nosgnn0i 27571	If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ ∅ ≠ 𝑋
Theorem	noreson 27572	The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No )
Theorem	sltintdifex 27573*	If 𝐴 <s 𝐵, then the intersection of all the ordinals that have differing signs in 𝐴 and 𝐵 exists. (Contributed by Scott Fenton, 22-Feb-2012.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ) → (𝐴 <s 𝐵 → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ V))
Theorem	sltres 27574	If the restrictions of two surreals to a given ordinal obey surreal less-than, then so do the two surreals themselves. (Contributed by Scott Fenton, 4-Sep-2011.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) → ((𝐴 ↾ 𝑋) <s (𝐵 ↾ 𝑋) → 𝐴 <s 𝐵))
Theorem	noxp1o 27575	The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.)
⊢ (𝐴 ∈ On → (𝐴 × {1o}) ∈ No )
Theorem	noseponlem 27576*	Lemma for nosepon 27577. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥))
Theorem	nosepon 27577*	Given two unequal surreals, the minimal ordinal at which they differ is an ordinal. (Contributed by Scott Fenton, 21-Sep-2020.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ On)
Theorem	noextend 27578	Extending a surreal by one sign value results in a new surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ (𝐴 ∈ No → (𝐴 ∪ {⟨dom 𝐴, 𝑋⟩}) ∈ No )
Theorem	noextendseq 27579	Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No )
Theorem	noextenddif 27580*	Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ 𝑋 ∈ {1o, 2o}    ⇒   ⊢ (𝐴 ∈ No → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ ((𝐴 ∪ {⟨dom 𝐴, 𝑋⟩})‘𝑥)} = dom 𝐴)
Theorem	noextendlt 27581	Extending a surreal with a negative sign results in a smaller surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ (𝐴 ∈ No → (𝐴 ∪ {⟨dom 𝐴, 1o⟩}) <s 𝐴)
Theorem	noextendgt 27582	Extending a surreal with a positive sign results in a bigger surreal. (Contributed by Scott Fenton, 22-Nov-2021.)
⊢ (𝐴 ∈ No → 𝐴 <s (𝐴 ∪ {⟨dom 𝐴, 2o⟩}))
Theorem	nolesgn2o 27583	Given 𝐴 less-than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2o, then 𝐵(𝑋) = 2o. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐵‘𝑋) = 2o)
Theorem	nolesgn2ores 27584	Given 𝐴 less-than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 2o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 2o) ∧ ¬ 𝐵 <s 𝐴) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋))
Theorem	nogesgn1o 27585	Given 𝐴 greater than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 1o, then 𝐵(𝑋) = 1o. (Contributed by Scott Fenton, 9-Aug-2024.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐵‘𝑋) = 1o)
Theorem	nogesgn1ores 27586	Given 𝐴 greater than or equal to 𝐵, equal to 𝐵 up to 𝑋, and 𝐴(𝑋) = 1o, then (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋). (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝑋 ∈ On) ∧ ((𝐴 ↾ 𝑋) = (𝐵 ↾ 𝑋) ∧ (𝐴‘𝑋) = 1o) ∧ ¬ 𝐴 <s 𝐵) → (𝐴 ↾ suc 𝑋) = (𝐵 ↾ suc 𝑋))
15.1.2  Ordering
Theorem	sltsolem1 27587	Lemma for sltso 27588. The "sign expansion" binary relation totally orders the surreal signs. (Contributed by Scott Fenton, 8-Jun-2011.)
⊢ {⟨1o, ∅⟩, ⟨1o, 2o⟩, ⟨∅, 2o⟩} Or ({1o, 2o} ∪ {∅})
Theorem	sltso 27588	Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.)
⊢ <s Or No
15.1.3  Birthday Function
Theorem	bdayfo 27589	The birthday function maps the surreals onto the ordinals. Axiom B of [Alling] p. 184. (Proof shortened on 14-Apr-2012 by SF). (Contributed by Scott Fenton, 11-Jun-2011.)
⊢ bday : No –onto→On
15.1.4  Density
Theorem	fvnobday 27590	The value of a surreal at its birthday is ∅. (Contributed by Scott Fenton, 14-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.)
⊢ (𝐴 ∈ No → (𝐴‘( bday ‘𝐴)) = ∅)
Theorem	nosepnelem 27591*	Lemma for nosepne 27592. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))
Theorem	nosepne 27592*	The value of two non-equal surreals at the first place they differ is different. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}))
Theorem	nosep1o 27593*	If the value of a surreal at a separator is 1o then the surreal is lesser. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) = 1o) → 𝐴 <s 𝐵)
Theorem	nosep2o 27594*	If the value of a surreal at a separator is 2o then the surreal is greater. (Contributed by Scott Fenton, 7-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ (𝐴‘∩ {𝑥 ∈ On ∣ (𝐵‘𝑥) ≠ (𝐴‘𝑥)}) = 2o) → 𝐵 <s 𝐴)
Theorem	nosepdmlem 27595*	Lemma for nosepdm 27596. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵))
Theorem	nosepdm 27596*	The first place two surreals differ is an element of the larger of their domains. (Contributed by Scott Fenton, 24-Nov-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ∈ (dom 𝐴 ∪ dom 𝐵))
Theorem	nosepeq 27597*	The values of two surreals at a point less than their separators are equal. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) ∧ 𝑋 ∈ ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) → (𝐴‘𝑋) = (𝐵‘𝑋))
Theorem	nosepssdm 27598*	Given two non-equal surreals, their separator is less-than or equal to the domain of one of them. Part of Lemma 2.1.1 of [Lipparini] p. 3. (Contributed by Scott Fenton, 6-Dec-2021.)
⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 ≠ 𝐵) → ∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)} ⊆ dom 𝐴)
Theorem	nodenselem4 27599*	Lemma for nodense 27604. Show that a particular abstraction is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ 𝐴 <s 𝐵) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ On)
Theorem	nodenselem5 27600*	Lemma for nodense 27604. If the birthdays of two distinct surreals are equal, then the ordinal from nodenselem4 27599 is an element of that birthday. (Contributed by Scott Fenton, 16-Jun-2011.)
⊢ (((𝐴 ∈ No ∧ 𝐵 ∈ No ) ∧ (( bday ‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∩ {𝑎 ∈ On ∣ (𝐴‘𝑎) ≠ (𝐵‘𝑎)} ∈ ( bday ‘𝐴))