Home | Intuitionistic Logic Explorer Theorem List (p. 78 of 139) | < 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 | 1idsr 7701 | 1 is an identity element for multiplication. (Contributed by Jim Kingdon, 5-Jan-2020.) |
Theorem | 00sr 7702 | A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.) |
Theorem | ltasrg 7703 | Ordering property of addition. (Contributed by NM, 10-May-1996.) |
Theorem | pn0sr 7704 | A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) |
Theorem | negexsr 7705* | Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) |
Theorem | recexgt0sr 7706* | The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) |
Theorem | recexsrlem 7707* | The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) |
Theorem | addgt0sr 7708 | The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) |
Theorem | ltadd1sr 7709 | Adding one to a signed real yields a larger signed real. (Contributed by Jim Kingdon, 7-Jul-2021.) |
Theorem | ltm1sr 7710 | Adding minus one to a signed real yields a smaller signed real. (Contributed by Jim Kingdon, 21-Jan-2024.) |
Theorem | mulgt0sr 7711 | The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) |
Theorem | aptisr 7712 | Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.) |
Theorem | mulextsr1lem 7713 | Lemma for mulextsr1 7714. (Contributed by Jim Kingdon, 17-Feb-2020.) |
Theorem | mulextsr1 7714 | Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.) |
Theorem | archsr 7715* | For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression , is the embedding of the positive integer into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.) |
Theorem | srpospr 7716* | Mapping from a signed real greater than zero to a positive real. (Contributed by Jim Kingdon, 25-Jun-2021.) |
Theorem | prsrcl 7717 | Mapping from a positive real to a signed real. (Contributed by Jim Kingdon, 25-Jun-2021.) |
Theorem | prsrpos 7718 | Mapping from a positive real to a signed real yields a result greater than zero. (Contributed by Jim Kingdon, 25-Jun-2021.) |
Theorem | prsradd 7719 | Mapping from positive real addition to signed real addition. (Contributed by Jim Kingdon, 29-Jun-2021.) |
Theorem | prsrlt 7720 | Mapping from positive real ordering to signed real ordering. (Contributed by Jim Kingdon, 29-Jun-2021.) |
Theorem | prsrriota 7721* | Mapping a restricted iota from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.) |
Theorem | caucvgsrlemcl 7722* | Lemma for caucvgsr 7735. Terms of the sequence from caucvgsrlemgt1 7728 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.) |
Theorem | caucvgsrlemasr 7723* | Lemma for caucvgsr 7735. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.) |
Theorem | caucvgsrlemfv 7724* | Lemma for caucvgsr 7735. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.) |
Theorem | caucvgsrlemf 7725* | Lemma for caucvgsr 7735. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) |
Theorem | caucvgsrlemcau 7726* | Lemma for caucvgsr 7735. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.) |
Theorem | caucvgsrlembound 7727* | Lemma for caucvgsr 7735. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.) |
Theorem | caucvgsrlemgt1 7728* | Lemma for caucvgsr 7735. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.) |
Theorem | caucvgsrlemoffval 7729* | Lemma for caucvgsr 7735. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
Theorem | caucvgsrlemofff 7730* | Lemma for caucvgsr 7735. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
Theorem | caucvgsrlemoffcau 7731* | Lemma for caucvgsr 7735. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
Theorem | caucvgsrlemoffgt1 7732* | Lemma for caucvgsr 7735. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
Theorem | caucvgsrlemoffres 7733* | Lemma for caucvgsr 7735. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.) |
Theorem | caucvgsrlembnd 7734* | Lemma for caucvgsr 7735. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.) |
Theorem | caucvgsr 7735* |
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 7645 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 7734). 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 7730). 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 7645 to get a limit (see caucvgsrlemgt1 7728). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7728). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7733). (Contributed by Jim Kingdon, 20-Jun-2021.) |
Theorem | ltpsrprg 7736 | 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 7737 | Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
Theorem | map2psrprg 7738* | Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) |
Theorem | suplocsrlemb 7739* | Lemma for suplocsr 7742. The set is located. (Contributed by Jim Kingdon, 18-Jan-2024.) |
Theorem | suplocsrlempr 7740* | Lemma for suplocsr 7742. The set has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.) |
Theorem | suplocsrlem 7741* | Lemma for suplocsr 7742. The set has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.) |
Theorem | suplocsr 7742* | An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.) |
Syntax | cc 7743 | Class of complex numbers. |
Syntax | cr 7744 | Class of real numbers. |
Syntax | cc0 7745 | Extend class notation to include the complex number 0. |
Syntax | c1 7746 | Extend class notation to include the complex number 1. |
Syntax | ci 7747 | Extend class notation to include the complex number i. |
Syntax | caddc 7748 | Addition on complex numbers. |
Syntax | cltrr 7749 | 'Less than' predicate (defined over real subset of complex numbers). |
Syntax | cmul 7750 | Multiplication on complex numbers. The token is a center dot. |
Definition | df-c 7751 | Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.) |
Definition | df-0 7752 | Define the complex number 0. (Contributed by NM, 22-Feb-1996.) |
Definition | df-1 7753 | Define the complex number 1. (Contributed by NM, 22-Feb-1996.) |
Definition | df-i 7754 | Define the complex number (the imaginary unit). (Contributed by NM, 22-Feb-1996.) |
Definition | df-r 7755 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) |
Definition | df-add 7756* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) |
Definition | df-mul 7757* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) |
Definition | df-lt 7758* | Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | opelcn 7759 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) |
Theorem | opelreal 7760 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | elreal 7761* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) |
Theorem | elrealeu 7762* | The real number mapping in elreal 7761 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.) |
Theorem | elreal2 7763 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) |
Theorem | 0ncn 7764 | 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 7765 which is a related property. (Contributed by NM, 2-May-1996.) |
Theorem | cnm 7765* | 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 7766 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) |
Theorem | addcnsr 7767 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) |
Theorem | mulcnsr 7768 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) |
Theorem | eqresr 7769 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | addresr 7770 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | mulresr 7771 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) |
Theorem | ltresr 7772 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Theorem | ltresr2 7773 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) |
Theorem | dfcnqs 7774 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in . The trick involves qsid 6558, 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 7751), 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 7775 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7774 and mulcnsrec 7776. (Contributed by NM, 13-Aug-1995.) |
Theorem | mulcnsrec 7776 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6557, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7774. (Contributed by NM, 13-Aug-1995.) |
Theorem | addvalex 7777 | 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 7870. (Contributed by Jim Kingdon, 14-Jul-2021.) |
Theorem | pitonnlem1 7778* | Lemma for pitonn 7781. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.) |
Theorem | pitonnlem1p1 7779 | Lemma for pitonn 7781. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.) |
Theorem | pitonnlem2 7780* | Lemma for pitonn 7781. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.) |
Theorem | pitonn 7781* | Mapping from to . (Contributed by Jim Kingdon, 22-Apr-2020.) |
Theorem | pitoregt0 7782* | Embedding from to yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | pitore 7783* | Embedding from to . Similar to pitonn 7781 but separate in the sense that we have not proved nnssre 8853 yet. (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | recnnre 7784* | Embedding the reciprocal of a natural number into . (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | peano1nnnn 7785* | One is an element of . This is a counterpart to 1nn 8860 designed for real number axioms which involve natural numbers (notably, axcaucvg 7833). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | peano2nnnn 7786* | A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 8861 designed for real number axioms which involve to natural numbers (notably, axcaucvg 7833). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.) |
Theorem | ltrennb 7787* | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 13-Jul-2021.) |
Theorem | ltrenn 7788* | Ordering of natural numbers with or . (Contributed by Jim Kingdon, 12-Jul-2021.) |
Theorem | recidpipr 7789* | Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.) |
Theorem | recidpirqlemcalc 7790 | Lemma for recidpirq 7791. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.) |
Theorem | recidpirq 7791* | A real number times its reciprocal is one, where reciprocal is expressed with . (Contributed by Jim Kingdon, 15-Jul-2021.) |
Theorem | axcnex 7792 | The complex numbers form a set. Use cnex 7869 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
Theorem | axresscn 7793 | 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 7837. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
Theorem | ax1cn 7794 | 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 7838. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
Theorem | ax1re 7795 |
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 7839.
In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 7838 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 7796 | 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 7840. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
Theorem | axaddcl 7797 | 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 7841 be used later. Instead, in most cases use addcl 7870. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
Theorem | axaddrcl 7798 | 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 7842 be used later. Instead, in most cases use readdcl 7871. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
Theorem | axmulcl 7799 | 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 7843 be used later. Instead, in most cases use mulcl 7872. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
Theorem | axmulrcl 7800 | 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 7844 be used later. Instead, in most cases use remulcl 7873. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |