Home | Metamath
Proof Explorer Theorem List (p. 118 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 | eluz 11701 | Membership in an upper set of integers. (Contributed by NM, 2-Oct-2005.) |
Theorem | uzid 11702 | Membership of the least member in an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
Theorem | uzn0 11703 | The upper integers are all nonempty. (Contributed by Mario Carneiro, 16-Jan-2014.) |
Theorem | uztrn 11704 | Transitive law for sets of upper integers. (Contributed by NM, 20-Sep-2005.) |
Theorem | uztrn2 11705 | Transitive law for sets of upper integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | uzneg 11706 | Contraposition law for upper integers. (Contributed by NM, 28-Nov-2005.) |
Theorem | uzssz 11707 | An upper set of integers is a subset of all integers. (Contributed by NM, 2-Sep-2005.) (Revised by Mario Carneiro, 3-Nov-2013.) |
Theorem | uzss 11708 | Subset relationship for two sets of upper integers. (Contributed by NM, 5-Sep-2005.) |
Theorem | uztric 11709 | Totality of the ordering relation on integers, stated in terms of upper integers. (Contributed by NM, 6-Jul-2005.) (Revised by Mario Carneiro, 25-Jun-2013.) |
Theorem | uz11 11710 | The upper integers function is one-to-one. (Contributed by NM, 12-Dec-2005.) |
Theorem | eluzp1m1 11711 | Membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
Theorem | eluzp1l 11712 | Strict ordering implied by membership in the next upper set of integers. (Contributed by NM, 12-Sep-2005.) |
Theorem | eluzp1p1 11713 | Membership in the next upper set of integers. (Contributed by NM, 5-Oct-2005.) |
Theorem | eluzaddi 11714 | Membership in a later upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) |
Theorem | eluzsubi 11715 | Membership in an earlier upper set of integers. (Contributed by Paul Chapman, 22-Nov-2007.) |
Theorem | eluzadd 11716 | Membership in a later upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | eluzsub 11717 | Membership in an earlier upper set of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | uzm1 11718 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | uznn0sub 11719 | The nonnegative difference of integers is a nonnegative integer. (Contributed by NM, 4-Sep-2005.) |
Theorem | uzin 11720 | Intersection of two upper intervals of integers. (Contributed by Mario Carneiro, 24-Dec-2013.) |
Theorem | uzp1 11721 | Choices for an element of an upper interval of integers. (Contributed by Jeff Madsen, 2-Sep-2009.) |
Theorem | nn0uz 11722 | Nonnegative integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
Theorem | nnuz 11723 | Positive integers expressed as an upper set of integers. (Contributed by NM, 2-Sep-2005.) |
Theorem | elnnuz 11724 | A positive integer expressed as a member of an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
Theorem | elnn0uz 11725 | A nonnegative integer expressed as a member an upper set of integers. (Contributed by NM, 6-Jun-2006.) |
Theorem | eluz2nn 11726 | An integer is greater than or equal to 2 is a positive integer. (Contributed by AV, 3-Nov-2018.) |
Theorem | eluzge2nn0 11727 | If an integer is greater than or equal to 2, then it is a nonnegative integer. (Contributed by AV, 27-Aug-2018.) (Proof shortened by AV, 3-Nov-2018.) |
Theorem | eluz2n0 11728 | An integer greater than or equal to 2 is not 0. (Contributed by AV, 25-May-2020.) |
Theorem | uzuzle23 11729 | An integer in the upper set of integers starting at 3 is element of the upper set of integers starting at 2. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
Theorem | eluzge3nn 11730 | If an integer is greater than 3, then it is a positive integer. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
Theorem | uz3m2nn 11731 | An integer greater than or equal to 3 decreased by 2 is a positive integer, analogous to uz2m1nn 11763. (Contributed by Alexander van der Vekens, 17-Sep-2018.) |
Theorem | 1eluzge0 11732 | 1 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
Theorem | 2eluzge0 11733 | 2 is an integer greater than or equal to 0. (Contributed by Alexander van der Vekens, 8-Jun-2018.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | 2eluzge1 11734 | 2 is an integer greater than or equal to 1. (Contributed by Alexander van der Vekens, 8-Jun-2018.) |
Theorem | uznnssnn 11735 | The upper integers starting from a natural are a subset of the naturals. (Contributed by Scott Fenton, 29-Jun-2013.) |
Theorem | raluz 11736* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
Theorem | raluz2 11737* | Restricted universal quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
Theorem | rexuz 11738* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
Theorem | rexuz2 11739* | Restricted existential quantification in an upper set of integers. (Contributed by NM, 9-Sep-2005.) |
Theorem | 2rexuz 11740* | Double existential quantification in an upper set of integers. (Contributed by NM, 3-Nov-2005.) |
Theorem | peano2uz 11741 | Second Peano postulate for an upper set of integers. (Contributed by NM, 7-Sep-2005.) |
Theorem | peano2uzs 11742 | Second Peano postulate for an upper set of integers. (Contributed by Mario Carneiro, 26-Dec-2013.) |
Theorem | peano2uzr 11743 | Reversed second Peano axiom for upper integers. (Contributed by NM, 2-Jan-2006.) |
Theorem | uzaddcl 11744 | Addition closure law for an upper set of integers. (Contributed by NM, 4-Jun-2006.) |
Theorem | nn0pzuz 11745 | The sum of a nonnegative integer and an integer is an integer greater than or equal to that integer. (Contributed by Alexander van der Vekens, 3-Oct-2018.) |
Theorem | uzind4 11746* | Induction on the upper set of integers that starts at an integer . The first four hypotheses give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 7-Sep-2005.) |
Theorem | uzind4ALT 11747* | Induction on the upper set of integers that starts at an integer . The last four hypotheses give us the substitution instances we need; the first two are the basis and the induction step. Either uzind4 11746 or uzind4ALT 11747 may be used; see comment for nnind 11038. (Contributed by NM, 7-Sep-2005.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | uzind4s 11748* | Induction on the upper set of integers that starts at an integer , using explicit substitution. The hypotheses are the basis and the induction step. (Contributed by NM, 4-Nov-2005.) |
Theorem | uzind4s2 11749* | Induction on the upper set of integers that starts at an integer , using explicit substitution. The hypotheses are the basis and the induction step. Use this instead of uzind4s 11748 when and must be distinct in . (Contributed by NM, 16-Nov-2005.) |
Theorem | uzind4i 11750* | Induction on the upper integers that start at . The first hypothesis specifies the lower bound, the next four give us the substitution instances we need, and the last two are the basis and the induction step. (Contributed by NM, 4-Sep-2005.) |
Theorem | uzwo 11751* | Well-ordering principle: any nonempty subset of an upper set of integers has the least element. (Contributed by NM, 8-Oct-2005.) |
Theorem | uzwo2 11752* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. (Contributed by NM, 8-Oct-2005.) |
Theorem | nnwo 11753* | Well-ordering principle: any nonempty set of positive integers has a least element. Theorem I.37 (well-ordering principle) of [Apostol] p. 34. (Contributed by NM, 17-Aug-2001.) |
Theorem | nnwof 11754* | Well-ordering principle: any nonempty set of positive integers has a least element. This version allows and to be present in as long as they are effectively not free. (Contributed by NM, 17-Aug-2001.) (Revised by Mario Carneiro, 15-Oct-2016.) |
Theorem | nnwos 11755* | Well-ordering principle: any nonempty set of positive integers has a least element (schema form). (Contributed by NM, 17-Aug-2001.) |
Theorem | indstr 11756* | Strong Mathematical Induction for positive integers (inference schema). (Contributed by NM, 17-Aug-2001.) |
Theorem | eluznn0 11757 | Membership in a nonnegative upper set of integers implies membership in . (Contributed by Paul Chapman, 22-Jun-2011.) |
Theorem | eluznn 11758 | Membership in a positive upper set of integers implies membership in . (Contributed by JJ, 1-Oct-2018.) |
Theorem | eluz2b1 11759 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
Theorem | eluz2gt1 11760 | An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.) |
Theorem | eluz2b2 11761 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
Theorem | eluz2b3 11762 | Two ways to say "an integer greater than or equal to 2." (Contributed by Paul Chapman, 23-Nov-2012.) |
Theorem | uz2m1nn 11763 | One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | 1nuz2 11764 | 1 is not in . (Contributed by Paul Chapman, 21-Nov-2012.) |
Theorem | elnn1uz2 11765 | A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
Theorem | uz2mulcl 11766 | Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.) |
Theorem | indstr2 11767* | Strong Mathematical Induction for positive integers (inference schema). The first two hypotheses give us the substitution instances we need; the last two are the basis and the induction step. (Contributed by Paul Chapman, 21-Nov-2012.) |
Theorem | uzinfi 11768 | Extract the lower bound of an upper set of integers as its infimum. (Contributed by NM, 7-Oct-2005.) (Revised by AV, 4-Sep-2020.) |
inf | ||
Theorem | nninf 11769 | The infimum of the set of positive integers is one. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | nn0inf 11770 | The infimum of the set of nonnegative integers is zero. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | infssuzle 11771 | The infimum of a subset of an upper set of integers is less than or equal to all members of the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | infssuzcl 11772 | The infimum of a subset of an upper set of integers belongs to the subset. (Contributed by NM, 11-Oct-2005.) (Revised by AV, 5-Sep-2020.) |
inf | ||
Theorem | ublbneg 11773* | The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | eqreznegel 11774* | Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | supminf 11775* | The supremum of a bounded-above set of reals is the negation of the infimum of that set's image under negation. (Contributed by Paul Chapman, 21-Mar-2011.) ( Revised by AV, 13-Sep-2020.) |
inf | ||
Theorem | lbzbi 11776* | If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.) |
Theorem | zsupss 11777* | Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 10014.) (Contributed by Mario Carneiro, 21-Apr-2015.) |
Theorem | suprzcl2 11778* | The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 11457 avoids ax-pre-sup 10014.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) |
Theorem | suprzub 11779* | The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) |
Theorem | uzsupss 11780* | Any bounded subset of an upper set of integers has a supremum. (Contributed by Mario Carneiro, 22-Jul-2014.) (Revised by Mario Carneiro, 21-Apr-2015.) |
Theorem | nn01to3 11781 | A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.) |
Theorem | nn0ge2m1nnALT 11782 | Alternate proof of nn0ge2m1nn 11360: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is a positive integer. This version is proved using eluz2 11693, a theorem for upper sets of integers, which are defined later than the positive and nonnegative integers. This proof is, however, much shorter than the proof of nn0ge2m1nn 11360. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | uzwo3 11783* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 11752 allows the lower bound to be any real number. See also nnwo 11753 and nnwos 11755. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.) |
Theorem | zmin 11784* | There is a unique smallest integer greater than or equal to a given real number. (Contributed by NM, 12-Nov-2004.) (Revised by Mario Carneiro, 13-Jun-2014.) |
Theorem | zmax 11785* | There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.) |
Theorem | zbtwnre 11786* | There is a unique integer between a real number and the number plus one. Exercise 5 of [Apostol] p. 28. (Contributed by NM, 13-Nov-2004.) |
Theorem | rebtwnz 11787* | There is a unique greatest integer less than or equal to a real number. Exercise 4 of [Apostol] p. 28. (Contributed by NM, 15-Nov-2004.) |
Syntax | cq 11788 | Extend class notation to include the class of rationals. |
Definition | df-q 11789 | Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 11790 for the relation "is rational." (Contributed by NM, 8-Jan-2002.) |
Theorem | elq 11790* | Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.) |
Theorem | qmulz 11791* | If is rational, then some integer multiple of it is an integer. (Contributed by NM, 7-Nov-2008.) (Revised by Mario Carneiro, 22-Jul-2014.) |
Theorem | znq 11792 | The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.) |
Theorem | qre 11793 | A rational number is a real number. (Contributed by NM, 14-Nov-2002.) |
Theorem | zq 11794 | An integer is a rational number. (Contributed by NM, 9-Jan-2002.) |
Theorem | zssq 11795 | The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.) |
Theorem | nn0ssq 11796 | The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
Theorem | nnssq 11797 | The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
Theorem | qssre 11798 | The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.) |
Theorem | qsscn 11799 | The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
Theorem | qex 11800 | The set of rational numbers exists. See also qexALT 11803. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |