P. 68 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6701-6800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pitonnlem1 6701*	Lemma for pitonn 6704. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.)
|- <.[ <.( <. { l | l <Q [ <. 1o , 1o >.] ~Q } , {u | [ <. 1o , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. = 1
Theorem	pitonnlem1p1 6702	Lemma for pitonn 6704. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- (A e. P. -> [ <.(A +P. ( 1P +P. 1P)) , ( 1P +P. 1P) >.] ~R = [ <.(A +P. 1P) , 1P >.] ~R )
Theorem	pitonnlem2 6703*	Lemma for pitonn 6704. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)
|- ( K e. N. -> ( <.[ <.( <. { l | l <Q [ <. K , 1o >.] ~Q } , {u | [ <. K , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. + 1) = <.[ <.( <. { l | l <Q [ <.( K +N 1o) , 1o >.] ~Q } , {u | [ <.( K +N 1o) , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >.)
Theorem	pitonn 6704*	Mapping from N. to NN. (Contributed by Jim Kingdon, 22-Apr-2020.)
|- ( n e. N. -> <.[ <.( <. { l | l <Q [ <. n , 1o >.] ~Q } , {u | [ <. n , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R , 0R >. e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) })
3.1.2  Final derivation of real and complex number postulates
Theorem	axcnex 6705	The complex numbers form a set. Use cnex 6763 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 6706	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 6735. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 6707	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 6736. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	ax1re 6708	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 6737. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6736 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.)
|- 1 e. RR
Theorem	axicn 6709	_i 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 6738. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 6710	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 6739 be used later. Instead, in most cases use addcl 6764. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
Theorem	axaddrcl 6711	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 6740 be used later. Instead, in most cases use readdcl 6765. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Theorem	axmulcl 6712	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 6741 be used later. Instead, in most cases use mulcl 6766. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
Theorem	axmulrcl 6713	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 6742 be used later. Instead, in most cases use remulcl 6767. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ((A e. RR /\ B e. RR) -> (A x. B) e. RR)
Theorem	axaddcom 6714	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 6743 be used later. Instead, use addcom 6907. 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.)
|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
Theorem	axmulcom 6715	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 6744 be used later. Instead, use mulcom 6768. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A x. B) = (B x. A))
Theorem	axaddass 6716	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 6745 be used later. Instead, use addass 6769. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))
Theorem	axmulass 6717	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 6746. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A x. B) x. C) = (A x. (B x. C)))
Theorem	axdistr 6718	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 6747 be used later. Instead, use adddi 6771. (Contributed by NM, 2-Sep-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A x. (B + C)) = ((A x. B) + (A x. C)))
Theorem	axi2m1 6719	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 6748. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- (( _i x. _i) + 1) = 0
Theorem	ax0lt1 6720	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 6749. The version of this axiom in the Metamath Proof Explorer reads 1 =/= 0; here we change it to 0 <RR 1. The proof of 0 <RR 1 from 1 =/= 0 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.)
|- 0 <RR 1
Theorem	ax1rid 6721	1 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 6750. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- (A e. RR -> (A x. 1) = A)
Theorem	ax0id 6722	0 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 6751. 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.)
|- (A e. CC -> (A + 0) = A)
Theorem	axrnegex 6723*	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 6752. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- (A e. RR -> E.x e. RR (A + x) = 0)
Theorem	axprecex 6724*	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 6753. In treatments which assume excluded middle, the 0 <RR A condition is generally replaced by A =/= 0, and it may not be necessary to state that the reciproacal is positive. (Contributed by Jim Kingdon, 6-Feb-2020.) (New usage is discouraged.)
|- ((A e. RR /\ 0 <RR A) -> E.x e. RR ( 0 <RR x /\ (A x. x) = 1))
Theorem	axcnre 6725*	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 6754. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- (A e. CC -> E.x e. RR E.y e. RR A = (x + ( _i x. y)))
Theorem	axpre-ltirr 6726	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 6755. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- (A e. RR -> -. A <RR A)
Theorem	axpre-ltwlin 6727	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 6756. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <RR B -> (A <RR C \/ C <RR B)))
Theorem	axpre-lttrn 6728	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 6757. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <RR B /\ B <RR C) -> A <RR C))
Theorem	axpre-apti 6729	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 6758. (Contributed by Jim Kingdon, 29-Jan-2020.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR /\ -. (A <RR B \/ B <RR A)) -> A = B)
Theorem	axpre-ltadd 6730	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 6759. (Contributed by NM, 11-May-1996.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <RR B -> ( C + A) <RR ( C + B)))
Theorem	axpre-mulgt0 6731	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 6760. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR) -> (( 0 <RR A /\ 0 <RR B) -> 0 <RR (A x. B)))
Theorem	axpre-mulext 6732	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulext 6761. (Contributed by Jim Kingdon, 18-Feb-2020.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A x. C) <RR (B x. C) -> (A <RR B \/ B <RR A)))
Theorem	axarch 6733*	Archimedean axiom. The Archimedean property is more naturally stated once we have defined NN. Unless we find another way to state it, we'll just use the right hand side of dfnn2 7657 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 6762. (Contributed by Jim Kingdon, 22-Apr-2020.) (New usage is discouraged.)
|- (A e. RR -> E. n e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) }A <RR n)
3.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 6734	The complex numbers form a set. Proofs should normally use cnex 6763 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 6735	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6706. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 6736	1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6707. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-1re 6737	1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6708. Proofs should use 1re 6784 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 6738	_i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6709. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 6739	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 6710. Proofs should normally use addcl 6764 instead, which asserts the same thing but follows our naming conventions for closures. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
Axiom	ax-addrcl 6740	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 6711. Proofs should normally use readdcl 6765 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Axiom	ax-mulcl 6741	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 6712. Proofs should normally use mulcl 6766 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
Axiom	ax-mulrcl 6742	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 6713. Proofs should normally use remulcl 6767 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. RR /\ B e. RR) -> (A x. B) e. RR)
Axiom	ax-addcom 6743	Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6714. Proofs should normally use addcom 6907 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 17-Jan-2020.)
|- ((A e. CC /\ B e. CC) -> (A + B) = (B + A))
Axiom	ax-mulcom 6744	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 6715. Proofs should normally use mulcom 6768 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. CC /\ B e. CC) -> (A x. B) = (B x. A))
Axiom	ax-addass 6745	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 6716. Proofs should normally use addass 6769 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))
Axiom	ax-mulass 6746	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 6717. Proofs should normally use mulass 6770 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A x. B) x. C) = (A x. (B x. C)))
Axiom	ax-distr 6747	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 6718. Proofs should normally use adddi 6771 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A x. (B + C)) = ((A x. B) + (A x. C)))
Axiom	ax-i2m1 6748	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 6719. (Contributed by NM, 29-Jan-1995.)
|- (( _i x. _i) + 1) = 0
Theorem	ax-0lt1 6749	0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6720. Proofs should normally use 0lt1 6898 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 6750	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 6721. (Contributed by NM, 29-Jan-1995.)
|- (A e. RR -> (A x. 1) = A)
Axiom	ax-0id 6751	0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6722. Proofs should normally use addid1 6908 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- (A e. CC -> (A + 0) = A)
Axiom	ax-rnegex 6752*	Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 6723. (Contributed by Eric Schmidt, 21-May-2007.)
|- (A e. RR -> E.x e. RR (A + x) = 0)
Axiom	ax-precex 6753*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6724. (Contributed by Jim Kingdon, 6-Feb-2020.)
|- ((A e. RR /\ 0 <RR A) -> E.x e. RR ( 0 <RR x /\ (A x. x) = 1))
Axiom	ax-cnre 6754*	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 6725. For naming consistency, use cnre 6781 for new proofs. (New usage is discouraged.) (Contributed by NM, 9-May-1999.)
|- (A e. CC -> E.x e. RR E.y e. RR A = (x + ( _i x. y)))
Axiom	ax-pre-ltirr 6755	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6755. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- (A e. RR -> -. A <RR A)
Axiom	ax-pre-ltwlin 6756	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6727. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <RR B -> (A <RR C \/ C <RR B)))
Axiom	ax-pre-lttrn 6757	Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 6728. (Contributed by NM, 13-Oct-2005.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A <RR B /\ B <RR C) -> A <RR C))
Axiom	ax-pre-apti 6758	Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6729. (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ((A e. RR /\ B e. RR /\ -. (A <RR B \/ B <RR A)) -> A = B)
Axiom	ax-pre-ltadd 6759	Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 6730. (Contributed by NM, 13-Oct-2005.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> (A <RR B -> ( C + A) <RR ( C + B)))
Axiom	ax-pre-mulgt0 6760	The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 6731. (Contributed by NM, 13-Oct-2005.)
|- ((A e. RR /\ B e. RR) -> (( 0 <RR A /\ 0 <RR B) -> 0 <RR (A x. B)))
Axiom	ax-pre-mulext 6761	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by theorem axpre-mulext 6732 (Contributed by Jim Kingdon, 18-Feb-2020.)
|- ((A e. RR /\ B e. RR /\ C e. RR) -> ((A x. C) <RR (B x. C) -> (A <RR B \/ B <RR A)))
Axiom	ax-arch 6762*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by theorem axarch 6733. This axiom should not be used directly; instead use arch 7914 (which is the same, but stated in terms of NN and <). (Contributed by Jim Kingdon, 2-May-2020.) (New usage is discouraged.)
|- (A e. RR -> E. n e. |^| {x | ( 1 e. x /\ A.y e. x (y + 1) e. x) }A <RR n)
3.2  Derive the basic properties from the field axioms
3.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 6763	Alias for ax-cnex 6734. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 6764	Alias for ax-addcl 6739, for naming consistency with addcli 6789. Use this theorem instead of ax-addcl 6739 or axaddcl 6710. (Contributed by NM, 10-Mar-2008.)
|- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
Theorem	readdcl 6765	Alias for ax-addrcl 6740, for naming consistency with readdcli 6798. (Contributed by NM, 10-Mar-2008.)
|- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Theorem	mulcl 6766	Alias for ax-mulcl 6741, for naming consistency with mulcli 6790. (Contributed by NM, 10-Mar-2008.)
|- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
Theorem	remulcl 6767	Alias for ax-mulrcl 6742, for naming consistency with remulcli 6799. (Contributed by NM, 10-Mar-2008.)
|- ((A e. RR /\ B e. RR) -> (A x. B) e. RR)
Theorem	mulcom 6768	Alias for ax-mulcom 6744, for naming consistency with mulcomi 6791. (Contributed by NM, 10-Mar-2008.)
|- ((A e. CC /\ B e. CC) -> (A x. B) = (B x. A))
Theorem	addass 6769	Alias for ax-addass 6745, for naming consistency with addassi 6793. (Contributed by NM, 10-Mar-2008.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) + C) = (A + (B + C)))
Theorem	mulass 6770	Alias for ax-mulass 6746, for naming consistency with mulassi 6794. (Contributed by NM, 10-Mar-2008.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A x. B) x. C) = (A x. (B x. C)))
Theorem	adddi 6771	Alias for ax-distr 6747, for naming consistency with adddii 6795. (Contributed by NM, 10-Mar-2008.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> (A x. (B + C)) = ((A x. B) + (A x. C)))
Theorem	recn 6772	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- (A e. RR -> A e. CC)
Theorem	reex 6773	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 6774	Reals are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- RR e. { RR , CC }
Theorem	cnelprrecn 6775	Complex numbers are a subset of the pair of real and complex numbers (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
|- CC e. { RR , CC }
Theorem	adddir 6776	Distributive law for complex numbers (right-distributivity). (Contributed by NM, 10-Oct-2004.)
|- ((A e. CC /\ B e. CC /\ C e. CC) -> ((A + B) x. C) = ((A x. C) + (B x. C)))
Theorem	0cn 6777	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 6778	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- (ph -> 0 e. CC)
Theorem	c0ex 6779	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 6780	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 6781*	Alias for ax-cnre 6754, for naming consistency. (Contributed by NM, 3-Jan-2013.)
|- (A e. CC -> E.x e. RR E.y e. RR A = (x + ( _i x. y)))
Theorem	mulid1 6782	1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013.)
|- (A e. CC -> (A x. 1) = A)
Theorem	mulid2 6783	Identity law for multiplication. Note: see mulid1 6782 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- (A e. CC -> ( 1 x. A) = A)
Theorem	1re 6784	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
Theorem	0re 6785	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 6786	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- (ph -> 0 e. RR)
Theorem	mulid1i 6787	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>   |- (A x. 1) = A
Theorem	mulid2i 6788	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>   |- ( 1 x. A) = A
Theorem	addcli 6789	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   =>   |- (A + B) e. CC
Theorem	mulcli 6790	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   =>   |- (A x. B) e. CC
Theorem	mulcomi 6791	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   =>   |- (A x. B) = (B x. A)
Theorem	mulcomli 6792	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   &   |- (A x. B) = C   =>   |- (B x. A) = C
Theorem	addassi 6793	Associative law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ((A + B) + C) = (A + (B + C))
Theorem	mulassi 6794	Associative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ((A x. B) x. C) = (A x. (B x. C))
Theorem	adddii 6795	Distributive law (left-distributivity). (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- (A x. (B + C)) = ((A x. B) + (A x. C))
Theorem	adddiri 6796	Distributive law (right-distributivity). (Contributed by NM, 16-Feb-1995.)
|- A e. CC   &   |- B e. CC   &   |- C e. CC   =>   |- ((A + B) x. C) = ((A x. C) + (B x. C))
Theorem	recni 6797	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>   |- A e. CC
Theorem	readdcli 6798	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &   |- B e. RR   =>   |- (A + B) e. RR
Theorem	remulcli 6799	Closure law for multiplication of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &   |- B e. RR   =>   |- (A x. B) e. RR
Theorem	1red 6800	1 is an real number, deductive form (common case). (Contributed by David A. Wheeler, 6-Dec-2018.)
|- (ph -> 1 e. RR)