Home | Intuitionistic Logic Explorer Theorem List (p. 69 of 95) | < 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 | ||
Axiom | ax-pre-mulext 6801 |
Strong extensionality of multiplication (expressed in terms of ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 6772
(Contributed by Jim Kingdon, 18-Feb-2020.) |
Axiom | ax-arch 6802* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 6773.
This axiom should not be used directly; instead use arch 7954 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
Theorem | cnex 6803 | Alias for ax-cnex 6774. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | addcl 6804 | Alias for ax-addcl 6779, for naming consistency with addcli 6829. Use this theorem instead of ax-addcl 6779 or axaddcl 6750. (Contributed by NM, 10-Mar-2008.) |
Theorem | readdcl 6805 | Alias for ax-addrcl 6780, for naming consistency with readdcli 6838. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcl 6806 | Alias for ax-mulcl 6781, for naming consistency with mulcli 6830. (Contributed by NM, 10-Mar-2008.) |
Theorem | remulcl 6807 | Alias for ax-mulrcl 6782, for naming consistency with remulcli 6839. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcom 6808 | Alias for ax-mulcom 6784, for naming consistency with mulcomi 6831. (Contributed by NM, 10-Mar-2008.) |
Theorem | addass 6809 | Alias for ax-addass 6785, for naming consistency with addassi 6833. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulass 6810 | Alias for ax-mulass 6786, for naming consistency with mulassi 6834. (Contributed by NM, 10-Mar-2008.) |
Theorem | adddi 6811 | Alias for ax-distr 6787, for naming consistency with adddii 6835. (Contributed by NM, 10-Mar-2008.) |
Theorem | recn 6812 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Theorem | reex 6813 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | reelprrecn 6814 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | cnelprrecn 6815 | Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | adddir 6816 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
Theorem | 0cn 6817 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
Theorem | 0cnd 6818 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | c0ex 6819 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1ex 6820 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | cnre 6821* | Alias for ax-cnre 6794, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Theorem | mulid1 6822 | is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mulid2 6823 | Identity law for multiplication. Note: see mulid1 6822 for commuted version. (Contributed by NM, 8-Oct-1999.) |
Theorem | 1re 6824 | is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
Theorem | 0re 6825 | is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | 0red 6826 | is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1i 6827 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | mulid2i 6828 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | addcli 6829 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcli 6830 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomi 6831 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomli 6832 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | addassi 6833 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulassi 6834 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | adddii 6835 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
Theorem | adddiri 6836 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
Theorem | recni 6837 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Theorem | readdcli 6838 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | remulcli 6839 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | 1red 6840 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 1cnd 6841 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1d 6842 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulid2d 6843 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcld 6844 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcld 6845 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcomd 6846 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addassd 6847 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulassd 6848 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddid 6849 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddird 6850 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | recnd 6851 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
Theorem | readdcld 6852 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | remulcld 6853 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Syntax | cpnf 6854 | Plus infinity. |
Syntax | cmnf 6855 | Minus infinity. |
Syntax | cxr 6856 | The set of extended reals (includes plus and minus infinity). |
Syntax | clt 6857 | 'Less than' predicate (extended to include the extended reals). |
Syntax | cle 6858 | Extend wff notation to include the 'less than or equal to' relation. |
Definition | df-pnf 6859 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that
be a set not in and
different from
(df-mnf 6860). 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 6864
and mnfnre 6865, 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 6860 | 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 6865). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
Definition | df-xr 6861 | 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 6862* | 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 6863 | Define 'less than or equal to' on the extended real subset of complex numbers. (Contributed by NM, 13-Oct-2005.) |
Theorem | pnfnre 6864 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | mnfnre 6865 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | ressxr 6866 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | rexpssxrxp 6867 | 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 6868 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Theorem | 0xr 6869 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | renepnf 6870 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | renemnf 6871 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | rexrd 6872 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renepnfd 6873 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renemnfd 6874 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | rexri 6875 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
Theorem | renfdisj 6876 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltrelxr 6877 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | ltrel 6878 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
Theorem | lerelxr 6879 | 'Less than or equal' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | lerel 6880 | 'Less or equal to' is a relation. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 28-Apr-2015.) |
Theorem | xrlenlt 6881 | 'Less than or equal to' expressed in terms of 'less than', for extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | ltxrlt 6882 | 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 6883 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltirr 6795 with ordering on the extended reals. New proofs should use ltnr 6892 instead for naming consistency. (New usage is discouraged.) (Contributed by Jim Kingdon, 15-Jan-2020.) |
Theorem | axltwlin 6884 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-ltwlin 6796 with ordering on the extended reals. (Contributed by Jim Kingdon, 15-Jan-2020.) |
Theorem | axlttrn 6885 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This restates ax-pre-lttrn 6797 with ordering on the extended reals. New proofs should use lttr 6889 instead for naming consistency. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axltadd 6886 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-ltadd 6799 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | axapti 6887 | Apartness of reals is tight. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-apti 6798 with ordering on the extended reals.) (Contributed by Jim Kingdon, 29-Jan-2020.) |
Theorem | axmulgt0 6888 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. (This restates ax-pre-mulgt0 6800 with ordering on the extended reals.) (Contributed by NM, 13-Oct-2005.) |
Theorem | lttr 6889 | Alias for axlttrn 6885, for naming consistency with lttri 6919. New proofs should generally use this instead of ax-pre-lttrn 6797. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulgt0 6890 | The product of two positive numbers is positive. (Contributed by NM, 10-Mar-2008.) |
Theorem | lenlt 6891 | '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 6892 | 'Less than' is irreflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltso 6893 | 'Less than' is a strict ordering. (Contributed by NM, 19-Jan-1997.) |
Theorem | gtso 6894 | 'Greater than' is a strict ordering. (Contributed by JJ, 11-Oct-2018.) |
Theorem | lttri3 6895 | Tightness of real apartness. (Contributed by NM, 5-May-1999.) |
Theorem | letri3 6896 | Tightness of real apartness. (Contributed by NM, 14-May-1999.) |
Theorem | ltleletr 6897 | Transitive law, weaker form of . (Contributed by AV, 14-Oct-2018.) |
Theorem | letr 6898 | Transitive law. (Contributed by NM, 12-Nov-1999.) |
Theorem | leid 6899 | 'Less than or equal to' is reflexive. (Contributed by NM, 18-Aug-1999.) |
Theorem | ltne 6900 | 'Less than' implies not equal. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 16-Sep-2015.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |