P. 351 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35001-35100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	mzpclall 35001	The set of all functions with the signature of a polynomial is a polynomially closed set. This is a lemma to show that the intersection in df-mzp 34998 is well-defined. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> ( ZZ ^m ( ZZ ^m V ) ) e. (mzPolyCld ` V ) )
Theorem	mzpcln0 35002	Corrolary of mzpclall 35001: polynomially closed function sets are not empty. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPolyCld ` V ) =/= (/) )
Theorem	mzpcl1 35003	Defining property 1 of a polynomially closed function set P: it contains all constant functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. ZZ ) -> ( ( ZZ ^m V ) X. { F } ) e. P )
Theorem	mzpcl2 35004*	Defining property 2 of a polynomially closed function set P: it contains all projections. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` F ) ) e. P )
Theorem	mzpcl34 35005	Defining properties 3 and 4 of a polynomially closed function set P: it is closed under pointwise addition and multiplication. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( P e. (mzPolyCld ` V ) /\ F e. P /\ G e. P ) -> ( ( F oF + G ) e. P /\ ( F oF x. G ) e. P ) )
Theorem	mzpval 35006	Value of the mzPoly function. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPoly ` V ) = |^| (mzPolyCld ` V ) )
Theorem	dmmzp 35007	mzPoly is defined for all index sets which are sets. This is used with elfvdm 5874 to eliminate sethood antecedents. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- dom mzPoly = _V
Theorem	mzpincl 35008	Polynomial closedness is a universal first-order property and passes to intersections. This is where the closure properties of the polynomial ring itself are proved. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( V e. _V -> (mzPoly ` V ) e. (mzPolyCld ` V ) )
Theorem	mzpconst 35009	Constant functions are polynomial. See also mzpconstmpt 35014. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( V e. _V /\ C e. ZZ ) -> ( ( ZZ ^m V ) X. { C } ) e. (mzPoly ` V ) )
Theorem	mzpf 35010	A polynomial function is a function from the coordinate space to the integers. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( F e. (mzPoly ` V ) -> F : ( ZZ ^m V ) --> ZZ )
Theorem	mzpproj 35011*	A projection function is polynomial. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( V e. _V /\ X e. V ) -> ( g e. ( ZZ ^m V ) |-> ( g ` X ) ) e. (mzPoly ` V ) )
Theorem	mzpadd 35012	The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 35015. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. (mzPoly ` V ) /\ B e. (mzPoly ` V ) ) -> ( A oF + B ) e. (mzPoly ` V ) )
Theorem	mzpmul 35013	The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 35016. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( A e. (mzPoly ` V ) /\ B e. (mzPoly ` V ) ) -> ( A oF x. B ) e. (mzPoly ` V ) )
Theorem	mzpconstmpt 35014*	A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 35015, mzpmulmpt 35016, mzpnegmpt 35018, mzpsubmpt 35017, mzpexpmpt 35019) can be used to build proofs that functions which are "manifestly polynomial", in the sense of being a maps-to containing constants, projections, and simple arithmetic operations, are actually polynomial functions. There is no mzpprojmpt because mzpproj 35011 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( V e. _V /\ C e. ZZ ) -> ( x e. ( ZZ ^m V ) |-> C ) e. (mzPoly ` V ) )
Theorem	mzpaddmpt 35015*	Sum of polynomial functions is polynomial. Maps-to version of mzpadd 35012. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A + B ) ) e. (mzPoly ` V ) )
Theorem	mzpmulmpt 35016*	Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 35016. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A x. B ) ) e. (mzPoly ` V ) )
Theorem	mzpsubmpt 35017*	The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ ( x e. ( ZZ ^m V ) |-> B ) e. (mzPoly ` V ) ) -> ( x e. ( ZZ ^m V ) |-> ( A - B ) ) e. (mzPoly ` V ) )
Theorem	mzpnegmpt 35018*	Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.)
|- ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) -> ( x e. ( ZZ ^m V ) |-> -u A ) e. (mzPoly ` V ) )
Theorem	mzpexpmpt 35019*	Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( ( x e. ( ZZ ^m V ) |-> A ) e. (mzPoly ` V ) /\ D e. NN0 ) -> ( x e. ( ZZ ^m V ) |-> ( A ^ D ) ) e. (mzPoly ` V ) )
Theorem	mzpindd 35020*	"Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.)
|- ( ( ph /\ f e. ZZ ) -> ch )   &    |- ( ( ph /\ f e. V ) -> th )   &    |- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> ze )   &    |- ( ( ph /\ ( f : ( ZZ ^m V ) --> ZZ /\ ta ) /\ ( g : ( ZZ ^m V ) --> ZZ /\ et ) ) -> si )   &    |- ( x = ( ( ZZ ^m V ) X. { f } ) -> ( ps <-> ch ) )   &    |- ( x = ( g e. ( ZZ ^m V ) |-> ( g ` f ) ) -> ( ps <-> th ) )   &    |- ( x = f -> ( ps <-> ta ) )   &    |- ( x = g -> ( ps <-> et ) )   &    |- ( x = ( f oF + g ) -> ( ps <-> ze ) )   &    |- ( x = ( f oF x. g ) -> ( ps <-> si ) )   &    |- ( x = A -> ( ps <-> rh ) )   =>    |- ( ( ph /\ A e. (mzPoly ` V ) ) -> rh )
Theorem	mzpmfp 35021	Relationship between multivariate Z-polynomials and general multivariate polynomial functions. (Contributed by Stefan O'Rear, 20-Mar-2015.) (Revised by AV, 13-Jun-2019.)
|- (mzPoly ` I ) = ran ( I eval ℤring )
Theorem	mzpsubst 35022*	Substituting polynomials for the variables of a polynomial results in a polynomial. G is expected to depend on y and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( W e. _V /\ F e. (mzPoly ` V ) /\ A. y e. V G e. (mzPoly ` W ) ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( y e. V |-> ( G ` x ) ) ) ) e. (mzPoly ` W ) )
Theorem	mzprename 35023*	Simplified version of mzpsubst 35022 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.)
|- ( ( W e. _V /\ F e. (mzPoly ` V ) /\ R : V --> W ) -> ( x e. ( ZZ ^m W ) |-> ( F ` ( x o. R ) ) ) e. (mzPoly ` W ) )
Theorem	mzpresrename 35024*	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 35025*	Lemma for mzpcompact2 35026. (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 35026*	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 35027	coeq0 5331 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 35028	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 35029	Extend class notation to include the family of Diophantine sets.
class Dioph
Definition	df-dioph 35030*	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 14689 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 35037. (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 35031*	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 35032*	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 35033*	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 35034*	Lemma for eldioph2 35036. 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 35035*	Lemma for eldioph2 35036. 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 35036*	Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 35026. (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 35037*	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 35047 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 35038	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 35039*	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 35031 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 35040*	Inference version of eldioph3b 35039 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 35041	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 35042	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 35043	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 35044	Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( N e. ZZ -> ( ZZ \ ( ZZ>= ` ( N + 1 ) ) ) ~~ om )
Theorem	elmapresaun 35045	fresaun 5738 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 35046	fresaunres2 5739 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 35047	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 35048	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 35049	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 35050*	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 35051*	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 35052*	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 35053	The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> (/) e. (Dioph ` A ) )
Theorem	vdioph 35054	The "universal" set (as large as possible given eldiophss 35049) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.)
|- ( A e. NN0 -> ( NN0 ^m ( 1 ... A ) ) e. (Dioph ` A ) )
Theorem	anrabdioph 35055*	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 35056*	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 35057*	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 35058*	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 35059*	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 35060*	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 3352 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 35061*	Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6311 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 35062*	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 35063*	Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6311 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 35064*	Exchange a substitution with 4 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 35065*	Exchange a substitution with 4 existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6311 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 35066*	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 35067*	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 35068*	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 35069*	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 35070*	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 35071*	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 35072*	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 35073*	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 35074*	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 35075*	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 35076*	Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 2796. (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 35077*	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 35078*	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 35079*	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 35080*	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 35081*	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 35082*	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 35083*	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 35084*	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 35085*	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 35086*	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 35087*	Forward-only version of eldioph4b 35086. (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 35088*	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 35089*	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 35090*	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 35091*	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 35092*	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 35093	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 35094*	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 35095*	Lemma for rencldnfi 35096. (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 35096*	A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 35095 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 35097	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 35098	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 35099*	Lemma for irrapx1 35105. Divides the unit interval into B half-open sections and using the pigeonhole principle fphpdo 35092 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 35100*	Lemma for irrapx1 35105. 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 ) ) )