Home | Metamath
Proof Explorer Theorem List (p. 119 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 | nnq 11801 | A positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
Theorem | qcn 11802 | A rational number is a complex number. (Contributed by NM, 2-Aug-2004.) |
Theorem | qexALT 11803 | Alternate proof of qex 11800. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | qaddcl 11804 | Closure of addition of rationals. (Contributed by NM, 1-Aug-2004.) |
Theorem | qnegcl 11805 | Closure law for the negative of a rational. (Contributed by NM, 2-Aug-2004.) (Revised by Mario Carneiro, 15-Sep-2014.) |
Theorem | qmulcl 11806 | Closure of multiplication of rationals. (Contributed by NM, 1-Aug-2004.) |
Theorem | qsubcl 11807 | Closure of subtraction of rationals. (Contributed by NM, 2-Aug-2004.) |
Theorem | qreccl 11808 | Closure of reciprocal of rationals. (Contributed by NM, 3-Aug-2004.) |
Theorem | qdivcl 11809 | Closure of division of rationals. (Contributed by NM, 3-Aug-2004.) |
Theorem | qrevaddcl 11810 | Reverse closure law for addition of rationals. (Contributed by NM, 2-Aug-2004.) |
Theorem | nnrecq 11811 | The reciprocal of a positive integer is rational. (Contributed by NM, 17-Nov-2004.) |
Theorem | irradd 11812 | The sum of an irrational number and a rational number is irrational. (Contributed by NM, 7-Nov-2008.) |
Theorem | irrmul 11813 | The product of an irrational with a nonzero rational is irrational. (Contributed by NM, 7-Nov-2008.) |
Theorem | rpnnen1lem2 11814* | Lemma for rpnnen1 11820. (Contributed by Mario Carneiro, 12-May-2013.) |
Theorem | rpnnen1lem1 11815* | Lemma for rpnnen1 11820. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem3 11816* | Lemma for rpnnen1 11820. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem4 11817* | Lemma for rpnnen1 11820. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem5 11818* | Lemma for rpnnen1 11820. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 13-Aug-2021.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem6 11819* | Lemma for rpnnen1 11820. (Contributed by Mario Carneiro, 12-May-2013.) (Revised by NM, 15-Aug-2021.) (Proof modification is discouraged.) |
Theorem | rpnnen1 11820 | One half of rpnnen 14956, 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 11819) 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 11026 and qex 11800, or nnexALT 11022 and qexALT 11803. 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.) |
Theorem | rpnnen1lem1OLD 11821* | Lemma for rpnnen1OLD 11825. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem1 11815 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem3OLD 11822* | Lemma for rpnnen1OLD 11825. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem3 11816 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem4OLD 11823* | Lemma for rpnnen1OLD 11825. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem4 11817 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | rpnnen1lem5OLD 11824* | Lemma for rpnnen1OLD 11825. (Contributed by Mario Carneiro, 12-May-2013.) Obsolete version of rpnnen1lem5 11818 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | rpnnen1OLD 11825* | One half of rpnnen 14956, where we show an injection from the real numbers to sequences of rational numbers. Specifically, we map a real number to the sequence 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. (Contributed by Mario Carneiro, 13-May-2013.) (Revised by Mario Carneiro, 16-Jun-2013.) Obsolete version of rpnnen1 11820 as of 13-Aug-2021. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | reexALT 11826 | Alternate proof of reex 10027. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 23-Aug-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | cnref1o 11827* | There is a natural one-to-one mapping from to , where we map to . In our construction of the complex numbers, this is in fact our definition of (see df-c 9942), 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.) |
Theorem | cnexALT 11828 | The set of complex numbers exists. This theorem shows that ax-cnex 9992 is redundant if we assume ax-rep 4771. See also ax-cnex 9992. (Contributed by NM, 30-Jul-2004.) (Revised by Mario Carneiro, 16-Jun-2013.) (Proof modification is discouraged.) (New usage is discouraged.) |
Theorem | xrex 11829 | The set of extended reals exists. (Contributed by NM, 24-Dec-2006.) |
Theorem | addex 11830 | The addition operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Theorem | mulex 11831 | The multiplication operation is a set. (Contributed by NM, 19-Oct-2004.) (Revised by Mario Carneiro, 17-Nov-2014.) |
Syntax | crp 11832 | Extend class notation to include the class of positive reals. |
Definition | df-rp 11833 | Define the set of positive reals. Definition of positive numbers in [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
Theorem | elrp 11834 | Membership in the set of positive reals. (Contributed by NM, 27-Oct-2007.) |
Theorem | elrpii 11835 | Membership in the set of positive reals. (Contributed by NM, 23-Feb-2008.) |
Theorem | 1rp 11836 | 1 is a positive real. (Contributed by Jeff Hankins, 23-Nov-2008.) |
Theorem | 2rp 11837 | 2 is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | 3rp 11838 | 3 is a positive real. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | rpre 11839 | A positive real is a real. (Contributed by NM, 27-Oct-2007.) |
Theorem | rpxr 11840 | A positive real is an extended real. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Theorem | rpcn 11841 | A positive real is a complex number. (Contributed by NM, 11-Nov-2008.) |
Theorem | nnrp 11842 | A positive integer is a positive real. (Contributed by NM, 28-Nov-2008.) |
Theorem | rpssre 11843 | The positive reals are a subset of the reals. (Contributed by NM, 24-Feb-2008.) |
Theorem | rpgt0 11844 | A positive real is greater than zero. (Contributed by FL, 27-Dec-2007.) |
Theorem | rpge0 11845 | A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008.) |
Theorem | rpregt0 11846 | A positive real is a positive real number. (Contributed by NM, 11-Nov-2008.) (Revised by Mario Carneiro, 31-Jan-2014.) |
Theorem | rprege0 11847 | A positive real is a nonnegative real number. (Contributed by Mario Carneiro, 31-Jan-2014.) |
Theorem | rpne0 11848 | A positive real is nonzero. (Contributed by NM, 18-Jul-2008.) |
Theorem | rprene0 11849 | A positive real is a nonzero real number. (Contributed by NM, 11-Nov-2008.) |
Theorem | rpcnne0 11850 | A positive real is a nonzero complex number. (Contributed by NM, 11-Nov-2008.) |
Theorem | rpcndif0 11851 | A positive real number is a complex number not being 0. (Contributed by AV, 29-May-2020.) |
Theorem | ralrp 11852 | Quantification over positive reals. (Contributed by NM, 12-Feb-2008.) |
Theorem | rexrp 11853 | Quantification over positive reals. (Contributed by Mario Carneiro, 21-May-2014.) |
Theorem | rpaddcl 11854 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
Theorem | rpmulcl 11855 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
Theorem | rpdivcl 11856 | Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007.) |
Theorem | rpreccl 11857 | Closure law for reciprocation of positive reals. (Contributed by Jeff Hankins, 23-Nov-2008.) |
Theorem | rphalfcl 11858 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 31-Jan-2014.) |
Theorem | rpgecl 11859 | A number greater or equal to a positive real is positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rphalflt 11860 | Half of a positive real is less than the original number. (Contributed by Mario Carneiro, 21-May-2014.) |
Theorem | rerpdivcl 11861 | Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008.) |
Theorem | ge0p1rp 11862 | A nonnegative number plus one is a positive number. (Contributed by Mario Carneiro, 5-Oct-2015.) |
Theorem | rpneg 11863 | Either a nonzero real or its negation is a positive real, but not both. Axiom 8 of [Apostol] p. 20. (Contributed by NM, 7-Nov-2008.) |
Theorem | negelrp 11864 | Elementhood of a negation in the positive real numbers. (Contributed by Thierry Arnoux, 19-Sep-2018.) |
Theorem | 0nrp 11865 | Zero is not a positive real. Axiom 9 of [Apostol] p. 20. (Contributed by NM, 27-Oct-2007.) |
Theorem | ltsubrp 11866 | Subtracting a positive real from another number decreases it. (Contributed by FL, 27-Dec-2007.) |
Theorem | ltaddrp 11867 | Adding a positive number to another number increases it. (Contributed by FL, 27-Dec-2007.) |
Theorem | difrp 11868 | Two ways to say one number is less than another. (Contributed by Mario Carneiro, 21-May-2014.) |
Theorem | elrpd 11869 | Membership in the set of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | nnrpd 11870 | A positive integer is a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | zgt1rpn0n1 11871 | An integer greater than 1 is a positive real number not equal to 0 or 1. Useful for working with integer logarithm bases (which is a common case, e.g. base 2, base 3 or base 10). (Contributed by Thierry Arnoux, 26-Sep-2017.) |
Theorem | rpred 11872 | A positive real is a real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpxrd 11873 | A positive real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpcnd 11874 | A positive real is a complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpgt0d 11875 | A positive real is greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpge0d 11876 | A positive real is greater than or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpne0d 11877 | A positive real is nonzero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpregt0d 11878 | A positive real is real and greater than zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rprege0d 11879 | A positive real is real and greater or equal to zero. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rprene0d 11880 | A positive real is a nonzero real number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpcnne0d 11881 | A positive real is a nonzero complex number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpreccld 11882 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rprecred 11883 | Closure law for reciprocation of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rphalfcld 11884 | Closure law for half of a positive real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | reclt1d 11885 | The reciprocal of a positive number less than 1 is greater than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | recgt1d 11886 | The reciprocal of a positive number greater than 1 is less than 1. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpaddcld 11887 | Closure law for addition of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpmulcld 11888 | Closure law for multiplication of positive reals. Part of Axiom 7 of [Apostol] p. 20. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rpdivcld 11889 | Closure law for division of positive reals. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltrecd 11890 | The reciprocal of both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lerecd 11891 | The reciprocal of both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltrec1d 11892 | Reciprocal swap in a 'less than' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lerec2d 11893 | Reciprocal swap in a 'less than or equal to' relation. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lediv2ad 11894 | Division of both sides of 'less than or equal to' into a nonnegative number. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ltdiv2d 11895 | Division of a positive number by both sides of 'less than'. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | lediv2d 11896 | Division of a positive number by both sides of 'less than or equal to'. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | ledivdivd 11897 | Invert ratios of positive numbers and swap their ordering. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | divge1 11898 | The ratio of a number over a smaller positive number is larger than 1. (Contributed by Glauco Siliprandi, 5-Apr-2020.) |
Theorem | divlt1lt 11899 | A real number divided by a positive real number is less than 1 iff the real number is less than the positive real number. (Contributed by AV, 25-May-2020.) |
Theorem | divle1le 11900 | A real number divided by a positive real number is less than or equal to 1 iff the real number is less than or equal to the positive real number. (Contributed by AV, 29-Jun-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |