![]() |
Metamath
Proof Explorer Theorem List (p. 417 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pell1qrgaplem 41601 | Lemma for pell1qrgap 41602. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (((π· β β β§ (π΄ β β0 β§ π΅ β β0)) β§ (1 < (π΄ + ((ββπ·) Β· π΅)) β§ ((π΄β2) β (π· Β· (π΅β2))) = 1)) β ((ββ(π· + 1)) + (ββπ·)) β€ (π΄ + ((ββπ·) Β· π΅))) | ||
Theorem | pell1qrgap 41602 | 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 41603 | Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·) β§ 1 < π΄) β ((ββ(π· + 1)) + (ββπ·)) β€ π΄) | ||
Theorem | pell14qrgapw 41604 | 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 41605 | 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 41606* | 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 41607* | 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 41608* | 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 41609 | The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β β) | ||
Theorem | pellfundge 41610 | Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β ((ββ(π· + 1)) + (ββπ·)) β€ (PellFundβπ·)) | ||
Theorem | pellfundgt1 41611 | Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β 1 < (PellFundβπ·)) | ||
Theorem | pellfundlb 41612 | 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 41613* | 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 41614 |
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 41604. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β (Pell1QRβπ·)) | ||
Theorem | pellfund14gap 41615 | 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 41616 | The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ (π· β (β β β»NN) β (PellFundβπ·) β β+) | ||
Theorem | pellfundne1 41617 | 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 41618 | General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 26275 instead. |
β’ ((π΄ β β+ β§ π΅ β β+ β§ π΅ β 1) β ((logβπ΄) / (logβπ΅)) β β) | ||
Theorem | reglogltb 41619 | General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 26286 instead. |
β’ (((π΄ β β+ β§ π΅ β β+) β§ (πΆ β β+ β§ 1 < πΆ)) β (π΄ < π΅ β ((logβπ΄) / (logβπΆ)) < ((logβπ΅) / (logβπΆ)))) | ||
Theorem | reglogleb 41620 | General logarithm preserves β€. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 26285 instead. |
β’ (((π΄ β β+ β§ π΅ β β+) β§ (πΆ β β+ β§ 1 < πΆ)) β (π΄ β€ π΅ β ((logβπ΄) / (logβπΆ)) β€ ((logβπ΅) / (logβπΆ)))) | ||
Theorem | reglogmul 41621 | Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 26279 instead. |
β’ ((π΄ β β+ β§ π΅ β β+ β§ (πΆ β β+ β§ πΆ β 1)) β ((logβ(π΄ Β· π΅)) / (logβπΆ)) = (((logβπ΄) / (logβπΆ)) + ((logβπ΅) / (logβπΆ)))) | ||
Theorem | reglogexp 41622 | Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 26278 instead. |
β’ ((π΄ β β+ β§ π β β€ β§ (πΆ β β+ β§ πΆ β 1)) β ((logβ(π΄βπ)) / (logβπΆ)) = (π Β· ((logβπ΄) / (logβπΆ)))) | ||
Theorem | reglogbas 41623 | General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 26270 instead. |
β’ ((πΆ β β+ β§ πΆ β 1) β ((logβπΆ) / (logβπΆ)) = 1) | ||
Theorem | reglog1 41624 | General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 26271 instead. |
β’ ((πΆ β β+ β§ πΆ β 1) β ((logβ1) / (logβπΆ)) = 0) | ||
Theorem | reglogexpbas 41625 | 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 26282 instead. |
β’ ((π β β€ β§ (πΆ β β+ β§ πΆ β 1)) β ((logβ(πΆβπ)) / (logβπΆ)) = π) | ||
Theorem | pellfund14 41626* | Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β βπ₯ β β€ π΄ = ((PellFundβπ·)βπ₯)) | ||
Theorem | pellfund14b 41627* | 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 41628 | Extend class notation to include the Robertson-Matiyasevich X sequence. |
class Xrm | ||
Syntax | crmy 41629 | Extend class notation to include the Robertson-Matiyasevich Y sequence. |
class Yrm | ||
Definition | df-rmx 41630* | Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 41642 and rmxyval 41644 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 41631* | Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 41643 and rmxyval 41644 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 41632* | Value of the X sequence. Not used after rmxyval 41644 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm π) = (1st β(β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)))) | ||
Theorem | rmyfval 41633* | Value of the Y sequence. Not used after rmxyval 41644 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm π) = (2nd β(β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)))) | ||
Theorem | rmspecsqrtnq 41634 | 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 41635 | 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 41636 | 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 41637 | 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 41638* | 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 41639* | Obsolete version of rmxyelqirr 41638 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 41640* | The function used to extract rational and irrational parts in df-rmx 41630 and df-rmy 41631 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 41641* | Lemma for frmx 41642 and frmy 41643. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (β‘(π β (β0 Γ β€) β¦ ((1st βπ) + ((ββ((π΄β2) β 1)) Β· (2nd βπ))))β((π΄ + (ββ((π΄β2) β 1)))βπ)) β (β0 Γ β€)) | ||
Theorem | frmx 41642 | The X sequence is a nonnegative integer. See rmxnn 41680 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ Xrm :((β€β₯β2) Γ β€)βΆβ0 | ||
Theorem | frmy 41643 | The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ Yrm :((β€β₯β2) Γ β€)βΆβ€ | ||
Theorem | rmxyval 41644 | 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 41645 | 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 41646* | 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 41647 | 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 41648 | 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 41649 | 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 41650 | Addition formula for X and Y sequences. See rmxadd 41656 and rmyadd 41660 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 41651 | 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 41652 | 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 41653 | Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 41649, rmxyadd 41650, rmxy0 41652, and rmxy1 41651 via qirropth 41636 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 41654 | 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 41655 | 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 41656 | 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 41657 | Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Yrm -π) = -(π΄ Yrm π)) | ||
Theorem | rmy0 41658 | 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 41659 | 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 41660 | 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 41661 | 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 41662 | 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 41663 | 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 41664 | 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 41665 | 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 41666 | The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 41658 and rmy1 41659. 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 41667 | 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 41668 | "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 41669 | "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 41670* | 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 41671* | 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) β (π₯ < π¦ β (πΉβπ₯) < (πΉβπ¦))) β β’ ((π β§ π΄ β β€ β§ π΅ β β€) β (π΄ < π΅ β (πΉβπ΄) < (πΉβπ΅))) | ||
Theorem | monotoddzz 41672* | A function (given implicitly) 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) β (π₯ < π¦ β πΈ < πΉ)) & β’ ((π β§ π₯ β β€) β πΈ β β) & β’ ((π β§ π¦ β β€) β πΊ = -πΉ) & β’ (π₯ = π΄ β πΈ = πΆ) & β’ (π₯ = π΅ β πΈ = π·) & β’ (π₯ = π¦ β πΈ = πΉ) & β’ (π₯ = -π¦ β πΈ = πΊ) β β’ ((π β§ π΄ β β€ β§ π΅ β β€) β (π΄ < π΅ β πΆ < π·)) | ||
Theorem | oddcomabszz 41673* | An odd function which takes nonnegative values on nonnegative arguments commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
β’ ((π β§ π₯ β β€) β π΄ β β) & β’ ((π β§ π₯ β β€ β§ 0 β€ π₯) β 0 β€ π΄) & β’ ((π β§ π¦ β β€) β πΆ = -π΅) & β’ (π₯ = π¦ β π΄ = π΅) & β’ (π₯ = -π¦ β π΄ = πΆ) & β’ (π₯ = π· β π΄ = πΈ) & β’ (π₯ = (absβπ·) β π΄ = πΉ) β β’ ((π β§ π· β β€) β (absβπΈ) = πΉ) | ||
Theorem | 2nn0ind 41674* | Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ π & β’ π & β’ (π¦ β β β ((π β§ π) β π)) & β’ (π₯ = 0 β (π β π)) & β’ (π₯ = 1 β (π β π)) & β’ (π₯ = (π¦ β 1) β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + 1) β (π β π)) & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β β0 β π) | ||
Theorem | zindbi 41675* | Inductively transfer a property to the integers if it holds for zero and passes between adjacent integers in either direction. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ (π¦ β β€ β (π β π)) & β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = (π¦ + 1) β (π β π)) & β’ (π₯ = 0 β (π β π)) & β’ (π₯ = π΄ β (π β π)) β β’ (π΄ β β€ β (π β π)) | ||
Theorem | rmxypos 41676 | For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0) β (0 < (π΄ Xrm π) β§ 0 β€ (π΄ Yrm π))) | ||
Theorem | ltrmynn0 41677 | The Y-sequence is strictly monotonic on β0. Strengthened by ltrmy 41681. (Contributed by Stefan O'Rear, 24-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0 β§ π β β0) β (π < π β (π΄ Yrm π) < (π΄ Yrm π))) | ||
Theorem | ltrmxnn0 41678 | The X-sequence is strictly monotonic on β0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0 β§ π β β0) β (π < π β (π΄ Xrm π) < (π΄ Xrm π))) | ||
Theorem | lermxnn0 41679 | The X-sequence is monotonic on β0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0 β§ π β β0) β (π β€ π β (π΄ Xrm π) β€ (π΄ Xrm π))) | ||
Theorem | rmxnn 41680 | The X-sequence is defined to range over β0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π΄ Xrm π) β β) | ||
Theorem | ltrmy 41681 | The Y-sequence is strictly monotonic over β€. (Contributed by Stefan O'Rear, 25-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€ β§ π β β€) β (π < π β (π΄ Yrm π) < (π΄ Yrm π))) | ||
Theorem | rmyeq0 41682 | Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β (π = 0 β (π΄ Yrm π) = 0)) | ||
Theorem | rmyeq 41683 | Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€ β§ π β β€) β (π = π β (π΄ Yrm π) = (π΄ Yrm π))) | ||
Theorem | lermy 41684 | Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€ β§ π β β€) β (π β€ π β (π΄ Yrm π) β€ (π΄ Yrm π))) | ||
Theorem | rmynn 41685 | Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β) β (π΄ Yrm π) β β) | ||
Theorem | rmynn0 41686 | Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0) β (π΄ Yrm π) β β0) | ||
Theorem | rmyabs 41687 | Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π΅ β β€) β (absβ(π΄ Yrm π΅)) = (π΄ Yrm (absβπ΅))) | ||
Theorem | jm2.24nn 41688 | X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of [JonesMatijasevic] p. 697 restricted to β. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < (π΄ Xrm π)) | ||
Theorem | jm2.17a 41689 | First half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0) β (((2 Β· π΄) β 1)βπ) β€ (π΄ Yrm (π + 1))) | ||
Theorem | jm2.17b 41690 | Weak form of the second half of lemma 2.17 of [JonesMatijasevic] p. 696, allowing induction to start lower. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0) β (π΄ Yrm (π + 1)) β€ ((2 Β· π΄)βπ)) | ||
Theorem | jm2.17c 41691 | Second half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 15-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β) β (π΄ Yrm ((π + 1) + 1)) < ((2 Β· π΄)β(π + 1))) | ||
Theorem | jm2.24 41692 | Lemma 2.24 of [JonesMatijasevic] p. 697 extended to β€. Could be eliminated with a more careful proof of jm2.26lem3 41730. (Contributed by Stefan O'Rear, 3-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β€) β ((π΄ Yrm (π β 1)) + (π΄ Yrm π)) < (π΄ Xrm π)) | ||
Theorem | rmygeid 41693 | Y(n) increases faster than n. Used implicitly without proof or comment in lemma 2.27 of [JonesMatijasevic] p. 697. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
β’ ((π΄ β (β€β₯β2) β§ π β β0) β π β€ (π΄ Yrm π)) | ||
Theorem | congtr 41694 | A wff of the form π΄ β₯ (π΅ β πΆ) is interpreted as a congruential equation. This is similar to (π΅ mod π΄) = (πΆ mod π΄), but is defined such that behavior is regular for zero and negative values of π΄. To use this concept effectively, we need to show that congruential equations behave similarly to normal equations; first a transitivity law. Idea for the future: If there was a congruential equation symbol, it could incorporate type constraints, so that most of these would not need them. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π· β β€) β§ (π΄ β₯ (π΅ β πΆ) β§ π΄ β₯ (πΆ β π·))) β π΄ β₯ (π΅ β π·)) | ||
Theorem | congadd 41695 | If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π· β β€ β§ πΈ β β€) β§ (π΄ β₯ (π΅ β πΆ) β§ π΄ β₯ (π· β πΈ))) β π΄ β₯ ((π΅ + π·) β (πΆ + πΈ))) | ||
Theorem | congmul 41696 | If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π· β β€ β§ πΈ β β€) β§ (π΄ β₯ (π΅ β πΆ) β§ π΄ β₯ (π· β πΈ))) β π΄ β₯ ((π΅ Β· π·) β (πΆ Β· πΈ))) | ||
Theorem | congsym 41697 | Congruence mod π΄ is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π΄ β₯ (π΅ β πΆ))) β π΄ β₯ (πΆ β π΅)) | ||
Theorem | congneg 41698 | If two integers are congruent mod π΄, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€) β§ (πΆ β β€ β§ π΄ β₯ (π΅ β πΆ))) β π΄ β₯ (-π΅ β -πΆ)) | ||
Theorem | congsub 41699 | If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.) |
β’ (((π΄ β β€ β§ π΅ β β€ β§ πΆ β β€) β§ (π· β β€ β§ πΈ β β€) β§ (π΄ β₯ (π΅ β πΆ) β§ π΄ β₯ (π· β πΈ))) β π΄ β₯ ((π΅ β π·) β (πΆ β πΈ))) | ||
Theorem | congid 41700 | Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.) |
β’ ((π΄ β β€ β§ π΅ β β€) β π΄ β₯ (π΅ β π΅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |