Home | Metamath
Proof Explorer Theorem List (p. 101 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 | ||
Axiom | ax-addass 10001 | Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by theorem axaddass 9977. Proofs should normally use addass 10023 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulass 10002 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by theorem axmulass 9978. Proofs should normally use mulass 10024 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-distr 10003 | Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9979. Proofs should normally use adddi 10025 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-i2m1 10004 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by theorem axi2m1 9980. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-1ne0 10005 | 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 9981. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-1rid 10006 | is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9982. Weakened from the original axiom in the form of statement in mulid1 10037, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-rnegex 10007* | Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 9983. (Contributed by Eric Schmidt, 21-May-2007.) |
Axiom | ax-rrecex 10008* | Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by theorem axrrecex 9984. (Contributed by Eric Schmidt, 11-Apr-2007.) |
Axiom | ax-cnre 10009* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, justified by theorem axcnre 9985. For naming consistency, use cnre 10036 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
Axiom | ax-pre-lttri 10010 | Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by theorem axpre-lttri 9986. Note: The more general version for extended reals is axlttri 10109. Normally new proofs would use xrlttri 11972. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-lttrn 10011 | Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn 9987. Note: The more general version for extended reals is axlttrn 10110. Normally new proofs would use lttr 10114. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-ltadd 10012 | Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd 9988. Normally new proofs would use axltadd 10111. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulgt0 10013 | The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by theorem axpre-mulgt0 9989. Normally new proofs would use axmulgt0 10112. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-sup 10014* | A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by theorem axpre-sup 9990. Note: Normally new proofs would use axsup 10113. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-addf 10015 |
Addition is an operation on the complex numbers. This deprecated axiom is
provided for historical compatibility but is not a bona fide axiom for
complex numbers (independent of set theory) since it cannot be interpreted
as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific addcl 10018 should be used. Note that uses of ax-addf 10015 can
be eliminated by using the defined operation
in place of , from which
this axiom (with the defined operation in place of ) follows as a
theorem.
This axiom is justified by theorem axaddf 9966. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
Axiom | ax-mulf 10016 |
Multiplication is an operation on the complex numbers. This deprecated
axiom is provided for historical compatibility but is not a bona fide
axiom for complex numbers (independent of set theory) since it cannot be
interpreted as a first- or second-order statement (see
http://us.metamath.org/downloads/schmidt-cnaxioms.pdf).
It may be
deleted in the future and should be avoided for new theorems. Instead,
the less specific ax-mulcl 9998 should be used. Note that uses of ax-mulf 10016
can be eliminated by using the defined operation
in place of , from which
this axiom (with the defined operation in place of ) follows as a
theorem.
This axiom is justified by theorem axmulf 9967. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
Theorem | cnex 10017 | Alias for ax-cnex 9992. See also cnexALT 11828. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | addcl 10018 | Alias for ax-addcl 9996, for naming consistency with addcli 10044. Use this theorem instead of ax-addcl 9996 or axaddcl 9972. (Contributed by NM, 10-Mar-2008.) |
Theorem | readdcl 10019 | Alias for ax-addrcl 9997, for naming consistency with readdcli 10053. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcl 10020 | Alias for ax-mulcl 9998, for naming consistency with mulcli 10045. (Contributed by NM, 10-Mar-2008.) |
Theorem | remulcl 10021 | Alias for ax-mulrcl 9999, for naming consistency with remulcli 10054. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcom 10022 | Alias for ax-mulcom 10000, for naming consistency with mulcomi 10046. (Contributed by NM, 10-Mar-2008.) |
Theorem | addass 10023 | Alias for ax-addass 10001, for naming consistency with addassi 10048. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulass 10024 | Alias for ax-mulass 10002, for naming consistency with mulassi 10049. (Contributed by NM, 10-Mar-2008.) |
Theorem | adddi 10025 | Alias for ax-distr 10003, for naming consistency with adddii 10050. (Contributed by NM, 10-Mar-2008.) |
Theorem | recn 10026 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Theorem | reex 10027 | The real numbers form a set. See also reexALT 11826. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | reelprrecn 10028 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | cnelprrecn 10029 | Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | elimne0 10030 | Hypothesis for weak deduction theorem to eliminate . (Contributed by NM, 15-May-1999.) |
Theorem | adddir 10031 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
Theorem | 0cn 10032 | 0 is a complex number. See also 0cnALT 10270. (Contributed by NM, 19-Feb-2005.) |
Theorem | 0cnd 10033 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | c0ex 10034 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1ex 10035 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | cnre 10036* | Alias for ax-cnre 10009, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Theorem | mulid1 10037 | is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mulid2 10038 | Identity law for multiplication. Note: see mulid1 10037 for commuted version. (Contributed by NM, 8-Oct-1999.) |
Theorem | 1re 10039 | is a real number. This used to be one of our postulates for complex numbers, but Eric Schmidt discovered that it could be derived from a weaker postulate, ax-1cn 9994, by exploiting properties of the imaginary unit . (Contributed by Eric Schmidt, 11-Apr-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | 0re 10040 | is a real number. See also 0reALT 10378. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | 0red 10041 | is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1i 10042 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | mulid2i 10043 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | addcli 10044 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcli 10045 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomi 10046 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomli 10047 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | addassi 10048 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulassi 10049 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | adddii 10050 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
Theorem | adddiri 10051 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
Theorem | recni 10052 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Theorem | readdcli 10053 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | remulcli 10054 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | 1red 10055 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 1cnd 10056 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1d 10057 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulid2d 10058 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcld 10059 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcld 10060 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcomd 10061 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addassd 10062 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulassd 10063 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddid 10064 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddird 10065 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddirp1d 10066 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | joinlmuladdmuld 10067 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
Theorem | recnd 10068 | Deduction from real number to complex number. (Contributed by NM, 26-Oct-1999.) |
Theorem | readdcld 10069 | Closure law for addition of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | remulcld 10070 | Closure law for multiplication of reals. (Contributed by Mario Carneiro, 27-May-2016.) |
Syntax | cpnf 10071 | Plus infinity. |
Syntax | cmnf 10072 | Minus infinity. |
Syntax | cxr 10073 | The set of extended reals (includes plus and minus infinity). |
Syntax | clt 10074 | 'Less than' predicate (extended to include the extended reals). |
Syntax | cle 10075 | Extend wff notation to include the 'less than or equal to' relation. |
Definition | df-pnf 10076 |
Define plus infinity. Note that the definition is arbitrary, requiring
only that
be a set not in and
different from
(df-mnf 10077). 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 10081,
mnfnre 10082, and pnfnemnf 10094.
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 10077 | 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 10082 and pnfnemnf 10094). (Contributed by NM, 13-Oct-2005.) (New usage is discouraged.) |
Definition | df-xr 10078 | 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 10079* | 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 10080 | Define 'less than or equal to' on the extended real subset of complex numbers. Theorem leloe 10124 relates it to 'less than' for reals. (Contributed by NM, 13-Oct-2005.) |
Theorem | pnfnre 10081 | Plus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | mnfnre 10082 | Minus infinity is not a real number. (Contributed by NM, 13-Oct-2005.) |
Theorem | ressxr 10083 | The standard reals are a subset of the extended reals. (Contributed by NM, 14-Oct-2005.) |
Theorem | rexpssxrxp 10084 | 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 10085 | A standard real is an extended real. (Contributed by NM, 14-Oct-2005.) |
Theorem | 0xr 10086 | Zero is an extended real. (Contributed by Mario Carneiro, 15-Jun-2014.) |
Theorem | renepnf 10087 | No (finite) real equals plus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | renemnf 10088 | No real equals minus infinity. (Contributed by NM, 14-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | rexrd 10089 | A standard real is an extended real. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renepnfd 10090 | No (finite) real equals plus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | renemnfd 10091 | No real equals minus infinity. (Contributed by Mario Carneiro, 28-May-2016.) |
Theorem | pnfxr 10092 | 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 10093 | Plus infinity exists (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | pnfnemnf 10094 | Plus and minus infinity are different elements of . (Contributed by NM, 14-Oct-2005.) |
Theorem | mnfnepnf 10095 | Minus and plus infinity are different (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | mnfxr 10096 | 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 10097 | A standard real is an extended real (inference form.) (Contributed by David Moews, 28-Feb-2017.) |
Theorem | renfdisj 10098 | The reals and the infinities are disjoint. (Contributed by NM, 25-Oct-2005.) (Proof shortened by Andrew Salmon, 19-Nov-2011.) |
Theorem | ltrelxr 10099 | 'Less than' is a relation on extended reals. (Contributed by Mario Carneiro, 28-Apr-2015.) |
Theorem | ltrel 10100 | 'Less than' is a relation. (Contributed by NM, 14-Oct-2005.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |