Home | Intuitionistic Logic Explorer Theorem List (p. 79 of 133) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > ILE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Type | Label | Description |
---|---|---|
Statement | ||
Syntax | cle 7801 | Extend wff notation to include the 'less than or equal to' relation. |
Definition | df-pnf 7802 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that
be a set not in and
different from
(df-mnf 7803). We use to
make it independent of the
construction of , and Cantor's Theorem will show that it is
different from any member of and therefore . See pnfnre 7807
and mnfnre 7808, and we'll also be able to prove .
A simpler possibility is to define as and as , but that approach requires the Axiom of Regularity to show that and are different from each other and from all members of . (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
Definition | df-mnf 7803 | Define minus infinity as the power set of plus infinity. Note that the definition is arbitrary, requiring only that be a set not in and different from (see mnfnre 7808). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
Definition | df-xr 7804 | Define the set of extended reals that includes plus and minus infinity. Definition 12-3.1 of [Gleason] p. 173. (Contributed by NM, 13-Oct-2005.) |
Definition | df-ltxr 7805* | Define 'less than' on the set of extended reals. Definition 12-3.1 of [Gleason] p. 173. Note that in our postulates for complex numbers, is primitive and not necessarily a relation on . (Contributed by NM, 13-Oct-2005.) |
Definition | df-le 7806 | Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.) |
Theorem | pnfnre 7807 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | mnfnre 7808 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | ressxr 7809 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | rexpssxrxp 7810 | The Cartesian product of standard reals are a subset of the Cartesian product of extended reals (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | rexr 7811 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Theorem | 0xr 7812 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | renepnf 7813 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | renemnf 7814 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | rexrd 7815 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renepnfd 7816 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renemnfd 7817 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | pnfxr 7818 | Plus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) |
Theorem | pnfex 7819 | Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | pnfnemnf 7820 | Plus and minus infinity are different elements of . (Contributed by NM, 14-Oct-2005.) |
Theorem | mnfnepnf 7821 | Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | mnfxr 7822 | Minus infinity belongs to the set of extended reals. (Contributed by NM, 13-Oct-2005.) (Proof shortened by Anthony Hart, 29-Aug-2011.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | rexri 7823 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
Theorem | renfdisj 7824 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltrelxr 7825 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | ltrel 7826 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
Theorem | lerelxr 7827 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | lerel 7828 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | xrlenlt 7829 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | ltxrlt 7830 | The standard less-than and the extended real less-than are identical when restricted to the non-extended reals . (Contributed by NM, 13-Oct-2005.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | axltirr 7831 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7732 with ordering on the extended reals. New proofs should use ltnr 7841 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) |
Theorem | axltwlin 7832 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7733 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) |
Theorem | axlttrn 7833 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7734 with ordering on the extended reals. New proofs should use lttr 7838 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axltadd 7834 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7736 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axapti 7835 | Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7735 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.) |
Theorem | axmulgt0 7836 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7737 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axsuploc 7837* | An inhabited, bounded-above, located set of reals has a supremum. Axiom for real and complex numbers, derived from ZF set theory. (This restates ax-pre-suploc 7741 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
Theorem | lttr 7838 | Alias for axlttrn 7833, for naming consistency with lttri 7868. New proofs should generally use this instead of ax-pre-lttrn 7734. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulgt0 7839 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
Theorem | lenlt 7840 | 'Less than or equal to' expressed in terms of 'less than'. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 13-May-1999.) |
Theorem | ltnr 7841 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltso 7842 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
Theorem | gtso 7843 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
Theorem | lttri3 7844 | Tightness of real apartness. (Contributed by NM, 5-May-1999.) |
Theorem | letri3 7845 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | ltleletr 7846 | Transitive law, weaker form of . (Contributed by AV, 14-Oct-2018.) |
Theorem | letr 7847 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
Theorem | leid 7848 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltne 7849 | 'Less than' implies not equal. See also ltap 8395 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
Theorem | ltnsym 7850 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
Theorem | ltle 7851 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
Theorem | lelttr 7852 | Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.) |
Theorem | ltletr 7853 | Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.) |
Theorem | ltnsym2 7854 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | eqle 7855 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
Theorem | ltnri 7856 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | eqlei 7857 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
Theorem | eqlei2 7858 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
Theorem | gtneii 7859 | 'Less than' implies not equal. See also gtapii 8396 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.) |
Theorem | ltneii 7860 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
Theorem | lttri3i 7861 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | letri3i 7862 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | ltnsymi 7863 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
Theorem | lenlti 7864 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
Theorem | ltlei 7865 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
Theorem | ltleii 7866 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
Theorem | ltnei 7867 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
Theorem | lttri 7868 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
Theorem | lelttri 7869 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
Theorem | ltletri 7870 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
Theorem | letri 7871 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
Theorem | le2tri3i 7872 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
Theorem | mulgt0i 7873 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | mulgt0ii 7874 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
Theorem | ltnrd 7875 | 'Less than' is irreflexive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | gtned 7876 | 'Less than' implies not equal. See also gtapd 8399 which is the same but for apartness. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltned 7877 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lttri3d 7878 | Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | letri3d 7879 | Tightness of real apartness. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | lenltd 7880 | 'Less than or equal to' in terms of 'less than'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltled 7881 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | ltnsymd 7882 | 'Less than' implies 'less than or equal to'. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | nltled 7883 | 'Not less than ' implies 'less than or equal to'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | lensymd 7884 | 'Less than or equal to' implies 'not less than'. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | mulgt0d 7885 | The product of two positive numbers is positive. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | letrd 7886 | Transitive law deduction for 'less than or equal to'. (Contributed by NM, 20-May-2005.) |
Theorem | lelttrd 7887 | Transitive law deduction for 'less than or equal to', 'less than'. (Contributed by NM, 8-Jan-2006.) |
Theorem | lttrd 7888 | Transitive law deduction for 'less than'. (Contributed by NM, 9-Jan-2006.) |
Theorem | 0lt1 7889 | 0 is less than 1. Theorem I.21 of [Apostol] p. 20. Part of definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 17-Jan-1997.) |
Theorem | ltntri 7890 | Negative trichotomy property for real numbers. It is well known that we cannot prove real number trichotomy, . Does that mean there is a pair of real numbers where none of those hold (that is, where we can refute each of those three relationships)? Actually, no, as shown here. This is another example of distinguishing between being unable to prove something, or being able to refute it. (Contributed by Jim Kingdon, 13-Aug-2023.) |
Theorem | mul12 7891 | Commutative/associative law for multiplication. (Contributed by NM, 30-Apr-2005.) |
Theorem | mul32 7892 | Commutative/associative law. (Contributed by NM, 8-Oct-1999.) |
Theorem | mul31 7893 | Commutative/associative law. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mul4 7894 | Rearrangement of 4 factors. (Contributed by NM, 8-Oct-1999.) |
Theorem | muladd11 7895 | A simple product of sums expansion. (Contributed by NM, 21-Feb-2005.) |
Theorem | 1p1times 7896 | Two times a number. (Contributed by NM, 18-May-1999.) (Revised by Mario Carneiro, 27-May-2016.) |
Theorem | peano2cn 7897 | A theorem for complex numbers analogous the second Peano postulate peano2 4509. (Contributed by NM, 17-Aug-2005.) |
Theorem | peano2re 7898 | A theorem for reals analogous the second Peano postulate peano2 4509. (Contributed by NM, 5-Jul-2005.) |
Theorem | addcom 7899 | Addition commutes. (Contributed by Jim Kingdon, 17-Jan-2020.) |
Theorem | addid1 7900 | is an additive identity. (Contributed by Jim Kingdon, 16-Jan-2020.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |