HomeTheorem List (p. 276 of 498)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 276 of 498) | < Previous Next > |
| Bad symbols? Try the
GIF version. |
||
|
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
||
| Color key: | Metamath Proof Explorer
(1-30853) |
Hilbert Space Explorer
(30854-32376) |
Users' Mathboxes
(32377-49784) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pntrlog2bnd 27501* | 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 27502* | Lemma for pntpbnd 27505. (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 27503* | Lemma for pntpbnd 27505. (Contributed by Mario Carneiro, 11-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ (0(,)1)) & ⊢ 𝑋 = (exp‘(2 / 𝐸)) & ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) & ⊢ 𝐶 = (𝐴 + 2) & ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) & ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) | ||
| Theorem | pntpbnd2 27504* | Lemma for pntpbnd 27505. (Contributed by Mario Carneiro, 11-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ (0(,)1)) & ⊢ 𝑋 = (exp‘(2 / 𝐸)) & ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) & ⊢ 𝐶 = (𝐴 + 2) & ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) & ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | pntpbnd 27505* | Lemma for pnt 27531. 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 27506 | Lemma for pntibnd 27510. (Contributed by Mario Carneiro, 10-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) ⇒ ⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | ||
| Theorem | pntibndlem2a 27507* | Lemma for pntibndlem2 27508. (Contributed by Mario Carneiro, 7-Jun-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2))) & ⊢ 𝐶 = ((2 · 𝐵) + (log‘2)) & ⊢ (𝜑 → 𝐸 ∈ (0(,)1)) & ⊢ (𝜑 → 𝑍 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))) | ||
| Theorem | pntibndlem2 27508* | Lemma for pntibnd 27510. 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 27509* | Lemma for pntibnd 27510. Package up pntibndlem2 27508 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 27510* | Lemma for pnt 27531. 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 27511 | Lemma for pnt 27531. 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 27512* | Lemma for pnt 27531. 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 27513* | Lemma for pnt 27531. 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 27514* | Lemma for pnt 27531. 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 27515* | Lemma for pnt 27531. 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 27516* | Lemma for pnt 27531. 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 27517* | Lemma for pnt 27531. 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 27518* | Lemma for pntlemj 27520. (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 27519* | Lemma for pntlemj 27520. (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 27520* | Lemma for pnt 27531. The induction step. Using pntibnd 27510, 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 27521* | Lemma for pnt 27531. Eliminate some assumptions from pntlemj 27520. (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 27522* | Lemma for pnt 27531. Add up the pieces in pntlemi 27521 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 27523* | Lemma for pnt 27531. 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 27524* | Lemma for pnt 27531. 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 27525* | Lemma for pnt 27531. Package up pntlemo 27524 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 27526* | Lemma for pnt 27531. 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 27527* | Lemma for pnt 27531. 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 27528* | Lemma for pnt 27531. 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 27529 | The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1 | ||
| Theorem | pnt2 27530 | The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 | ||
| Theorem | pnt 27531 | 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 | ||
| Theorem | abvcxp 27532* | 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 27533* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ (𝑃 ∈ ℙ → (𝐽‘𝑃) = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑥))))) | ||
| Theorem | padicval 27534* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽‘𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑋)))) | ||
| Theorem | ostth2lem1 27535* | Lemma for ostth2 27554, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 27554. 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 27536 | The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ℚ = (Base‘𝑄) | ||
| Theorem | qdrng 27537 | The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ DivRing | ||
| Theorem | qrng0 27538 | The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 0 = (0g‘𝑄) | ||
| Theorem | qrng1 27539 | The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 1 = (1r‘𝑄) | ||
| Theorem | qrngneg 27540 | The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋) | ||
| Theorem | qrngdiv 27541 | The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌)) | ||
| Theorem | qabvle 27542 | 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 27543 | Induct the product rule abvmul 20736 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁)) | ||
| Theorem | ostthlem1 27544* | Lemma for ostth 27556. 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 27545* | Lemma for ostth 27556. Refine ostthlem1 27544 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 27546 | 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 27547* | 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 27548* | 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 27549* | 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 27550* | - Lemma for ostth 27556: 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 20736 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 27544 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 27551* | Lemma for ostth2 27554. (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 27552* | Lemma for ostth2 27554. (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 27553* | Lemma for ostth2 27554. (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 27554* | - Lemma for ostth 27556: 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 27555* | - Lemma for ostth 27556: 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 27556* | 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 𝐽 𝐹 = (𝑦 ∈ ℚ ↦ ((𝑔‘𝑦)↑𝑐𝑎)))) | ||
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. | ||
| Syntax | csur 27557 | Declare the class of all surreal numbers (see df-no 27560). |
| class No | ||
| Syntax | cslt 27558 | Declare the less-than relation over surreal numbers (see df-slt 27561). |
| class <s | ||
| Syntax | cbday 27559 | Declare the birthday function for surreal numbers (see df-bday 27562). |
| class bday | ||
| Definition | df-no 27560* |
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 27561* | 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 27562 | 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 27563* | 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 | elnoOLD 27564* | Obsolete version of elno 27563 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 27565* | 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 27566 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴) | ||
| Theorem | nofun 27567 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → Fun 𝐴) | ||
| Theorem | nodmon 27568 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) | ||
| Theorem | norn 27569 | 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 27570 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴)) | ||
| Theorem | nodmord 27571 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → Ord dom 𝐴) | ||
| Theorem | elno2 27572 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
| ⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o})) | ||
| Theorem | elno3 27573 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On)) | ||
| Theorem | sltval2 27574* | 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 27575 | 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 27576 | ∅ is not a surreal sign. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ ¬ ∅ ∈ {1o, 2o} | ||
| Theorem | nosgnn0i 27577 | If 𝑋 is a surreal sign, then it is not null. (Contributed by Scott Fenton, 3-Aug-2011.) |
| ⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ ∅ ≠ 𝑋 | ||
| Theorem | noreson 27578 | The restriction of a surreal to an ordinal is still a surreal. (Contributed by Scott Fenton, 4-Sep-2011.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ↾ 𝐵) ∈ No ) | ||
| Theorem | sltintdifex 27579* | 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 27580 | 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 27581 | The Cartesian product of an ordinal and {1o} is a surreal. (Contributed by Scott Fenton, 12-Jun-2011.) |
| ⊢ (𝐴 ∈ On → (𝐴 × {1o}) ∈ No ) | ||
| Theorem | noseponlem 27582* | Lemma for nosepon 27583. Consider a case of proper subset domain. (Contributed by Scott Fenton, 21-Sep-2020.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ dom 𝐴 ∈ dom 𝐵) → ¬ ∀𝑥 ∈ On (𝐴‘𝑥) = (𝐵‘𝑥)) | ||
| Theorem | nosepon 27583* | 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 27584 | 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 27585 | Extend a surreal by a sequence of ordinals. (Contributed by Scott Fenton, 30-Nov-2021.) |
| ⊢ 𝑋 ∈ {1o, 2o} ⇒ ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No ) | ||
| Theorem | noextenddif 27586* | 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 27587 | 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 27588 | 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 27589 | 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 27590 | 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 27591 | 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 27592 | 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 𝑋)) | ||
| Theorem | sltsolem1 27593 | Lemma for sltso 27594. 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 27594 | Less-than totally orders the surreals. Axiom O of [Alling] p. 184. (Contributed by Scott Fenton, 9-Jun-2011.) |
| ⊢ <s Or No | ||
| Theorem | bdayfo 27595 | 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 | ||
| Theorem | fvnobday 27596 | 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 27597* | Lemma for nosepne 27598. (Contributed by Scott Fenton, 24-Nov-2021.) |
| ⊢ ((𝐴 ∈ No ∧ 𝐵 ∈ No ∧ 𝐴 <s 𝐵) → (𝐴‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)}) ≠ (𝐵‘∩ {𝑥 ∈ On ∣ (𝐴‘𝑥) ≠ (𝐵‘𝑥)})) | ||
| Theorem | nosepne 27598* | 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 27599* | 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 27600* | 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 𝐴) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |