P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	elpell1qr 35401*	Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> ( A e. (Pell1QR ` D ) <-> ( A e. RR /\ E. z e. NN0 E. w e. NN0 ( A = ( z + ( ( sqr ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) ) )
Theorem	pell14qrval 35402*	Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (Pell14QR ` D ) = { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqr ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )
Theorem	elpell14qr 35403*	Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> ( A e. (Pell14QR ` D ) <-> ( A e. RR /\ E. z e. NN0 E. w e. ZZ ( A = ( z + ( ( sqr ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) ) )
Theorem	pell1234qrval 35404*	Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (Pell1234QR ` D ) = { y e. RR | E. z e. ZZ E. w e. ZZ ( y = ( z + ( ( sqr ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )
Theorem	elpell1234qr 35405*	Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> ( A e. (Pell1234QR ` D ) <-> ( A e. RR /\ E. z e. ZZ E. w e. ZZ ( A = ( z + ( ( sqr ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) ) ) )
Theorem	pell1234qrre 35406	General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1234QR ` D ) ) -> A e. RR )
Theorem	pell1234qrne0 35407	No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1234QR ` D ) ) -> A =/= 0 )
Theorem	pell1234qrreccl 35408	General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1234QR ` D ) ) -> ( 1 / A ) e. (Pell1234QR ` D ) )
Theorem	pell1234qrmulcl 35409	General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1234QR ` D ) /\ B e. (Pell1234QR ` D ) ) -> ( A x. B ) e. (Pell1234QR ` D ) )
Theorem	pell14qrss1234 35410	A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (Pell14QR ` D ) C_ (Pell1234QR ` D ) )
Theorem	pell14qrre 35411	A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> A e. RR )
Theorem	pell14qrne0 35412	A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> A =/= 0 )
Theorem	pell14qrgt0 35413	A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> 0 < A )
Theorem	pell14qrrp 35414	A positive Pell solution is a positive real. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> A e. RR+ )
Theorem	pell1234qrdich 35415	A general Pell solution is either a positive solution, or its negation is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1234QR ` D ) ) -> ( A e. (Pell14QR ` D ) \/ -u A e. (Pell14QR ` D ) ) )
Theorem	elpell14qr2 35416	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.)
|- ( D e. ( NN \ ◻NN ) -> ( A e. (Pell14QR ` D ) <-> ( A e. (Pell1234QR ` D ) /\ 0 < A ) ) )
Theorem	pell14qrmulcl 35417	Positive Pell solutions are closed under multiplication. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ B e. (Pell14QR ` D ) ) -> ( A x. B ) e. (Pell14QR ` D ) )
Theorem	pell14qrreccl 35418	Positive Pell solutions are closed under reciprocal. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> ( 1 / A ) e. (Pell14QR ` D ) )
Theorem	pell14qrdivcl 35419	Positive Pell solutions are closed under division. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ B e. (Pell14QR ` D ) ) -> ( A / B ) e. (Pell14QR ` D ) )
Theorem	pell14qrexpclnn0 35420	Lemma for pell14qrexpcl 35421. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ B e. NN0 ) -> ( A ^ B ) e. (Pell14QR ` D ) )
Theorem	pell14qrexpcl 35421	Positive Pell solutions are closed under integer powers. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ B e. ZZ ) -> ( A ^ B ) e. (Pell14QR ` D ) )
Theorem	pell1qrss14 35422	First-quadrant Pell solutions are a subset of the positive solutions. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (Pell1QR ` D ) C_ (Pell14QR ` D ) )
Theorem	pell14qrdich 35423	A positive Pell solution is either in the first quadrant, or its reciprocal is. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) ) -> ( A e. (Pell1QR ` D ) \/ ( 1 / A ) e. (Pell1QR ` D ) ) )
Theorem	pell1qrge1 35424	A Pell solution in the first quadrant is at least 1. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1QR ` D ) ) -> 1 <_ A )
Theorem	pell1qr1 35425	1 is a Pell solution and in the first quadrant as one. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> 1 e. (Pell1QR ` D ) )
Theorem	elpell1qr2 35426	The first quadrant solutions are precisely the positive Pell solutions which are at least one. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> ( A e. (Pell1QR ` D ) <-> ( A e. (Pell14QR ` D ) /\ 1 <_ A ) ) )
Theorem	pell1qrgaplem 35427	Lemma for pell1qrgap 35428. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( ( D e. NN /\ ( A e. NN0 /\ B e. NN0 ) ) /\ ( 1 < ( A + ( ( sqr ` D ) x. B ) ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) ) -> ( ( sqr ` ( D + 1 ) ) + ( sqr ` D ) ) <_ ( A + ( ( sqr ` D ) x. B ) ) )
Theorem	pell1qrgap 35428	First-quadrant Pell solutions are bounded away from 1. (This particular bound allows us to prove exact values for the fundamental solution later.) (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell1QR ` D ) /\ 1 < A ) -> ( ( sqr ` ( D + 1 ) ) + ( sqr ` D ) ) <_ A )
Theorem	pell14qrgap 35429	Positive Pell solutions are bounded away from 1. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ 1 < A ) -> ( ( sqr ` ( D + 1 ) ) + ( sqr ` D ) ) <_ A )
Theorem	pell14qrgapw 35430	Positive Pell solutions are bounded away from 1, with a friendlier bound. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ 1 < A ) -> 2 < A )
Theorem	pellqrexplicit 35431	Condition for a calculated real to be a Pell solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( ( D e. ( NN \ ◻NN ) /\ A e. NN0 /\ B e. NN0 ) /\ ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = 1 ) -> ( A + ( ( sqr ` D ) x. B ) ) e. (Pell1QR ` D ) )
21.23.24  Pell equations 3: characterizing fundamental solution
Theorem	infmrgelbi 35432*	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.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> B <_ sup ( A , RR , `' < ) )
Theorem	pellqrex 35433*	There is a nontrivial solution of a Pell equation in the first quadrant. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> E. x e. (Pell1QR ` D ) 1 < x )
Theorem	pellfundval 35434*	Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) = sup ( { x e. (Pell14QR ` D ) | 1 < x } , RR , `' < ) )
Theorem	pellfundre 35435	The fundamental solution of a Pell equation exists as a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) e. RR )
Theorem	pellfundge 35436	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 35437	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 35438	A nontrivial first quadrant solution is at least as large as the fundamental solution. (Contributed by Stefan O'Rear, 19-Sep-2014.)
|- ( ( D e. ( NN \ ◻NN ) /\ A e. (Pell14QR ` D ) /\ 1 < A ) -> (PellFund ` D ) <_ A )
Theorem	pellfundglb 35439*	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 35440	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 35430. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) e. (Pell1QR ` D ) )
Theorem	pellfund14gap 35441	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 35442	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 35443	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 35444	General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 23575 instead.
|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( ( log ` A ) / ( log ` B ) ) e. RR )
Theorem	reglogltb 35445	General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 23586 instead.
|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A < B <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogleb 35446	General logarithm preserves <_. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 23585 instead.
|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A <_ B <-> ( ( log ` A ) / ( log ` C ) ) <_ ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogmul 35447	Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 23579 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 35448	Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 23578 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 35449	General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 23570 instead.
|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )
Theorem	reglog1 35450	General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 23571 instead.
|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` 1 ) / ( log ` C ) ) = 0 )
Theorem	reglogexpbas 35451	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 23582 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 35452*	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 35453*	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 35454	Extend class notation to include the Robertson-Matiyasevich X sequence.
class Xrm
Syntax	crmy 35455	Extend class notation to include the Robertson-Matiyasevich Y sequence.
class Yrm
Definition	df-rmx 35456*	Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 35467 and rmxyval 35469 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 35457*	Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 35468 and rmxyval 35469 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 35458*	Value of the X sequence. Not used after rmxyval 35469 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 35459*	Value of the Y sequence. Not used after rmxyval 35469 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 35460	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 35461	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 35462	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 35463	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 35464*	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 35465*	The function used to extract rational and irrational parts in df-rmx 35456 and df-rmy 35457 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 35466*	Lemma for frmx 35467 and frmy 35468. (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 35467	The X sequence is a nonnegative integer. See rmxnn 35507 for a strengthening. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- Xrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> NN0
Theorem	frmy 35468	The Y sequence is an integer. (Contributed by Stefan O'Rear, 22-Sep-2014.)
|- Yrm : ( ( ZZ>= ` 2 ) X. ZZ ) --> ZZ
Theorem	rmxyval 35469	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 35470	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 35471*	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 35472	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 35473	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 35474	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 35475	Addition formula for X and Y sequences. See rmxadd 35481 and rmyadd 35485 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 35476	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 35477	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 35478	Negation law (even function) for the X sequence. The method of proof used for the previous four theorems rmxyneg 35474, rmxyadd 35475, rmxy0 35477, and rmxy1 35476 via qirropth 35462 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 35479	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 35480	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 35481	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 35482	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 35483	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 35484	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 35485	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 35486	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 35487	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 35488	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 35489	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 35490	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 35491	The Y sequence is a Lucas sequence, definable via this second-order recurrence with rmy0 35483 and rmy1 35484. 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 35492	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 35493	"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 35494	"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 35495*	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 35496*	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 35497*	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 35498*	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 35499*	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 35500*	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 ) )