![]() |
Metamath
Proof Explorer Theorem List (p. 130 of 479) | < 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | eluznn0 12901 | Membership in a nonnegative upper set of integers implies membership in โ0. (Contributed by Paul Chapman, 22-Jun-2011.) |
โข ((๐ โ โ0 โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ0) | ||
Theorem | eluznn 12902 | Membership in a positive upper set of integers implies membership in โ. (Contributed by JJ, 1-Oct-2018.) |
โข ((๐ โ โ โง ๐ โ (โคโฅโ๐)) โ ๐ โ โ) | ||
Theorem | eluz2b1 12903 | Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.) |
โข (๐ โ (โคโฅโ2) โ (๐ โ โค โง 1 < ๐)) | ||
Theorem | eluz2gt1 12904 | An integer greater than or equal to 2 is greater than 1. (Contributed by AV, 24-May-2020.) |
โข (๐ โ (โคโฅโ2) โ 1 < ๐) | ||
Theorem | eluz2b2 12905 | Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.) |
โข (๐ โ (โคโฅโ2) โ (๐ โ โ โง 1 < ๐)) | ||
Theorem | eluz2b3 12906 | Two ways to say "an integer greater than or equal to 2". (Contributed by Paul Chapman, 23-Nov-2012.) |
โข (๐ โ (โคโฅโ2) โ (๐ โ โ โง ๐ โ 1)) | ||
Theorem | uz2m1nn 12907 | One less than an integer greater than or equal to 2 is a positive integer. (Contributed by Paul Chapman, 17-Nov-2012.) |
โข (๐ โ (โคโฅโ2) โ (๐ โ 1) โ โ) | ||
Theorem | 1nuz2 12908 | 1 is not in (โคโฅโ2). (Contributed by Paul Chapman, 21-Nov-2012.) |
โข ยฌ 1 โ (โคโฅโ2) | ||
Theorem | elnn1uz2 12909 | A positive integer is either 1 or greater than or equal to 2. (Contributed by Paul Chapman, 17-Nov-2012.) |
โข (๐ โ โ โ (๐ = 1 โจ ๐ โ (โคโฅโ2))) | ||
Theorem | uz2mulcl 12910 | Closure of multiplication of integers greater than or equal to 2. (Contributed by Paul Chapman, 26-Oct-2012.) |
โข ((๐ โ (โคโฅโ2) โง ๐ โ (โคโฅโ2)) โ (๐ ยท ๐) โ (โคโฅโ2)) | ||
Theorem | indstr2 12911* | 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.) |
โข (๐ฅ = 1 โ (๐ โ ๐)) & โข (๐ฅ = ๐ฆ โ (๐ โ ๐)) & โข ๐ & โข (๐ฅ โ (โคโฅโ2) โ (โ๐ฆ โ โ (๐ฆ < ๐ฅ โ ๐) โ ๐)) โ โข (๐ฅ โ โ โ ๐) | ||
Theorem | uzinfi 12912 | 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 12913 | The infimum of the set of positive integers is one. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.) |
โข inf(โ, โ, < ) = 1 | ||
Theorem | nn0inf 12914 | The infimum of the set of nonnegative integers is zero. (Contributed by NM, 16-Jun-2005.) (Revised by AV, 5-Sep-2020.) |
โข inf(โ0, โ, < ) = 0 | ||
Theorem | infssuzle 12915 | 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 12916 | 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 12917* | The image under negation of a bounded-above set of reals is bounded below. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ โ โ๐ฅ โ โ โ๐ฆ โ {๐ง โ โ โฃ -๐ง โ ๐ด}๐ฅ โค ๐ฆ) | ||
Theorem | eqreznegel 12918* | Two ways to express the image under negation of a set of integers. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ด โ โค โ {๐ง โ โ โฃ -๐ง โ ๐ด} = {๐ง โ โค โฃ -๐ง โ ๐ด}) | ||
Theorem | supminf 12919* | 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.) |
โข ((๐ด โ โ โง ๐ด โ โ โง โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) = -inf({๐ง โ โ โฃ -๐ง โ ๐ด}, โ, < )) | ||
Theorem | lbzbi 12920* | If a set of reals is bounded below, it is bounded below by an integer. (Contributed by Paul Chapman, 21-Mar-2011.) |
โข (๐ด โ โ โ (โ๐ฅ โ โ โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ โ โ๐ฅ โ โค โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ)) | ||
Theorem | zsupss 12921* | Any nonempty bounded subset of integers has a supremum in the set. (The proof does not use ax-pre-sup 11188.) (Contributed by Mario Carneiro, 21-Apr-2015.) |
โข ((๐ด โ โค โง ๐ด โ โ โง โ๐ฅ โ โค โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ โ๐ฅ โ ๐ด (โ๐ฆ โ ๐ด ยฌ ๐ฅ < ๐ฆ โง โ๐ฆ โ ๐ต (๐ฆ < ๐ฅ โ โ๐ง โ ๐ด ๐ฆ < ๐ง))) | ||
Theorem | suprzcl2 12922* | The supremum of a bounded-above set of integers is a member of the set. (This version of suprzcl 12642 avoids ax-pre-sup 11188.) (Contributed by Mario Carneiro, 21-Apr-2015.) (Revised by Mario Carneiro, 24-Dec-2016.) |
โข ((๐ด โ โค โง ๐ด โ โ โง โ๐ฅ โ โค โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ) โ sup(๐ด, โ, < ) โ ๐ด) | ||
Theorem | suprzub 12923* | The supremum of a bounded-above set of integers is greater than any member of the set. (Contributed by Mario Carneiro, 21-Apr-2015.) |
โข ((๐ด โ โค โง โ๐ฅ โ โค โ๐ฆ โ ๐ด ๐ฆ โค ๐ฅ โง ๐ต โ ๐ด) โ ๐ต โค sup(๐ด, โ, < )) | ||
Theorem | uzsupss 12924* | 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 12925 | A (nonnegative) integer between 1 and 3 must be 1, 2 or 3. (Contributed by Alexander van der Vekens, 13-Sep-2018.) |
โข ((๐ โ โ0 โง 1 โค ๐ โง ๐ โค 3) โ (๐ = 1 โจ ๐ = 2 โจ ๐ = 3)) | ||
Theorem | nn0ge2m1nnALT 12926 | Alternate proof of nn0ge2m1nn 12541: 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 12828, 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 12541. (Contributed by Alexander van der Vekens, 1-Aug-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
โข ((๐ โ โ0 โง 2 โค ๐) โ (๐ โ 1) โ โ) | ||
Theorem | uzwo3 12927* | Well-ordering principle: any nonempty subset of an upper set of integers has a unique least element. This generalization of uzwo2 12896 allows the lower bound ๐ต to be any real number. See also nnwo 12897 and nnwos 12899. (Contributed by NM, 12-Nov-2004.) (Proof shortened by Mario Carneiro, 2-Oct-2015.) (Proof shortened by AV, 27-Sep-2020.) |
โข ((๐ต โ โ โง (๐ด โ {๐ง โ โค โฃ ๐ต โค ๐ง} โง ๐ด โ โ )) โ โ!๐ฅ โ ๐ด โ๐ฆ โ ๐ด ๐ฅ โค ๐ฆ) | ||
Theorem | zmin 12928* | 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 12929* | There is a unique largest integer less than or equal to a given real number. (Contributed by NM, 15-Nov-2004.) |
โข (๐ด โ โ โ โ!๐ฅ โ โค (๐ฅ โค ๐ด โง โ๐ฆ โ โค (๐ฆ โค ๐ด โ ๐ฆ โค ๐ฅ))) | ||
Theorem | zbtwnre 12930* | 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.) |
โข (๐ด โ โ โ โ!๐ฅ โ โค (๐ด โค ๐ฅ โง ๐ฅ < (๐ด + 1))) | ||
Theorem | rebtwnz 12931* | 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.) |
โข (๐ด โ โ โ โ!๐ฅ โ โค (๐ฅ โค ๐ด โง ๐ด < (๐ฅ + 1))) | ||
Syntax | cq 12932 | Extend class notation to include the class of rationals. |
class โ | ||
Definition | df-q 12933 | Define the set of rational numbers. Based on definition of rationals in [Apostol] p. 22. See elq 12934 for the relation "is rational". (Contributed by NM, 8-Jan-2002.) |
โข โ = ( / โ (โค ร โ)) | ||
Theorem | elq 12934* | Membership in the set of rationals. (Contributed by NM, 8-Jan-2002.) (Revised by Mario Carneiro, 28-Jan-2014.) |
โข (๐ด โ โ โ โ๐ฅ โ โค โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ)) | ||
Theorem | qmulz 12935* | 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 12936 | The ratio of an integer and a positive integer is a rational number. (Contributed by NM, 12-Jan-2002.) |
โข ((๐ด โ โค โง ๐ต โ โ) โ (๐ด / ๐ต) โ โ) | ||
Theorem | qre 12937 | A rational number is a real number. (Contributed by NM, 14-Nov-2002.) |
โข (๐ด โ โ โ ๐ด โ โ) | ||
Theorem | zq 12938 | An integer is a rational number. (Contributed by NM, 9-Jan-2002.) (Proof shortened by Steven Nguyen, 23-Mar-2023.) |
โข (๐ด โ โค โ ๐ด โ โ) | ||
Theorem | qred 12939 | A rational number is a real number. (Contributed by Glauco Siliprandi, 26-Jun-2021.) |
โข (๐ โ ๐ด โ โ) โ โข (๐ โ ๐ด โ โ) | ||
Theorem | zssq 12940 | The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002.) |
โข โค โ โ | ||
Theorem | nn0ssq 12941 | The nonnegative integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
โข โ0 โ โ | ||
Theorem | nnssq 12942 | The positive integers are a subset of the rationals. (Contributed by NM, 31-Jul-2004.) |
โข โ โ โ | ||
Theorem | qssre 12943 | The rationals are a subset of the reals. (Contributed by NM, 9-Jan-2002.) |
โข โ โ โ | ||
Theorem | qsscn 12944 | The rationals are a subset of the complex numbers. (Contributed by NM, 2-Aug-2004.) |
โข โ โ โ | ||
Theorem | qex 12945 | The set of rational numbers exists. See also qexALT 12948. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข โ โ V | ||
Theorem | nnq 12946 | A positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
โข (๐ด โ โ โ ๐ด โ โ) | ||
Theorem | qcn 12947 | A rational number is a complex number. (Contributed by NM, 2-Aug-2004.) |
โข (๐ด โ โ โ ๐ด โ โ) | ||
Theorem | qexALT 12948 | Alternate proof of qex 12945. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข โ โ V | ||
Theorem | qaddcl 12949 | Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด + ๐ต) โ โ) | ||
Theorem | qnegcl 12950 | Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.) |
โข (๐ด โ โ โ -๐ด โ โ) | ||
Theorem | qmulcl 12951 | Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ยท ๐ต) โ โ) | ||
Theorem | qsubcl 12952 | Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด โ ๐ต) โ โ) | ||
Theorem | qreccl 12953 | Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.) |
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 / ๐ด) โ โ) | ||
Theorem | qdivcl 12954 | Closure of division of rationals. (Contributed by NM, 3-Aug-2004.) |
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด / ๐ต) โ โ) | ||
Theorem | qrevaddcl 12955 | Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.) |
โข (๐ต โ โ โ ((๐ด โ โ โง (๐ด + ๐ต) โ โ) โ ๐ด โ โ)) | ||
Theorem | nnrecq 12956 | The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
โข (๐ด โ โ โ (1 / ๐ด) โ โ) | ||
Theorem | irradd 12957 | The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.) |
โข ((๐ด โ (โ โ โ) โง ๐ต โ โ) โ (๐ด + ๐ต) โ (โ โ โ)) | ||
Theorem | irrmul 12958 | The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.) |
โข ((๐ด โ (โ โ โ) โง ๐ต โ โ โง ๐ต โ 0) โ (๐ด ยท ๐ต) โ (โ โ โ)) | ||
Theorem | elpq 12959* | A positive rational is the quotient of two positive integers. (Contributed by AV, 29-Dec-2022.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ)) | ||
Theorem | elpqb 12960* | A class is a positive rational iff it is the quotient of two positive integers. (Contributed by AV, 30-Dec-2022.) |
โข ((๐ด โ โ โง 0 < ๐ด) โ โ๐ฅ โ โ โ๐ฆ โ โ ๐ด = (๐ฅ / ๐ฆ)) | ||
Theorem | rpnnen1lem2 12961* | Lemma for rpnnen1 12967. (Contributed by Mario Carneiro, 12-May-2013.) |
โข ๐ = {๐ โ โค โฃ (๐ / ๐) < ๐ฅ} & โข ๐น = (๐ฅ โ โ โฆ (๐ โ โ โฆ (sup(๐, โ, < ) / ๐))) โ โข ((๐ฅ โ โ โง ๐ โ โ) โ sup(๐, โ, < ) โ โค) | ||
Theorem | rpnnen1lem1 12962* | Lemma for rpnnen1 12967. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
โข ๐ = {๐ โ โค โฃ (๐ / ๐) < ๐ฅ} & โข ๐น = (๐ฅ โ โ โฆ (๐ โ โ โฆ (sup(๐, โ, < ) / ๐))) & โข โ โ V & โข โ โ V โ โข (๐ฅ โ โ โ (๐นโ๐ฅ) โ (โ โm โ)) | ||
Theorem | rpnnen1lem3 12963* | Lemma for rpnnen1 12967. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
โข ๐ = {๐ โ โค โฃ (๐ / ๐) < ๐ฅ} & โข ๐น = (๐ฅ โ โ โฆ (๐ โ โ โฆ (sup(๐, โ, < ) / ๐))) & โข โ โ V & โข โ โ V โ โข (๐ฅ โ โ โ โ๐ โ ran (๐นโ๐ฅ)๐ โค ๐ฅ) | ||
Theorem | rpnnen1lem4 12964* | Lemma for rpnnen1 12967. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
โข ๐ = {๐ โ โค โฃ (๐ / ๐) < ๐ฅ} & โข ๐น = (๐ฅ โ โ โฆ (๐ โ โ โฆ (sup(๐, โ, < ) / ๐))) & โข โ โ V & โข โ โ V โ โข (๐ฅ โ โ โ sup(ran (๐นโ๐ฅ), โ, < ) โ โ) | ||
Theorem | rpnnen1lem5 12965* | Lemma for rpnnen1 12967. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
โข ๐ = {๐ โ โค โฃ (๐ / ๐) < ๐ฅ} & โข ๐น = (๐ฅ โ โ โฆ (๐ โ โ โฆ (sup(๐, โ, < ) / ๐))) & โข โ โ V & โข โ โ V โ โข (๐ฅ โ โ โ sup(ran (๐นโ๐ฅ), โ, < ) = ๐ฅ) | ||
Theorem | rpnnen1lem6 12966* | Lemma for rpnnen1 12967. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.) |
โข ๐ = {๐ โ โค โฃ (๐ / ๐) < ๐ฅ} & โข ๐น = (๐ฅ โ โ โฆ (๐ โ โ โฆ (sup(๐, โ, < ) / ๐))) & โข โ โ V & โข โ โ V โ โข โ โผ (โ โm โ) | ||
Theorem | rpnnen1 12967 | One half of rpnnen 16170, where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number ๐ฅ to the sequence (๐นโ๐ฅ):โโถโ (see rpnnen1lem6 12966) such that ((๐นโ๐ฅ)โ๐) is the largest rational number with denominator ๐ that is strictly less than ๐ฅ. In this manner, we get a monotonically increasing sequence that converges to ๐ฅ, and since each sequence converges to a unique real number, this mapping from reals to sequences of rational numbers is injective. Note: The โ and โ existence hypotheses provide for use with either nnex 12218 and qex 12945, or nnexALT 12214 and qexALT 12948. The proof should not be modified to use any of those 4 theorems. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 16-Jun-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.) |
โข โ โ V & โข โ โ V โ โข โ โผ (โ โm โ) | ||
Theorem | reexALT 12968 | Alternate proof of reex 11201. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข โ โ V | ||
Theorem | cnref1o 12969* | There is a natural one-to-one mapping from (โ ร โ) to โ, where we map โจ๐ฅ, ๐ฆโฉ to (๐ฅ + (i ยท ๐ฆ)). In our construction of the complex numbers, this is in fact our definition of โ (see df-c 11116), but in the axiomatic treatment we can only show that there is the expected mapping between these two sets. (Contributed by Mario Carneiro, 16-Jun-2013.) (Revised by Mario Carneiro, 17-Feb-2014.) |
โข ๐น = (๐ฅ โ โ, ๐ฆ โ โ โฆ (๐ฅ + (i ยท ๐ฆ))) โ โข ๐น:(โ ร โ)โ1-1-ontoโโ | ||
Theorem | cnexALT 12970 | The set of complex numbers exists. This theorem shows that ax-cnex 11166 is redundant if we assume ax-rep 5286. See also ax-cnex 11166. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
โข โ โ V | ||
Theorem | xrex 12971 | The set of extended reals exists. (Contributed by NM, 24-Dec-2006.) |
โข โ* โ V | ||
Theorem | addex 12972 | The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข + โ V | ||
Theorem | mulex 12973 | The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
โข ยท โ V | ||
Syntax | crp 12974 | Extend class notation to include the class of positive reals. |
class โ+ | ||
Definition | df-rp 12975 | Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
โข โ+ = {๐ฅ โ โ โฃ 0 < ๐ฅ} | ||
Theorem | elrp 12976 | Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
โข (๐ด โ โ+ โ (๐ด โ โ โง 0 < ๐ด)) | ||
Theorem | elrpii 12977 | Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.) |
โข ๐ด โ โ & โข 0 < ๐ด โ โข ๐ด โ โ+ | ||
Theorem | 1rp 12978 | 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.) |
โข 1 โ โ+ | ||
Theorem | 2rp 12979 | 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
โข 2 โ โ+ | ||
Theorem | 3rp 12980 | 3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
โข 3 โ โ+ | ||
Theorem | rpssre 12981 | The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.) |
โข โ+ โ โ | ||
Theorem | rpre 12982 | A positive real is a real. (Contributed by NM, 27-Oct-2007.) (Proof shortened by Steven Nguyen, 8-Oct-2022.) |
โข (๐ด โ โ+ โ ๐ด โ โ) | ||
Theorem | rpxr 12983 | A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.) |
โข (๐ด โ โ+ โ ๐ด โ โ*) | ||
Theorem | rpcn 12984 | A positive real is a complex number. (Contributed by NM, 11-Nov-2008.) |
โข (๐ด โ โ+ โ ๐ด โ โ) | ||
Theorem | nnrp 12985 | A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.) |
โข (๐ด โ โ โ ๐ด โ โ+) | ||
Theorem | rpgt0 12986 | A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.) |
โข (๐ด โ โ+ โ 0 < ๐ด) | ||
Theorem | rpge0 12987 | A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.) |
โข (๐ด โ โ+ โ 0 โค ๐ด) | ||
Theorem | rpregt0 12988 | A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
โข (๐ด โ โ+ โ (๐ด โ โ โง 0 < ๐ด)) | ||
Theorem | rprege0 12989 | A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.) |
โข (๐ด โ โ+ โ (๐ด โ โ โง 0 โค ๐ด)) | ||
Theorem | rpne0 12990 | A positive real is nonzero. (Contributed by NM, 18-Jul-2008.) |
โข (๐ด โ โ+ โ ๐ด โ 0) | ||
Theorem | rprene0 12991 | A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.) |
โข (๐ด โ โ+ โ (๐ด โ โ โง ๐ด โ 0)) | ||
Theorem | rpcnne0 12992 | A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.) |
โข (๐ด โ โ+ โ (๐ด โ โ โง ๐ด โ 0)) | ||
Theorem | rpcndif0 12993 | A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020.) |
โข (๐ด โ โ+ โ ๐ด โ (โ โ {0})) | ||
Theorem | ralrp 12994 | Quantification over positive reals. (Contributed by NM, 12-Feb-2008.) |
โข (โ๐ฅ โ โ+ ๐ โ โ๐ฅ โ โ (0 < ๐ฅ โ ๐)) | ||
Theorem | rexrp 12995 | Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.) |
โข (โ๐ฅ โ โ+ ๐ โ โ๐ฅ โ โ (0 < ๐ฅ โง ๐)) | ||
Theorem | rpaddcl 12996 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
โข ((๐ด โ โ+ โง ๐ต โ โ+) โ (๐ด + ๐ต) โ โ+) | ||
Theorem | rpmulcl 12997 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
โข ((๐ด โ โ+ โง ๐ต โ โ+) โ (๐ด ยท ๐ต) โ โ+) | ||
Theorem | rpmtmip 12998 | "Minus times minus is plus", see also nnmtmip 12238, holds for positive reals, too (formalized to "The product of two negative reals is a positive real"). "The reason for this" in this case is that (-๐ด ยท -๐ต) = (๐ด ยท ๐ต) for all complex numbers ๐ด and ๐ต because of mul2neg 11653, ๐ด and ๐ต are complex numbers because of rpcn 12984, and (๐ด ยท ๐ต) โ โ+ because of rpmulcl 12997. Note that the opposites -๐ด and -๐ต of the positive reals ๐ด and ๐ต are negative reals. (Contributed by AV, 23-Dec-2022.) |
โข ((๐ด โ โ+ โง ๐ต โ โ+) โ (-๐ด ยท -๐ต) โ โ+) | ||
Theorem | rpdivcl 12999 | Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.) |
โข ((๐ด โ โ+ โง ๐ต โ โ+) โ (๐ด / ๐ต) โ โ+) | ||
Theorem | rpreccl 13000 | Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.) |
โข (๐ด โ โ+ โ (1 / ๐ด) โ โ+) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |