Home | Intuitionistic Logic Explorer Theorem List (p. 78 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 | ||
Theorem | axpre-ltadd 7701 | 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 7743. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulgt0 7702 | 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 7744. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulext 7703 |
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 7745.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
Theorem | rereceu 7704* | The reciprocal from axprecex 7695 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recriota 7705* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | axarch 7706* |
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 8729 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 7746. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
Theorem | peano5nnnn 7707* | Peano's inductive postulate. This is a counterpart to peano5nni 8730 designed for real number axioms which involve natural numbers (notably, axcaucvg 7715). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nnindnn 7708* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8743 designed for real number axioms which involve natural numbers (notably, axcaucvg 7715). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nntopi 7709* | Mapping from to . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | axcaucvglemcl 7710* | Lemma for axcaucvg 7715. Mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemf 7711* | Lemma for axcaucvg 7715. Mapping to and yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemval 7712* | Lemma for axcaucvg 7715. Value of sequence when mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemcau 7713* | Lemma for axcaucvg 7715. The result of mapping to and satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemres 7714* | Lemma for axcaucvg 7715. Mapping the limit from and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvg 7715* |
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 7747. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
Theorem | axpre-suploclemres 7716* | Lemma for axpre-suploc 7717. The result. The proof just needs to define as basically the same set as (but expressed as a subset of rather than a subset of ), and apply suplocsr 7624. (Contributed by Jim Kingdon, 24-Jan-2024.) |
Theorem | axpre-suploc 7717* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 7748. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
Axiom | ax-cnex 7718 | The complex numbers form a set. Proofs should normally use cnex 7751 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-resscn 7719 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7675. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1cn 7720 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7676. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1re 7721 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7677. Proofs should use 1re 7772 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
Axiom | ax-icn 7722 | is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7678. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-addcl 7723 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7679. Proofs should normally use addcl 7752 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 7724 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7680. Proofs should normally use readdcl 7753 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulcl 7725 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7681. Proofs should normally use mulcl 7754 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulrcl 7726 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7682. Proofs should normally use remulcl 7755 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addcom 7727 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7685. Proofs should normally use addcom 7906 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
Axiom | ax-mulcom 7728 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7686. Proofs should normally use mulcom 7756 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addass 7729 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7687. Proofs should normally use addass 7757 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulass 7730 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7688. Proofs should normally use mulass 7758 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-distr 7731 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7689. Proofs should normally use adddi 7759 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-i2m1 7732 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7690. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0lt1 7733 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7691. Proofs should normally use 0lt1 7896 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-1rid 7734 | is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7692. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0id 7735 |
is an identity element
for real addition. Axiom for real and
complex numbers, justified by theorem ax0id 7693.
Proofs should normally use addid1 7907 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
Axiom | ax-rnegex 7736* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7694. (Contributed by Eric Schmidt, 21-May-2007.) |
Axiom | ax-precex 7737* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7695. (Contributed by Jim Kingdon, 6-Feb-2020.) |
Axiom | ax-cnre 7738* | 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 7696. For naming consistency, use cnre 7769 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
Axiom | ax-pre-ltirr 7739 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7739. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-ltwlin 7740 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7698. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-lttrn 7741 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7699. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-apti 7742 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7700. (Contributed by Jim Kingdon, 29-Jan-2020.) |
Axiom | ax-pre-ltadd 7743 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7701. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulgt0 7744 | The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 7702. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-mulext 7745 |
Strong extensionality of multiplication (expressed in terms of ).
Axiom for real and complex numbers, justified by theorem axpre-mulext 7703
(Contributed by Jim Kingdon, 18-Feb-2020.) |
Axiom | ax-arch 7746* |
Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for
real and complex numbers, justified by theorem axarch 7706.
This axiom should not be used directly; instead use arch 8981 (which is the same, but stated in terms of and ). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.) |
Axiom | ax-caucvg 7747* |
Completeness. Axiom for real and complex numbers, justified by theorem
axcaucvg 7715.
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 10760 (which is the same, but stated in terms of the and notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.) |
Axiom | ax-pre-suploc 7748* |
An inhabited, bounded-above, located set of reals has a supremum.
Locatedness here means that given , either there is an element of the set greater than , or is an upper bound. Although this and ax-caucvg 7747 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7747. (Contributed by Jim Kingdon, 23-Jan-2024.) |
Axiom | ax-addf 7749 |
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
https://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 7752 should be used. Note that uses of ax-addf 7749 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 7683. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
Axiom | ax-mulf 7750 |
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
https://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 7725 should be used. Note that uses of ax-mulf 7750
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 7684. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.) |
Theorem | cnex 7751 | Alias for ax-cnex 7718. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | addcl 7752 | Alias for ax-addcl 7723, for naming consistency with addcli 7777. Use this theorem instead of ax-addcl 7723 or axaddcl 7679. (Contributed by NM, 10-Mar-2008.) |
Theorem | readdcl 7753 | Alias for ax-addrcl 7724, for naming consistency with readdcli 7786. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcl 7754 | Alias for ax-mulcl 7725, for naming consistency with mulcli 7778. (Contributed by NM, 10-Mar-2008.) |
Theorem | remulcl 7755 | Alias for ax-mulrcl 7726, for naming consistency with remulcli 7787. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulcom 7756 | Alias for ax-mulcom 7728, for naming consistency with mulcomi 7779. (Contributed by NM, 10-Mar-2008.) |
Theorem | addass 7757 | Alias for ax-addass 7729, for naming consistency with addassi 7781. (Contributed by NM, 10-Mar-2008.) |
Theorem | mulass 7758 | Alias for ax-mulass 7730, for naming consistency with mulassi 7782. (Contributed by NM, 10-Mar-2008.) |
Theorem | adddi 7759 | Alias for ax-distr 7731, for naming consistency with adddii 7783. (Contributed by NM, 10-Mar-2008.) |
Theorem | recn 7760 | A real number is a complex number. (Contributed by NM, 10-Aug-1999.) |
Theorem | reex 7761 | The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.) |
Theorem | reelprrecn 7762 | Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | cnelprrecn 7763 | 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 7764 | Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.) |
Theorem | 0cn 7765 | 0 is a complex number. (Contributed by NM, 19-Feb-2005.) |
Theorem | 0cnd 7766 | 0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Theorem | c0ex 7767 | 0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | 1ex 7768 | 1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.) |
Theorem | cnre 7769* | Alias for ax-cnre 7738, for naming consistency. (Contributed by NM, 3-Jan-2013.) |
Theorem | mulid1 7770 | is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.) |
Theorem | mulid2 7771 | Identity law for multiplication. Note: see mulid1 7770 for commuted version. (Contributed by NM, 8-Oct-1999.) |
Theorem | 1re 7772 | is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.) |
Theorem | 0re 7773 | is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.) |
Theorem | 0red 7774 | is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1i 7775 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | mulid2i 7776 | Identity law for multiplication. (Contributed by NM, 14-Feb-1995.) |
Theorem | addcli 7777 | Closure law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcli 7778 | Closure law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomi 7779 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulcomli 7780 | Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | addassi 7781 | Associative law for addition. (Contributed by NM, 23-Nov-1994.) |
Theorem | mulassi 7782 | Associative law for multiplication. (Contributed by NM, 23-Nov-1994.) |
Theorem | adddii 7783 | Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.) |
Theorem | adddiri 7784 | Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.) |
Theorem | recni 7785 | A real number is a complex number. (Contributed by NM, 1-Mar-1995.) |
Theorem | readdcli 7786 | Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | remulcli 7787 | Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.) |
Theorem | 1red 7788 | 1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | 1cnd 7789 | 1 is a complex number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.) |
Theorem | mulid1d 7790 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulid2d 7791 | Identity law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addcld 7792 | Closure law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcld 7793 | Closure law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulcomd 7794 | Commutative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | addassd 7795 | Associative law for addition. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | mulassd 7796 | Associative law for multiplication. (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddid 7797 | Distributive law (left-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddird 7798 | Distributive law (right-distributivity). (Contributed by Mario Carneiro, 27-May-2016.) |
Theorem | adddirp1d 7799 | Distributive law, plus 1 version. (Contributed by Glauco Siliprandi, 11-Dec-2019.) |
Theorem | joinlmuladdmuld 7800 | Join AB+CB into (A+C) on LHS. (Contributed by David A. Wheeler, 26-Oct-2019.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |