HomeTheorem List (p. 378 of 429)
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. 378 of 429) | < 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-27903) |
Hilbert Space Explorer
(27904-29428) |
Users' Mathboxes
(29429-42879) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | rencldnfilem 37701* | Lemma for rencldnfi 37702. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ (𝐴 ≠ ∅ ∧ ¬ 𝐵 ∈ 𝐴)) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin) | ||
| Theorem | rencldnfi 37702* | A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 37701 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ (((𝐴 ⊆ ℝ ∧ 𝐵 ∈ ℝ ∧ ¬ 𝐵 ∈ 𝐴) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐴 (abs‘(𝑦 − 𝐵)) < 𝑥) → ¬ 𝐴 ∈ Fin) | ||
| Theorem | irrapxlem1 37703* | Lemma for irrapx1 37709. Divides the unit interval into 𝐵 half-open sections and using the pigeonhole principle fphpdo 37698 finds two multiples of 𝐴 in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (0...𝐵)∃𝑦 ∈ (0...𝐵)(𝑥 < 𝑦 ∧ (⌊‘(𝐵 · ((𝐴 · 𝑥) mod 1))) = (⌊‘(𝐵 · ((𝐴 · 𝑦) mod 1))))) | ||
| Theorem | irrapxlem2 37704* | Lemma for irrapx1 37709. Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (0...𝐵)∃𝑦 ∈ (0...𝐵)(𝑥 < 𝑦 ∧ (abs‘(((𝐴 · 𝑥) mod 1) − ((𝐴 · 𝑦) mod 1))) < (1 / 𝐵))) | ||
| Theorem | irrapxlem3 37705* | Lemma for irrapx1 37709. By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ (1...𝐵)∃𝑦 ∈ ℕ0 (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / 𝐵)) | ||
| Theorem | irrapxlem4 37706* | Lemma for irrapx1 37709. Eliminate ranges, use positivity of the input to force positivity of the output by increasing 𝐵 as needed. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℕ) → ∃𝑥 ∈ ℕ ∃𝑦 ∈ ℕ (abs‘((𝐴 · 𝑥) − 𝑦)) < (1 / if(𝑥 ≤ 𝐵, 𝐵, 𝑥))) | ||
| Theorem | irrapxlem5 37707* | Lemma for irrapx1 37709. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ ℚ (0 < 𝑥 ∧ (abs‘(𝑥 − 𝐴)) < 𝐵 ∧ (abs‘(𝑥 − 𝐴)) < ((denom‘𝑥)↑-2))) | ||
| Theorem | irrapxlem6 37708* | Lemma for irrapx1 37709. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) → ∃𝑥 ∈ {𝑦 ∈ ℚ ∣ (0 < 𝑦 ∧ (abs‘(𝑦 − 𝐴)) < ((denom‘𝑦)↑-2))} (abs‘(𝑥 − 𝐴)) < 𝐵) | ||
| Theorem | irrapx1 37709* | 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 37710 | Lemma for pellex 37716. 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 37711 | Lemma for pellex 37716. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ 𝐴 ∈ ℕ ∧ 𝐵 ∈ ℕ) ∧ (abs‘((𝐴 / 𝐵) − (√‘𝐷))) < (𝐵↑-2)) → (abs‘((𝐴↑2) − (𝐷 · (𝐵↑2)))) < (1 + (2 · (√‘𝐷)))) | ||
| Theorem | pellexlem3 37712* | Lemma for pellex 37716. 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 37713* | Lemma for pellex 37716. Invoking irrapx1 37709, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ (((𝑦↑2) − (𝐷 · (𝑧↑2))) ≠ 0 ∧ (abs‘((𝑦↑2) − (𝐷 · (𝑧↑2)))) < (1 + (2 · (√‘𝐷)))))} ≈ ℕ) | ||
| Theorem | pellexlem5 37714* | Lemma for pellex 37716. Invoking fiphp3d 37700, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
| ⊢ ((𝐷 ∈ ℕ ∧ ¬ (√‘𝐷) ∈ ℚ) → ∃𝑥 ∈ ℤ (𝑥 ≠ 0 ∧ {⟨𝑦, 𝑧⟩ ∣ ((𝑦 ∈ ℕ ∧ 𝑧 ∈ ℕ) ∧ ((𝑦↑2) − (𝐷 · (𝑧↑2))) = 𝑥)} ≈ ℕ)) | ||
| Theorem | pellexlem6 37715* | Lemma for pellex 37716. 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 37716* | 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 37717 | Extend class notation to include the set of square positive integers. |
| class ◻NN | ||
| Syntax | cpell1qr 37718 | Extend class notation to include the class of quadrant-1 Pell solutions. |
| class Pell1QR | ||
| Syntax | cpell1234qr 37719 | Extend class notation to include the class of any-quadrant Pell solutions. |
| class Pell1234QR | ||
| Syntax | cpell14qr 37720 | Extend class notation to include the class of positive Pell solutions. |
| class Pell14QR | ||
| Syntax | cpellfund 37721 | Extend class notation to include the Pell-equation fundamental solution function. |
| class PellFund | ||
| Definition | df-squarenn 37722 | Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ◻NN = {𝑥 ∈ ℕ ∣ (√‘𝑥) ∈ ℚ} | ||
| Definition | df-pell1qr 37723* | 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 37724* | 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 37725* | Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ Pell1234QR = (𝑥 ∈ (ℕ ∖ ◻NN) ↦ {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝑥) · 𝑤)) ∧ ((𝑧↑2) − (𝑥 · (𝑤↑2))) = 1)}) | ||
| Definition | df-pellfund 37726* | 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 37727* | 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 37728* | 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 37729* | Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell14qr 37730* | Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell14QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℕ0 ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell1234qrval 37731* | Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1234QR‘𝐷) = {𝑦 ∈ ℝ ∣ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝑦 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)}) | ||
| Theorem | elpell1234qr 37732* | Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (𝐴 ∈ (Pell1234QR‘𝐷) ↔ (𝐴 ∈ ℝ ∧ ∃𝑧 ∈ ℤ ∃𝑤 ∈ ℤ (𝐴 = (𝑧 + ((√‘𝐷) · 𝑤)) ∧ ((𝑧↑2) − (𝐷 · (𝑤↑2))) = 1)))) | ||
| Theorem | pell1234qrre 37733 | General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ∈ ℝ) | ||
| Theorem | pell1234qrne0 37734 | No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → 𝐴 ≠ 0) | ||
| Theorem | pell1234qrreccl 37735 | General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷)) → (1 / 𝐴) ∈ (Pell1234QR‘𝐷)) | ||
| Theorem | pell1234qrmulcl 37736 | General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1234QR‘𝐷) ∧ 𝐵 ∈ (Pell1234QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell1234QR‘𝐷)) | ||
| Theorem | pell14qrss1234 37737 | A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell14QR‘𝐷) ⊆ (Pell1234QR‘𝐷)) | ||
| Theorem | pell14qrre 37738 | A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ) | ||
| Theorem | pell14qrne0 37739 | A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ≠ 0) | ||
| Theorem | pell14qrgt0 37740 | A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 0 < 𝐴) | ||
| Theorem | pell14qrrp 37741 | A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → 𝐴 ∈ ℝ+) | ||
| Theorem | pell1234qrdich 37742 | 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 37743 | 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 37744 | Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 · 𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrreccl 37745 | Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → (1 / 𝐴) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrdivcl 37746 | Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ (Pell14QR‘𝐷)) → (𝐴 / 𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrexpclnn0 37747 | Lemma for pell14qrexpcl 37748. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℕ0) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrexpcl 37748 | Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 𝐵 ∈ ℤ) → (𝐴↑𝐵) ∈ (Pell14QR‘𝐷)) | ||
| Theorem | pell1qrss14 37749 | First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (Pell1QR‘𝐷) ⊆ (Pell14QR‘𝐷)) | ||
| Theorem | pell14qrdich 37750 | 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 37751 | A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷)) → 1 ≤ 𝐴) | ||
| Theorem | pell1qr1 37752 | 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 37753 | 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 37754 | Lemma for pell1qrgap 37755. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (((𝐷 ∈ ℕ ∧ (𝐴 ∈ ℕ0 ∧ 𝐵 ∈ ℕ0)) ∧ (1 < (𝐴 + ((√‘𝐷) · 𝐵)) ∧ ((𝐴↑2) − (𝐷 · (𝐵↑2))) = 1)) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (𝐴 + ((√‘𝐷) · 𝐵))) | ||
| Theorem | pell1qrgap 37755 | First-quadrant Pell solutions are bounded away from 1. (This particular bound allows us to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell1QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) | ||
| Theorem | pell14qrgap 37756 | Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷) ∧ 1 < 𝐴) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ 𝐴) | ||
| Theorem | pell14qrgapw 37757 | 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 37758 | 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 37759* | 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 37760* | 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 37761* | 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 37762 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ) | ||
| Theorem | pellfundge 37763 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → ((√‘(𝐷 + 1)) + (√‘𝐷)) ≤ (PellFund‘𝐷)) | ||
| Theorem | pellfundgt1 37764 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → 1 < (PellFund‘𝐷)) | ||
| Theorem | pellfundlb 37765 | 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 37766* | 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 37767 |
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 37757. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ (Pell1QR‘𝐷)) | ||
| Theorem | pellfund14gap 37768 | 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 37769 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ (𝐷 ∈ (ℕ ∖ ◻NN) → (PellFund‘𝐷) ∈ ℝ+) | ||
| Theorem | pellfundne1 37770 | 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 37771 | General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 24556 instead. |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ 𝐵 ≠ 1) → ((log‘𝐴) / (log‘𝐵)) ∈ ℝ) | ||
| Theorem | reglogltb 37772 | General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 24567 instead. |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 < 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) < ((log‘𝐵) / (log‘𝐶)))) | ||
| Theorem | reglogleb 37773 | General logarithm preserves ≤. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 24566 instead. |
| ⊢ (((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+) ∧ (𝐶 ∈ ℝ+ ∧ 1 < 𝐶)) → (𝐴 ≤ 𝐵 ↔ ((log‘𝐴) / (log‘𝐶)) ≤ ((log‘𝐵) / (log‘𝐶)))) | ||
| Theorem | reglogmul 37774 | Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 24560 instead. |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ+ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴 · 𝐵)) / (log‘𝐶)) = (((log‘𝐴) / (log‘𝐶)) + ((log‘𝐵) / (log‘𝐶)))) | ||
| Theorem | reglogexp 37775 | Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 24559 instead. |
| ⊢ ((𝐴 ∈ ℝ+ ∧ 𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐴↑𝑁)) / (log‘𝐶)) = (𝑁 · ((log‘𝐴) / (log‘𝐶)))) | ||
| Theorem | reglogbas 37776 | General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 24551 instead. |
| ⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘𝐶) / (log‘𝐶)) = 1) | ||
| Theorem | reglog1 37777 | General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 24552 instead. |
| ⊢ ((𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1) → ((log‘1) / (log‘𝐶)) = 0) | ||
| Theorem | reglogexpbas 37778 | 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 24563 instead. |
| ⊢ ((𝑁 ∈ ℤ ∧ (𝐶 ∈ ℝ+ ∧ 𝐶 ≠ 1)) → ((log‘(𝐶↑𝑁)) / (log‘𝐶)) = 𝑁) | ||
| Theorem | pellfund14 37779* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
| ⊢ ((𝐷 ∈ (ℕ ∖ ◻NN) ∧ 𝐴 ∈ (Pell14QR‘𝐷)) → ∃𝑥 ∈ ℤ 𝐴 = ((PellFund‘𝐷)↑𝑥)) | ||
| Theorem | pellfund14b 37780* | 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 37781 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
| class Xrm | ||
| Syntax | crmy 37782 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
| class Yrm | ||
| Definition | df-rmx 37783* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 37795 and rmxyval 37797 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 37784* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 37796 and rmxyval 37797 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 37785* | Value of the X sequence. Not used after rmxyval 37797 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Xrm 𝑁) = (1st ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
| Theorem | rmyfval 37786* | Value of the Y sequence. Not used after rmxyval 37797 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (𝐴 Yrm 𝑁) = (2nd ‘(◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)))) | ||
| Theorem | rmspecsqrtnq 37787 | 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 | rmspecsqrtnqOLD 37788 | Obsolete version of rmspecsqrtnq 37787 as of 2-Aug-2021. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ (ℤ≥‘2) → (√‘((𝐴↑2) − 1)) ∈ (ℂ ∖ ℚ)) | ||
| Theorem | rmspecnonsq 37789 | 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 37790 | 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 37791 | 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 37792* | The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → ((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁) ∈ {𝑎 ∣ ∃𝑐 ∈ ℕ0 ∃𝑑 ∈ ℤ 𝑎 = (𝑐 + ((√‘((𝐴↑2) − 1)) · 𝑑))}) | ||
| Theorem | rmxypairf1o 37793* | The function used to extract rational and irrational parts in df-rmx 37783 and df-rmy 37784 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 37794* | Lemma for frmx 37795 and frmy 37796. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ ((𝐴 ∈ (ℤ≥‘2) ∧ 𝑁 ∈ ℤ) → (◡(𝑏 ∈ (ℕ0 × ℤ) ↦ ((1st ‘𝑏) + ((√‘((𝐴↑2) − 1)) · (2nd ‘𝑏))))‘((𝐴 + (√‘((𝐴↑2) − 1)))↑𝑁)) ∈ (ℕ0 × ℤ)) | ||
| Theorem | frmx 37795 | The X sequence is a nonnegative integer. See rmxnn 37835 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ Xrm :((ℤ≥‘2) × ℤ)⟶ℕ0 | ||
| Theorem | frmy 37796 | The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
| ⊢ Yrm :((ℤ≥‘2) × ℤ)⟶ℤ | ||
| Theorem | rmxyval 37797 | 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 37798 | 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 37799* | 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 37800 | 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) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |