P. 354 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35301-35400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mzpresrename 35301*	A polynomial is a polynomial over all larger index sets. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
|- ( ( W e. _V /\ V C_ W /\ F e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x |` V ) ) ) e. (mzPoly ` W ) )
Theorem	mzpcompact2lem 35302*	Lemma for mzpcompact2 35303. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- B e. _V   =>    |- ( A e. (mzPoly ` B ) -> E. a e. Fin E. b e. (mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )
Theorem	mzpcompact2 35303*	Polynomials are finitary objects and can only reference a finite number of variables, even if the index set is infinite. Thus, every polynomial can be expressed as a (uniquely minimal, although we do not prove that) polynomial on a finite number of variables, which is then extended by adding an arbitrary set of ignored variables. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( A e. (mzPoly ` B ) -> E. a e. Fin E. b e. (mzPoly ` a ) ( a C_ B /\ A = ( c e. ( ZZ ^m B ) |-> ( b ` ( c |` a ) ) ) ) )
21.23.9  Miscellanea for Diophantine sets 1
Theorem	coeq0i 35304	coeq0 5364 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- ( ( A : C --> D /\ B : E --> F /\ ( C i^i F ) = (/) ) -> ( A o. B ) = (/) )
Theorem	fzsplit1nn0 35305	Split a finite 1-based set of integers in the middle, allowing either end to be empty ( ( 1 ... 0 )). (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( A e. NN0 /\ B e. NN0 /\ A <_ B ) -> ( 1 ... B ) = ( ( 1 ... A ) u. ( ( A + 1 ) ... B ) ) )
21.23.10  Diophantine sets 1: definitions
Syntax	cdioph 35306	Extend class notation to include the family of Diophantine sets.
class Dioph
Definition	df-dioph 35307*	A Diophantine set is a set of positive integers which is a projection of the zero set of some polynomial. This definition somewhat awkwardly mixes ZZ (via mzPoly) and NN0 (to define the zero sets); the former could be avoided by considering coincidence sets of NN0 polynomials at the cost of requiring two, and the second is driven by consistency with our mu-recursive functions and the requirements of the Davis-Putnam-Robinson-Matiyasevich proof. Both are avoidable at a complexity cost. In particular, it is a consequence of 4sq 14877 that implicitly restricting variables to NN0 adds no expressive power over allowing them to range over ZZ. While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b 35314. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- Dioph = ( n e. NN0 |-> ran ( k e. ( ZZ>= ` n ) , p e. (mzPoly ` ( 1 ... k ) ) |-> { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... n ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldiophb 35308*	Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.)
|- ( D e. (Dioph ` N ) <-> ( N e. NN0 /\ E. k e. ( ZZ>= ` N ) E. p e. (mzPoly ` ( 1 ... k ) ) D = { t | E. u e. ( NN0 ^m ( 1 ... k ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldioph 35309*	Condition for a set to be Diophantine (unpacking existential quantifier) (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( N e. NN0 /\ K e. ( ZZ>= ` N ) /\ P e. (mzPoly ` ( 1 ... K ) ) ) -> { t | E. u e. ( NN0 ^m ( 1 ... K ) ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. (Dioph ` N ) )
Theorem	diophrw 35310*	Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.)
|- ( ( S e. _V /\ M : T -1-1-> S /\ ( M |` O ) = ( _I |` O ) ) -> { a | E. b e. ( NN0 ^m S ) ( a = ( b |` O ) /\ ( ( d e. ( ZZ ^m S ) |-> ( P ` ( d o. M ) ) ) ` b ) = 0 ) } = { a | E. c e. ( NN0 ^m T ) ( a = ( c |` O ) /\ ( P ` c ) = 0 ) } )
Theorem	eldioph2lem1 35311*	Lemma for eldioph2 35313. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( N e. NN0 /\ A e. Fin /\ ( 1 ... N ) C_ A ) -> E. d e. ( ZZ>= ` N ) E. e e. _V ( e : ( 1 ... d ) -1-1-onto-> A /\ ( e |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
Theorem	eldioph2lem2 35312*	Lemma for eldioph2 35313. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( ( N e. NN0 /\ -. S e. Fin ) /\ ( ( 1 ... N ) C_ S /\ A e. ( ZZ>= ` N ) ) ) -> E. c ( c : ( 1 ... A ) -1-1-> S /\ ( c |` ( 1 ... N ) ) = ( _I |` ( 1 ... N ) ) ) )
Theorem	eldioph2 35313*	Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 35303. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.)
|- ( ( N e. NN0 /\ ( S e. _V /\ ( 1 ... N ) C_ S ) /\ P e. (mzPoly ` S ) ) -> { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. (Dioph ` N ) )
Theorem	eldioph2b 35314*	While Diophantine sets were defined to have a finite number of witness variables consequtively following the observable variables, this is not necessary; they can equivalently be taken to use any witness set ( S \ ( 1 ... N ) ). For instance, in diophin 35324 we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014.)
|- ( ( ( N e. NN0 /\ S e. _V ) /\ ( -. S e. Fin /\ ( 1 ... N ) C_ S ) ) -> ( A e. (Dioph ` N ) <-> E. p e. (mzPoly ` S ) A = { t | E. u e. ( NN0 ^m S ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldiophelnn0 35315	Remove antecedent on B from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. (Dioph ` B ) -> B e. NN0 )
Theorem	eldioph3b 35316*	Define Diophantine sets in terms of polynomials with variables indexed by NN. This avoids a quantifier over the number of witness variables and will be easier to use than eldiophb 35308 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. (Dioph ` N ) <-> ( N e. NN0 /\ E. p e. (mzPoly ` NN ) A = { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( p ` u ) = 0 ) } ) )
Theorem	eldioph3 35317*	Inference version of eldioph3b 35316 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ P e. (mzPoly ` NN ) ) -> { t | E. u e. ( NN0 ^m NN ) ( t = ( u |` ( 1 ... N ) ) /\ ( P ` u ) = 0 ) } e. (Dioph ` N ) )
21.23.11  Diophantine sets 2 miscellanea
Theorem	ellz1 35318	Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( B e. ZZ -> ( A e. ( ZZ \ ( ZZ>= ` ( B + 1 ) ) ) <-> ( A e. ZZ /\ A <_ B ) ) )
Theorem	lzunuz 35319	The union of a lower set of integers and an upper set of integers which abut or overlap is all of the integers. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( ( A e. ZZ /\ B e. ZZ /\ B <_ ( A + 1 ) ) -> ( ( ZZ \ ( ZZ>= ` ( A + 1 ) ) ) u. ( ZZ>= ` B ) ) = ZZ )
Theorem	fz1eqin 35320	Express a one-based finite range as the intersection of lower integers with NN. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( N e. NN0 -> ( 1 ... N ) = ( ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) i^i NN ) )
Theorem	lzenom 35321	Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ om )
Theorem	elmapresaun 35322	fresaun 5771 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( F u. G ) e. ( C ^m ( A u. B ) ) )
Theorem	elmapresaunres2 35323	fresaunres2 5772 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.)
|- ( ( F e. ( C ^m A ) /\ G e. ( C ^m B ) /\ ( F |` ( A i^i B ) ) = ( G |` ( A i^i B ) ) ) -> ( ( F u. G ) |` B ) = G )
21.23.12  Diophantine sets 2: union and intersection. Monotone Boolean algebra
Theorem	diophin 35324	If two sets are Diophantine, so is their intersection. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( A e. (Dioph ` N ) /\ B e. (Dioph ` N ) ) -> ( A i^i B ) e. (Dioph ` N ) )
Theorem	diophun 35325	If two sets are Diophantine, so is their union. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( ( A e. (Dioph ` N ) /\ B e. (Dioph ` N ) ) -> ( A u. B ) e. (Dioph ` N ) )
Theorem	eldiophss 35326	Diophantine sets are sets of tuples of nonnegative integers. (Contributed by Stefan O'Rear, 10-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- ( A e. (Dioph ` B ) -> A C_ ( NN0 ^m ( 1 ... B ) ) )
21.23.13  Diophantine sets 3: construction
Theorem	diophrex 35327*	Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ M e. ( ZZ>= ` N ) /\ S e. (Dioph ` M ) ) -> { t | E. u e. S t = ( u |` ( 1 ... N ) ) } e. (Dioph ` N ) )
Theorem	eq0rabdioph 35328*	This is the first of a number of theorems which allow sets to be proven Diophantine by syntactic induction, and models the correspondence between Diophantine sets and monotone existential first-order logic. This first theorem shows that the zero set of an implicit polynomial is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = 0 } e. (Dioph ` N ) )
Theorem	eqrabdioph 35329*	Diophantine set builder for equality of polynomial expressions. Note that the two expressions need not be nonnegative; only variables are so constrained. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A = B } e. (Dioph ` N ) )
Theorem	0dioph 35330	The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> (/) e. (Dioph ` A ) )
Theorem	vdioph 35331	The "universal" set (as large as possible given eldiophss 35326) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> ( NN0 ^m ( 1 ... A ) ) e. (Dioph ` A ) )
Theorem	anrabdioph 35332*	Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps ) } e. (Dioph ` N ) )
Theorem	orrabdioph 35333*	Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps ) } e. (Dioph ` N ) )
Theorem	3anrabdioph 35334*	Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph /\ ps /\ ch ) } e. (Dioph ` N ) )
Theorem	3orrabdioph 35335*	Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( { t e. ( NN0 ^m ( 1 ... N ) ) | ph } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ps } e. (Dioph ` N ) /\ { t e. ( NN0 ^m ( 1 ... N ) ) | ch } e. (Dioph ` N ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | ( ph \/ ps \/ ch ) } e. (Dioph ` N ) )
21.23.14  Diophantine sets 4 miscellanea
Theorem	2sbcrex 35336*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
|- ( [. A / a ]. [. B / b ]. E. c e. C ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )
Theorem	sbcrexgOLD 35337*	Interchange class substitution and restricted existential quantifier. (Contributed by NM, 15-Nov-2005.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) Obsolete as of 18-Aug-2018. Use sbcrex 3381 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> ( [. A / x ]. E. y e. B ph <-> E. y e. B [. A / x ]. ph ) )
Theorem	2sbcrexOLD 35338*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6339 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- A e. _V   &    |- B e. _V   =>    |- ( [. A / a ]. [. B / b ]. E. c e. C ph <-> E. c e. C [. A / a ]. [. B / b ]. ph )
Theorem	sbc2rex 35339*	Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
|- ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph )
Theorem	sbc2rexgOLD 35340*	Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6339 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> ( [. A / a ]. E. b e. B E. c e. C ph <-> E. b e. B E. c e. C [. A / a ]. ph ) )
Theorem	sbc4rex 35341*	Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.)
|- ( [. A / a ]. E. b e. B E. c e. C E. d e. D E. e e. E ph <-> E. b e. B E. c e. C E. d e. D E. e e. E [. A / a ]. ph )
Theorem	sbc4rexgOLD 35342*	Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6339 instead. (New usage is discouraged.) (Proof modification is discouraged.)
|- ( A e. V -> ( [. A / a ]. E. b e. B E. c e. C E. d e. D E. e e. E ph <-> E. b e. B E. c e. C E. d e. D E. e e. E [. A / a ]. ph ) )
Theorem	sbcrot3 35343*	Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- ( [. A / a ]. [. B / b ]. [. C / c ]. ph <-> [. B / b ]. [. C / c ]. [. A / a ]. ph )
Theorem	sbcrot5 35344*	Rotate a sequence of five explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- ( [. A / a ]. [. B / b ]. [. C / c ]. [. D / d ]. [. E / e ]. ph <-> [. B / b ]. [. C / c ]. [. D / d ]. [. E / e ]. [. A / a ]. ph )
Theorem	sbccomieg 35345*	Commute two explicit substitutions, using an implicit substitution to rewrite the exiting substitution. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.)
|- ( a = A -> B = C )   =>    |- ( [. A / a ]. [. B / b ]. ph <-> [. C / b ]. [. A / a ]. ph )
21.23.15  Diophantine sets 4: Quantification
Theorem	rexrabdioph 35346*	Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- M = ( N + 1 )   &    |- ( v = ( t ` M ) -> ( ps <-> ch ) )   &    |- ( u = ( t |` ( 1 ... N ) ) -> ( ch <-> ph ) )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | ph } e. (Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ps } e. (Dioph ` N ) )
Theorem	rexfrabdioph 35347*	Diophantine set builder for existential quantifier, explicit substitution. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- M = ( N + 1 )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... M ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. ph } e. (Dioph ` M ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 ph } e. (Dioph ` N ) )
Theorem	2rexfrabdioph 35348*	Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- M = ( N + 1 )   &    |- L = ( M + 1 )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... L ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. ph } e. (Dioph ` L ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 ph } e. (Dioph ` N ) )
Theorem	3rexfrabdioph 35349*	Diophantine set builder for existential quantifier, explicit substitution, two variables. (Contributed by Stefan O'Rear, 17-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- M = ( N + 1 )   &    |- L = ( M + 1 )   &    |- K = ( L + 1 )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... K ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. ph } e. (Dioph ` K ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 ph } e. (Dioph ` N ) )
Theorem	4rexfrabdioph 35350*	Diophantine set builder for existential quantifier, explicit substitution, four variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- M = ( N + 1 )   &    |- L = ( M + 1 )   &    |- K = ( L + 1 )   &    |- J = ( K + 1 )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... J ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. ph } e. (Dioph ` J ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 E. y e. NN0 ph } e. (Dioph ` N ) )
Theorem	6rexfrabdioph 35351*	Diophantine set builder for existential quantifier, explicit substitution, six variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- M = ( N + 1 )   &    |- L = ( M + 1 )   &    |- K = ( L + 1 )   &    |- J = ( K + 1 )   &    |- I = ( J + 1 )   &    |- H = ( I + 1 )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... H ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. ph } e. (Dioph ` H ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 ph } e. (Dioph ` N ) )
Theorem	7rexfrabdioph 35352*	Diophantine set builder for existential quantifier, explicit substitution, seven variables. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.)
|- M = ( N + 1 )   &    |- L = ( M + 1 )   &    |- K = ( L + 1 )   &    |- J = ( K + 1 )   &    |- I = ( J + 1 )   &    |- H = ( I + 1 )   &    |- G = ( H + 1 )   =>    |- ( ( N e. NN0 /\ { t e. ( NN0 ^m ( 1 ... G ) ) | [. ( t |` ( 1 ... N ) ) / u ]. [. ( t ` M ) / v ]. [. ( t ` L ) / w ]. [. ( t ` K ) / x ]. [. ( t ` J ) / y ]. [. ( t ` I ) / z ]. [. ( t ` H ) / p ]. [. ( t ` G ) / q ]. ph } e. (Dioph ` G ) ) -> { u e. ( NN0 ^m ( 1 ... N ) ) | E. v e. NN0 E. w e. NN0 E. x e. NN0 E. y e. NN0 E. z e. NN0 E. p e. NN0 E. q e. NN0 ph } e. (Dioph ` N ) )
21.23.16  Diophantine sets 5: Arithmetic sets
Theorem	rabdiophlem1 35353*	Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 2825. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) -> A. t e. ( NN0 ^m ( 1 ... N ) ) A e. ZZ )
Theorem	rabdiophlem2 35354*	Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- M = ( N + 1 )   =>    |- ( ( N e. NN0 /\ ( u e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) ) -> ( t e. ( ZZ ^m ( 1 ... M ) ) |-> [_ ( t |` ( 1 ... N ) ) / u ]_ A ) e. (mzPoly ` ( 1 ... M ) ) )
Theorem	elnn0rabdioph 35355*	Diophantine set builder for nonnegativity constraints. The first builder which uses a witness variable internally; an expression is nonnegative if there is a nonnegative integer equal to it. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN0 } e. (Dioph ` N ) )
Theorem	rexzrexnn0 35356*	Rewrite a quantification over integers into a quantification over naturals. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( x = y -> ( ph <-> ps ) )   &    |- ( x = -u y -> ( ph <-> ch ) )   =>    |- ( E. x e. ZZ ph <-> E. y e. NN0 ( ps \/ ch ) )
Theorem	lerabdioph 35357*	Diophantine set builder for the less or equals relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A <_ B } e. (Dioph ` N ) )
Theorem	eluzrabdioph 35358*	Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ M e. ZZ /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. ( ZZ>= ` M ) } e. (Dioph ` N ) )
Theorem	elnnrabdioph 35359*	Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A e. NN } e. (Dioph ` N ) )
Theorem	ltrabdioph 35360*	Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A < B } e. (Dioph ` N ) )
Theorem	nerabdioph 35361*	Diophantine set builder for inequality. This not quite trivial theorem touches on something important; Diophantine sets are not closed under negation, but they contain an important subclass that is, namely the recursive sets. With this theorem and De Morgan's laws, all quantifier-free formulae can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A =/= B } e. (Dioph ` N ) )
Theorem	dvdsrabdioph 35362*	Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( N e. NN0 /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> A ) e. (mzPoly ` ( 1 ... N ) ) /\ ( t e. ( ZZ ^m ( 1 ... N ) ) |-> B ) e. (mzPoly ` ( 1 ... N ) ) ) -> { t e. ( NN0 ^m ( 1 ... N ) ) | A || B } e. (Dioph ` N ) )
21.23.17  Diophantine sets 6: reusability. renumbering of variables
Theorem	eldioph4b 35363*	Membership in Dioph expressed using a quantified union to add witness variables instead of a restriction to remove them. (Contributed by Stefan O'Rear, 16-Oct-2014.)
|- W e. _V   &    |- -. W e. Fin   &    |- ( W i^i NN ) = (/)   =>    |- ( S e. (Dioph ` N ) <-> ( N e. NN0 /\ E. p e. (mzPoly ` ( W u. ( 1 ... N ) ) ) S = { t e. ( NN0 ^m ( 1 ... N ) ) | E. w e. ( NN0 ^m W ) ( p ` ( t u. w ) ) = 0 } ) )
Theorem	eldioph4i 35364*	Forward-only version of eldioph4b 35363. (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 35365*	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 35366*	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 35367*	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 35368*	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 35369*	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 35370	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 35371*	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 35372*	Lemma for rencldnfi 35373. (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 35373*	A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 35372 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	icodiamlt 35374	Two elements in a half-open interval have separation strictly less than the difference between the endpoints. (Contributed by Stefan O'Rear, 12-Sep-2014.)
|- ( ( ( A e. RR /\ B e. RR ) /\ ( C e. ( A [,) B ) /\ D e. ( A [,) B ) ) ) -> ( abs ` ( C - D ) ) < ( B - A ) )
Theorem	modelico 35375	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 35376*	Lemma for irrapx1 35382. Divides the unit interval into B half-open sections and using the pigeonhole principle fphpdo 35369 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 35377*	Lemma for irrapx1 35382. 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 35378*	Lemma for irrapx1 35382. 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 35379*	Lemma for irrapx1 35382. 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 35380*	Lemma for irrapx1 35382. 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 35381*	Lemma for irrapx1 35382. 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 35382*	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 35383	Lemma for pellex 35389. 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 35384	Lemma for pellex 35389. 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 35385*	Lemma for pellex 35389. 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 35386*	Lemma for pellex 35389. Invoking irrapx1 35382, 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 35387*	Lemma for pellex 35389. Invoking fiphp3d 35371, 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 35388*	Lemma for pellex 35389. 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 35389*	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 35390	Extend class notation to include the set of square positive integers.
class ◻NN
Syntax	cpell1qr 35391	Extend class notation to include the class of quadrant-1 Pell solutions.
class Pell1QR
Syntax	cpell1234qr 35392	Extend class notation to include the class of any-quadrant Pell solutions.
class Pell1234QR
Syntax	cpell14qr 35393	Extend class notation to include the class of positive Pell solutions.
class Pell14QR
Syntax	cpellfund 35394	Extend class notation to include the Pell-equation fundamental solution function.
class PellFund
Definition	df-squarenn 35395	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 35396*	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 35397*	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 35398*	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 35399*	A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.)
|- PellFund = ( x e. ( NN \ ◻NN ) |-> sup ( { z e. (Pell14QR ` x ) | 1 < z } , RR , `' < ) )
Theorem	pell1qrval 35400*	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 ) } )