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	recexgt0sr 6701*	The reciprocal of a positive signed real exists and is positive. (Contributed by Jim Kingdon, 6-Feb-2020.)
|- ( 0R <R A -> E.x e. R. ( 0R <R x /\ (A .R x) = 1R))
Theorem	recexsrlem 6702*	The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.)
|- ( 0R <R A -> E.x e. R. (A .R x) = 1R)
Theorem	addgt0sr 6703	The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.)
|- (( 0R <R A /\ 0R <R B) -> 0R <R (A +R B))
Theorem	mulgt0sr 6704	The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.)
|- (( 0R <R A /\ 0R <R B) -> 0R <R (A .R B))
Theorem	aptisr 6705	Apartness of signed reals is tight. (Contributed by Jim Kingdon, 29-Jan-2020.)
|- ((A e. R. /\ B e. R. /\ -. (A <R B \/ B <R A)) -> A = B)
Theorem	mulextsr1lem 6706	Lemma for mulextsr1 6707. (Contributed by Jim Kingdon, 17-Feb-2020.)
|- ((( X e. P. /\ Y e. P.) /\ ( Z e. P. /\ W e. P.) /\ ( U e. P. /\ V e. P.)) -> (((( X .P. U) +P. ( Y .P. V)) +P. (( Z .P. V) +P. ( W .P. U))) <P ((( X .P. V) +P. ( Y .P. U)) +P. (( Z .P. U) +P. ( W .P. V))) -> (( X +P. W) <P ( Y +P. Z) \/ ( Z +P. Y) <P ( W +P. X))))
Theorem	mulextsr1 6707	Strong extensionality of multiplication of signed reals. (Contributed by Jim Kingdon, 18-Feb-2020.)
|- ((A e. R. /\ B e. R. /\ C e. R.) -> ((A .R C) <R (B .R C) -> (A <R B \/ B <R A)))
Theorem	archsr 6708*	For any signed real, there is an integer that is greater than it. This is also known as the "archimedean property". The expression [ <.( <. { l | l <Q [ <.x , 1o >.] ~Q }, {u | [ <.x , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R is the embedding of the positive integer x into the signed reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
|- (A e. R. -> E.x e. N. A <R [ <.( <. { l | l <Q [ <.x , 1o >.] ~Q } , {u | [ <.x , 1o >.] ~Q <Q u } >. +P. 1P) , 1P >.] ~R )
Syntax	cc 6709	Class of complex numbers.
class CC
Syntax	cr 6710	Class of real numbers.
class RR
Syntax	cc0 6711	Extend class notation to include the complex number 0.
class 0
Syntax	c1 6712	Extend class notation to include the complex number 1.
class 1
Syntax	ci 6713	Extend class notation to include the complex number i.
class _i
Syntax	caddc 6714	Addition on complex numbers.
class +
Syntax	cltrr 6715	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 6716	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 6717	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- CC = ( R. X. R.)
Definition	df-0 6718	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
|- 0 = <. 0R , 0R >.
Definition	df-1 6719	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
|- 1 = <. 1R , 0R >.
Definition	df-i 6720	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
|- _i = <. 0R , 1R >.
Definition	df-r 6721	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
|- RR = ( R. X. { 0R })
Definition	df-add 6722*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
|- + = { <. <.x , y >. , z >. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w , v >. /\ y = <.u , f >.) /\ z = <.(w +R u) , (v +R f) >.)) }
Definition	df-mul 6723*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
|- x. = { <. <.x , y >. , z >. | ((x e. CC /\ y e. CC) /\ E.wE.vE.uE.f((x = <.w , v >. /\ y = <.u , f >.) /\ z = <.((w .R u) +R ( -1R .R (v .R f))) , ((v .R u) +R (w .R f)) >.)) }
Definition	df-lt 6724*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR = { <.x , y >. | ((x e. RR /\ y e. RR) /\ E.zE.w((x = <.z , 0R >. /\ y = <.w , 0R >.) /\ z <R w)) }
Theorem	opelcn 6725	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
|- ( <.A , B >. e. CC <-> (A e. R. /\ B e. R.))
Theorem	opelreal 6726	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- ( <.A , 0R >. e. RR <-> A e. R.)
Theorem	elreal 6727*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
|- (A e. RR <-> E.x e. R. <.x , 0R >. = A)
Theorem	elreal2 6728	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
|- (A e. RR <-> (( 1st ` A) e. R. /\ A = <.( 1st ` A) , 0R >.))
Theorem	0ncn 6729	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.)
|- -. (/) e. CC
Theorem	ltrelre 6730	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR C_ ( RR X. RR)
Theorem	addcnsr 6731	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
|- (((A e. R. /\ B e. R.) /\ ( C e. R. /\ D e. R.)) -> ( <.A , B >. + <. C , D >.) = <.(A +R C) , (B +R D) >.)
Theorem	mulcnsr 6732	Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.)
|- (((A e. R. /\ B e. R.) /\ ( C e. R. /\ D e. R.)) -> ( <.A , B >. x. <. C , D >.) = <.((A .R C) +R ( -1R .R (B .R D))) , ((B .R C) +R (A .R D)) >.)
Theorem	eqresr 6733	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- A e. _V   =>   |- ( <.A , 0R >. = <.B , 0R >. <-> A = B)
Theorem	addresr 6734	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- ((A e. R. /\ B e. R.) -> ( <.A , 0R >. + <.B , 0R >.) = <.(A +R B) , 0R >.)
Theorem	mulresr 6735	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- ((A e. R. /\ B e. R.) -> ( <.A , 0R >. x. <.B , 0R >.) = <.(A .R B) , 0R >.)
Theorem	ltresr 6736	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
|- ( <.A , 0R >. <RR <.B , 0R >. <-> A <R B)
Theorem	ltresr2 6737	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
|- ((A e. RR /\ B e. RR) -> (A <RR B <-> ( 1st ` A) <R ( 1st ` B)))
Theorem	dfcnqs 6738	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 6107, 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 CC is a quotient set, even though it is not (compare df-c 6717), 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.)
|- CC = (( R. X. R.) /. `' _E )
Theorem	addcnsrec 6739	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 6738 and mulcnsrec 6740. (Contributed by NM, 13-Aug-1995.)
|- (((A e. R. /\ B e. R.) /\ ( C e. R. /\ D e. R.)) -> ([ <.A , B >.] `' _E + [ <. C , D >.] `' _E ) = [ <.(A +R C) , (B +R D) >.] `' _E )
Theorem	mulcnsrec 6740	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6106, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 6738. (Contributed by NM, 13-Aug-1995.)
|- (((A e. R. /\ B e. R.) /\ ( C e. R. /\ D e. R.)) -> ([ <.A , B >.] `' _E x. [ <. C , D >.] `' _E ) = [ <.((A .R C) +R ( -1R .R (B .R D))) , ((B .R C) +R (A .R D)) >.] `' _E )
Theorem	pitonnlem1 6741*	Lemma for pitonn 6744. 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 6742	Lemma for pitonn 6744. 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 6743*	Lemma for pitonn 6744. 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 6744*	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 6745	The complex numbers form a set. Use cnex 6803 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 6746	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 6775. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 6747	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 6776. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	ax1re 6748	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 6777. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 6776 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 6749	_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 6778. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 6750	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 6779 be used later. Instead, in most cases use addcl 6804. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
Theorem	axaddrcl 6751	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 6780 be used later. Instead, in most cases use readdcl 6805. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Theorem	axmulcl 6752	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 6781 be used later. Instead, in most cases use mulcl 6806. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A x. B) e. CC)
Theorem	axmulrcl 6753	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 6782 be used later. Instead, in most cases use remulcl 6807. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ((A e. RR /\ B e. RR) -> (A x. B) e. RR)
Theorem	axaddcom 6754	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 6783 be used later. Instead, use addcom 6947. 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 6755	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 6784 be used later. Instead, use mulcom 6808. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ((A e. CC /\ B e. CC) -> (A x. B) = (B x. A))
Theorem	axaddass 6756	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 6785 be used later. Instead, use addass 6809. (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 6757	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 6786. (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 6758	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 6787 be used later. Instead, use adddi 6811. (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 6759	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 6788. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- (( _i x. _i) + 1) = 0
Theorem	ax0lt1 6760	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 6789. 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 6761	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 6790. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- (A e. RR -> (A x. 1) = A)
Theorem	ax0id 6762	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 6791. 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 6763*	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 6792. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- (A e. RR -> E.x e. RR (A + x) = 0)
Theorem	axprecex 6764*	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 6793. 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 6765*	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 6794. (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 6766	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 6795. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- (A e. RR -> -. A <RR A)
Theorem	axpre-ltwlin 6767	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 6796. (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 6768	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 6797. (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 6769	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 6798. (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 6770	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 6799. (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 6771	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 6800. (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 6772	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 6801. (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 6773*	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 7697 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 6802. (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 6774	The complex numbers form a set. Proofs should normally use cnex 6803 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 6775	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by theorem axresscn 6746. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 6776	1 is a complex number. Axiom for real and complex numbers, justified by theorem ax1cn 6747. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-1re 6777	1 is a real number. Axiom for real and complex numbers, justified by theorem ax1re 6748. Proofs should use 1re 6824 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 6778	_i is a complex number. Axiom for real and complex numbers, justified by theorem axicn 6749. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 6779	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by theorem axaddcl 6750. Proofs should normally use addcl 6804 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 6780	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axaddrcl 6751. Proofs should normally use readdcl 6805 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ((A e. RR /\ B e. RR) -> (A + B) e. RR)
Axiom	ax-mulcl 6781	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by theorem axmulcl 6752. Proofs should normally use mulcl 6806 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 6782	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by theorem axmulrcl 6753. Proofs should normally use remulcl 6807 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 6783	Addition commutes. Axiom for real and complex numbers, justified by theorem axaddcom 6754. Proofs should normally use addcom 6947 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 6784	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by theorem axmulcom 6755. Proofs should normally use mulcom 6808 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 6785	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axaddass 6756. Proofs should normally use addass 6809 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 6786	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by theorem axmulass 6757. Proofs should normally use mulass 6810 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 6787	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by theorem axdistr 6758. Proofs should normally use adddi 6811 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 6788	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by theorem axi2m1 6759. (Contributed by NM, 29-Jan-1995.)
|- (( _i x. _i) + 1) = 0
Theorem	ax-0lt1 6789	0 is less than 1. Axiom for real and complex numbers, justified by theorem ax0lt1 6760. Proofs should normally use 0lt1 6938 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 6790	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by theorem ax1rid 6761. (Contributed by NM, 29-Jan-1995.)
|- (A e. RR -> (A x. 1) = A)
Axiom	ax-0id 6791	0 is an identity element for real addition. Axiom for real and complex numbers, justified by theorem ax0id 6762. Proofs should normally use addid1 6948 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- (A e. CC -> (A + 0) = A)
Axiom	ax-rnegex 6792*	Existence of negative of real number. Axiom for real and complex numbers, justified by theorem axrnegex 6763. (Contributed by Eric Schmidt, 21-May-2007.)
|- (A e. RR -> E.x e. RR (A + x) = 0)
Axiom	ax-precex 6793*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by theorem axprecex 6764. (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 6794*	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 6765. For naming consistency, use cnre 6821 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 6795	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by theorem ax-pre-ltirr 6795. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- (A e. RR -> -. A <RR A)
Axiom	ax-pre-ltwlin 6796	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by theorem axpre-ltwlin 6767. (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 6797	Ordering on reals is transitive. Axiom for real and complex numbers, justified by theorem axpre-lttrn 6768. (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 6798	Apartness of reals is tight. Axiom for real and complex numbers, justified by theorem axpre-apti 6769. (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 6799	Ordering property of addition on reals. Axiom for real and complex numbers, justified by theorem axpre-ltadd 6770. (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 6800	The product of two positive reals is positive. Axiom for real and complex numbers, justified by theorem axpre-mulgt0 6771. (Contributed by NM, 13-Oct-2005.)
|- ((A e. RR /\ B e. RR) -> (( 0 <RR A /\ 0 <RR B) -> 0 <RR (A x. B)))