| Metamath
Proof Explorer Theorem List (p. 277 of 494) | < 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: | (1-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | selberg3lem1 27601* | Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27595 (written here as Σ𝑛 ≤ 𝑥, Λ(𝑛)ψ(𝑥 / 𝑛)). Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)) | ||
| Theorem | selberg3lem2 27602* | Lemma for selberg3 27603. Equation 10.4.21 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | selberg3 27603* | Introduce a log weighting on the summands of Σ𝑚 · 𝑛 ≤ 𝑥, Λ(𝑚)Λ(𝑛), the core of selberg2 27595 (written here as Σ𝑛 ≤ 𝑥, Λ(𝑛)ψ(𝑥 / 𝑛)). Equation 10.6.7 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ (((((ψ‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) | ||
| Theorem | selberg4lem1 27604* | Lemma for selberg4 27605. Equation 10.4.20 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝐴) ⇒ ⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)) | ||
| Theorem | selberg4 27605* | The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form Σ𝑖𝑗𝑘 ≤ 𝑥, Λ(𝑖)Λ(𝑗)Λ(𝑘); we eliminate one of the nested sums by using the definition of ψ(𝑥) = Σ𝑘 ≤ 𝑥, Λ(𝑘). This statement can thus equivalently be written ψ(𝑥)log↑2(𝑥) = 2Σ𝑖𝑗𝑘 ≤ 𝑥, Λ(𝑖)Λ(𝑗)Λ(𝑘) + 𝑂(𝑥log𝑥). Equation 10.4.23 of [Shapiro], p. 422. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | pntrval 27606* | Define the residual of the second Chebyshev function. The goal is to have 𝑅(𝑥) ∈ 𝑜(𝑥), or 𝑅(𝑥) / 𝑥 ⇝𝑟 0. (Contributed by Mario Carneiro, 8-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝐴 ∈ ℝ+ → (𝑅‘𝐴) = ((ψ‘𝐴) − 𝐴)) | ||
| Theorem | pntrf 27607 | Functionality of the residual. Lemma for pnt 27658. (Contributed by Mario Carneiro, 8-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ 𝑅:ℝ+⟶ℝ | ||
| Theorem | pntrmax 27608* | There is a bound on the residual valid for all 𝑥. (Contributed by Mario Carneiro, 9-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ ∃𝑐 ∈ ℝ+ ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑐 | ||
| Theorem | pntrsumo1 27609* | A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝑥 ∈ ℝ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ∈ 𝑂(1) | ||
| Theorem | pntrsumbnd 27610* | A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 25-May-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ ∃𝑐 ∈ ℝ+ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (1...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 | ||
| Theorem | pntrsumbnd2 27611* | A bound on a sum over 𝑅. Equation 10.1.16 of [Shapiro], p. 403. (Contributed by Mario Carneiro, 14-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ ∃𝑐 ∈ ℝ+ ∀𝑘 ∈ ℕ ∀𝑚 ∈ ℤ (abs‘Σ𝑛 ∈ (𝑘...𝑚)((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝑐 | ||
| Theorem | selbergr 27612* | Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.2 of [Shapiro], p. 428. (Contributed by Mario Carneiro, 16-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝑥 ∈ ℝ+ ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + Σ𝑑 ∈ (1...(⌊‘𝑥))((Λ‘𝑑) · (𝑅‘(𝑥 / 𝑑)))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | selberg3r 27613* | Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.8 of [Shapiro], p. 429. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (𝑅‘(𝑥 / 𝑛))) · (log‘𝑛)))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | selberg4r 27614* | Selberg's symmetry formula, using the residual of the second Chebyshev function. Equation 10.6.11 of [Shapiro], p. 430. (Contributed by Mario Carneiro, 30-May-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (𝑅‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | selberg34r 27615* | The sum of selberg3r 27613 and selberg4r 27614. (Contributed by Mario Carneiro, 31-May-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) | ||
| Theorem | pntsval 27616* | Define the "Selberg function", whose asymptotic behavior is the content of selberg 27592. (Contributed by Mario Carneiro, 31-May-2016.) |
| ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) ⇒ ⊢ (𝐴 ∈ ℝ → (𝑆‘𝐴) = Σ𝑛 ∈ (1...(⌊‘𝐴))((Λ‘𝑛) · ((log‘𝑛) + (ψ‘(𝐴 / 𝑛))))) | ||
| Theorem | pntsf 27617* | Functionality of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016.) |
| ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) ⇒ ⊢ 𝑆:ℝ⟶ℝ | ||
| Theorem | selbergs 27618* | 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 27619* | 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 27620* | 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 27621* | The sum of selberg3r 27613 and selberg4r 27614. (Contributed by Mario Carneiro, 31-May-2016.) |
| ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) & ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) ⇒ ⊢ (𝑥 ∈ (1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1) | ||
| Theorem | pntrlog2bndlem2 27622* | Lemma for pntrlog2bnd 27628. 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 27623* | Lemma for pntrlog2bnd 27628. 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 27624* | Lemma for pntrlog2bnd 27628. 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 27625* | Lemma for pntrlog2bnd 27628. 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 27626* | Lemma for pntrlog2bndlem6 27627. (Contributed by Mario Carneiro, 7-Jun-2016.) |
| ⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈ (1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) & ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ 𝑇 = (𝑎 ∈ ℝ ↦ if(𝑎 ∈ ℝ+, (𝑎 · (log‘𝑎)), 0)) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑦 ∈ ℝ+ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐵) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 1 ≤ 𝐴) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1...(⌊‘𝑥)) = ((1...(⌊‘(𝑥 / 𝐴))) ∪ (((⌊‘(𝑥 / 𝐴)) + 1)...(⌊‘𝑥)))) | ||
| Theorem | pntrlog2bndlem6 27627* | Lemma for pntrlog2bnd 27628. 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 27628* | 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 27629* | Lemma for pntpbnd 27632. (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 27630* | Lemma for pntpbnd 27632. (Contributed by Mario Carneiro, 11-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ (0(,)1)) & ⊢ 𝑋 = (exp‘(2 / 𝐸)) & ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) & ⊢ 𝐶 = (𝐴 + 2) & ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) & ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) ⇒ ⊢ (𝜑 → Σ𝑛 ∈ (((⌊‘𝑌) + 1)...(⌊‘(𝐾 · 𝑌)))(abs‘((𝑅‘𝑛) / (𝑛 · (𝑛 + 1)))) ≤ 𝐴) | ||
| Theorem | pntpbnd2 27631* | Lemma for pntpbnd 27632. (Contributed by Mario Carneiro, 11-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐸 ∈ (0(,)1)) & ⊢ 𝑋 = (exp‘(2 / 𝐸)) & ⊢ (𝜑 → 𝑌 ∈ (𝑋(,)+∞)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ (𝜑 → ∀𝑖 ∈ ℕ ∀𝑗 ∈ ℤ (abs‘Σ𝑦 ∈ (𝑖...𝑗)((𝑅‘𝑦) / (𝑦 · (𝑦 + 1)))) ≤ 𝐴) & ⊢ 𝐶 = (𝐴 + 2) & ⊢ (𝜑 → 𝐾 ∈ ((exp‘(𝐶 / 𝐸))[,)+∞)) & ⊢ (𝜑 → ¬ ∃𝑦 ∈ ℕ ((𝑌 < 𝑦 ∧ 𝑦 ≤ (𝐾 · 𝑌)) ∧ (abs‘((𝑅‘𝑦) / 𝑦)) ≤ 𝐸)) ⇒ ⊢ ¬ 𝜑 | ||
| Theorem | pntpbnd 27632* | Lemma for pnt 27658. 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 27633 | Lemma for pntibnd 27637. (Contributed by Mario Carneiro, 10-Apr-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) ⇒ ⊢ (𝜑 → 𝐿 ∈ (0(,)1)) | ||
| Theorem | pntibndlem2a 27634* | Lemma for pntibndlem2 27635. (Contributed by Mario Carneiro, 7-Jun-2016.) |
| ⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦ ((ψ‘𝑎) − 𝑎)) & ⊢ (𝜑 → 𝐴 ∈ ℝ+) & ⊢ 𝐿 = ((1 / 4) / (𝐴 + 3)) & ⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) & ⊢ (𝜑 → 𝐵 ∈ ℝ+) & ⊢ 𝐾 = (exp‘(𝐵 / (𝐸 / 2))) & ⊢ 𝐶 = ((2 · 𝐵) + (log‘2)) & ⊢ (𝜑 → 𝐸 ∈ (0(,)1)) & ⊢ (𝜑 → 𝑍 ∈ ℝ+) & ⊢ (𝜑 → 𝑁 ∈ ℕ) ⇒ ⊢ ((𝜑 ∧ 𝑢 ∈ (𝑁[,]((1 + (𝐿 · 𝐸)) · 𝑁))) → (𝑢 ∈ ℝ ∧ 𝑁 ≤ 𝑢 ∧ 𝑢 ≤ ((1 + (𝐿 · 𝐸)) · 𝑁))) | ||
| Theorem | pntibndlem2 27635* | Lemma for pntibnd 27637. 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 27636* | Lemma for pntibnd 27637. Package up pntibndlem2 27635 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 27637* | Lemma for pnt 27658. 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 27638 | Lemma for pnt 27658. 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 27639* | Lemma for pnt 27658. 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 27640* | Lemma for pnt 27658. 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 27641* | Lemma for pnt 27658. 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 27642* | Lemma for pnt 27658. 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 27643* | Lemma for pnt 27658. 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 27644* | Lemma for pnt 27658. 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 27645* | Lemma for pntlemj 27647. (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 27646* | Lemma for pntlemj 27647. (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 27647* | Lemma for pnt 27658. The induction step. Using pntibnd 27637, 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 27648* | Lemma for pnt 27658. Eliminate some assumptions from pntlemj 27647. (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 27649* | Lemma for pnt 27658. Add up the pieces in pntlemi 27648 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 27650* | Lemma for pnt 27658. 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 27651* | Lemma for pnt 27658. 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 27652* | Lemma for pnt 27658. Package up pntlemo 27651 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 27653* | Lemma for pnt 27658. 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 27654* | Lemma for pnt 27658. 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 27655* | Lemma for pnt 27658. 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 27656 | The Prime Number Theorem, version 3: the second Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟 1 | ||
| Theorem | pnt2 27657 | The Prime Number Theorem, version 2: the first Chebyshev function tends asymptotically to 𝑥. (Contributed by Mario Carneiro, 1-Jun-2016.) |
| ⊢ (𝑥 ∈ ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 | ||
| Theorem | pnt 27658 | 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 27659* | 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 27660* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ (𝑃 ∈ ℙ → (𝐽‘𝑃) = (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑥))))) | ||
| Theorem | padicval 27661* | Value of the p-adic absolute value. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝐽 = (𝑞 ∈ ℙ ↦ (𝑥 ∈ ℚ ↦ if(𝑥 = 0, 0, (𝑞↑-(𝑞 pCnt 𝑥))))) ⇒ ⊢ ((𝑃 ∈ ℙ ∧ 𝑋 ∈ ℚ) → ((𝐽‘𝑃)‘𝑋) = if(𝑋 = 0, 0, (𝑃↑-(𝑃 pCnt 𝑋)))) | ||
| Theorem | ostth2lem1 27662* | Lemma for ostth2 27681, although it is just a simple statement about exponentials which does not involve any specifics of ostth2 27681. 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 27663 | The base set of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ℚ = (Base‘𝑄) | ||
| Theorem | qdrng 27664 | The rationals form a division ring. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 𝑄 ∈ DivRing | ||
| Theorem | qrng0 27665 | The zero element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 0 = (0g‘𝑄) | ||
| Theorem | qrng1 27666 | The unity element of the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ 1 = (1r‘𝑄) | ||
| Theorem | qrngneg 27667 | The additive inverse in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ (𝑋 ∈ ℚ → ((invg‘𝑄)‘𝑋) = -𝑋) | ||
| Theorem | qrngdiv 27668 | The division operation in the field of rationals. (Contributed by Mario Carneiro, 8-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) ⇒ ⊢ ((𝑋 ∈ ℚ ∧ 𝑌 ∈ ℚ ∧ 𝑌 ≠ 0) → (𝑋(/r‘𝑄)𝑌) = (𝑋 / 𝑌)) | ||
| Theorem | qabvle 27669 | 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 27670 | Induct the product rule abvmul 20822 to find the absolute value of a power. (Contributed by Mario Carneiro, 10-Sep-2014.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ 𝐴 = (AbsVal‘𝑄) ⇒ ⊢ ((𝐹 ∈ 𝐴 ∧ 𝑀 ∈ ℚ ∧ 𝑁 ∈ ℕ0) → (𝐹‘(𝑀↑𝑁)) = ((𝐹‘𝑀)↑𝑁)) | ||
| Theorem | ostthlem1 27671* | Lemma for ostth 27683. 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 27672* | Lemma for ostth 27683. Refine ostthlem1 27671 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 27673 | 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 27674* | 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 27675* | 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 27676* | 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 27677* | - Lemma for ostth 27683: 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 20822 of the absolute value, 𝐹 is equal to 1 on all the integers, and ostthlem1 27671 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 27678* | Lemma for ostth2 27681. (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 27679* | Lemma for ostth2 27681. (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 27680* | Lemma for ostth2 27681. (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 27681* | - Lemma for ostth 27683: 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 27682* | - Lemma for ostth 27683: 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 27683* | 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 27684 | Declare the class of all surreal numbers (see df-no 27687). |
| class No | ||
| Syntax | cslt 27685 | Declare the less-than relation over surreal numbers (see df-slt 27688). |
| class <s | ||
| Syntax | cbday 27686 | Declare the birthday function for surreal numbers (see df-bday 27689). |
| class bday | ||
| Definition | df-no 27687* |
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 27688* | 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 27689 | 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 27690* | Membership in the surreals. (Contributed by Scott Fenton, 11-Jun-2011.) (Proof shortened by SF, 14-Apr-2012.) Avoid ax-rep 5279. (Revised by SN, 5-Jun-2025.) |
| ⊢ (𝐴 ∈ No ↔ ∃𝑥 ∈ On 𝐴:𝑥⟶{1o, 2o}) | ||
| Theorem | elnoOLD 27691* | Obsolete version of elno 27690 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 27692* | 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 27693 | The value of the birthday function within the surreals. (Contributed by Scott Fenton, 14-Jun-2011.) |
| ⊢ (𝐴 ∈ No → ( bday ‘𝐴) = dom 𝐴) | ||
| Theorem | nofun 27694 | A surreal is a function. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → Fun 𝐴) | ||
| Theorem | nodmon 27695 | The domain of a surreal is an ordinal. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → dom 𝐴 ∈ On) | ||
| Theorem | norn 27696 | 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 27697 | A surreal is a function over its birthday. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → 𝐴 Fn ( bday ‘𝐴)) | ||
| Theorem | nodmord 27698 | The domain of a surreal has the ordinal property. (Contributed by Scott Fenton, 16-Jun-2011.) |
| ⊢ (𝐴 ∈ No → Ord dom 𝐴) | ||
| Theorem | elno2 27699 | An alternative condition for membership in No . (Contributed by Scott Fenton, 21-Mar-2012.) |
| ⊢ (𝐴 ∈ No ↔ (Fun 𝐴 ∧ dom 𝐴 ∈ On ∧ ran 𝐴 ⊆ {1o, 2o})) | ||
| Theorem | elno3 27700 | Another condition for membership in No . (Contributed by Scott Fenton, 14-Apr-2012.) |
| ⊢ (𝐴 ∈ No ↔ (𝐴:dom 𝐴⟶{1o, 2o} ∧ dom 𝐴 ∈ On)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |