Home | Metamath
Proof Explorer Theorem List (p. 88 of 328) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-ltr 8701* | Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8759, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |
Definition | df-0r 8702 | Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 8759, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Definition | df-1r 8703 | Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8759, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Definition | df-m1r 8704 | Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 8759, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Theorem | enrbreq 8705 | Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
Theorem | enrer 8706 | The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (New usage is discouraged.) |
Theorem | enreceq 8707 | Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.) |
Theorem | enrex 8708 | The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
Theorem | ltrelsr 8709 | Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.) |
Theorem | addcmpblnr 8710 | Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
Theorem | mulcmpblnrlem 8711 | Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.) |
Theorem | mulcmpblnr 8712 | Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.) |
Theorem | addsrpr 8713 | Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |
Theorem | mulsrpr 8714 | Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |
Theorem | ltsrpr 8715 | Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.) |
Theorem | gt0srpr 8716 | Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | 0nsr 8717 | The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.) |
Theorem | 0r 8718 | The constant is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Theorem | 1sr 8719 | The constant is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Theorem | m1r 8720 | The constant is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Theorem | addclsr 8721 | Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.) |
Theorem | mulclsr 8722 | Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
Theorem | dmaddsr 8723 | Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
Theorem | dmmulsr 8724 | Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.) |
Theorem | addcomsr 8725 | Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
Theorem | addasssr 8726 | Addition of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
Theorem | mulcomsr 8727 | Multiplication of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
Theorem | mulasssr 8728 | Multiplication of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
Theorem | distrsr 8729 | Multiplication of signed reals is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.) |
Theorem | m1p1sr 8730 | Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
Theorem | m1m1sr 8731 | Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
Theorem | ltsosr 8732 | Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.) (New usage is discouraged.) |
Theorem | 0lt1sr 8733 | 0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.) |
Theorem | 1ne0sr 8734 | 1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.) |
Theorem | 0idsr 8735 | The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.) |
Theorem | 1idsr 8736 | 1 is an identity element for multiplication. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
Theorem | 00sr 8737 | A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.) |
Theorem | ltasr 8738 | Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
Theorem | pn0sr 8739 | A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
Theorem | negexsr 8740* | Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
Theorem | recexsrlem 8741* | The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
Theorem | addgt0sr 8742 | The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
Theorem | mulgt0sr 8743 | The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.) |
Theorem | sqgt0sr 8744 | The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
Theorem | recexsr 8745* | The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
Theorem | mappsrpr 8746 | Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
Theorem | ltpsrpr 8747 | Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
Theorem | map2psrpr 8748* | Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
Theorem | supsrlem 8749* | Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
Theorem | supsr 8750* | A non-empty, bounded set of signed reals has a supremum. (Cotributed by Mario Carneiro, 15-Jun-2013.) (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
Syntax | cc 8751 | Class of complex numbers. |
Syntax | cr 8752 | Class of real numbers. |
Syntax | cc0 8753 | Extend class notation to include the complex number 0. |
Syntax | c1 8754 | Extend class notation to include the complex number 1. |
Syntax | ci 8755 | Extend class notation to include the complex number i. |
Syntax | caddc 8756 | Addition on complex numbers. |
Syntax | cltrr 8757 | 'Less than' predicate (defined over real subset of complex numbers). |
Syntax | cmul 8758 | Multiplication on complex numbers. The token is a center dot. |
Definition | df-c 8759 | Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 8786. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Definition | df-0 8760 | Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Definition | df-1 8761 | Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Definition | df-i 8762 | Define the complex number (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Definition | df-r 8763 | Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Definition | df-add 8764* | Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.) |
Definition | df-mul 8765* | Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Definition | df-lt 8766* | Define 'less than' on the real subset of complex numbers. Proofs should typically use instead; see df-ltxr 8888. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Theorem | opelcn 8767 | Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.) |
Theorem | opelreal 8768 | Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Theorem | elreal 8769* | Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
Theorem | elreal2 8770 | Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.) |
Theorem | 0ncn 8771 | 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. (Contributed by NM, 2-May-1996.) (New usage is discouraged.) |
Theorem | ltrelre 8772 | 'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Theorem | addcnsr 8773 | Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) (New usage is discouraged.) |
Theorem | mulcnsr 8774 | Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.) |
Theorem | eqresr 8775 | Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
Theorem | addresr 8776 | Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
Theorem | mulresr 8777 | Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.) |
Theorem | ltresr 8778 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Theorem | ltresr2 8779 | Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.) |
Theorem | dfcnqs 8780 | Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in from those in . The trick involves qsid 6741, 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 8759), 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.) (New usage is discouraged.) |
Theorem | addcnsrec 8781 | Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 8780 and mulcnsrec 8782. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) |
Theorem | mulcnsrec 8782 |
Technical trick to permit re-use of some equivalence class lemmas for
operation laws. The trick involves ecid 6740,
which shows that the coset of
the converse epsilon relation (which is not an equivalence relation)
leaves a set unchanged. See also dfcnqs 8780.
Note: This is the last lemma (from which the axioms will be derived) in the construction of real and complex numbers. The construction starts at cnpi 8482. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.) |
Theorem | axaddf 8783 | 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 8789. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 8832. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
Theorem | axmulf 8784 | 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 8791. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 8833. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.) |
Theorem | axcnex 8785 | The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 10366), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 4147 in later theorems by invoking the axiom ax-cnex 8809 instead of cnexALT 10366. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.) |
Theorem | axresscn 8786 | The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 8810. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.) |
Theorem | ax1cn 8787 | 1 is a complex number. Axiom 2 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 8811. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.) |
Theorem | axicn 8788 | is a complex number. Axiom 3 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 8812. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.) |
Theorem | axaddcl 8789 | Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 8813 be used later. Instead, in most cases use addcl 8835. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.) |
Theorem | axaddrcl 8790 | Closure law for addition in the real subfield of complex numbers. Axiom 5 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 8814 be used later. Instead, in most cases use readdcl 8836. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.) |
Theorem | axmulcl 8791 | Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 8815 be used later. Instead, in most cases use mulcl 8837. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.) |
Theorem | axmulrcl 8792 | Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 8816 be used later. Instead, in most cases use remulcl 8838. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.) |
Theorem | axmulcom 8793 | Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcom 8817 be used later. Instead, use mulcom 8839. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.) |
Theorem | axaddass 8794 | 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 9 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addass 8818 be used later. Instead, use addass 8840. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axmulass 8795 | Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-mulass 8819. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.) |
Theorem | axdistr 8796 | Distributive law for complex numbers. Axiom 11 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-distr 8820 be used later. Instead, use adddi 8842. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.) |
Theorem | axi2m1 8797 | i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-i2m1 8821. (Contributed by NM, 5-May-1996.) (New usage is discouraged.) |
Theorem | ax1ne0 8798 | 1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1ne0 8822. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.) |
Theorem | ax1rid 8799 | is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, derived from ZF set theory. Weakened from the original axiom in the form of statement in mulid1 8851, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 8823. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.) |
Theorem | axrnegex 8800* | Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rnegex 8824. (Contributed by NM, 15-May-1996.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |