HomeTheorem List (p. 429 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. 429 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-30880) |
Hilbert Space Explorer
(30881-32403) |
Users' Mathboxes
(32404-49778) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | irrapx1 42801* | Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in [vandenDries] p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℝ+ ∖ ℚ) → {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} ≈ ℕ) | ||
| Theorem | pellexlem1 42802 | Lemma for pellex 42808. Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of [vandenDries] p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ ¬ (√‘𝐷) ∈ ℚ) → ((𝐴↑2) − (𝐷 · (𝐵↑2))) ≠ 0) | ||
| Theorem | pellexlem2 42803 | Lemma for pellex 42808. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷)))) | ||
| Theorem | pellexlem3 42804* | Lemma for pellex 42808. To each good rational approximation of (√‘𝐷), there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {𝑥 ∈ ℚ ∣ (0 < 𝑥 ∧ (abs‘(𝑥 − (√‘𝐷))) < ((denom‘𝑥)↑-2))} ≼ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))}) | ||
| Theorem | pellexlem4 42805* | Lemma for pellex 42808. Invoking irrapx1 42801, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ) | ||
| Theorem | pellexlem5 42806* | Lemma for pellex 42808. Invoking fiphp3d 42792, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)) | ||
| Theorem | pellexlem6 42807* | Lemma for pellex 42808. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ (𝜑 → 𝐴 ∈ ℕ) & ⊢ (𝜑 → 𝐵 ∈ ℕ) & ⊢ (𝜑 → 𝐶 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ ℕ) & ⊢ (𝜑 → ¬ (√‘𝐷) ∈ ℚ) & ⊢ (𝜑 → 𝐸 ∈ ℕ) & ⊢ (𝜑 → 𝐹 ∈ ℕ) & ⊢ (𝜑 → ¬ (𝐴 = 𝐸 ∧ 𝐵 = 𝐹)) & ⊢ (𝜑 → 𝐶 ≠ 0) & ⊢ (𝜑 → ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 𝐶) & ⊢ (𝜑 → ((𝐸↑2) − (𝐷 · (𝐹↑2))) = 𝐶) & ⊢ (𝜑 → (𝐴 mod (abs‘𝐶)) = (𝐸 mod (abs‘𝐶))) & ⊢ (𝜑 → (𝐵 mod (abs‘𝐶)) = (𝐹 mod (abs‘𝐶))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ ℕ ∃𝑏 ∈ ℕ ((𝑎↑2) − (𝐷 · (𝑏↑2))) = 1) | ||
| Theorem | pellex 42808* | Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ ((𝑥↑2) − (𝐷 · (𝑦↑2))) = 1) | ||
| Syntax | csquarenn 42809 | Extend class notation to include the set of square positive integers. |
| class ◻NN | ||
| Syntax | cpell1qr 42810 | Extend class notation to include the class of quadrant-1 Pell solutions. |
| class Pell1QR | ||
| Syntax | cpell1234qr 42811 | Extend class notation to include the class of any-quadrant Pell solutions. |
| class Pell1234QR | ||
| Syntax | cpell14qr 42812 | Extend class notation to include the class of positive Pell solutions. |
| class Pell14QR | ||
| Syntax | cpellfund 42813 | Extend class notation to include the Pell-equation fundamental solution function. |
| class PellFund | ||
| Definition | df-squarenn 42814 | Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ◻NN = {𝑥 ∈ ℕ ∣ (√‘𝑥) ∈ ℚ} | ||
| Definition | df-pell1qr 42815* | Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ Pell1QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) | ||
| Definition | df-pell14qr 42816* | Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ Pell14QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) | ||
| Definition | df-pell1234qr 42817* | Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ Pell1234QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) | ||
| Definition | df-pellfund 42818* | A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.) |
| ⊢ PellFund = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ inf({𝑧 ∈ (Pell14QR‘𝑥) ∣ 1 < 𝑧}, ℝ, < )) | ||
| Theorem | pell1qrval 42819* | Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell1qr 42820* | Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℕ0 (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell14qrval 42821* | Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell14qr 42822* | Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell1234qrval 42823* | Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1234QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell1234qr 42824* | Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell1234qrre 42825 | General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ∈ ℝ) | ||
| Theorem | pell1234qrne0 42826 | No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ≠ 0) | ||
| Theorem | pell1234qrreccl 42827 | General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (1 / 𝐴) ∈ (Pell1234QR‘𝐷)) | ||
| Theorem | pell1234qrmulcl 42828 | General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷)) | ||
| Theorem | pell14qrss1234 42829 | A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) ⊆ (Pell1234QR‘𝐷)) | ||
| Theorem | pell14qrre 42830 | A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ) | ||
| Theorem | pell14qrne0 42831 | A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ≠ 0) | ||
| Theorem | pell14qrgt0 42832 | A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴) | ||
| Theorem | pell14qrrp 42833 | A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ+) | ||
| Theorem | pell1234qrdich 42834 | A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (𝐴 ∈ (Pell14QR‘𝐷) ∨ -𝐴 ∈ (Pell14QR‘𝐷))) | ||
| Theorem | elpell14qr2 42835 | A number is a positive Pell solution iff it is positive and a Pell solution, justifying our name choice. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ (Pell1234QR‘𝐷) ∧ 0 < 𝐴))) | ||
| Theorem | pell14qrmulcl 42836 | Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrreccl 42837 | Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 / 𝐴) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrdivcl 42838 | Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 / 𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrexpclnn0 42839 | Lemma for pell14qrexpcl 42840. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrexpcl 42840 | Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell1qrss14 42841 | First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrdich 42842 | A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (𝐴 ∈ (Pell1QR‘𝐷) ∨ (1 / 𝐴) ∈ (Pell1QR‘𝐷))) | ||
| Theorem | pell1qrge1 42843 | A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴) | ||
| Theorem | pell1qr1 42844 | 1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 ∈ (Pell1QR‘𝐷)) | ||
| Theorem | elpell1qr2 42845 | The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1QR‘𝐷) ↔ (𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 ≤ 𝐴))) | ||
| Theorem | pell1qrgaplem 42846 | Lemma for pell1qrgap 42847. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵))) | ||
| Theorem | pell1qrgap 42847 | First-quadrant Pell solutions are bounded away from 1. (This particular bound allows to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) | ||
| Theorem | pell14qrgap 42848 | Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) | ||
| Theorem | pell14qrgapw 42849 | Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → 2 < 𝐴) | ||
| Theorem | pellqrexplicit 42850 | Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1) → (𝐴 + ((√‘𝐷) · 𝐵)) ∈ (Pell1QR‘𝐷)) | ||
| Theorem | infmrgelbi 42851* | Any lower bound of a nonempty set of real numbers is less than or equal to its infimum, one-direction version. (Contributed by Stefan O'Rear, 1-Sep-2013.) (Revised by AV, 17-Sep-2020.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ 𝐵 ∈ ℝ) ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑥) → 𝐵 ≤ inf(𝐴, ℝ, < )) | ||
| Theorem | pellqrex 42852* | There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ∃𝑥 ∈ (Pell1QR‘𝐷)1 < 𝑥) | ||
| Theorem | pellfundval 42853* | Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) = inf({𝑥 ∈ (Pell14QR‘𝐷) ∣ 1 < 𝑥}, ℝ, < )) | ||
| Theorem | pellfundre 42854 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ) | ||
| Theorem | pellfundge 42855 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷)) | ||
| Theorem | pellfundgt1 42856 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷)) | ||
| Theorem | pellfundlb 42857 | A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) (Proof shortened by AV, 15-Sep-2020.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → (PellFund‘𝐷) ≤ 𝐴) | ||
| Theorem | pellfundglb 42858* | If a real is larger than the fundamental solution, there is a nontrivial solution less than it. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ ℝ ∧ (PellFund‘𝐷) < 𝐴) → ∃𝑥 ∈ (Pell1QR‘𝐷)((PellFund‘𝐷) ≤ 𝑥 ∧ 𝑥 < 𝐴)) | ||
| Theorem | pellfundex 42859 |
The fundamental solution as an infimum is itself a solution, showing
that the solution set is discrete.
Since the fundamental solution is an infimum, there must be an element ge to Fund and lt 2*Fund. If this element is equal to the fundamental solution we're done, otherwise use the infimum again to find another element which must be ge Fund and lt the first element; their ratio is a group element in (1,2), contradicting pell14qrgapw 42849. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) | ||
| Theorem | pellfund14gap 42860 | There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ (1 ≤ 𝐴 ∧ 𝐴 < (PellFund‘𝐷))) → 𝐴 = 1) | ||
| Theorem | pellfundrp 42861 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+) | ||
| Theorem | pellfundne1 42862 | The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ≠ 1) | ||
Section should be obsolete because its contents are covered by section "Logarithms to an arbitrary base" now. | ||
| Theorem | reglogcl 42863 | General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 26699 instead. |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ) | ||
| Theorem | reglogltb 42864 | General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 26710 instead. |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶)))) | ||
| Theorem | reglogleb 42865 | General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 26709 instead. |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶)))) | ||
| Theorem | reglogmul 42866 | Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 26703 instead. |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶)))) | ||
| Theorem | reglogexp 42867 | Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 26702 instead. |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶)))) | ||
| Theorem | reglogbas 42868 | General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 26694 instead. |
| ⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1) | ||
| Theorem | reglog1 42869 | General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 26695 instead. |
| ⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0) | ||
| Theorem | reglogexpbas 42870 | General log of a power of the base is the exponent. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbexp 26706 instead. |
| ⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁) | ||
| Theorem | pellfund14 42871* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥)) | ||
| Theorem | pellfund14b 42872* | The positive Pell solutions are precisely the integer powers of the fundamental solution. To get the general solution set (which we will not be using), throw in a copy of Z/2Z. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥))) | ||
| Syntax | crmx 42873 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
| class Xrm | ||
| Syntax | crmy 42874 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
| class Yrm | ||
| Definition | df-rmx 42875* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 42886 and rmxyval 42888 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ Xrm = (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))) | ||
| Definition | df-rmy 42876* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 42887 and rmxyval 42888 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ Yrm = (𝑎 ∈ (ℤ≥‘2), 𝑛 ∈ ℤ ↦ (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝑎↑2) − 1)) · (2nd ‘𝑏))))‘((𝑎 + (√‘((𝑎↑2) − 1)))↑𝑛)))) | ||
| Theorem | rmxfval 42877* | Value of the X sequence. Not used after rmxyval 42888 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) = (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
| Theorem | rmyfval 42878* | Value of the Y sequence. Not used after rmxyval 42888 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
| Theorem | rmspecsqrtnq 42879 | The discriminant used to define the X and Y sequences has an irrational square root. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof shortened by AV, 2-Aug-2021.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖ ℚ)) | ||
| Theorem | rmspecnonsq 42880 | The discriminant used to define the X and Y sequences is a nonsquare positive integer and thus a valid Pell equation discriminant. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴↑2) − 1) ∈ (ℕ ∖ ◻NN)) | ||
| Theorem | qirropth 42881 | This lemma implements the concept of "equate rational and irrational parts", used to prove many arithmetical properties of the X and Y sequences. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℂ ∖ ℚ) ∧ (𝐵 ∈ ℚ ∧ 𝐶 ∈ ℚ) ∧ (𝐷 ∈ ℚ ∧ 𝐸 ∈ ℚ)) → ((𝐵 + (𝐴 · 𝐶)) = (𝐷 + (𝐴 · 𝐸)) ↔ (𝐵 = 𝐷 ∧ 𝐶 = 𝐸))) | ||
| Theorem | rmspecfund 42882 | The base of exponent used to define the X and Y sequences is the fundamental solution of the corresponding Pell equation. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (PellFund‘((𝐴↑2) − 1)) = (𝐴 + (√‘((𝐴↑2) − 1)))) | ||
| Theorem | rmxyelqirr 42883* | The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof shortened by SN, 23-Dec-2024.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ∈ {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) | ||
| Theorem | rmxypairf1o 42884* | The function used to extract rational and irrational parts in df-rmx 42875 and df-rmy 42876 in fact achieves a one-to-one mapping from the quadratic irrationals to pairs of integers. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏)))):(ℕ0 × ℤ)–1-1-onto→{𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) | ||
| Theorem | rmxyelxp 42885* | Lemma for frmx 42886 and frmy 42887. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ)) | ||
| Theorem | frmx 42886 | The X sequence is a nonnegative integer. See rmxnn 42924 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0 | ||
| Theorem | frmy 42887 | The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ | ||
| Theorem | rmxyval 42888 | Main definition of the X and Y sequences. Compare definition 2.3 of [JonesMatijasevic] p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm 𝑁) + ((√‘((𝐴↑2) − 1)) · (𝐴 Yrm 𝑁))) = ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) | ||
| Theorem | rmspecpos 42889 | The discriminant used to define the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴↑2) − 1) ∈ ℝ+) | ||
| Theorem | rmxycomplete 42890* | The X and Y sequences taken together enumerate all solutions to the corresponding Pell equation in the right half-plane. This is Metamath 100 proof #39. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑋 ∈ ℕ0 ∧ 𝑌 ∈ ℤ) → (((𝑋↑2) − (((𝐴↑2) − 1) · (𝑌↑2))) = 1 ↔ ∃𝑛 ∈ ℤ (𝑋 = (𝐴 Xrm 𝑛) ∧ 𝑌 = (𝐴 Yrm 𝑛)))) | ||
| Theorem | rmxynorm 42891 | The X and Y sequences define a solution to the corresponding Pell equation. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (((𝐴 Xrm 𝑁)↑2) − (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑁)↑2))) = 1) | ||
| Theorem | rmbaserp 42892 | The base of exponentiation for the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 + (√‘((𝐴↑2) − 1))) ∈ ℝ+) | ||
| Theorem | rmxyneg 42893 | Negation law for X and Y sequences. JonesMatijasevic is inconsistent on whether the X and Y sequences have domain ℕ0 or ℤ; we use ℤ consistently to avoid the need for a separate subtraction law. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁) ∧ (𝐴 Yrm -𝑁) = -(𝐴 Yrm 𝑁))) | ||
| Theorem | rmxyadd 42894 | Addition formula for X and Y sequences. See rmxadd 42900 and rmyadd 42904 for most uses. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁)))) ∧ (𝐴 Yrm (𝑀 + 𝑁)) = (((𝐴 Yrm 𝑀) · (𝐴 Xrm 𝑁)) + ((𝐴 Xrm 𝑀) · (𝐴 Yrm 𝑁))))) | ||
| Theorem | rmxy1 42895 | Value of the X and Y sequences at 1. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴 Xrm 1) = 𝐴 ∧ (𝐴 Yrm 1) = 1)) | ||
| Theorem | rmxy0 42896 | Value of the X and Y sequences at 0. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → ((𝐴 Xrm 0) = 1 ∧ (𝐴 Yrm 0) = 0)) | ||
| Theorem | rmxneg 42897 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 42893, rmxyadd 42894, rmxy0 42896, and rmxy1 42895 via qirropth 42881 results in two theorems at once, but typical use requires only one, so this group of theorems serves to separate the cases. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm -𝑁) = (𝐴 Xrm 𝑁)) | ||
| Theorem | rmx0 42898 | Value of X sequence at 0. Part 1 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Xrm 0) = 1) | ||
| Theorem | rmx1 42899 | Value of X sequence at 1. Part 2 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (𝐴 Xrm 1) = 𝐴) | ||
| Theorem | rmxadd 42900 | Addition formula for X sequence. Equation 2.7 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm (𝑀 + 𝑁)) = (((𝐴 Xrm 𝑀) · (𝐴 Xrm 𝑁)) + (((𝐴↑2) − 1) · ((𝐴 Yrm 𝑀) · (𝐴 Yrm 𝑁))))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |