P. 358 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35701-35800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	eldioph4i 35701*	Forward-only version of eldioph4b 35700. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- W e. _V   &    |- -. W e. Fin   &    |- ( W i^i NN ) = (/)   =>    |- ( ( N e. NN0 /\ P e. (mzPoly ` ( W u. ( 1 ... N ) ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( P ` ( t u. w ) ) = 0 } e. (Dioph ` N ) )
Theorem	diophren 35702*	Change variables in a Diophantine set, using class notation. This allows already proved Diophantine sets to be reused in contexts with more variables. (Contributed by Stefan O'Rear, 16-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
|- ( ( S e. (Dioph ` N ) /\ M e. NN0 /\ F : ( 1 ... N ) --> ( 1 ... M ) ) -> { a e. ( NN0 ^m ( 1 ... M ) ) | ( a o. F ) e. S } e. (Dioph ` M ) )
Theorem	rabrenfdioph 35703*	Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- ( ( B e. NN0 /\ F : ( 1 ... A ) --> ( 1 ... B ) /\ { a e. ( NN0 ^m ( 1 ... A ) ) | ph } e. (Dioph ` A ) ) -> { b e. ( NN0 ^m ( 1 ... B ) ) | [. ( b o. F ) / a ]. ph } e. (Dioph ` B ) )
Theorem	rabren3dioph 35704*	Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014.)
|- ( ( ( a ` 1 ) = ( b ` X ) /\ ( a ` 2 ) = ( b ` Y ) /\ ( a ` 3 ) = ( b ` Z ) ) -> ( ph <-> ps ) )   &    |- X e. ( 1 ... N )   &    |- Y e. ( 1 ... N )   &    |- Z e. ( 1 ... N )   =>    |- ( ( N e. NN0 /\ { a e. ( NN0 ^m ( 1 ... 3 ) ) | ph } e. (Dioph ` 3 ) ) -> { b e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) )
21.23.18  Pigeonhole Principle and cardinality helpers
Theorem	fphpd 35705*	Pigeonhole principle expressed with implicit substitution. If the range is smaller than the domain, two inputs must be mapped to the same output. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ph -> B ~< A )   &    |- ( ( ph /\ x e. A ) -> C e. B )   &    |- ( x = y -> C = D )   =>    |- ( ph -> E. x e. A E. y e. A ( x =/= y /\ C = D ) )
Theorem	fphpdo 35706*	Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ph -> A C_ RR )   &    |- ( ph -> B e. _V )   &    |- ( ph -> B ~< A )   &    |- ( ( ph /\ z e. A ) -> C e. B )   &    |- ( z = x -> C = D )   &    |- ( z = y -> C = E )   =>    |- ( ph -> E. x e. A E. y e. A ( x < y /\ D = E ) )
Theorem	ctbnfien 35707	An infinite subset of a countable set is countable, without using choice. (Contributed by Stefan O'Rear, 19-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( ( X ~~ om /\ Y ~~ om ) /\ ( A C_ X /\ -. A e. Fin ) ) -> A ~~ Y )
Theorem	fiphp3d 35708*	Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.)
|- ( ph -> A ~~ NN )   &    |- ( ph -> B e. Fin )   &    |- ( ( ph /\ x e. A ) -> D e. B )   =>    |- ( ph -> E. y e. B { x e. A | D = y } ~~ NN )
21.23.19  A non-closed set of reals is infinite
Theorem	rencldnfilem 35709*	Lemma for rencldnfi 35710. (Contributed by Stefan O'Rear, 18-Oct-2014.)
|- ( ( ( A C_ RR /\ B e. RR /\ ( A =/= (/) /\ -. B e. A ) ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> -. A e. Fin )
Theorem	rencldnfi 35710*	A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 35709 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.)
|- ( ( ( A C_ RR /\ B e. RR /\ -. B e. A ) /\ A. x e. RR+ E. y e. A ( abs ` ( y - B ) ) < x ) -> -. A e. Fin )
21.23.20  Miscellanea for Lagrange's theorem
Theorem	modelico 35711	Modular reduction produces a half-open interval. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( A e. RR /\ B e. RR+ ) -> ( A mod B ) e. ( 0 [,) B ) )
21.23.21  Lagrange's rational approximation theorem
Theorem	irrapxlem1 35712*	Lemma for irrapx1 35718. Divides the unit interval into B half-open sections and using the pigeonhole principle fphpdo 35706 finds two multiples of A in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( A e. RR+ /\ B e. NN ) -> E. x e. ( 0 ... B ) E. y e. ( 0 ... B ) ( x < y /\ ( |_ ` ( B x. ( ( A x. x ) mod 1 ) ) ) = ( |_ ` ( B x. ( ( A x. y ) mod 1 ) ) ) ) )
Theorem	irrapxlem2 35713*	Lemma for irrapx1 35718. Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( A e. RR+ /\ B e. NN ) -> E. x e. ( 0 ... B ) E. y e. ( 0 ... B ) ( x < y /\ ( abs ` ( ( ( A x. x ) mod 1 ) - ( ( A x. y ) mod 1 ) ) ) < ( 1 / B ) ) )
Theorem	irrapxlem3 35714*	Lemma for irrapx1 35718. By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. RR+ /\ B e. NN ) -> E. x e. ( 1 ... B ) E. y e. NN0 ( abs ` ( ( A x. x ) - y ) ) < ( 1 / B ) )
Theorem	irrapxlem4 35715*	Lemma for irrapx1 35718. Eliminate ranges, use positivity of the input to force positivity of the output by increasing B as needed. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. RR+ /\ B e. NN ) -> E. x e. NN E. y e. NN ( abs ` ( ( A x. x ) - y ) ) < ( 1 / if ( x <_ B , B , x ) ) )
Theorem	irrapxlem5 35716*	Lemma for irrapx1 35718. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> E. x e. QQ ( 0 < x /\ ( abs ` ( x - A ) ) < B /\ ( abs ` ( x - A ) ) < ( (denom ` x ) ^ -u 2 ) ) )
Theorem	irrapxlem6 35717*	Lemma for irrapx1 35718. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.)
|- ( ( A e. RR+ /\ B e. RR+ ) -> E. x e. { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( (denom ` y ) ^ -u 2 ) ) } ( abs ` ( x - A ) ) < B )
Theorem	irrapx1 35718*	Dirichlet's approximation theorem. Every positive irrational number has infinitely many rational approximations which are closer than the inverse squares of their reduced denominators. Lemma 61 in [vandenDries] p. 42. (Contributed by Stefan O'Rear, 14-Sep-2014.)
|- ( A e. ( RR+ \ QQ ) -> { y e. QQ | ( 0 < y /\ ( abs ` ( y - A ) ) < ( (denom ` y ) ^ -u 2 ) ) } ~~ NN )
21.23.22  Pell equations 1: A nontrivial solution always exists
Theorem	pellexlem1 35719	Lemma for pellex 35725. Arithmetical core of pellexlem3, norm lower bound. This begins Dirichlet's proof of the Pell equation solution existence; the proof here follows theorem 62 of [vandenDries] p. 43. (Contributed by Stefan O'Rear, 14-Sep-2014.)
|- ( ( ( D e. NN /\ A e. NN /\ B e. NN ) /\ -. ( sqr ` D ) e. QQ ) -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) =/= 0 )
Theorem	pellexlem2 35720	Lemma for pellex 35725. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.)
|- ( ( ( D e. NN /\ A e. NN /\ B e. NN ) /\ ( abs ` ( ( A / B ) - ( sqr ` D ) ) ) < ( B ^ -u 2 ) ) -> ( abs ` ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqr ` D ) ) ) )
Theorem	pellexlem3 35721*	Lemma for pellex 35725. To each good rational approximation of ( sqr ` D ), there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.)
|- ( ( D e. NN /\ -. ( sqr ` D ) e. QQ ) -> { x e. QQ | ( 0 < x /\ ( abs ` ( x - ( sqr ` D ) ) ) < ( (denom ` x ) ^ -u 2 ) ) } ~<_ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) =/= 0 /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqr ` D ) ) ) ) ) } )
Theorem	pellexlem4 35722*	Lemma for pellex 35725. Invoking irrapx1 35718, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.)
|- ( ( D e. NN /\ -. ( sqr ` D ) e. QQ ) -> { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) =/= 0 /\ ( abs ` ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) ) < ( 1 + ( 2 x. ( sqr ` D ) ) ) ) ) } ~~ NN )
Theorem	pellexlem5 35723*	Lemma for pellex 35725. Invoking fiphp3d 35708, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.)
|- ( ( D e. NN /\ -. ( sqr ` D ) e. QQ ) -> E. x e. ZZ ( x =/= 0 /\ { <. y , z >. | ( ( y e. NN /\ z e. NN ) /\ ( ( y ^ 2 ) - ( D x. ( z ^ 2 ) ) ) = x ) } ~~ NN ) )
Theorem	pellexlem6 35724*	Lemma for pellex 35725. Doing a field division between near solutions get us to norm 1, and the modularity constraint ensures we still have an integer. Returning NN guarantees that we are not returning the trivial solution (1,0). We are not explicitly defining the Pell-field, Pell-ring, and Pell-norm explicitly because after this construction is done we will never use them. This is mostly basic algebraic number theory and could be simplified if a generic framework for that were in place. (Contributed by Stefan O'Rear, 19-Oct-2014.)
|- ( ph -> A e. NN )   &    |- ( ph -> B e. NN )   &    |- ( ph -> C e. ZZ )   &    |- ( ph -> D e. NN )   &    |- ( ph -> -. ( sqr ` D ) e. QQ )   &    |- ( ph -> E e. NN )   &    |- ( ph -> F e. NN )   &    |- ( ph -> -. ( A = E /\ B = F ) )   &    |- ( ph -> C =/= 0 )   &    |- ( ph -> ( ( A ^ 2 ) - ( D x. ( B ^ 2 ) ) ) = C )   &    |- ( ph -> ( ( E ^ 2 ) - ( D x. ( F ^ 2 ) ) ) = C )   &    |- ( ph -> ( A mod ( abs ` C ) ) = ( E mod ( abs ` C ) ) )   &    |- ( ph -> ( B mod ( abs ` C ) ) = ( F mod ( abs ` C ) ) )   =>    |- ( ph -> E. a e. NN E. b e. NN ( ( a ^ 2 ) - ( D x. ( b ^ 2 ) ) ) = 1 )
Theorem	pellex 35725*	Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.)
|- ( ( D e. NN /\ -. ( sqr ` D ) e. QQ ) -> E. x e. NN E. y e. NN ( ( x ^ 2 ) - ( D x. ( y ^ 2 ) ) ) = 1 )
21.23.23  Pell equations 2: Algebraic number theory of the solution set
Syntax	csquarenn 35726	Extend class notation to include the set of square positive integers.
class ◻NN
Syntax	cpell1qr 35727	Extend class notation to include the class of quadrant-1 Pell solutions.
class Pell1QR
Syntax	cpell1234qr 35728	Extend class notation to include the class of any-quadrant Pell solutions.
class Pell1234QR
Syntax	cpell14qr 35729	Extend class notation to include the class of positive Pell solutions.
class Pell14QR
Syntax	cpellfund 35730	Extend class notation to include the Pell-equation fundamental solution function.
class PellFund
Syntax	cpellfundold 35731	Extend class notation to include the Pell-equation fundamental solution function (old version).
class PellFund
Definition	df-squarenn 35732	Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ◻NN = { x e. NN | ( sqr ` x ) e. QQ }
Definition	df-pell1qr 35733*	Define the solutions of a Pell equation in the first quadrant. To avoid pair pain, we represent this via the canonical embedding into the reals. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- Pell1QR = ( x e. ( NN \ ◻NN ) |-> { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
Definition	df-pell14qr 35734*	Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- Pell14QR = ( x e. ( NN \ ◻NN ) |-> { y e. RR | E. z e. NN0 E. w e. ZZ ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
Definition	df-pell1234qr 35735*	Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- Pell1234QR = ( x e. ( NN \ ◻NN ) |-> { y e. RR | E. z e. ZZ E. w e. ZZ ( y = ( z + ( ( sqr ` x ) x. w ) ) /\ ( ( z ^ 2 ) - ( x x. ( w ^ 2 ) ) ) = 1 ) } )
Definition	df-pellfund 35736*	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 = ( x e. ( NN \ ◻NN ) |-> inf ( { z e. (Pell14QR ` x ) | 1 < z } , RR , < ) )
Definition	df-pellfundOLD 35737*	A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) Obsolete version of df-pellfund 35736 as of 17-Sep-2020. (New usage is discouraged.)
|- PellFund = ( x e. ( NN \ ◻NN ) |-> sup ( { z e. (Pell14QR ` x ) | 1 < z } , RR , `' < ) )
Theorem	pell1qrval 35738*	Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (Pell1QR ` D ) = { y e. RR | E. z e. NN0 E. w e. NN0 ( y = ( z + ( ( sqr ` D ) x. w ) ) /\ ( ( z ^ 2 ) - ( D x. ( w ^ 2 ) ) ) = 1 ) } )
Theorem	elpell1qr 35739*	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 35740*	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 35741*	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 35742*	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 35743*	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 35744	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 35745	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 35746	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 35747	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 35748	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 35749	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 35750	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 35751	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 35752	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 35753	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 35754	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 35755	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 35756	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 35757	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 35758	Lemma for pell14qrexpcl 35759. (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 35759	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 35760	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 35761	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 35762	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 35763	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 35764	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 35765	Lemma for pell1qrgap 35766. (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 35766	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 35767	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 35768	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 35769	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 35770*	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.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> B <_ inf ( A , RR , < ) )
Theorem	infmrgelbiOLD 35771*	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.) Obsolete version of infmrgelbi 35770 as of 17-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.)
|- ( ( ( A C_ RR /\ A =/= (/) /\ B e. RR ) /\ A. x e. A B <_ x ) -> B <_ sup ( A , RR , `' < ) )
Theorem	pellqrex 35772*	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 35773*	Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) (Revised by AV, 17-Sep-2020.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) = inf ( { x e. (Pell14QR ` D ) | 1 < x } , RR , < ) )
Theorem	pellfundvalOLD 35774*	Value of the fundamental solution of a Pell equation. (Contributed by Stefan O'Rear, 18-Sep-2014.) Obsolete version of pellfundval 35773 as of 17-Sep-2020. ( (New usage is discouraged.) (Proof modification is discouraged.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) = sup ( { x e. (Pell14QR ` D ) | 1 < x } , RR , `' < ) )
Theorem	pellfundre 35775	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 35776	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 35777	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 35778	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 35779*	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 35780	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 35768. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- ( D e. ( NN \ ◻NN ) -> (PellFund ` D ) e. (Pell1QR ` D ) )
Theorem	pellfund14gap 35781	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 35782	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 35783	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 35784	General logarithm is a real number. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbcl 23766 instead.
|- ( ( A e. RR+ /\ B e. RR+ /\ B =/= 1 ) -> ( ( log ` A ) / ( log ` B ) ) e. RR )
Theorem	reglogltb 35785	General logarithm preserves "less than". (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logblt 23777 instead.
|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A < B <-> ( ( log ` A ) / ( log ` C ) ) < ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogleb 35786	General logarithm preserves <_. (Contributed by Stefan O'Rear, 19-Oct-2014.) (New usage is discouraged.) Use logbleb 23776 instead.
|- ( ( ( A e. RR+ /\ B e. RR+ ) /\ ( C e. RR+ /\ 1 < C ) ) -> ( A <_ B <-> ( ( log ` A ) / ( log ` C ) ) <_ ( ( log ` B ) / ( log ` C ) ) ) )
Theorem	reglogmul 35787	Multiplication law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbmul 23770 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 35788	Power law for general log. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use relogbzexp 23769 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 35789	General log of the base is 1. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logbid1 23761 instead.
|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` C ) / ( log ` C ) ) = 1 )
Theorem	reglog1 35790	General log of 1 is 0. (Contributed by Stefan O'Rear, 19-Sep-2014.) (New usage is discouraged.) Use logb1 23762 instead.
|- ( ( C e. RR+ /\ C =/= 1 ) -> ( ( log ` 1 ) / ( log ` C ) ) = 0 )
Theorem	reglogexpbas 35791	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 23773 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 35792*	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 35793*	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 35794	Extend class notation to include the Robertson-Matiyasevich X sequence.
class Xrm
Syntax	crmy 35795	Extend class notation to include the Robertson-Matiyasevich Y sequence.
class Yrm
Definition	df-rmx 35796*	Define the X sequence as the rational part of some solution of a special Pell equation. See frmx 35807 and rmxyval 35809 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 35797*	Define the X sequence as the irrational part of some solution of a special Pell equation. See frmy 35808 and rmxyval 35809 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 35798*	Value of the X sequence. Not used after rmxyval 35809 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 35799*	Value of the Y sequence. Not used after rmxyval 35809 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 35800	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 ) )