P. 359 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35801-35900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pellfundge 35801	Lower bound on the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> ( ( sqr ` ( D + 1 ) ) + ( sqr ` D ) ) <_ (PellFund ` D ) )
Theorem	pellfundgt1 35802	Weak lower bound on the Pell fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> 1 < (PellFund ` D ) )
Theorem	pellfundlb 35803	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.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ 1 < A ) -> (PellFund ` D ) <_ A )
Theorem	pellfundglb 35804*	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.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. RR /\ (PellFund ` D ) < A ) -> E. x e. (Pell1QR ` D ) ( (PellFund ` D ) <_ x /\ x < A ) )
Theorem	pellfundex 35805	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 35793. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) e. (Pell1QR ` D ) )
Theorem	pellfund14gap 35806	There are no solutions between 1 and the fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ ( 1 <_ A /\ A < (PellFund ` D ) ) ) -> A = 1 )
Theorem	pellfundrp 35807	The fundamental Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) e. RR+ )
Theorem	pellfundne1 35808	The fundamental Pell solution is never 1. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) =/= 1 )
21.23.25  Logarithm laws generalized to an arbitrary base Section should be obsolete because its contents are covered by section "Logarithms to an arbitrary base" now.
Theorem	reglogcl 35809	General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 23789 instead.
|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( ( log ` A ) / ( log ` B ) ) e. RR )
Theorem	reglogltb 35810	General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 23800 instead.
|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A < B <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogleb 35811	General logarithm preserves <_. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 23799 instead.
|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A <_ B <-> ( ( log ` A ) / ( log ` C ) ) <_ ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogmul 35812	Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 23793 instead.
|- ( ( A e. RR+ /\ B e. RR+ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A x. B ) ) / ( log ` C ) ) = ( ( ( log ` A ) / ( log ` C ) ) + ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogexp 35813	Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 23792 instead.
|- ( ( A e. RR+ /\ N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( A ^ N ) ) / ( log ` C ) ) = ( N x. ( ( log ` A ) / ( log ` C ) ) ) )
Theorem	reglogbas 35814	General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 23784 instead.
|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )
Theorem	reglog1 35815	General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 23785 instead.
|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` 1 ) / ( log ` C ) ) = 0 )
Theorem	reglogexpbas 35816	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 23796 instead.
|- ( ( N e. ZZ /\ ( C e. RR+ /\ C =/= 1 ) ) -> ( ( log ` ( C ^ N ) ) / ( log ` C ) ) = N )
21.23.26  Pell equations 4: the positive solution group is infinite cyclic
Theorem	pellfund14 35817*	Every positive Pell solution is a power of the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> E. x e. ZZ A = ( (PellFund ` D ) ^ x ) )
Theorem	pellfund14b 35818*	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.)
|- ( D e. ( NN \ ◻NN ) -> ( A e. (Pell14QR ` D ) <-> E. x e. ZZ A = ( (PellFund ` D ) ^ x ) ) )
21.23.27  X and Y sequences 1: Definition and recurrence laws
Syntax	crmx 35819	Extend class notation to include the Robertson-Matiyasevich X sequence.
class Xrm
Syntax	crmy 35820	Extend class notation to include the Robertson-Matiyasevich Y sequence.
class Yrm
Definition	df-rmx 35821*	Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 35832 and rmxyval 35834 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- Xrm = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )
Definition	df-rmy 35822*	Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 35833 and rmxyval 35834 for a more useful but non-eliminable definition. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- Yrm = ( a e. ( ZZ>= ` 2 ) , n e. ZZ |-> ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( a ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( a + ( sqr ` ( ( a ^ 2 ) - 1 ) ) ) ^ n ) ) ) )
Theorem	rmxfval 35823*	Value of the X sequence. Not used after rmxyval 35834 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm N ) = ( 1st ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) ) )
Theorem	rmyfval 35824*	Value of the Y sequence. Not used after rmxyval 35834 is proved. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm N ) = ( 2nd ` ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) ) )
Theorem	rmspecsqrtnq 35825	The discriminant used to define the X and Y sequences has an irrational square root. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( sqr ` ( ( A ^ 2 ) - 1 ) ) e. ( CC \ QQ ) )
Theorem	rmspecnonsq 35826	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.)
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. ( NN \ ◻NN ) )
Theorem	qirropth 35827	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.)
|- ( ( A e. ( CC \ QQ ) /\ ( B e. QQ /\ C e. QQ ) /\ ( D e. QQ /\ E e. QQ ) ) -> ( ( B + ( A x. C ) ) = ( D + ( A x. E ) ) <-> ( B = D /\ C = E ) ) )
Theorem	rmspecfund 35828	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.)
|- ( A e. ( ZZ>= ` 2 ) -> (PellFund ` ( ( A ^ 2 ) - 1 ) ) = ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) )
Theorem	rmxyelqirr 35829*	The solutions used to construct the X and Y sequences are quadratic irrationals. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) e. { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
Theorem	rmxypairf1o 35830*	The function used to extract rational and irrational parts in df-rmx 35821 and df-rmy 35822 in fact achieves a one-to-one mapping from the quadratic irrationals to pairs of integers. (Contributed by Stefan O'Rear, 21-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) : ( NN0 X. ZZ ) -1-1-onto-> { a | E. c e. NN0 E. d e. ZZ a = ( c + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. d ) ) } )
Theorem	rmxyelxp 35831*	Lemma for frmx 35832 and frmy 35833. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( `' ( b e. ( NN0 X. ZZ ) |-> ( ( 1st ` b ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( 2nd ` b ) ) ) ) ` ( ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) ) e. ( NN0 X. ZZ ) )
Theorem	frmx 35832	The X sequence is a nonnegative integer. See rmxnn 35872 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- Xrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
Theorem	frmy 35833	The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- Yrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
Theorem	rmxyval 35834	Main definition of the X and Y sequences. Compare definition 2.3 of [JonesMatijasevic] p. 694. (Contributed by Stefan O'Rear, 19-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A Xrm N ) + ( ( sqr ` ( ( A ^ 2 ) - 1 ) ) x. ( A Yrm N ) ) ) = ( ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) ^ N ) )
Theorem	rmspecpos 35835	The discriminant used to define the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A ^ 2 ) - 1 ) e. RR+ )
Theorem	rmxycomplete 35836*	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ X e. NN0 /\ Y e. ZZ ) -> ( ( ( X ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( Y ^ 2 ) ) ) = 1 <-> E. n e. ZZ ( X = ( A Xrm n ) /\ Y = ( A Yrm n ) ) ) )
Theorem	rmxynorm 35837	The X and Y sequences define a solution to the corresponding Pell equation. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( ( A Xrm N ) ^ 2 ) - ( ( ( A ^ 2 ) - 1 ) x. ( ( A Yrm N ) ^ 2 ) ) ) = 1 )
Theorem	rmbaserp 35838	The base of exponentiation for the X and Y sequences is a positive real. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A + ( sqr ` ( ( A ^ 2 ) - 1 ) ) ) e. RR+ )
Theorem	rmxyneg 35839	Negation law for X and Y sequences. JonesMatijasevic is inconsistent on whether the X and Y sequences have domain NN0 or ZZ; we use ZZ consistently to avoid the need for a separate subtraction law. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A Xrm -u N ) = ( A Xrm N ) /\ ( A Yrm -u N ) = -u ( A Yrm N ) ) )
Theorem	rmxyadd 35840	Addition formula for X and Y sequences. See rmxadd 35846 and rmyadd 35850 for most uses. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( ( A Xrm ( M + N ) ) = ( ( ( A Xrm M ) x. ( A Xrm N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A Yrm M ) x. ( A Yrm N ) ) ) ) /\ ( A Yrm ( M + N ) ) = ( ( ( A Yrm M ) x. ( A Xrm N ) ) + ( ( A Xrm M ) x. ( A Yrm N ) ) ) ) )
Theorem	rmxy1 35841	Value of the X and Y sequences at 1. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A Xrm 1 ) = A /\ ( A Yrm 1 ) = 1 ) )
Theorem	rmxy0 35842	Value of the X and Y sequences at 0. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( ( A Xrm 0 ) = 1 /\ ( A Yrm 0 ) = 0 ) )
Theorem	rmxneg 35843	Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 35839, rmxyadd 35840, rmxy0 35842, and rmxy1 35841 via qirropth 35827 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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm -u N ) = ( A Xrm N ) )
Theorem	rmx0 35844	Value of X sequence at 0. Part 1 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Xrm 0 ) = 1 )
Theorem	rmx1 35845	Value of X sequence at 1. Part 2 of equation 2.11 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Xrm 1 ) = A )
Theorem	rmxadd 35846	Addition formula for X sequence. Equation 2.7 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A Xrm ( M + N ) ) = ( ( ( A Xrm M ) x. ( A Xrm N ) ) + ( ( ( A ^ 2 ) - 1 ) x. ( ( A Yrm M ) x. ( A Yrm N ) ) ) ) )
Theorem	rmyneg 35847	Negation formula for Y sequence (odd function). (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm -u N ) = -u ( A Yrm N ) )
Theorem	rmy0 35848	Value of Y sequence at 0. Part 1 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Yrm 0 ) = 0 )
Theorem	rmy1 35849	Value of Y sequence at 1. Part 2 of equation 2.12 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( A e. ( ZZ>= ` 2 ) -> ( A Yrm 1 ) = 1 )
Theorem	rmyadd 35850	Addition formula for Y sequence. Equation 2.8 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( A Yrm ( M + N ) ) = ( ( ( A Yrm M ) x. ( A Xrm N ) ) + ( ( A Xrm M ) x. ( A Yrm N ) ) ) )
Theorem	rmxp1 35851	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( N + 1 ) ) = ( ( ( A Xrm N ) x. A ) + ( ( ( A ^ 2 ) - 1 ) x. ( A Yrm N ) ) ) )
Theorem	rmyp1 35852	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N + 1 ) ) = ( ( ( A Yrm N ) x. A ) + ( A Xrm N ) ) )
Theorem	rmxm1 35853	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( N - 1 ) ) = ( ( A x. ( A Xrm N ) ) - ( ( ( A ^ 2 ) - 1 ) x. ( A Yrm N ) ) ) )
Theorem	rmym1 35854	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N - 1 ) ) = ( ( ( A Yrm N ) x. A ) - ( A Xrm N ) ) )
Theorem	rmxluc 35855	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( N + 1 ) ) = ( ( ( 2 x. A ) x. ( A Xrm N ) ) - ( A Xrm ( N - 1 ) ) ) )
Theorem	rmyluc 35856	The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 35848 and rmy1 35849. Part 3 of equation 2.12 of [JonesMatijasevic] p. 695. JonesMatijasevic uses this theorem to redefine the X and Y sequences to have domain ( ZZ X. ZZ ), 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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N + 1 ) ) = ( ( 2 x. ( ( A Yrm N ) x. A ) ) - ( A Yrm ( N - 1 ) ) ) )
Theorem	rmyluc2 35857	Lucas sequence property of Y with better output ordering. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( N + 1 ) ) = ( ( ( 2 x. A ) x. ( A Yrm N ) ) - ( A Yrm ( N - 1 ) ) ) )
Theorem	rmxdbl 35858	"Double-angle formula" for X-values. Equation 2.13 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm ( 2 x. N ) ) = ( ( 2 x. ( ( A Xrm N ) ^ 2 ) ) - 1 ) )
Theorem	rmydbl 35859	"Double-angle formula" for Y-values. Equation 2.14 of [JonesMatijasevic] p. 695. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Yrm ( 2 x. N ) ) = ( ( 2 x. ( A Xrm N ) ) x. ( A Yrm N ) ) )
21.23.28  Ordering and induction lemmas for the integers
Theorem	monotuz 35860*	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.)
|- ( ( ph /\ y e. H ) -> F < G )   &    |- ( ( ph /\ x e. H ) -> C e. RR )   &    |- H = ( ZZ>= ` I )   &    |- ( x = ( y + 1 ) -> C = G )   &    |- ( x = y -> C = F )   &    |- ( x = A -> C = D )   &    |- ( x = B -> C = E )   =>    |- ( ( ph /\ ( A e. H /\ B e. H ) ) -> ( A < B <-> D < E ) )
Theorem	monotoddzzfi 35861*	A function which is odd and monotonic on NN0 is monotonic on ZZ. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.)
|- ( ( ph /\ x e. ZZ ) -> ( F ` x ) e. RR )   &    |- ( ( ph /\ x e. ZZ ) -> ( F ` -u x ) = -u ( F ` x ) )   &    |- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> ( F ` x ) < ( F ` y ) ) )   =>    |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> ( F ` A ) < ( F ` B ) ) )
Theorem	monotoddzz 35862*	A function (given implicitly) which is odd and monotonic on NN0 is monotonic on ZZ. This proof is far too long. (Contributed by Stefan O'Rear, 25-Sep-2014.)
|- ( ( ph /\ x e. NN0 /\ y e. NN0 ) -> ( x < y -> E < F ) )   &    |- ( ( ph /\ x e. ZZ ) -> E e. RR )   &    |- ( ( ph /\ y e. ZZ ) -> G = -u F )   &    |- ( x = A -> E = C )   &    |- ( x = B -> E = D )   &    |- ( x = y -> E = F )   &    |- ( x = -u y -> E = G )   =>    |- ( ( ph /\ A e. ZZ /\ B e. ZZ ) -> ( A < B <-> C < D ) )
Theorem	oddcomabszz 35863*	An odd function which takes nonnegative values on nonnegative arguments commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( ph /\ x e. ZZ ) -> A e. RR )   &    |- ( ( ph /\ x e. ZZ /\ 0 <_ x ) -> 0 <_ A )   &    |- ( ( ph /\ y e. ZZ ) -> C = -u B )   &    |- ( x = y -> A = B )   &    |- ( x = -u y -> A = C )   &    |- ( x = D -> A = E )   &    |- ( x = ( abs ` D ) -> A = F )   =>    |- ( ( ph /\ D e. ZZ ) -> ( abs ` E ) = F )
Theorem	2nn0ind 35864*	Induction on nonnegative integers with two base cases, for use with Lucas-type sequences. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ps   &    |- ch   &    |- ( y e. NN -> ( ( th /\ ta ) -> et ) )   &    |- ( x = 0 -> ( ph <-> ps ) )   &    |- ( x = 1 -> ( ph <-> ch ) )   &    |- ( x = ( y - 1 ) -> ( ph <-> th ) )   &    |- ( x = y -> ( ph <-> ta ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> et ) )   &    |- ( x = A -> ( ph <-> rh ) )   =>    |- ( A e. NN0 -> rh )
Theorem	zindbi 35865*	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.)
|- ( y e. ZZ -> ( ps <-> ch ) )   &    |- ( x = y -> ( ph <-> ps ) )   &    |- ( x = ( y + 1 ) -> ( ph <-> ch ) )   &    |- ( x = 0 -> ( ph <-> th ) )   &    |- ( x = A -> ( ph <-> ta ) )   =>    |- ( A e. ZZ -> ( th <-> ta ) )
Theorem	expmordi 35866	Mantissa ordering relationship for exponentiation. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( 0 <_ A /\ A < B ) /\ N e. NN ) -> ( A ^ N ) < ( B ^ N ) )
Theorem	rpexpmord 35867	Mantissa ordering relationship for exponentiation of positive reals. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( N e. NN /\ A e. RR+ /\ B e. RR+ ) -> ( A < B <-> ( A ^ N ) < ( B ^ N ) ) )
21.23.29  X and Y sequences 2: Order properties
Theorem	rmxypos 35868	For all nonnegative indices, X is positive and Y is nonnegative. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( 0 < ( A Xrm N ) /\ 0 <_ ( A Yrm N ) ) )
Theorem	ltrmynn0 35869	The Y-sequence is strictly monotonic on NN0. Strengthened by ltrmy 35873. (Contributed by Stefan O'Rear, 24-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A Yrm M ) < ( A Yrm N ) ) )
Theorem	ltrmxnn0 35870	The X-sequence is strictly monotonic on NN0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M < N <-> ( A Xrm M ) < ( A Xrm N ) ) )
Theorem	lermxnn0 35871	The X-sequence is monotonic on NN0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. NN0 /\ N e. NN0 ) -> ( M <_ N <-> ( A Xrm M ) <_ ( A Xrm N ) ) )
Theorem	rmxnn 35872	The X-sequence is defined to range over NN0 but never actually takes the value 0. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( A Xrm N ) e. NN )
Theorem	ltrmy 35873	The Y-sequence is strictly monotonic over ZZ. (Contributed by Stefan O'Rear, 25-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M < N <-> ( A Yrm M ) < ( A Yrm N ) ) )
Theorem	rmyeq0 35874	Y is zero only at zero. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( N = 0 <-> ( A Yrm N ) = 0 ) )
Theorem	rmyeq 35875	Y is one-to-one. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M = N <-> ( A Yrm M ) = ( A Yrm N ) ) )
Theorem	lermy 35876	Y is monotonic (non-strict). (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ M e. ZZ /\ N e. ZZ ) -> ( M <_ N <-> ( A Yrm M ) <_ ( A Yrm N ) ) )
Theorem	rmynn 35877	Yrm is positive for positive arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A Yrm N ) e. NN )
Theorem	rmynn0 35878	Yrm is nonnegative for nonnegative arguments. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A Yrm N ) e. NN0 )
Theorem	rmyabs 35879	Yrm commutes with abs. (Contributed by Stefan O'Rear, 26-Sep-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ B e. ZZ ) -> ( abs ` ( A Yrm B ) ) = ( A Yrm ( abs ` B ) ) )
Theorem	jm2.24nn 35880	X(n) is strictly greater than Y(n) + Y(n-1). Lemma 2.24 of [JonesMatijasevic] p. 697 restricted to NN. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) < ( A Xrm N ) )
Theorem	jm2.17a 35881	First half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 14-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( ( ( 2 x. A ) - 1 ) ^ N ) <_ ( A Yrm ( N + 1 ) ) )
Theorem	jm2.17b 35882	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> ( A Yrm ( N + 1 ) ) <_ ( ( 2 x. A ) ^ N ) )
Theorem	jm2.17c 35883	Second half of lemma 2.17 of [JonesMatijasevic] p. 696. (Contributed by Stefan O'Rear, 15-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN ) -> ( A Yrm ( ( N + 1 ) + 1 ) ) < ( ( 2 x. A ) ^ ( N + 1 ) ) )
Theorem	jm2.24 35884	Lemma 2.24 of [JonesMatijasevic] p. 697 extended to ZZ. Could be eliminated with a more careful proof of jm2.26lem3 35927. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. ZZ ) -> ( ( A Yrm ( N - 1 ) ) + ( A Yrm N ) ) < ( A Xrm N ) )
Theorem	rmygeid 35885	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.)
|- ( ( A e. ( ZZ>= ` 2 ) /\ N e. NN0 ) -> N <_ ( A Yrm N ) )
21.23.30  Congruential equations
Theorem	congtr 35886	A wff of the form A || ( B - C ) is interpreted as a congruential equation. This is similar to ( B mod A ) = ( C mod A ), but is defined such that behavior is regular for zero and negative values of A. 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.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( A || ( B - C ) /\ A || ( C - D ) ) ) -> A || ( B - D ) )
Theorem	congadd 35887	If two pairs of numbers are componentwise congruent, so are their sums. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B + D ) - ( C + E ) ) )
Theorem	congmul 35888	If two pairs of numbers are componentwise congruent, so are their products. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B x. D ) - ( C x. E ) ) )
Theorem	congsym 35889	Congruence mod A is a symmetric/commutative relation. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( C - B ) )
Theorem	congneg 35890	If two integers are congruent mod A, so are their negatives. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ A || ( B - C ) ) ) -> A || ( -u B - -u C ) )
Theorem	congsub 35891	If two pairs of numbers are componentwise congruent, so are their differences. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( D e. ZZ /\ E e. ZZ ) /\ ( A || ( B - C ) /\ A || ( D - E ) ) ) -> A || ( ( B - D ) - ( C - E ) ) )
Theorem	congid 35892	Every integer is congruent to itself mod every base. (Contributed by Stefan O'Rear, 1-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> A || ( B - B ) )
Theorem	mzpcong 35893*	Polynomials commute with congruences. (Does this characterize them?) (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( F e. (mzPoly ` V ) /\ ( X e. ( ZZ ^m V ) /\ Y e. ( ZZ ^m V ) ) /\ ( N e. ZZ /\ A. k e. V N || ( ( X ` k ) - ( Y ` k ) ) ) ) -> N || ( ( F ` X ) - ( F ` Y ) ) )
Theorem	congrep 35894*	Every integer is congruent to some number in the fundamental domain. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. NN /\ N e. ZZ ) -> E. a e. ( 0 ... ( A - 1 ) ) A || ( a - N ) )
Theorem	congabseq 35895	If two integers are congruent, they are either equal or separated by at least the congruence base. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( ( A e. NN /\ B e. ZZ /\ C e. ZZ ) /\ A || ( B - C ) ) -> ( ( abs ` ( B - C ) ) < A <-> B = C ) )
21.23.31  Alternating congruential equations
Theorem	acongid 35896	A wff like that in this theorem will be known as an "alternating congruence". A special symbol might be considered if more uses come up. They have many of the same properties as normal congruences, starting with reflexivity. JonesMatijasevic uses "a ≡ ± b (mod c)" for this construction. The disjunction of divisibility constraints seems to adequately capture the concept, but it's rather verbose and somewhat inelegant. Use of an explicit equivalence relation might also work. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ ) -> ( A || ( B - B ) \/ A || ( B - -u B ) ) )
Theorem	acongsym 35897	Symmetry of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( A || ( B - C ) \/ A || ( B - -u C ) ) ) -> ( A || ( C - B ) \/ A || ( C - -u B ) ) )
Theorem	acongneg2 35898	Negate right side of alternating congruence. Makes essential use of the "alternating" part. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ /\ C e. ZZ ) /\ ( A || ( B - -u C ) \/ A || ( B - -u -u C ) ) ) -> ( A || ( B - C ) \/ A || ( B - -u C ) ) )
Theorem	acongtr 35899	Transitivity of alternating congruence. (Contributed by Stefan O'Rear, 2-Oct-2014.)
|- ( ( ( A e. ZZ /\ B e. ZZ ) /\ ( C e. ZZ /\ D e. ZZ ) /\ ( ( A || ( B - C ) \/ A || ( B - -u C ) ) /\ ( A || ( C - D ) \/ A || ( C - -u D ) ) ) ) -> ( A || ( B - D ) \/ A || ( B - -u D ) ) )
Theorem	acongeq12d 35900	Substitution deduction for alternating congruence. (Contributed by Stefan O'Rear, 3-Oct-2014.)
|- ( ph -> B = C )   &    |- ( ph -> D = E )   =>    |- ( ph -> ( ( A || ( B - D ) \/ A || ( B - -u D ) ) <-> ( A || ( C - E ) \/ A || ( C - -u E ) ) ) )