Home | Metamath
Proof Explorer Theorem List (p. 411 of 470) | < 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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | diophren 41001* | Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.) |
β’ ((π β (Diophβπ) β§ π β β0 β§ πΉ:(1...π)βΆ(1...π)) β {π β (β0 βm (1...π)) β£ (π β πΉ) β π} β (Diophβπ)) | ||
Theorem | rabrenfdioph 41002* | Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ ((π΅ β β0 β§ πΉ:(1...π΄)βΆ(1...π΅) β§ {π β (β0 βm (1...π΄)) β£ π} β (Diophβπ΄)) β {π β (β0 βm (1...π΅)) β£ [(π β πΉ) / π]π} β (Diophβπ΅)) | ||
Theorem | rabren3dioph 41003* | Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ (((πβ1) = (πβπ) β§ (πβ2) = (πβπ) β§ (πβ3) = (πβπ)) β (π β π)) & β’ π β (1...π) & β’ π β (1...π) & β’ π β (1...π) β β’ ((π β β0 β§ {π β (β0 βm (1...3)) β£ π} β (Diophβ3)) β {π β (β0 βm (1...π)) β£ π} β (Diophβπ)) | ||
Theorem | fphpd 41004* | Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ (π β π΅ βΊ π΄) & β’ ((π β§ π₯ β π΄) β πΆ β π΅) & β’ (π₯ = π¦ β πΆ = π·) β β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ β π¦ β§ πΆ = π·)) | ||
Theorem | fphpdo 41005* | Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β V) & β’ (π β π΅ βΊ π΄) & β’ ((π β§ π§ β π΄) β πΆ β π΅) & β’ (π§ = π₯ β πΆ = π·) & β’ (π§ = π¦ β πΆ = πΈ) β β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ < π¦ β§ π· = πΈ)) | ||
Theorem | ctbnfien 41006 | An infinite subset of a countable set is countable, without using choice. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ (((π β Ο β§ π β Ο) β§ (π΄ β π β§ Β¬ π΄ β Fin)) β π΄ β π) | ||
Theorem | fiphp3d 41007* | Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄) β π· β π΅) β β’ (π β βπ¦ β π΅ {π₯ β π΄ β£ π· = π¦} β β) | ||
Theorem | rencldnfilem 41008* | Lemma for rencldnfi 41009. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ (π΄ β β β§ Β¬ π΅ β π΄)) β§ βπ₯ β β+ βπ¦ β π΄ (absβ(π¦ β π΅)) < π₯) β Β¬ π΄ β Fin) | ||
Theorem | rencldnfi 41009* | A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 41008 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ Β¬ π΅ β π΄) β§ βπ₯ β β+ βπ¦ β π΄ (absβ(π¦ β π΅)) < π₯) β Β¬ π΄ β Fin) | ||
Theorem | irrapxlem1 41010* | Lemma for irrapx1 41016. Divides the unit interval into π΅ half-open sections and using the pigeonhole principle fphpdo 41005 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 41011* | Lemma for irrapx1 41016. 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 41012* | Lemma for irrapx1 41016. 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 41013* | Lemma for irrapx1 41016. 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 41014* | Lemma for irrapx1 41016. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β+) β βπ₯ β β (0 < π₯ β§ (absβ(π₯ β π΄)) < π΅ β§ (absβ(π₯ β π΄)) < ((denomβπ₯)β-2))) | ||
Theorem | irrapxlem6 41015* | Lemma for irrapx1 41016. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β+) β βπ₯ β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} (absβ(π₯ β π΄)) < π΅) | ||
Theorem | irrapx1 41016* | 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 41017 | Lemma for pellex 41023. 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 41018 | Lemma for pellex 41023. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
β’ (((π· β β β§ π΄ β β β§ π΅ β β) β§ (absβ((π΄ / π΅) β (ββπ·))) < (π΅β-2)) β (absβ((π΄β2) β (π· Β· (π΅β2)))) < (1 + (2 Β· (ββπ·)))) | ||
Theorem | pellexlem3 41019* | Lemma for pellex 41023. 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 41020* | Lemma for pellex 41023. Invoking irrapx1 41016, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
β’ ((π· β β β§ Β¬ (ββπ·) β β) β {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β· (ββπ·)))))} β β) | ||
Theorem | pellexlem5 41021* | Lemma for pellex 41023. Invoking fiphp3d 41007, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ ((π· β β β§ Β¬ (ββπ·) β β) β βπ₯ β β€ (π₯ β 0 β§ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ ((π¦β2) β (π· Β· (π§β2))) = π₯)} β β)) | ||
Theorem | pellexlem6 41022* | Lemma for pellex 41023. 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 41023* | 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 41024 | Extend class notation to include the set of square positive integers. |
class β»NN | ||
Syntax | cpell1qr 41025 | Extend class notation to include the class of quadrant-1 Pell solutions. |
class Pell1QR | ||
Syntax | cpell1234qr 41026 | Extend class notation to include the class of any-quadrant Pell solutions. |
class Pell1234QR | ||
Syntax | cpell14qr 41027 | Extend class notation to include the class of positive Pell solutions. |
class Pell14QR | ||
Syntax | cpellfund 41028 | Extend class notation to include the Pell-equation fundamental solution function. |
class PellFund | ||
Definition | df-squarenn 41029 | Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ β»NN = {π₯ β β β£ (ββπ₯) β β} | ||
Definition | df-pell1qr 41030* | 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 41031* | 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 41032* | Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ Pell1234QR = (π₯ β (β β β»NN) β¦ {π¦ β β β£ βπ§ β β€ βπ€ β β€ (π¦ = (π§ + ((ββπ₯) Β· π€)) β§ ((π§β2) β (π₯ Β· (π€β2))) = 1)}) | ||
Definition | df-pellfund 41033* | 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 41034* | 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 41035* | 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 41036* | Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell14QRβπ·) = {π¦ β β β£ βπ§ β β0 βπ€ β β€ (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell14qr 41037* | Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell14QRβπ·) β (π΄ β β β§ βπ§ β β0 βπ€ β β€ (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell1234qrval 41038* | Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell1234QRβπ·) = {π¦ β β β£ βπ§ β β€ βπ€ β β€ (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell1234qr 41039* | Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell1234QRβπ·) β (π΄ β β β§ βπ§ β β€ βπ€ β β€ (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell1234qrre 41040 | General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β π΄ β β) | ||
Theorem | pell1234qrne0 41041 | No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β π΄ β 0) | ||
Theorem | pell1234qrreccl 41042 | General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β (1 / π΄) β (Pell1234QRβπ·)) | ||
Theorem | pell1234qrmulcl 41043 | General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·) β§ π΅ β (Pell1234QRβπ·)) β (π΄ Β· π΅) β (Pell1234QRβπ·)) | ||
Theorem | pell14qrss1234 41044 | A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell14QRβπ·) β (Pell1234QRβπ·)) | ||
Theorem | pell14qrre 41045 | A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β β) | ||
Theorem | pell14qrne0 41046 | A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β 0) | ||
Theorem | pell14qrgt0 41047 | A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β 0 < π΄) | ||
Theorem | pell14qrrp 41048 | A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β β+) | ||
Theorem | pell1234qrdich 41049 | 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 41050 | 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 41051 | Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β (Pell14QRβπ·)) β (π΄ Β· π΅) β (Pell14QRβπ·)) | ||
Theorem | pell14qrreccl 41052 | Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β (1 / π΄) β (Pell14QRβπ·)) | ||
Theorem | pell14qrdivcl 41053 | Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β (Pell14QRβπ·)) β (π΄ / π΅) β (Pell14QRβπ·)) | ||
Theorem | pell14qrexpclnn0 41054 | Lemma for pell14qrexpcl 41055. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β β0) β (π΄βπ΅) β (Pell14QRβπ·)) | ||
Theorem | pell14qrexpcl 41055 | Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β β€) β (π΄βπ΅) β (Pell14QRβπ·)) | ||
Theorem | pell1qrss14 41056 | First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell1QRβπ·) β (Pell14QRβπ·)) | ||
Theorem | pell14qrdich 41057 | 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 41058 | A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1QRβπ·)) β 1 β€ π΄) | ||
Theorem | pell1qr1 41059 | 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 41060 | 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 41061 | Lemma for pell1qrgap 41062. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (((π· β β β§ (π΄ β β0 β§ π΅ β β0)) β§ (1 < (π΄ + ((ββπ·) Β· π΅)) β§ ((π΄β2) β (π· Β· (π΅β2))) = 1)) β ((ββ(π· + 1)) + (ββπ·)) β€ (π΄ + ((ββπ·) Β· π΅))) | ||
Theorem | pell1qrgap 41062 | 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 41063 | Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β ((ββ(π· + 1)) + (ββπ·)) β€ π΄) | ||
Theorem | pell14qrgapw 41064 | 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 41065 | 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 41066* | 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 41067* | 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 41068* | 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 41069 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β β) | ||
Theorem | pellfundge 41070 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β ((ββ(π· + 1)) + (ββπ·)) β€ (PellFundβπ·)) | ||
Theorem | pellfundgt1 41071 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β 1 < (PellFundβπ·)) | ||
Theorem | pellfundlb 41072 | 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 41073* | 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 41074 |
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 41064. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β (Pell1QRβπ·)) | ||
Theorem | pellfund14gap 41075 | 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 41076 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β β+) | ||
Theorem | pellfundne1 41077 | 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 41078 | General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 26045 instead. |
β’ ((π΄ β β+ β§ π΅ β β+ β§ π΅ β 1) β ((logβπ΄) / (logβπ΅)) β β) | ||
Theorem | reglogltb 41079 | General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 26056 instead. |
β’ (((π΄ β β+ β§ π΅ β β+) β§ (πΆ β β+ β§ 1 < πΆ)) β (π΄ < π΅ β ((logβπ΄) / (logβπΆ)) < ((logβπ΅) / (logβπΆ)))) | ||
Theorem | reglogleb 41080 | General logarithm preserves β€. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 26055 instead. |
β’ (((π΄ β β+ β§ π΅ β β+) β§ (πΆ β β+ β§ 1 < πΆ)) β (π΄ β€ π΅ β ((logβπ΄) / (logβπΆ)) β€ ((logβπ΅) / (logβπΆ)))) | ||
Theorem | reglogmul 41081 | Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 26049 instead. |
β’ ((π΄ β β+ β§ π΅ β β+ β§ (πΆ β β+ β§ πΆ β 1)) β ((logβ(π΄ Β· π΅)) / (logβπΆ)) = (((logβπ΄) / (logβπΆ)) + ((logβπ΅) / (logβπΆ)))) | ||
Theorem | reglogexp 41082 | Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 26048 instead. |
β’ ((π΄ β β+ β§ π β β€ β§ (πΆ β β+ β§ πΆ β 1)) β ((logβ(π΄βπ)) / (logβπΆ)) = (π Β· ((logβπ΄) / (logβπΆ)))) | ||
Theorem | reglogbas 41083 | General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 26040 instead. |
β’ ((πΆ β β+ β§ πΆ β 1) β ((logβπΆ) / (logβπΆ)) = 1) | ||
Theorem | reglog1 41084 | General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 26041 instead. |
β’ ((πΆ β β+ β§ πΆ β 1) β ((logβ1) / (logβπΆ)) = 0) | ||
Theorem | reglogexpbas 41085 | 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 26052 instead. |
β’ ((π β β€ β§ (πΆ β β+ β§ πΆ β 1)) β ((logβ(πΆβπ)) / (logβπΆ)) = π) | ||
Theorem | pellfund14 41086* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β βπ₯ β β€ π΄ = ((PellFundβπ·)βπ₯)) | ||
Theorem | pellfund14b 41087* | 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 41088 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
class Xrm | ||
Syntax | crmy 41089 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
class Yrm | ||
Definition | df-rmx 41090* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 41102 and rmxyval 41104 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 41091* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 41103 and rmxyval 41104 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 41092* | Value of the X sequence. Not used after rmxyval 41104 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm π) = (1st β(β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)))) | ||
Theorem | rmyfval 41093* | Value of the Y sequence. Not used after rmxyval 41104 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm π) = (2nd β(β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)))) | ||
Theorem | rmspecsqrtnq 41094 | 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 41095 | 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 41096 | 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 41097 | 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 41098* | 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 | rmxyelqirrOLD 41099* | Obsolete version of rmxyelqirr 41098 as of 23-Dec-2024. (Contributed by Stefan O'Rear, 21-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β ((π΄ + (ββ((π΄β2) β 1)))βπ) β {π β£ βπ β β0 βπ β β€ π = (π + ((ββ((π΄β2) β 1)) Β· π))}) | ||
Theorem | rmxypairf1o 41100* | The function used to extract rational and irrational parts in df-rmx 41090 and df-rmy 41091 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)) Β· π))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |