![]() |
Metamath
Proof Explorer Theorem List (p. 419 of 480) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eldioph2lem1 41801* | Lemma for eldioph2 41803. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ ((π β β0 β§ π΄ β Fin β§ (1...π) β π΄) β βπ β (β€β₯βπ)βπ β V (π:(1...π)β1-1-ontoβπ΄ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) | ||
Theorem | eldioph2lem2 41802* | Lemma for eldioph2 41803. Construct necessary renaming function for one direction. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ (((π β β0 β§ Β¬ π β Fin) β§ ((1...π) β π β§ π΄ β (β€β₯βπ))) β βπ(π:(1...π΄)β1-1βπ β§ (π βΎ (1...π)) = ( I βΎ (1...π)))) | ||
Theorem | eldioph2 41803* | Construct a Diophantine set from a polynomial with witness variables drawn from any set whatsoever, via mzpcompact2 41793. (Contributed by Stefan O'Rear, 8-Oct-2014.) (Revised by Stefan O'Rear, 5-Jun-2015.) |
β’ ((π β β0 β§ (π β V β§ (1...π) β π) β§ π β (mzPolyβπ)) β {π‘ β£ βπ’ β (β0 βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) | ||
Theorem | eldioph2b 41804* | 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 (π β (1...π)). For instance, in diophin 41813 we use this to take the two input sets to have disjoint witness sets. (Contributed by Stefan O'Rear, 8-Oct-2014.) |
β’ (((π β β0 β§ π β V) β§ (Β¬ π β Fin β§ (1...π) β π)) β (π΄ β (Diophβπ) β βπ β (mzPolyβπ)π΄ = {π‘ β£ βπ’ β (β0 βm π)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) | ||
Theorem | eldiophelnn0 41805 | Remove antecedent on π΅ from Diophantine set constructors. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π΄ β (Diophβπ΅) β π΅ β β0) | ||
Theorem | eldioph3b 41806* | 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 41798 in most cases. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π΄ β (Diophβπ) β (π β β0 β§ βπ β (mzPolyββ)π΄ = {π‘ β£ βπ’ β (β0 βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)})) | ||
Theorem | eldioph3 41807* | Inference version of eldioph3b 41806 with quantifier expanded. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ ((π β β0 β§ π β (mzPolyββ)) β {π‘ β£ βπ’ β (β0 βm β)(π‘ = (π’ βΎ (1...π)) β§ (πβπ’) = 0)} β (Diophβπ)) | ||
Theorem | ellz1 41808 | Membership in a lower set of integers. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
β’ (π΅ β β€ β (π΄ β (β€ β (β€β₯β(π΅ + 1))) β (π΄ β β€ β§ π΄ β€ π΅))) | ||
Theorem | lzunuz 41809 | 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.) |
β’ ((π΄ β β€ β§ π΅ β β€ β§ π΅ β€ (π΄ + 1)) β ((β€ β (β€β₯β(π΄ + 1))) βͺ (β€β₯βπ΅)) = β€) | ||
Theorem | fz1eqin 41810 | Express a one-based finite range as the intersection of lower integers with β. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
β’ (π β β0 β (1...π) = ((β€ β (β€β₯β(π + 1))) β© β)) | ||
Theorem | lzenom 41811 | Lower integers are countably infinite. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π β β€ β (β€ β (β€β₯β(π + 1))) β Ο) | ||
Theorem | elmapresaunres2 41812 | fresaunres2 6763 transposed to mappings. (Contributed by Stefan O'Rear, 9-Oct-2014.) |
β’ ((πΉ β (πΆ βm π΄) β§ πΊ β (πΆ βm π΅) β§ (πΉ βΎ (π΄ β© π΅)) = (πΊ βΎ (π΄ β© π΅))) β ((πΉ βͺ πΊ) βΎ π΅) = πΊ) | ||
Theorem | diophin 41813 | 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 41814 | 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 41815 | 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βπ΅) β π΄ β (β0 βm (1...π΅))) | ||
Theorem | diophrex 41816* | Projecting a Diophantine set by removing a coordinate results in a Diophantine set. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ ((π β β0 β§ π β (β€β₯βπ) β§ π β (Diophβπ)) β {π‘ β£ βπ’ β π π‘ = (π’ βΎ (1...π))} β (Diophβπ)) | ||
Theorem | eq0rabdioph 41817* | 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.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ = 0} β (Diophβπ)) | ||
Theorem | eqrabdioph 41818* | 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.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π)) β§ (π‘ β (β€ βm (1...π)) β¦ π΅) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ = π΅} β (Diophβπ)) | ||
Theorem | 0dioph 41819 | The null set is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π΄ β β0 β β β (Diophβπ΄)) | ||
Theorem | vdioph 41820 | The "universal" set (as large as possible given eldiophss 41815) is Diophantine. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (π΄ β β0 β (β0 βm (1...π΄)) β (Diophβπ΄)) | ||
Theorem | anrabdioph 41821* | Diophantine set builder for conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (({π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ) β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ)) β {π‘ β (β0 βm (1...π)) β£ (π β§ π)} β (Diophβπ)) | ||
Theorem | orrabdioph 41822* | Diophantine set builder for disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (({π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ) β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ)) β {π‘ β (β0 βm (1...π)) β£ (π β¨ π)} β (Diophβπ)) | ||
Theorem | 3anrabdioph 41823* | Diophantine set builder for ternary conjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (({π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ) β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ) β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ)) β {π‘ β (β0 βm (1...π)) β£ (π β§ π β§ π)} β (Diophβπ)) | ||
Theorem | 3orrabdioph 41824* | Diophantine set builder for ternary disjunctions. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ (({π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ) β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ) β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ)) β {π‘ β (β0 βm (1...π)) β£ (π β¨ π β¨ π)} β (Diophβπ)) | ||
Theorem | 2sbcrex 41825* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
β’ ([π΄ / π][π΅ / π]βπ β πΆ π β βπ β πΆ [π΄ / π][π΅ / π]π) | ||
Theorem | sbcrexgOLD 41826* | 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 3869 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β π β ([π΄ / π₯]βπ¦ β π΅ π β βπ¦ β π΅ [π΄ / π₯]π)) | ||
Theorem | 2sbcrexOLD 41827* | Exchange an existential quantifier with two substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 7454 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π΄ β V & β’ π΅ β V β β’ ([π΄ / π][π΅ / π]βπ β πΆ π β βπ β πΆ [π΄ / π][π΅ / π]π) | ||
Theorem | sbc2rex 41828* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
β’ ([π΄ / π]βπ β π΅ βπ β πΆ π β βπ β π΅ βπ β πΆ [π΄ / π]π) | ||
Theorem | sbc2rexgOLD 41829* | Exchange a substitution with two existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 7454 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β π β ([π΄ / π]βπ β π΅ βπ β πΆ π β βπ β π΅ βπ β πΆ [π΄ / π]π)) | ||
Theorem | sbc4rex 41830* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by NM, 24-Aug-2018.) |
β’ ([π΄ / π]βπ β π΅ βπ β πΆ βπ β π· βπ β πΈ π β βπ β π΅ βπ β πΆ βπ β π· βπ β πΈ [π΄ / π]π) | ||
Theorem | sbc4rexgOLD 41831* | Exchange a substitution with four existentials. (Contributed by Stefan O'Rear, 11-Oct-2014.) Obsolete as of 24-Aug-2018. Use csbov123 7454 instead. (New usage is discouraged.) (Proof modification is discouraged.) |
β’ (π΄ β π β ([π΄ / π]βπ β π΅ βπ β πΆ βπ β π· βπ β πΈ π β βπ β π΅ βπ β πΆ βπ β π· βπ β πΈ [π΄ / π]π)) | ||
Theorem | sbcrot3 41832* | Rotate a sequence of three explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ ([π΄ / π][π΅ / π][πΆ / π]π β [π΅ / π][πΆ / π][π΄ / π]π) | ||
Theorem | sbcrot5 41833* | Rotate a sequence of five explicit substitutions. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Mario Carneiro, 11-Dec-2016.) |
β’ ([π΄ / π][π΅ / π][πΆ / π][π· / π][πΈ / π]π β [π΅ / π][πΆ / π][π· / π][πΈ / π][π΄ / π]π) | ||
Theorem | sbccomieg 41834* | 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 41835* | Diophantine set builder for existential quantification. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ π = (π + 1) & β’ (π£ = (π‘βπ) β (π β π)) & β’ (π’ = (π‘ βΎ (1...π)) β (π β π)) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...π)) β£ π} β (Diophβπ)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 π} β (Diophβπ)) | ||
Theorem | rexfrabdioph 41836* | Diophantine set builder for existential quantifier, explicit substitution. (Contributed by Stefan O'Rear, 11-Oct-2014.) (Revised by Stefan O'Rear, 6-May-2015.) |
β’ π = (π + 1) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...π)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£]π} β (Diophβπ)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 π} β (Diophβπ)) | ||
Theorem | 2rexfrabdioph 41837* | 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.) |
β’ π = (π + 1) & β’ πΏ = (π + 1) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...πΏ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€]π} β (DiophβπΏ)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 βπ€ β β0 π} β (Diophβπ)) | ||
Theorem | 3rexfrabdioph 41838* | 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.) |
β’ π = (π + 1) & β’ πΏ = (π + 1) & β’ πΎ = (πΏ + 1) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...πΎ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯]π} β (DiophβπΎ)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 βπ€ β β0 βπ₯ β β0 π} β (Diophβπ)) | ||
Theorem | 4rexfrabdioph 41839* | 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.) |
β’ π = (π + 1) & β’ πΏ = (π + 1) & β’ πΎ = (πΏ + 1) & β’ π½ = (πΎ + 1) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...π½)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦]π} β (Diophβπ½)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 βπ€ β β0 βπ₯ β β0 βπ¦ β β0 π} β (Diophβπ)) | ||
Theorem | 6rexfrabdioph 41840* | 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.) |
β’ π = (π + 1) & β’ πΏ = (π + 1) & β’ πΎ = (πΏ + 1) & β’ π½ = (πΎ + 1) & β’ πΌ = (π½ + 1) & β’ π» = (πΌ + 1) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...π»)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π]π} β (Diophβπ»)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 βπ€ β β0 βπ₯ β β0 βπ¦ β β0 βπ§ β β0 βπ β β0 π} β (Diophβπ)) | ||
Theorem | 7rexfrabdioph 41841* | 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.) |
β’ π = (π + 1) & β’ πΏ = (π + 1) & β’ πΎ = (πΏ + 1) & β’ π½ = (πΎ + 1) & β’ πΌ = (π½ + 1) & β’ π» = (πΌ + 1) & β’ πΊ = (π» + 1) β β’ ((π β β0 β§ {π‘ β (β0 βm (1...πΊ)) β£ [(π‘ βΎ (1...π)) / π’][(π‘βπ) / π£][(π‘βπΏ) / π€][(π‘βπΎ) / π₯][(π‘βπ½) / π¦][(π‘βπΌ) / π§][(π‘βπ») / π][(π‘βπΊ) / π]π} β (DiophβπΊ)) β {π’ β (β0 βm (1...π)) β£ βπ£ β β0 βπ€ β β0 βπ₯ β β0 βπ¦ β β0 βπ§ β β0 βπ β β0 βπ β β0 π} β (Diophβπ)) | ||
Theorem | rabdiophlem1 41842* | Lemma for arithmetic diophantine sets. Convert polynomial-ness of an expression into a constraint suitable for ralimi 3082. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ ((π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π)) β βπ‘ β (β0 βm (1...π))π΄ β β€) | ||
Theorem | rabdiophlem2 41843* | Lemma for arithmetic diophantine sets. Reuse a polynomial expression under a new quantifier. (Contributed by Stefan O'Rear, 10-Oct-2014.) |
β’ π = (π + 1) β β’ ((π β β0 β§ (π’ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π))) β (π‘ β (β€ βm (1...π)) β¦ β¦(π‘ βΎ (1...π)) / π’β¦π΄) β (mzPolyβ(1...π))) | ||
Theorem | elnn0rabdioph 41844* | 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.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ β β0} β (Diophβπ)) | ||
Theorem | rexzrexnn0 41845* | Rewrite an existential quantification restricted to integers into an existential quantification restricted to naturals. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ (π₯ = π¦ β (π β π)) & β’ (π₯ = -π¦ β (π β π)) β β’ (βπ₯ β β€ π β βπ¦ β β0 (π β¨ π)) | ||
Theorem | lerabdioph 41846* | Diophantine set builder for the "less than or equal to" relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π)) β§ (π‘ β (β€ βm (1...π)) β¦ π΅) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ β€ π΅} β (Diophβπ)) | ||
Theorem | eluzrabdioph 41847* | Diophantine set builder for membership in a fixed upper set of integers. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π β β0 β§ π β β€ β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ β (β€β₯βπ)} β (Diophβπ)) | ||
Theorem | elnnrabdioph 41848* | Diophantine set builder for positivity. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ β β} β (Diophβπ)) | ||
Theorem | ltrabdioph 41849* | Diophantine set builder for the strict less than relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π)) β§ (π‘ β (β€ βm (1...π)) β¦ π΅) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ < π΅} β (Diophβπ)) | ||
Theorem | nerabdioph 41850* | 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 formulas can be negated. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π)) β§ (π‘ β (β€ βm (1...π)) β¦ π΅) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ β π΅} β (Diophβπ)) | ||
Theorem | dvdsrabdioph 41851* | Divisibility is a Diophantine relation. (Contributed by Stefan O'Rear, 11-Oct-2014.) |
β’ ((π β β0 β§ (π‘ β (β€ βm (1...π)) β¦ π΄) β (mzPolyβ(1...π)) β§ (π‘ β (β€ βm (1...π)) β¦ π΅) β (mzPolyβ(1...π))) β {π‘ β (β0 βm (1...π)) β£ π΄ β₯ π΅} β (Diophβπ)) | ||
Theorem | eldioph4b 41852* | 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.) |
β’ π β V & β’ Β¬ π β Fin & β’ (π β© β) = β β β’ (π β (Diophβπ) β (π β β0 β§ βπ β (mzPolyβ(π βͺ (1...π)))π = {π‘ β (β0 βm (1...π)) β£ βπ€ β (β0 βm π)(πβ(π‘ βͺ π€)) = 0})) | ||
Theorem | eldioph4i 41853* | Forward-only version of eldioph4b 41852. (Contributed by Stefan O'Rear, 16-Oct-2014.) |
β’ π β V & β’ Β¬ π β Fin & β’ (π β© β) = β β β’ ((π β β0 β§ π β (mzPolyβ(π βͺ (1...π)))) β {π‘ β (β0 βm (1...π)) β£ βπ€ β (β0 βm π)(πβ(π‘ βͺ π€)) = 0} β (Diophβπ)) | ||
Theorem | diophren 41854* | 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βπ) β§ π β β0 β§ πΉ:(1...π)βΆ(1...π)) β {π β (β0 βm (1...π)) β£ (π β πΉ) β π} β (Diophβπ)) | ||
Theorem | rabrenfdioph 41855* | Change variable numbers in a Diophantine class abstraction using explicit substitution. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ ((π΅ β β0 β§ πΉ:(1...π΄)βΆ(1...π΅) β§ {π β (β0 βm (1...π΄)) β£ π} β (Diophβπ΄)) β {π β (β0 βm (1...π΅)) β£ [(π β πΉ) / π]π} β (Diophβπ΅)) | ||
Theorem | rabren3dioph 41856* | Change variable numbers in a 3-variable Diophantine class abstraction. (Contributed by Stefan O'Rear, 17-Oct-2014.) |
β’ (((πβ1) = (πβπ) β§ (πβ2) = (πβπ) β§ (πβ3) = (πβπ)) β (π β π)) & β’ π β (1...π) & β’ π β (1...π) & β’ π β (1...π) β β’ ((π β β0 β§ {π β (β0 βm (1...3)) β£ π} β (Diophβ3)) β {π β (β0 βm (1...π)) β£ π} β (Diophβπ)) | ||
Theorem | fphpd 41857* | 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 41858* | Pigeonhole principle for sets of real numbers with implicit output reordering. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β V) & β’ (π β π΅ βΊ π΄) & β’ ((π β§ π§ β π΄) β πΆ β π΅) & β’ (π§ = π₯ β πΆ = π·) & β’ (π§ = π¦ β πΆ = πΈ) β β’ (π β βπ₯ β π΄ βπ¦ β π΄ (π₯ < π¦ β§ π· = πΈ)) | ||
Theorem | ctbnfien 41859 | 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.) |
β’ (((π β Ο β§ π β Ο) β§ (π΄ β π β§ Β¬ π΄ β Fin)) β π΄ β π) | ||
Theorem | fiphp3d 41860* | Infinite pigeonhole principle for partitioning an infinite set between finitely many buckets. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
β’ (π β π΄ β β) & β’ (π β π΅ β Fin) & β’ ((π β§ π₯ β π΄) β π· β π΅) β β’ (π β βπ¦ β π΅ {π₯ β π΄ β£ π· = π¦} β β) | ||
Theorem | rencldnfilem 41861* | Lemma for rencldnfi 41862. (Contributed by Stefan O'Rear, 18-Oct-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ (π΄ β β β§ Β¬ π΅ β π΄)) β§ βπ₯ β β+ βπ¦ β π΄ (absβ(π¦ β π΅)) < π₯) β Β¬ π΄ β Fin) | ||
Theorem | rencldnfi 41862* | A set of real numbers which comes arbitrarily close to some target yet excludes it is infinite. The work is done in rencldnfilem 41861 using infima; this theorem removes the requirement that A be nonempty. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ (((π΄ β β β§ π΅ β β β§ Β¬ π΅ β π΄) β§ βπ₯ β β+ βπ¦ β π΄ (absβ(π¦ β π΅)) < π₯) β Β¬ π΄ β Fin) | ||
Theorem | irrapxlem1 41863* | Lemma for irrapx1 41869. Divides the unit interval into π΅ half-open sections and using the pigeonhole principle fphpdo 41858 finds two multiples of π΄ in the same section mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β) β βπ₯ β (0...π΅)βπ¦ β (0...π΅)(π₯ < π¦ β§ (ββ(π΅ Β· ((π΄ Β· π₯) mod 1))) = (ββ(π΅ Β· ((π΄ Β· π¦) mod 1))))) | ||
Theorem | irrapxlem2 41864* | Lemma for irrapx1 41869. Two multiples in the same bucket means they are very close mod 1. (Contributed by Stefan O'Rear, 12-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β) β βπ₯ β (0...π΅)βπ¦ β (0...π΅)(π₯ < π¦ β§ (absβ(((π΄ Β· π₯) mod 1) β ((π΄ Β· π¦) mod 1))) < (1 / π΅))) | ||
Theorem | irrapxlem3 41865* | Lemma for irrapx1 41869. By subtraction, there is a multiple very close to an integer. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β) β βπ₯ β (1...π΅)βπ¦ β β0 (absβ((π΄ Β· π₯) β π¦)) < (1 / π΅)) | ||
Theorem | irrapxlem4 41866* | Lemma for irrapx1 41869. 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.) |
β’ ((π΄ β β+ β§ π΅ β β) β βπ₯ β β βπ¦ β β (absβ((π΄ Β· π₯) β π¦)) < (1 / if(π₯ β€ π΅, π΅, π₯))) | ||
Theorem | irrapxlem5 41867* | Lemma for irrapx1 41869. Switching to real intervals and fraction syntax. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β+) β βπ₯ β β (0 < π₯ β§ (absβ(π₯ β π΄)) < π΅ β§ (absβ(π₯ β π΄)) < ((denomβπ₯)β-2))) | ||
Theorem | irrapxlem6 41868* | Lemma for irrapx1 41869. Explicit description of a non-closed set. (Contributed by Stefan O'Rear, 13-Sep-2014.) |
β’ ((π΄ β β+ β§ π΅ β β+) β βπ₯ β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} (absβ(π₯ β π΄)) < π΅) | ||
Theorem | irrapx1 41869* | 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.) |
β’ (π΄ β (β+ β β) β {π¦ β β β£ (0 < π¦ β§ (absβ(π¦ β π΄)) < ((denomβπ¦)β-2))} β β) | ||
Theorem | pellexlem1 41870 | Lemma for pellex 41876. 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.) |
β’ (((π· β β β§ π΄ β β β§ π΅ β β) β§ Β¬ (ββπ·) β β) β ((π΄β2) β (π· Β· (π΅β2))) β 0) | ||
Theorem | pellexlem2 41871 | Lemma for pellex 41876. Arithmetical core of pellexlem3, norm upper bound. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
β’ (((π· β β β§ π΄ β β β§ π΅ β β) β§ (absβ((π΄ / π΅) β (ββπ·))) < (π΅β-2)) β (absβ((π΄β2) β (π· Β· (π΅β2)))) < (1 + (2 Β· (ββπ·)))) | ||
Theorem | pellexlem3 41872* | Lemma for pellex 41876. To each good rational approximation of (ββπ·), there exists a near-solution. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
β’ ((π· β β β§ Β¬ (ββπ·) β β) β {π₯ β β β£ (0 < π₯ β§ (absβ(π₯ β (ββπ·))) < ((denomβπ₯)β-2))} βΌ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β· (ββπ·)))))}) | ||
Theorem | pellexlem4 41873* | Lemma for pellex 41876. Invoking irrapx1 41869, we have infinitely many near-solutions. (Contributed by Stefan O'Rear, 14-Sep-2014.) |
β’ ((π· β β β§ Β¬ (ββπ·) β β) β {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ (((π¦β2) β (π· Β· (π§β2))) β 0 β§ (absβ((π¦β2) β (π· Β· (π§β2)))) < (1 + (2 Β· (ββπ·)))))} β β) | ||
Theorem | pellexlem5 41874* | Lemma for pellex 41876. Invoking fiphp3d 41860, we have infinitely many near-solutions for some specific norm. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ ((π· β β β§ Β¬ (ββπ·) β β) β βπ₯ β β€ (π₯ β 0 β§ {β¨π¦, π§β© β£ ((π¦ β β β§ π§ β β) β§ ((π¦β2) β (π· Β· (π§β2))) = π₯)} β β)) | ||
Theorem | pellexlem6 41875* | Lemma for pellex 41876. 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.) |
β’ (π β π΄ β β) & β’ (π β π΅ β β) & β’ (π β πΆ β β€) & β’ (π β π· β β) & β’ (π β Β¬ (ββπ·) β β) & β’ (π β πΈ β β) & β’ (π β πΉ β β) & β’ (π β Β¬ (π΄ = πΈ β§ π΅ = πΉ)) & β’ (π β πΆ β 0) & β’ (π β ((π΄β2) β (π· Β· (π΅β2))) = πΆ) & β’ (π β ((πΈβ2) β (π· Β· (πΉβ2))) = πΆ) & β’ (π β (π΄ mod (absβπΆ)) = (πΈ mod (absβπΆ))) & β’ (π β (π΅ mod (absβπΆ)) = (πΉ mod (absβπΆ))) β β’ (π β βπ β β βπ β β ((πβ2) β (π· Β· (πβ2))) = 1) | ||
Theorem | pellex 41876* | Every Pell equation has a nontrivial solution. Theorem 62 in [vandenDries] p. 43. (Contributed by Stefan O'Rear, 19-Oct-2014.) |
β’ ((π· β β β§ Β¬ (ββπ·) β β) β βπ₯ β β βπ¦ β β ((π₯β2) β (π· Β· (π¦β2))) = 1) | ||
Syntax | csquarenn 41877 | Extend class notation to include the set of square positive integers. |
class β»NN | ||
Syntax | cpell1qr 41878 | Extend class notation to include the class of quadrant-1 Pell solutions. |
class Pell1QR | ||
Syntax | cpell1234qr 41879 | Extend class notation to include the class of any-quadrant Pell solutions. |
class Pell1234QR | ||
Syntax | cpell14qr 41880 | Extend class notation to include the class of positive Pell solutions. |
class Pell14QR | ||
Syntax | cpellfund 41881 | Extend class notation to include the Pell-equation fundamental solution function. |
class PellFund | ||
Definition | df-squarenn 41882 | Define the set of square positive integers. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ β»NN = {π₯ β β β£ (ββπ₯) β β} | ||
Definition | df-pell1qr 41883* | 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 = (π₯ β (β β β»NN) β¦ {π¦ β β β£ βπ§ β β0 βπ€ β β0 (π¦ = (π§ + ((ββπ₯) Β· π€)) β§ ((π§β2) β (π₯ Β· (π€β2))) = 1)}) | ||
Definition | df-pell14qr 41884* | Define the positive solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ Pell14QR = (π₯ β (β β β»NN) β¦ {π¦ β β β£ βπ§ β β0 βπ€ β β€ (π¦ = (π§ + ((ββπ₯) Β· π€)) β§ ((π§β2) β (π₯ Β· (π€β2))) = 1)}) | ||
Definition | df-pell1234qr 41885* | Define the general solutions of a Pell equation. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ Pell1234QR = (π₯ β (β β β»NN) β¦ {π¦ β β β£ βπ§ β β€ βπ€ β β€ (π¦ = (π§ + ((ββπ₯) Β· π€)) β§ ((π§β2) β (π₯ Β· (π€β2))) = 1)}) | ||
Definition | df-pellfund 41886* | 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 = (π₯ β (β β β»NN) β¦ inf({π§ β (Pell14QRβπ₯) β£ 1 < π§}, β, < )) | ||
Theorem | pell1qrval 41887* | Value of the set of first-quadrant Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell1QRβπ·) = {π¦ β β β£ βπ§ β β0 βπ€ β β0 (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell1qr 41888* | Membership in a first-quadrant Pell solution set. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell1QRβπ·) β (π΄ β β β§ βπ§ β β0 βπ€ β β0 (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell14qrval 41889* | Value of the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell14QRβπ·) = {π¦ β β β£ βπ§ β β0 βπ€ β β€ (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell14qr 41890* | Membership in the set of positive Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell14QRβπ·) β (π΄ β β β§ βπ§ β β0 βπ€ β β€ (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell1234qrval 41891* | Value of the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell1234QRβπ·) = {π¦ β β β£ βπ§ β β€ βπ€ β β€ (π¦ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)}) | ||
Theorem | elpell1234qr 41892* | Membership in the set of general Pell solutions. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ (π· β (β β β»NN) β (π΄ β (Pell1234QRβπ·) β (π΄ β β β§ βπ§ β β€ βπ€ β β€ (π΄ = (π§ + ((ββπ·) Β· π€)) β§ ((π§β2) β (π· Β· (π€β2))) = 1)))) | ||
Theorem | pell1234qrre 41893 | General Pell solutions are (coded as) real numbers. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β π΄ β β) | ||
Theorem | pell1234qrne0 41894 | No solution to a Pell equation is zero. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β π΄ β 0) | ||
Theorem | pell1234qrreccl 41895 | General solutions of the Pell equation are closed under reciprocals. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·)) β (1 / π΄) β (Pell1234QRβπ·)) | ||
Theorem | pell1234qrmulcl 41896 | General solutions of the Pell equation are closed under multiplication. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell1234QRβπ·) β§ π΅ β (Pell1234QRβπ·)) β (π΄ Β· π΅) β (Pell1234QRβπ·)) | ||
Theorem | pell14qrss1234 41897 | A positive Pell solution is a general Pell solution. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ (π· β (β β β»NN) β (Pell14QRβπ·) β (Pell1234QRβπ·)) | ||
Theorem | pell14qrre 41898 | A positive Pell solution is a real number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β β) | ||
Theorem | pell14qrne0 41899 | A positive Pell solution is a nonzero number. (Contributed by Stefan O'Rear, 17-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β π΄ β 0) | ||
Theorem | pell14qrgt0 41900 | A positive Pell solution is a positive number. (Contributed by Stefan O'Rear, 18-Sep-2014.) |
β’ ((π· β (β β β»NN) β§ π΄ β (Pell14QRβπ·)) β 0 < π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |