P. 357 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35601-35700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	diophrw 35601*	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 35602*	Lemma for eldioph2 35604. 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 35603*	Lemma for eldioph2 35604. 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 35604*	Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 35594. (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 35605*	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 35615 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 35606	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 35607*	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 35599 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 35608*	Inference version of eldioph3b 35607 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 35609	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 35610	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 35611	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 35612	Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ om )
Theorem	elmapresaun 35613	fresaun 5754 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 35614	fresaunres2 5755 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 35615	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 35616	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 35617	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 35618*	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 35619*	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 35620*	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 35621	The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> (/) e. (Dioph ` A ) )
Theorem	vdioph 35622	The "universal" set (as large as possible given eldiophss 35617) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> ( NN0 ^m ( 1 ... A ) ) e. (Dioph ` A ) )
Theorem	anrabdioph 35623*	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 35624*	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 35625*	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 35626*	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 35627*	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 35628*	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 3343 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 35629*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6324 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 35630*	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 35631*	Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6324 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 35632*	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 35633*	Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6324 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 35634*	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 35635*	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 35636*	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 35637*	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 35638*	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 35639*	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 35640*	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 35641*	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 35642*	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 35643*	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 35644*	Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 2781. (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 35645*	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 35646*	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 35647*	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 35648*	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 35649*	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 35650*	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 35651*	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 35652*	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 35653*	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 35654*	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 35655*	Forward-only version of eldioph4b 35654. (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 35656*	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 35657*	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 35658*	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 35659*	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 35660*	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 35661	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 35662*	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 35663*	Lemma for rencldnfi 35664. (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 35664*	A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 35663 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 35665	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 35666*	Lemma for irrapx1 35672. Divides the unit interval into B half-open sections and using the pigeonhole principle fphpdo 35660 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 35667*	Lemma for irrapx1 35672. 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 35668*	Lemma for irrapx1 35672. 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 35669*	Lemma for irrapx1 35672. 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 35670*	Lemma for irrapx1 35672. 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 35671*	Lemma for irrapx1 35672. 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 35672*	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 35673	Lemma for pellex 35679. 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 35674	Lemma for pellex 35679. 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 35675*	Lemma for pellex 35679. 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 35676*	Lemma for pellex 35679. Invoking irrapx1 35672, 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 35677*	Lemma for pellex 35679. Invoking fiphp3d 35662, 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 35678*	Lemma for pellex 35679. 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 35679*	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 35680	Extend class notation to include the set of square positive integers.
class ◻NN
Syntax	cpell1qr 35681	Extend class notation to include the class of quadrant-1 Pell solutions.
class Pell1QR
Syntax	cpell1234qr 35682	Extend class notation to include the class of any-quadrant Pell solutions.
class Pell1234QR
Syntax	cpell14qr 35683	Extend class notation to include the class of positive Pell solutions.
class Pell14QR
Syntax	cpellfund 35684	Extend class notation to include the Pell-equation fundamental solution function.
class PellFund
Syntax	cpellfundold 35685	Extend class notation to include the Pell-equation fundamental solution function (old version).
class PellFund
Definition	df-squarenn 35686	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 35687*	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 35688*	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 35689*	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 35690*	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 35691*	A function mapping Pell discriminants to the corresponding fundamental solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) Obsolete version of df-pellfund 35690 as of 17-Sep-2020. (New usage is discouraged.)
|- PellFund = ( x e. ( NN \ ◻NN ) |-> sup ( { z e. (Pell14QR ` x ) | 1 < z } , RR , `' < ) )
Theorem	pell1qrval 35692*	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 35693*	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 35694*	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 35695*	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 35696*	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 35697*	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 35698	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 35699	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 35700	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 ) )