Home | Intuitionistic Logic Explorer Theorem List (p. 80 of 139) | < 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 | ||
Theorem | adddiri 7901 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
Theorem | recni 7902 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Theorem | readdcli 7903 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | remulcli 7904 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | 1red 7905 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 1cnd 7906 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1d 7907 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulid2d 7908 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcld 7909 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcld 7910 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcomd 7911 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addassd 7912 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulassd 7913 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddid 7914 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddird 7915 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddirp1d 7916 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | joinlmuladdmuld 7917 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
Theorem | recnd 7918 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
Theorem | readdcld 7919 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | remulcld 7920 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Syntax | cpnf 7921 | Plus infinity. |
Syntax | cmnf 7922 | Minus infinity. |
Syntax | cxr 7923 | The set of extended reals (includes plus and minus infinity). |
Syntax | clt 7924 | 'Less than' predicate (extended to include the extended reals). |
Syntax | cle 7925 | Extend wff notation to include the 'less than or equal to' relation. |
Definition | df-pnf 7926 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that
be a set not in and
different from
(df-mnf 7927). 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 7931
and mnfnre 7932, 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 7927 | 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 7932). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
Definition | df-xr 7928 | 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 7929* | 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 7930 | Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.) |
Theorem | pnfnre 7931 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | mnfnre 7932 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | ressxr 7933 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | rexpssxrxp 7934 | 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 7935 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Theorem | 0xr 7936 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | renepnf 7937 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | renemnf 7938 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | rexrd 7939 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renepnfd 7940 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renemnfd 7941 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | pnfxr 7942 | 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 7943 | Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | pnfnemnf 7944 | Plus and minus infinity are different elements of . (Contributed by NM, 14-Oct-2005.) |
Theorem | mnfnepnf 7945 | Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | mnfxr 7946 | 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 7947 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
Theorem | 1xr 7948 | is an extended real number. (Contributed by Glauco Siliprandi, 2-Jan-2022.) |
Theorem | renfdisj 7949 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltrelxr 7950 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | ltrel 7951 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
Theorem | lerelxr 7952 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | lerel 7953 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | xrlenlt 7954 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | ltxrlt 7955 | 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 7956 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 7856 with ordering on the extended reals. New proofs should use ltnr 7966 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) |
Theorem | axltwlin 7957 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 7857 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) |
Theorem | axlttrn 7958 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 7858 with ordering on the extended reals. New proofs should use lttr 7963 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axltadd 7959 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 7860 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axapti 7960 | Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 7859 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.) |
Theorem | axmulgt0 7961 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 7861 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axsuploc 7962* | 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 7865 with ordering on the extended reals.) (Contributed by Jim Kingdon, 30-Jan-2024.) |
Theorem | lttr 7963 | Alias for axlttrn 7958, for naming consistency with lttri 7994. New proofs should generally use this instead of ax-pre-lttrn 7858. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulgt0 7964 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
Theorem | lenlt 7965 | '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 7966 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltso 7967 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
Theorem | gtso 7968 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
Theorem | lttri3 7969 | Tightness of real apartness. (Contributed by NM, 5-May-1999.) |
Theorem | letri3 7970 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | ltleletr 7971 | Transitive law, weaker form of . (Contributed by AV, 14-Oct-2018.) |
Theorem | letr 7972 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
Theorem | leid 7973 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltne 7974 | 'Less than' implies not equal. See also ltap 8522 which is the same but for apartness. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
Theorem | ltnsym 7975 | 'Less than' is not symmetric. (Contributed by NM, 8-Jan-2002.) |
Theorem | eqlelt 7976 | Equality in terms of 'less than or equal to', 'less than'. (Contributed by NM, 7-Apr-2001.) |
Theorem | ltle 7977 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 25-Aug-1999.) |
Theorem | lelttr 7978 | Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 23-May-1999.) |
Theorem | ltletr 7979 | Transitive law. Part of Definition 11.2.7(vi) of [HoTT], p. (varies). (Contributed by NM, 25-Aug-1999.) |
Theorem | ltnsym2 7980 | 'Less than' is antisymmetric and irreflexive. (Contributed by NM, 13-Aug-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | eqle 7981 | Equality implies 'less than or equal to'. (Contributed by NM, 4-Apr-2005.) |
Theorem | ltnri 7982 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | eqlei 7983 | Equality implies 'less than or equal to'. (Contributed by NM, 23-May-1999.) (Revised by Alexander van der Vekens, 20-Mar-2018.) |
Theorem | eqlei2 7984 | Equality implies 'less than or equal to'. (Contributed by Alexander van der Vekens, 20-Mar-2018.) |
Theorem | gtneii 7985 | 'Less than' implies not equal. See also gtapii 8523 which is the same for apartness. (Contributed by Mario Carneiro, 30-Sep-2013.) |
Theorem | ltneii 7986 | 'Greater than' implies not equal. (Contributed by Mario Carneiro, 16-Sep-2015.) |
Theorem | lttri3i 7987 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | letri3i 7988 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | ltnsymi 7989 | 'Less than' is not symmetric. (Contributed by NM, 6-May-1999.) |
Theorem | lenlti 7990 | 'Less than or equal to' in terms of 'less than'. (Contributed by NM, 24-May-1999.) |
Theorem | ltlei 7991 | 'Less than' implies 'less than or equal to'. (Contributed by NM, 14-May-1999.) |
Theorem | ltleii 7992 | 'Less than' implies 'less than or equal to' (inference). (Contributed by NM, 22-Aug-1999.) |
Theorem | ltnei 7993 | 'Less than' implies not equal. (Contributed by NM, 28-Jul-1999.) |
Theorem | lttri 7994 | 'Less than' is transitive. Theorem I.17 of [Apostol] p. 20. (Contributed by NM, 14-May-1999.) |
Theorem | lelttri 7995 | 'Less than or equal to', 'less than' transitive law. (Contributed by NM, 14-May-1999.) |
Theorem | ltletri 7996 | 'Less than', 'less than or equal to' transitive law. (Contributed by NM, 14-May-1999.) |
Theorem | letri 7997 | 'Less than or equal to' is transitive. (Contributed by NM, 14-May-1999.) |
Theorem | le2tri3i 7998 | Extended trichotomy law for 'less than or equal to'. (Contributed by NM, 14-Aug-2000.) |
Theorem | mulgt0i 7999 | The product of two positive numbers is positive. (Contributed by NM, 16-May-1999.) |
Theorem | mulgt0ii 8000 | The product of two positive numbers is positive. (Contributed by NM, 18-May-1999.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |