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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-pell1234qr 41001* | Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ Pell1234QR = (π₯ β (β β β»NN) β¦ {π¦ β β β£ βπ§ β β€ βπ€ β β€ (π¦ = (π§ + ((ββπ₯) Β· π€)) β§ ((π§β2) β (π₯ Β· (π€β2))) = 1)}) | ||
Definition | df-pellfund 41002* | 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 41003* | 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 41004* | 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 41005* | Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell14QRβπ·) = {π¦ β β β£ βπ§ β β0 βπ€ β β€ (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell14qr 41006* | Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell14QRβπ·) β (π΄ β β β§ βπ§ β β0 βπ€ β β€ (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell1234qrval 41007* | Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell1234QRβπ·) = {π¦ β β β£ βπ§ β β€ βπ€ β β€ (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell1234qr 41008* | Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell1234QRβπ·) β (π΄ β β β§ βπ§ β β€ βπ€ β β€ (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell1234qrre 41009 | General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β π΄ β β) | ||
Theorem | pell1234qrne0 41010 | No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β π΄ β 0) | ||
Theorem | pell1234qrreccl 41011 | General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β (1 / π΄) β (Pell1234QRβπ·)) | ||
Theorem | pell1234qrmulcl 41012 | General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·) β§ π΅ β (Pell1234QRβπ·)) β (π΄ Β· π΅) β (Pell1234QRβπ·)) | ||
Theorem | pell14qrss1234 41013 | A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell14QRβπ·) β (Pell1234QRβπ·)) | ||
Theorem | pell14qrre 41014 | A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β β) | ||
Theorem | pell14qrne0 41015 | A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β 0) | ||
Theorem | pell14qrgt0 41016 | A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β 0 < π΄) | ||
Theorem | pell14qrrp 41017 | A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β β+) | ||
Theorem | pell1234qrdich 41018 | 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 41019 | 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 41020 | Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β (Pell14QRβπ·)) β (π΄ Β· π΅) β (Pell14QRβπ·)) | ||
Theorem | pell14qrreccl 41021 | Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β (1 / π΄) β (Pell14QRβπ·)) | ||
Theorem | pell14qrdivcl 41022 | Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β (Pell14QRβπ·)) β (π΄ / π΅) β (Pell14QRβπ·)) | ||
Theorem | pell14qrexpclnn0 41023 | Lemma for pell14qrexpcl 41024. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β β0) β (π΄βπ΅) β (Pell14QRβπ·)) | ||
Theorem | pell14qrexpcl 41024 | Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ π΅ β β€) β (π΄βπ΅) β (Pell14QRβπ·)) | ||
Theorem | pell1qrss14 41025 | First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell1QRβπ·) β (Pell14QRβπ·)) | ||
Theorem | pell14qrdich 41026 | 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 41027 | A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1QRβπ·)) β 1 β€ π΄) | ||
Theorem | pell1qr1 41028 | 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 41029 | 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 41030 | Lemma for pell1qrgap 41031. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (((π· β β β§ (π΄ β β0 β§ π΅ β β0)) β§ (1 < (π΄ + ((ββπ·) Β· π΅)) β§ ((π΄β2) β (π· Β· (π΅β2))) = 1)) β ((ββ(π· + 1)) + (ββπ·)) β€ (π΄ + ((ββπ·) Β· π΅))) | ||
Theorem | pell1qrgap 41031 | 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 41032 | Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β ((ββ(π· + 1)) + (ββπ·)) β€ π΄) | ||
Theorem | pell14qrgapw 41033 | 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 41034 | 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 41035* | 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 41036* | 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 41037* | 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 41038 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β β) | ||
Theorem | pellfundge 41039 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β ((ββ(π· + 1)) + (ββπ·)) β€ (PellFundβπ·)) | ||
Theorem | pellfundgt1 41040 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β 1 < (PellFundβπ·)) | ||
Theorem | pellfundlb 41041 | 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 41042* | 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 41043 |
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 41033. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β (Pell1QRβπ·)) | ||
Theorem | pellfund14gap 41044 | 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 41045 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β β+) | ||
Theorem | pellfundne1 41046 | 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 41047 | 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 41048 | 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 41049 | 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 41050 | 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 41051 | 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 41052 | 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 41053 | 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 41054 | 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 41055* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β βπ₯ β β€ π΄ = ((PellFundβπ·)βπ₯)) | ||
Theorem | pellfund14b 41056* | 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 41057 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
class Xrm | ||
Syntax | crmy 41058 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
class Yrm | ||
Definition | df-rmx 41059* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 41071 and rmxyval 41073 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 41060* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 41072 and rmxyval 41073 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 41061* | Value of the X sequence. Not used after rmxyval 41073 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm π) = (1st β(β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)))) | ||
Theorem | rmyfval 41062* | Value of the Y sequence. Not used after rmxyval 41073 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm π) = (2nd β(β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)))) | ||
Theorem | rmspecsqrtnq 41063 | 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 41064 | 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 41065 | 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 41066 | 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 41067* | 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 41068* | Obsolete version of rmxyelqirr 41067 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 41069* | The function used to extract rational and irrational parts in df-rmx 41059 and df-rmy 41060 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 41070* | Lemma for frmx 41071 and frmy 41072. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)) β (β0 Γ β€)) | ||
Theorem | frmx 41071 | The X sequence is a nonnegative integer. See rmxnn 41109 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ Xrm :((β€β₯β2) Γ β€)βΆβ0 | ||
Theorem | frmy 41072 | The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ Yrm :((β€β₯β2) Γ β€)βΆβ€ | ||
Theorem | rmxyval 41073 | 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 41074 | 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 41075* | 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 41076 | 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 41077 | 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 41078 | 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 41079 | Addition formula for X and Y sequences. See rmxadd 41085 and rmyadd 41089 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 41080 | 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 41081 | 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 41082 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 41078, rmxyadd 41079, rmxy0 41081, and rmxy1 41080 via qirropth 41065 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 41083 | 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 41084 | 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 41085 | 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 π))))) | ||
Theorem | rmyneg 41086 | Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm -π) = -(π΄ Yrm π)) | ||
Theorem | rmy0 41087 | Value of Y sequence at 0. Part 1 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ (π΄ β (β€β₯β2) β (π΄ Yrm 0) = 0) | ||
Theorem | rmy1 41088 | Value of Y sequence at 1. Part 2 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ (π΄ β (β€β₯β2) β (π΄ Yrm 1) = 1) | ||
Theorem | rmyadd 41089 | Addition formula for Y sequence. Equation 2.8 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€ β§ π β β€) β (π΄ Yrm (π + π)) = (((π΄ Yrm π) Β· (π΄ Xrm π)) + ((π΄ Xrm π) Β· (π΄ Yrm π)))) | ||
Theorem | rmxp1 41090 | Special addition-of-1 formula for X sequence. Part 1 of equation 2.9 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((π΄ Xrm π) Β· π΄) + (((π΄β2) β 1) Β· (π΄ Yrm π)))) | ||
Theorem | rmyp1 41091 | Special addition of 1 formula for Y sequence. Part 2 of equation 2.9 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = (((π΄ Yrm π) Β· π΄) + (π΄ Xrm π))) | ||
Theorem | rmxm1 41092 | Subtraction of 1 formula for X sequence. Part 1 of equation 2.10 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm (π β 1)) = ((π΄ Β· (π΄ Xrm π)) β (((π΄β2) β 1) Β· (π΄ Yrm π)))) | ||
Theorem | rmym1 41093 | Subtraction of 1 formula for Y sequence. Part 2 of equation 2.10 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm (π β 1)) = (((π΄ Yrm π) Β· π΄) β (π΄ Xrm π))) | ||
Theorem | rmxluc 41094 | The X sequence is a Lucas (second-order integer recurrence) sequence. Part 3 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm (π + 1)) = (((2 Β· π΄) Β· (π΄ Xrm π)) β (π΄ Xrm (π β 1)))) | ||
Theorem | rmyluc 41095 | The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 41087 and rmy1 41088. Part 3 of equation 2.12 of [JonesMatijasevic] p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain (β€ Γ β€), which simplifies some later theorems. It may shorten the derivation to use this as our initial definition. Incidentally, the X sequence satisfies the exact same recurrence. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = ((2 Β· ((π΄ Yrm π) Β· π΄)) β (π΄ Yrm (π β 1)))) | ||
Theorem | rmyluc2 41096 | Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm (π + 1)) = (((2 Β· π΄) Β· (π΄ Yrm π)) β (π΄ Yrm (π β 1)))) | ||
Theorem | rmxdbl 41097 | "Double-angle formula" for X-values. Equation 2.13 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm (2 Β· π)) = ((2 Β· ((π΄ Xrm π)β2)) β 1)) | ||
Theorem | rmydbl 41098 | "Double-angle formula" for Y-values. Equation 2.14 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm (2 Β· π)) = ((2 Β· (π΄ Xrm π)) Β· (π΄ Yrm π))) | ||
Theorem | monotuz 41099* | A function defined on an upper set of integers which increases at every adjacent pair is globally strictly monotonic by induction. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ ((π β§ π¦ β π») β πΉ < πΊ) & β’ ((π β§ π₯ β π») β πΆ β β) & β’ π» = (β€β₯βπΌ) & β’ (π₯ = (π¦ + 1) β πΆ = πΊ) & β’ (π₯ = π¦ β πΆ = πΉ) & β’ (π₯ = π΄ β πΆ = π·) & β’ (π₯ = π΅ β πΆ = πΈ) β β’ ((π β§ (π΄ β π» β§ π΅ β π»)) β (π΄ < π΅ β π· < πΈ)) | ||
Theorem | monotoddzzfi 41100* | A function which is odd and monotonic on β0 is monotonic on β€. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
β’ ((π β§ π₯ β β€) β (πΉβπ₯) β β) & β’ ((π β§ π₯ β β€) β (πΉβ-π₯) = -(πΉβπ₯)) & β’ ((π β§ π₯ β β0 β§ π¦ β β0) β (π₯ < π¦ β (πΉβπ₯) < (πΉβπ¦))) β β’ ((π β§ π΄ β β€ β§ π΅ β β€) β (π΄ < π΅ β (πΉβπ΄) < (πΉβπ΅))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |