Home | Metamath
Proof Explorer Theorem List (p. 374 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | mzpadd 37301 | The pointwise sum of two polynomial functions is a polynomial function. See also mzpaddmpt 37304. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
mzPoly mzPoly mzPoly | ||
Theorem | mzpmul 37302 | The pointwise product of two polynomial functions is a polynomial function. See also mzpmulmpt 37305. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
mzPoly mzPoly mzPoly | ||
Theorem | mzpconstmpt 37303* | A constant function expressed in maps-to notation is polynomial. This theorem and the several that follow (mzpaddmpt 37304, mzpmulmpt 37305, mzpnegmpt 37307, mzpsubmpt 37306, mzpexpmpt 37308) 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 37300 is already expressed using maps-to notation. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly | ||
Theorem | mzpaddmpt 37304* | Sum of polynomial functions is polynomial. Maps-to version of mzpadd 37301. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly mzPoly mzPoly | ||
Theorem | mzpmulmpt 37305* | Product of polynomial functions is polynomial. Maps-to version of mzpmulmpt 37305. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly mzPoly mzPoly | ||
Theorem | mzpsubmpt 37306* | The difference of two polynomial functions is polynomial. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
mzPoly mzPoly mzPoly | ||
Theorem | mzpnegmpt 37307* | Negation of a polynomial function. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
mzPoly mzPoly | ||
Theorem | mzpexpmpt 37308* | Raise a polynomial function to a (fixed) exponent. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly mzPoly | ||
Theorem | mzpindd 37309* | "Structural" induction to prove properties of all polynomial functions. (Contributed by Stefan O'Rear, 4-Oct-2014.) |
mzPoly | ||
Theorem | mzpmfp 37310 | 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 eval ℤring | ||
Theorem | mzpsubst 37311* | Substituting polynomials for the variables of a polynomial results in a polynomial. is expected to depend on and provide the polynomials which are being substituted. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly mzPoly mzPoly | ||
Theorem | mzprename 37312* | Simplified version of mzpsubst 37311 to simply relabel variables in a polynomial. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly mzPoly | ||
Theorem | mzpresrename 37313* | 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.) |
mzPoly mzPoly | ||
Theorem | mzpcompact2lem 37314* | Lemma for mzpcompact2 37315. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
mzPoly mzPoly | ||
Theorem | mzpcompact2 37315* | 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.) |
mzPoly mzPoly | ||
Theorem | coeq0i 37316 | coeq0 5644 but without explicitly introducing domain and range symbols. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
Theorem | fzsplit1nn0 37317 | Split a finite 1-based set of integers in the middle, allowing either end to be empty (). (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Syntax | cdioph 37318 | Extend class notation to include the family of Diophantine sets. |
Dioph | ||
Definition | df-dioph 37319* | 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 (via mzPoly) and (to define the zero sets); the former could be avoided by considering coincidence sets of 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 15668 that implicitly restricting variables to adds no expressive power over allowing them to range over . While this definition stipulates a specific index set for the polynomials, there is actually flexibility here, see eldioph2b 37326. (Contributed by Stefan O'Rear, 5-Oct-2014.) |
Dioph mzPoly | ||
Theorem | eldiophb 37320* | Initial expression of Diophantine property of a set. (Contributed by Stefan O'Rear, 5-Oct-2014.) (Revised by Mario Carneiro, 22-Sep-2015.) |
Dioph mzPoly | ||
Theorem | eldioph 37321* | Condition for a set to be Diophantine (unpacking existential quantifier). (Contributed by Stefan O'Rear, 5-Oct-2014.) |
mzPoly Dioph | ||
Theorem | diophrw 37322* | Renaming and adding unused witness variables does not change the Diophantine set coded by a polynomial. (Contributed by Stefan O'Rear, 7-Oct-2014.) |
Theorem | eldioph2lem1 37323* | Lemma for eldioph2 37325. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Theorem | eldioph2lem2 37324* | Lemma for eldioph2 37325. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Theorem | eldioph2 37325* | Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 37315. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.) |
mzPoly Dioph | ||
Theorem | eldioph2b 37326* | 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 . For instance, in diophin 37336 we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
Dioph mzPoly | ||
Theorem | eldiophelnn0 37327 | Remove antecedent on from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph | ||
Theorem | eldioph3b 37328* | Define Diophantine sets in terms of polynomials with variables indexed by . This avoids a quantifier over the number of witness variables and will be easier to use than eldiophb 37320 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph mzPoly | ||
Theorem | eldioph3 37329* | Inference version of eldioph3b 37328 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
mzPoly Dioph | ||
Theorem | ellz1 37330 | Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
Theorem | lzunuz 37331 | 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.) |
Theorem | fz1eqin 37332 | Express a one-based finite range as the intersection of lower integers with . (Contributed by Stefan O'Rear, 9-Oct-2014.) |
Theorem | lzenom 37333 | Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Theorem | elmapresaun 37334 | fresaun 6075 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
Theorem | elmapresaunres2 37335 | fresaunres2 6076 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
Theorem | diophin 37336 | 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.) |
Dioph Dioph Dioph | ||
Theorem | diophun 37337 | 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.) |
Dioph Dioph Dioph | ||
Theorem | eldiophss 37338 | 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.) |
Dioph | ||
Theorem | diophrex 37339* | Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph Dioph | ||
Theorem | eq0rabdioph 37340* | 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.) |
mzPoly Dioph | ||
Theorem | eqrabdioph 37341* | 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.) |
mzPoly mzPoly Dioph | ||
Theorem | 0dioph 37342 | The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph | ||
Theorem | vdioph 37343 | The "universal" set (as large as possible given eldiophss 37338) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph | ||
Theorem | anrabdioph 37344* | Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph Dioph Dioph | ||
Theorem | orrabdioph 37345* | Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph Dioph Dioph | ||
Theorem | 3anrabdioph 37346* | Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph Dioph Dioph Dioph | ||
Theorem | 3orrabdioph 37347* | Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph Dioph Dioph Dioph | ||
Theorem | 2sbcrex 37348* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
Theorem | sbcrexgOLD 37349* | 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 3514 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | 2sbcrexOLD 37350* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6687 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | sbc2rex 37351* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
Theorem | sbc2rexgOLD 37352* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6687 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | sbc4rex 37353* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
Theorem | sbc4rexgOLD 37354* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 6687 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | sbcrot3 37355* | Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
Theorem | sbcrot5 37356* | Rotate a sequence of five explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
Theorem | sbccomieg 37357* | 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.) |
Theorem | rexrabdioph 37358* | Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
Dioph Dioph | ||
Theorem | rexfrabdioph 37359* | Diophantine set builder for existential quantifier, explicit substitution. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
Dioph Dioph | ||
Theorem | 2rexfrabdioph 37360* | 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.) |
Dioph Dioph | ||
Theorem | 3rexfrabdioph 37361* | 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.) |
Dioph Dioph | ||
Theorem | 4rexfrabdioph 37362* | 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.) |
Dioph Dioph | ||
Theorem | 6rexfrabdioph 37363* | 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.) |
Dioph Dioph | ||
Theorem | 7rexfrabdioph 37364* | 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.) |
Dioph Dioph | ||
Theorem | rabdiophlem1 37365* | Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 2952. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
mzPoly | ||
Theorem | rabdiophlem2 37366* | Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
mzPoly mzPoly | ||
Theorem | elnn0rabdioph 37367* | 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.) |
mzPoly Dioph | ||
Theorem | rexzrexnn0 37368* | Rewrite a quantification over integers into a quantification over naturals. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
Theorem | lerabdioph 37369* | Diophantine set builder for the less or equals relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
mzPoly mzPoly Dioph | ||
Theorem | eluzrabdioph 37370* | Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
mzPoly Dioph | ||
Theorem | elnnrabdioph 37371* | Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
mzPoly Dioph | ||
Theorem | ltrabdioph 37372* | Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
mzPoly mzPoly Dioph | ||
Theorem | nerabdioph 37373* | 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.) |
mzPoly mzPoly Dioph | ||
Theorem | dvdsrabdioph 37374* | Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
mzPoly mzPoly Dioph | ||
Theorem | eldioph4b 37375* | 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.) |
Dioph mzPoly | ||
Theorem | eldioph4i 37376* | Forward-only version of eldioph4b 37375. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
mzPoly Dioph | ||
Theorem | diophren 37377* | 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.) |
Dioph Dioph | ||
Theorem | rabrenfdioph 37378* | Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
Dioph Dioph | ||
Theorem | rabren3dioph 37379* | Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
Dioph Dioph | ||
Theorem | fphpd 37380* | 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.) |
Theorem | fphpdo 37381* | Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
Theorem | ctbnfien 37382 | 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.) |
Theorem | fiphp3d 37383* | Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
Theorem | rencldnfilem 37384* | Lemma for rencldnfi 37385. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
Theorem | rencldnfi 37385* | A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 37384 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
Theorem | irrapxlem1 37386* | Lemma for irrapx1 37392. Divides the unit interval into half-open sections and using the pigeonhole principle fphpdo 37381 finds two multiples of in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
Theorem | irrapxlem2 37387* | Lemma for irrapx1 37392. Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
Theorem | irrapxlem3 37388* | Lemma for irrapx1 37392. By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
Theorem | irrapxlem4 37389* | Lemma for irrapx1 37392. Eliminate ranges, use positivity of the input to force positivity of the output by increasing as needed. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
Theorem | irrapxlem5 37390* | Lemma for irrapx1 37392. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom | ||
Theorem | irrapxlem6 37391* | Lemma for irrapx1 37392. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
denom | ||
Theorem | irrapx1 37392* | 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.) |
denom | ||
Theorem | pellexlem1 37393 | Lemma for pellex 37399. 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.) |
Theorem | pellexlem2 37394 | Lemma for pellex 37399. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
Theorem | pellexlem3 37395* | Lemma for pellex 37399. To each good rational approximation of , there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
denom | ||
Theorem | pellexlem4 37396* | Lemma for pellex 37399. Invoking irrapx1 37392, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
Theorem | pellexlem5 37397* | Lemma for pellex 37399. Invoking fiphp3d 37383, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
Theorem | pellexlem6 37398* | Lemma for pellex 37399. 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.) |
Theorem | pellex 37399* | Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
Syntax | csquarenn 37400 | Extend class notation to include the set of square positive integers. |
◻NN |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |