Home | Intuitionistic Logic Explorer Theorem List (p. 71 of 106) | < 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 | axmulrcl 7001 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 7041 be used later. Instead, in most cases use remulcl 7067. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
Theorem | axaddcom 7002 |
Addition commutes. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly, nor should the proven axiom ax-addcom 7042 be used later.
Instead, use addcom 7211.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on real number trichotomy and it is not known whether it is possible to prove this from the other axioms without it. (Contributed by Jim Kingdon, 17-Jan-2020.) (New usage is discouraged.) |
Theorem | axmulcom 7003 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 7043 be used later. Instead, use mulcom 7068. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
Theorem | axaddass 7004 | Addition of complex numbers is associative. This theorem transfers the associative laws for the real and imaginary signed real components of complex number pairs, to complex number addition itself. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 7044 be used later. Instead, use addass 7069. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axmulass 7005 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 7045. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
Theorem | axdistr 7006 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 7046 be used later. Instead, use adddi 7071. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axi2m1 7007 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 7047. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
Theorem | ax0lt1 7008 |
0 is less than 1. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-0lt1 7048.
The version of this axiom in the Metamath Proof Explorer reads ; here we change it to . The proof of from in the Metamath Proof Explorer (accessed 12-Jan-2020) relies on real number trichotomy. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | ax1rid 7009 | is an identity element for real multiplication. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 7049. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
Theorem | ax0id 7010 |
is an identity element
for real addition. Axiom for real and
complex numbers, derived from set theory. This construction-dependent
theorem should not be referenced directly; instead, use ax-0id 7050.
In the Metamath Proof Explorer this is not a complex number axiom but is instead proved from other axioms. That proof relies on excluded middle and it is not known whether it is possible to prove this from the other axioms without excluded middle. (Contributed by Jim Kingdon, 16-Jan-2020.) (New usage is discouraged.) |
Theorem | axrnegex 7011* | Existence of negative of real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 7051. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
Theorem | axprecex 7012* |
Existence of positive reciprocal of positive real number. Axiom for
real and complex numbers, derived from set theory. This
construction-dependent theorem should not be referenced directly;
instead, use ax-precex 7052.
In treatments which assume excluded middle, the condition is generally replaced by , and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.) |
Theorem | axcnre 7013* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 7053. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-ltirr 7014 | Real number less-than is irreflexive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltirr 7054. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-ltwlin 7015 | Real number less-than is weakly linear. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltwlin 7055. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-lttrn 7016 | Ordering on reals is transitive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 7056. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
Theorem | axpre-apti 7017 |
Apartness of reals is tight. Axiom for real and complex numbers,
derived from set theory. This construction-dependent theorem should not
be referenced directly; instead, use ax-pre-apti 7057.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-ltadd 7018 | Ordering property of addition on reals. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 7058. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulgt0 7019 | The product of two positive reals is positive. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 7059. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulext 7020 |
Strong extensionality of multiplication (expressed in terms of
).
Axiom for real and complex numbers, derived from set theory.
This construction-dependent theorem should not be referenced directly;
instead, use ax-pre-mulext 7060.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
Theorem | rereceu 7021* | The reciprocal from axprecex 7012 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recriota 7022* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | axarch 7023* |
Archimedean axiom. The Archimedean property is more naturally stated
once we have defined . Unless we find another way to state it,
we'll just use the right hand side of dfnn2 7992 in stating what we mean by
"natural number" in the context of this axiom.
This construction-dependent theorem should not be referenced directly; instead, use ax-arch 7061. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
Theorem | peano5nnnn 7024* | Peano's inductive postulate. This is a counterpart to peano5nni 7993 designed for real number axioms which involve natural numbers (notably, axcaucvg 7032). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nnindnn 7025* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8006 designed for real number axioms which involve natural numbers (notably, axcaucvg 7032). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nntopi 7026* | Mapping from to . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | axcaucvglemcl 7027* | Lemma for axcaucvg 7032. Mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemf 7028* | Lemma for axcaucvg 7032. Mapping to and yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemval 7029* | Lemma for axcaucvg 7032. Value of sequence when mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemcau 7030* | Lemma for axcaucvg 7032. The result of mapping to and satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemres 7031* | Lemma for axcaucvg 7032. Mapping the limit from and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvg 7032* |
Real number completeness axiom. A Cauchy sequence with a modulus of
convergence converges. This is basically Corollary 11.2.13 of [HoTT],
p. (varies). The HoTT book theorem has a modulus of convergence
(that is, a rate of convergence) specified by (11.2.9) in HoTT whereas
this theorem fixes the rate of convergence to say that all terms after
the nth term must be within of the nth term (it should
later
be able to prove versions of this theorem with a different fixed rate
or a modulus of convergence supplied as a hypothesis).
Because we are stating this axiom before we have introduced notations for or division, we use for the natural numbers and express a reciprocal in terms of . This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 7062. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
Axiom | ax-cnex 7033 | The complex numbers form a set. Proofs should normally use cnex 7063 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-resscn 7034 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6994. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1cn 7035 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6995. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1re 7036 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6996. Proofs should use 1re 7084 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
Axiom | ax-icn 7037 | is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6997. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-addcl 7038 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 6998. Proofs should normally use addcl 7064 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addrcl 7039 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 6999. Proofs should normally use readdcl 7065 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulcl 7040 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7000. Proofs should normally use mulcl 7066 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulrcl 7041 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7001. Proofs should normally use remulcl 7067 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addcom 7042 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7002. Proofs should normally use addcom 7211 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
Axiom | ax-mulcom 7043 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7003. Proofs should normally use mulcom 7068 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addass 7044 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7004. Proofs should normally use addass 7069 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulass 7045 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7005. Proofs should normally use mulass 7070 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-distr 7046 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7006. Proofs should normally use adddi 7071 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-i2m1 7047 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7007. (Contributed by NM, 29-Jan-1995.) |
Theorem | ax-0lt1 7048 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7008. Proofs should normally use 0lt1 7202 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-1rid 7049 | is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7009. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0id 7050 |
is an identity element
for real addition. Axiom for real and
complex numbers, justified by theorem ax0id 7010.
Proofs should normally use addid1 7212 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
Axiom | ax-rnegex 7051* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7011. (Contributed by Eric Schmidt, 21-May-2007.) |
Axiom | ax-precex 7052* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7012. (Contributed by Jim Kingdon, 6-Feb-2020.) |
Axiom | ax-cnre 7053* | A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom for real and complex numbers, justified by theorem axcnre 7013. For naming consistency, use cnre 7081 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
Axiom | ax-pre-ltirr 7054 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7054. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-ltwlin 7055 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7015. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-lttrn 7056 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7016. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-apti 7057 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7017. (Contributed by Jim Kingdon, 29-Jan-2020.) |
Axiom | ax-pre-ltadd 7058 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7018. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulgt0 7059 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7019. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulext 7060 |
Strong extensionality of multiplication (expressed in terms of ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7020
(Contributed by Jim Kingdon, 18-Feb-2020.) |
Axiom | ax-arch 7061* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7023.
This axiom should not be used directly; instead use arch 8236 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
Axiom | ax-caucvg 7062* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7032.
A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within of the nth term. This axiom should not be used directly; instead use caucvgre 9808 (which is the same, but stated in terms of the and notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) |
Theorem | cnex 7063 | Alias for ax-cnex 7033. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | addcl 7064 | Alias for ax-addcl 7038, for naming consistency with addcli 7089. Use this theorem instead of ax-addcl 7038 or axaddcl 6998. (Contributed by NM, 10-Mar-2008.) |
Theorem | readdcl 7065 | Alias for ax-addrcl 7039, for naming consistency with readdcli 7098. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcl 7066 | Alias for ax-mulcl 7040, for naming consistency with mulcli 7090. (Contributed by NM, 10-Mar-2008.) |
Theorem | remulcl 7067 | Alias for ax-mulrcl 7041, for naming consistency with remulcli 7099. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcom 7068 | Alias for ax-mulcom 7043, for naming consistency with mulcomi 7091. (Contributed by NM, 10-Mar-2008.) |
Theorem | addass 7069 | Alias for ax-addass 7044, for naming consistency with addassi 7093. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulass 7070 | Alias for ax-mulass 7045, for naming consistency with mulassi 7094. (Contributed by NM, 10-Mar-2008.) |
Theorem | adddi 7071 | Alias for ax-distr 7046, for naming consistency with adddii 7095. (Contributed by NM, 10-Mar-2008.) |
Theorem | recn 7072 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Theorem | reex 7073 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | reelprrecn 7074 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | cnelprrecn 7075 | 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 7076 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
Theorem | 0cn 7077 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
Theorem | 0cnd 7078 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | c0ex 7079 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1ex 7080 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | cnre 7081* | Alias for ax-cnre 7053, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Theorem | mulid1 7082 | is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mulid2 7083 | Identity law for multiplication. Note: see mulid1 7082 for commuted version. (Contributed by NM, 8-Oct-1999.) |
Theorem | 1re 7084 | is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
Theorem | 0re 7085 | is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | 0red 7086 | is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1i 7087 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | mulid2i 7088 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | addcli 7089 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcli 7090 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomi 7091 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomli 7092 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | addassi 7093 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulassi 7094 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | adddii 7095 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
Theorem | adddiri 7096 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
Theorem | recni 7097 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Theorem | readdcli 7098 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | remulcli 7099 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | 1red 7100 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |