Home | Intuitionistic Logic Explorer Theorem List (p. 77 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 | caucvgsrlemoffres 7601* | Lemma for caucvgsr 7603. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
Theorem | caucvgsrlembnd 7602* | Lemma for caucvgsr 7603. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.) |
Theorem | caucvgsr 7603* |
A Cauchy sequence of signed reals with a modulus of convergence
converges to a signed real. 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).
This is similar to caucvgprpr 7513 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 7602). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 7598). 3. Since a signed real (element of ) which is greater than zero can be mapped to a positive real (element of ), perform that mapping on each element of the sequence and invoke caucvgprpr 7513 to get a limit (see caucvgsrlemgt1 7596). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7596). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7601). (Contributed by Jim Kingdon, 20-Jun-2021.) |
Theorem | ltpsrprg 7604 | Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
Theorem | mappsrprg 7605 | Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
Theorem | map2psrprg 7606* | Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
Theorem | suplocsrlemb 7607* | Lemma for suplocsr 7610. The set is located. (Contributed by Jim Kingdon, 18-Jan-2024.) |
Theorem | suplocsrlempr 7608* | Lemma for suplocsr 7610. The set has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.) |
Theorem | suplocsrlem 7609* | Lemma for suplocsr 7610. The set has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.) |
Theorem | suplocsr 7610* | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
Syntax | cc 7611 | Class of complex numbers. |
Syntax | cr 7612 | Class of real numbers. |
Syntax | cc0 7613 | Extend class notation to include the complex number 0. |
Syntax | c1 7614 | Extend class notation to include the complex number 1. |
Syntax | ci 7615 | Extend class notation to include the complex number i. |
Syntax | caddc 7616 | Addition on complex numbers. |
Syntax | cltrr 7617 | 'Less than' predicate (defined over real subset of complex numbers). |
Syntax | cmul 7618 | Multiplication on complex numbers. The token is a center dot. |
Definition | df-c 7619 | Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.) |
Definition | df-0 7620 | Define the complex number 0. (Contributed by NM, 22-Feb-1996.) |
Definition | df-1 7621 | Define the complex number 1. (Contributed by NM, 22-Feb-1996.) |
Definition | df-i 7622 | Define the complex number (the imaginary unit). (Contributed by NM, 22-Feb-1996.) |
Definition | df-r 7623 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) |
Definition | df-add 7624* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) |
Definition | df-mul 7625* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) |
Definition | df-lt 7626* | Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | opelcn 7627 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) |
Theorem | opelreal 7628 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | elreal 7629* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) |
Theorem | elrealeu 7630* | The real number mapping in elreal 7629 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | elreal2 7631 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) |
Theorem | 0ncn 7632 | 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 7633 which is a related property. (Contributed by NM, 2-May-1996.) |
Theorem | cnm 7633* | 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 7634 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | addcnsr 7635 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
Theorem | mulcnsr 7636 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
Theorem | eqresr 7637 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | addresr 7638 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | mulresr 7639 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | ltresr 7640 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Theorem | ltresr2 7641 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Theorem | dfcnqs 7642 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in . The trick involves qsid 6487, 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 7619), 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 7643 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7642 and mulcnsrec 7644. (Contributed by NM, 13-Aug-1995.) |
Theorem | mulcnsrec 7644 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6486, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7642. (Contributed by NM, 13-Aug-1995.) |
Theorem | addvalex 7645 | 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 7738. (Contributed by Jim Kingdon, 14-Jul-2021.) |
Theorem | pitonnlem1 7646* | Lemma for pitonn 7649. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
Theorem | pitonnlem1p1 7647 | Lemma for pitonn 7649. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
Theorem | pitonnlem2 7648* | Lemma for pitonn 7649. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
Theorem | pitonn 7649* | Mapping from to . (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | pitoregt0 7650* | Embedding from to yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | pitore 7651* | Embedding from to . Similar to pitonn 7649 but separate in the sense that we have not proved nnssre 8717 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recnnre 7652* | Embedding the reciprocal of a natural number into . (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | peano1nnnn 7653* | One is an element of . This is a counterpart to 1nn 8724 designed for real number axioms which involve natural numbers (notably, axcaucvg 7701). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | peano2nnnn 7654* | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8725 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7701). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | ltrennb 7655* | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | ltrenn 7656* | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 12-Jul-2021.) |
Theorem | recidpipr 7657* | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) |
Theorem | recidpirqlemcalc 7658 | Lemma for recidpirq 7659. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
Theorem | recidpirq 7659* | A real number times its reciprocal is one, where reciprocal is expressed with . (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | axcnex 7660 | The complex numbers form a set. Use cnex 7737 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
Theorem | axresscn 7661 | 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 7705. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
Theorem | ax1cn 7662 | 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 7706. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
Theorem | ax1re 7663 |
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 7707.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7706 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 7664 | 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 7708. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
Theorem | axaddcl 7665 | 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 7709 be used later. Instead, in most cases use addcl 7738. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
Theorem | axaddrcl 7666 | 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 7710 be used later. Instead, in most cases use readdcl 7739. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
Theorem | axmulcl 7667 | 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 7711 be used later. Instead, in most cases use mulcl 7740. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
Theorem | axmulrcl 7668 | 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 7712 be used later. Instead, in most cases use remulcl 7741. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
Theorem | axaddf 7669 | 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 7665. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 7735. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
Theorem | axmulf 7670 | 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 7667. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 7736. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
Theorem | axaddcom 7671 |
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 7713 be used later.
Instead, use addcom 7892.
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 7672 | 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 7714 be used later. Instead, use mulcom 7742. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
Theorem | axaddass 7673 | 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 7715 be used later. Instead, use addass 7743. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axmulass 7674 | 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 7716. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
Theorem | axdistr 7675 | 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 7717 be used later. Instead, use adddi 7745. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axi2m1 7676 | 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 7718. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
Theorem | ax0lt1 7677 |
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 7719.
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 7678 | 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 7720. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
Theorem | ax0id 7679 |
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 7721.
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 7680* | 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 7722. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
Theorem | axprecex 7681* |
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 7723.
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 7682* | 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 7724. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-ltirr 7683 | 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 7725. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-ltwlin 7684 | 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 7726. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-lttrn 7685 | 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 7727. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.) |
Theorem | axpre-apti 7686 |
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 7728.
(Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.) |
Theorem | axpre-ltadd 7687 | 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 7729. (Contributed by NM, 11-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulgt0 7688 | 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 7730. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | axpre-mulext 7689 |
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 7731.
(Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.) |
Theorem | rereceu 7690* | The reciprocal from axprecex 7681 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recriota 7691* | Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | axarch 7692* |
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 8715 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 7732. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.) |
Theorem | peano5nnnn 7693* | Peano's inductive postulate. This is a counterpart to peano5nni 8716 designed for real number axioms which involve natural numbers (notably, axcaucvg 7701). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nnindnn 7694* | Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8729 designed for real number axioms which involve natural numbers (notably, axcaucvg 7701). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | nntopi 7695* | Mapping from to . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | axcaucvglemcl 7696* | Lemma for axcaucvg 7701. Mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemf 7697* | Lemma for axcaucvg 7701. Mapping to and yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemval 7698* | Lemma for axcaucvg 7701. Value of sequence when mapping to and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
Theorem | axcaucvglemcau 7699* | Lemma for axcaucvg 7701. The result of mapping to and satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.) |
Theorem | axcaucvglemres 7700* | Lemma for axcaucvg 7701. Mapping the limit from and . (Contributed by Jim Kingdon, 10-Jul-2021.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |