Home | Intuitionistic Logic Explorer Theorem List (p. 77 of 131) | < 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 | elrealeu 7601* | The real number mapping in elreal 7600 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | elreal2 7602 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) |
Theorem | 0ncn 7603 | The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. See also cnm 7604 which is a related property. (Contributed by NM, 2-May-1996.) |
Theorem | cnm 7604* | A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.) |
Theorem | ltrelre 7605 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | addcnsr 7606 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
Theorem | mulcnsr 7607 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
Theorem | eqresr 7608 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | addresr 7609 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | mulresr 7610 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | ltresr 7611 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Theorem | ltresr2 7612 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Theorem | dfcnqs 7613 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in . The trick involves qsid 6460, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that is a quotient set, even though it is not (compare df-c 7590), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.) |
Theorem | addcnsrec 7614 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7613 and mulcnsrec 7615. (Contributed by NM, 13-Aug-1995.) |
Theorem | mulcnsrec 7615 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6459, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7613. (Contributed by NM, 13-Aug-1995.) |
Theorem | addvalex 7616 | Existence of a sum. This is dependent on how we define so once we proceed to real number axioms we will replace it with theorems such as addcl 7709. (Contributed by Jim Kingdon, 14-Jul-2021.) |
Theorem | pitonnlem1 7617* | Lemma for pitonn 7620. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
Theorem | pitonnlem1p1 7618 | Lemma for pitonn 7620. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
Theorem | pitonnlem2 7619* | Lemma for pitonn 7620. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
Theorem | pitonn 7620* | Mapping from to . (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | pitoregt0 7621* | Embedding from to yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | pitore 7622* | Embedding from to . Similar to pitonn 7620 but separate in the sense that we have not proved nnssre 8684 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recnnre 7623* | Embedding the reciprocal of a natural number into . (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | peano1nnnn 7624* | One is an element of . This is a counterpart to 1nn 8691 designed for real number axioms which involve natural numbers (notably, axcaucvg 7672). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | peano2nnnn 7625* | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8692 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7672). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | ltrennb 7626* | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | ltrenn 7627* | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 12-Jul-2021.) |
Theorem | recidpipr 7628* | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) |
Theorem | recidpirqlemcalc 7629 | Lemma for recidpirq 7630. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
Theorem | recidpirq 7630* | A real number times its reciprocal is one, where reciprocal is expressed with . (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | axcnex 7631 | The complex numbers form a set. Use cnex 7708 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
Theorem | axresscn 7632 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 7676. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
Theorem | ax1cn 7633 | 1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 7677. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
Theorem | ax1re 7634 |
1 is a real number. Axiom for real and complex numbers, derived from set
theory. This construction-dependent theorem should not be referenced
directly; instead, use ax-1re 7678.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7677 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
Theorem | axicn 7635 | is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 7679. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
Theorem | axaddcl 7636 | Closure law for addition 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-addcl 7680 be used later. Instead, in most cases use addcl 7709. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
Theorem | axaddrcl 7637 | Closure law for addition 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-addrcl 7681 be used later. Instead, in most cases use readdcl 7710. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
Theorem | axmulcl 7638 | Closure law for multiplication 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-mulcl 7682 be used later. Instead, in most cases use mulcl 7711. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
Theorem | axmulrcl 7639 | 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 7683 be used later. Instead, in most cases use remulcl 7712. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
Theorem | axaddf 7640 | Addition is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axaddcl 7636. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 7706. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
Theorem | axmulf 7641 | Multiplication is an operation on the complex numbers. This theorem can be used as an alternate axiom for complex numbers in place of the less specific axmulcl 7638. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 7707. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
Theorem | axaddcom 7642 |
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 7684 be used later.
Instead, use addcom 7863.
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 7643 | 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 7685 be used later. Instead, use mulcom 7713. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
Theorem | axaddass 7644 | 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 7686 be used later. Instead, use addass 7714. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axmulass 7645 | 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 7687. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
Theorem | axdistr 7646 | 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 7688 be used later. Instead, use adddi 7716. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axi2m1 7647 | 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 7689. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
Theorem | ax0lt1 7648 |
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 7690.
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 7649 | 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 7691. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
Theorem | ax0id 7650 |
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 7692.
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 7651* | 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 7693. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
Theorem | axprecex 7652* |
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 7694.
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 7653* | 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 7695. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-ltirr 7654 | 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 7696. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-ltwlin 7655 | 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 7697. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-lttrn 7656 | 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 7698. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
Theorem | axpre-apti 7657 |
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 7699.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-ltadd 7658 | 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 7700. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulgt0 7659 | 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 7701. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulext 7660 |
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 7702.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
Theorem | rereceu 7661* | The reciprocal from axprecex 7652 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recriota 7662* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | axarch 7663* |
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 8682 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 7703. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
Theorem | peano5nnnn 7664* | Peano's inductive postulate. This is a counterpart to peano5nni 8683 designed for real number axioms which involve natural numbers (notably, axcaucvg 7672). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nnindnn 7665* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8696 designed for real number axioms which involve natural numbers (notably, axcaucvg 7672). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nntopi 7666* | Mapping from to . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | axcaucvglemcl 7667* | Lemma for axcaucvg 7672. Mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemf 7668* | Lemma for axcaucvg 7672. Mapping to and yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemval 7669* | Lemma for axcaucvg 7672. Value of sequence when mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemcau 7670* | Lemma for axcaucvg 7672. The result of mapping to and satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemres 7671* | Lemma for axcaucvg 7672. Mapping the limit from and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvg 7672* |
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 7704. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.) |
Theorem | axpre-suploclemres 7673* | Lemma for axpre-suploc 7674. 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 7581. (Contributed by Jim Kingdon, 24-Jan-2024.) |
Theorem | axpre-suploc 7674* |
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 7705. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.) |
Axiom | ax-cnex 7675 | The complex numbers form a set. Proofs should normally use cnex 7708 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-resscn 7676 | The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 7632. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1cn 7677 | 1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 7633. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-1re 7678 | 1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 7634. Proofs should use 1re 7729 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.) |
Axiom | ax-icn 7679 | is a complex number. Axiom for real and complex numbers, justified by theorem axicn 7635. (Contributed by NM, 1-Mar-1995.) |
Axiom | ax-addcl 7680 | Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 7636. Proofs should normally use addcl 7709 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 7681 | Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 7637. Proofs should normally use readdcl 7710 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulcl 7682 | Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 7638. Proofs should normally use mulcl 7711 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulrcl 7683 | Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 7639. Proofs should normally use remulcl 7712 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addcom 7684 | Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 7642. Proofs should normally use addcom 7863 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.) |
Axiom | ax-mulcom 7685 | Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 7643. Proofs should normally use mulcom 7713 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-addass 7686 | Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 7644. Proofs should normally use addass 7714 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-mulass 7687 | Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 7645. Proofs should normally use mulass 7715 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-distr 7688 | Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 7646. Proofs should normally use adddi 7716 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.) |
Axiom | ax-i2m1 7689 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 7647. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0lt1 7690 | 0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 7648. Proofs should normally use 0lt1 7853 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-1rid 7691 | is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 7649. (Contributed by NM, 29-Jan-1995.) |
Axiom | ax-0id 7692 |
is an identity element
for real addition. Axiom for real and
complex numbers, justified by theorem ax0id 7650.
Proofs should normally use addid1 7864 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.) |
Axiom | ax-rnegex 7693* | Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 7651. (Contributed by Eric Schmidt, 21-May-2007.) |
Axiom | ax-precex 7694* | Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 7652. (Contributed by Jim Kingdon, 6-Feb-2020.) |
Axiom | ax-cnre 7695* | 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 7653. For naming consistency, use cnre 7726 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.) |
Axiom | ax-pre-ltirr 7696 | Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 7696. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-ltwlin 7697 | Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 7655. (Contributed by Jim Kingdon, 12-Jan-2020.) |
Axiom | ax-pre-lttrn 7698 | Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 7656. (Contributed by NM, 13-Oct-2005.) |
Axiom | ax-pre-apti 7699 | Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 7657. (Contributed by Jim Kingdon, 29-Jan-2020.) |
Axiom | ax-pre-ltadd 7700 | Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 7658. (Contributed by NM, 13-Oct-2005.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |