P. 95 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 9401-9500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cc 9401	Class of complex numbers.
class CC
Syntax	cr 9402	Class of real numbers.
class RR
Syntax	cc0 9403	Extend class notation to include the complex number 0.
class 0
Syntax	c1 9404	Extend class notation to include the complex number 1.
class 1
Syntax	ci 9405	Extend class notation to include the complex number i.
class _i
Syntax	caddc 9406	Addition on complex numbers.
class +
Syntax	cltrr 9407	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 9408	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 9409	Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 9436. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- CC = ( R. X. R. )
Definition	df-0 9410	Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- 0 = <. 0R , 0R >.
Definition	df-1 9411	Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- 1 = <. 1R , 0R >.
Definition	df-i 9412	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- _i = <. 0R , 1R >.
Definition	df-r 9413	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- RR = ( R. X. { 0R } )
Definition	df-add 9414*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
|- + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
Definition	df-mul 9415*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. 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 9416*	Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 9544. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
Theorem	opelcn 9417	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
|- ( <. A , B >. e. CC <-> ( A e. R. /\ B e. R. ) )
Theorem	opelreal 9418	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- ( <. A , 0R >. e. RR <-> A e. R. )
Theorem	elreal 9419*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
Theorem	elreal2 9420	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
|- ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
Theorem	0ncn 9421	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.)
|- -. (/) e. CC
Theorem	ltrelre 9422	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- <RR C_ ( RR X. RR )
Theorem	addcnsr 9423	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. + <. C , D >. ) = <. ( A +R C ) , ( B +R D ) >. )
Theorem	mulcnsr 9424	Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- ( ( ( 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 9425	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
|- A e. _V   =>    |- ( <. A , 0R >. = <. B , 0R >. <-> A = B )
Theorem	addresr 9426	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , 0R >. )
Theorem	mulresr 9427	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( A .R B ) , 0R >. )
Theorem	ltresr 9428	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- ( <. A , 0R >. <RR <. B , 0R >. <-> A <R B )
Theorem	ltresr2 9429	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <RR B <-> ( 1st ` A ) <R ( 1st ` B ) ) )
Theorem	dfcnqs 9430	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 7295, 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 9409), 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.)
|- CC = ( ( R. X. R. ) /. `' _E )
Theorem	addcnsrec 9431	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 9430 and mulcnsrec 9432. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
|- ( ( ( 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 9432	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecid 7294, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 9430. 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 9133. (Contributed by NM, 13-Aug-1995.) (New usage is discouraged.)
|- ( ( ( 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 )
5.1.2  Final derivation of real and complex number postulates
Theorem	axaddf 9433	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 9439. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 9482. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- + : ( CC X. CC ) --> CC
Theorem	axmulf 9434	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 9441. This construction-dependent theorem should not be referenced directly; instead, use ax-mulf 9483. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- x. : ( CC X. CC ) --> CC
Theorem	axcnex 9435	The complex numbers form a set. This axiom is redundant in the presence of the other axioms (see cnexALT 11135), but the proof requires the axiom of replacement, while the derivation from the construction here does not. Thus, we can avoid ax-rep 4478 in later theorems by invoking the axiom ax-cnex 9459 instead of cnexALT 11135. Use cnex 9484 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 9436	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 9460. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 9437	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 9461. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	axicn 9438	_i 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 9462. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 9439	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 9463 be used later. Instead, in most cases use addcl 9485. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	axaddrcl 9440	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 9464 be used later. Instead, in most cases use readdcl 9486. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	axmulcl 9441	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 9465 be used later. Instead, in most cases use mulcl 9487. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	axmulrcl 9442	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 9466 be used later. Instead, in most cases use remulcl 9488. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	axmulcom 9443	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 9467 be used later. Instead, use mulcom 9489. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	axaddass 9444	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 9468 be used later. Instead, use addass 9490. (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 9445	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 9469. (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 9446	Distributive law for complex numbers (left-distributivity). 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 9470 be used later. Instead, use adddi 9492. (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 9447	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 9471. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( ( _i x. _i ) + 1 ) = 0
Theorem	ax1ne0 9448	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 9472. (Contributed by NM, 19-Mar-1996.) (New usage is discouraged.)
|- 1 =/= 0
Theorem	ax1rid 9449	1 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 9504, based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid 9473. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- ( A e. RR -> ( A x. 1 ) = A )
Theorem	axrnegex 9450*	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 9474. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Theorem	axrrecex 9451*	Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-rrecex 9475. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )
Theorem	axcnre 9452*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, derived from ZF set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-cnre 9476. (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-lttri 9453	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttri 9567. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttri 9477. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <RR B <-> -. ( A = B \/ B <RR A ) ) )
Theorem	axpre-lttrn 9454	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axlttrn 9568. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-lttrn 9478. (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-ltadd 9455	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axltadd 9569. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-ltadd 9479. (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 9456	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version for extended reals is axmulgt0 9570. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-mulgt0 9480. (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-sup 9457*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup 9571. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-sup 9481. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 16-Jun-2013.) (New usage is discouraged.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <RR x ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
Theorem	wuncn 9458	A weak universe containing om contains the complex number construction. This theorem is construction-dependent in the literal sense, but will also be satisfied by any other reasonable implementation of the complex numbers. (Contributed by Mario Carneiro, 2-Jan-2017.)
|- ( ph -> U e. WUni )   &    |- ( ph -> om e. U )   =>    |- ( ph -> CC e. U )
5.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 9459	The complex numbers form a set. This axiom is redundant - see cnexALT 11135- but we provide this axiom because the justification theorem axcnex 9435 does not use ax-rep 4478 even though the redundancy proof does. Proofs should normally use cnex 9484 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 9460	The real numbers are a subset of the complex numbers. Axiom 1 of 22 for real and complex numbers, justified by theorem axresscn 9436. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 9461	1 is a complex number. Axiom 2 of 22 for real and complex numbers, justified by theorem ax1cn 9437. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-icn 9462	_i is a complex number. Axiom 3 of 22 for real and complex numbers, justified by theorem axicn 9438. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 9463	Closure law for addition of complex numbers. Axiom 4 of 22 for real and complex numbers, justified by theorem axaddcl 9439. Proofs should normally use addcl 9485 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 9464	Closure law for addition in the real subfield of complex numbers. Axiom 6 of 23 for real and complex numbers, justified by theorem axaddrcl 9440. Proofs should normally use readdcl 9486 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Axiom	ax-mulcl 9465	Closure law for multiplication of complex numbers. Axiom 6 of 22 for real and complex numbers, justified by theorem axmulcl 9441. Proofs should normally use mulcl 9487 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 9466	Closure law for multiplication in the real subfield of complex numbers. Axiom 7 of 22 for real and complex numbers, justified by theorem axmulrcl 9442. Proofs should normally use remulcl 9488 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Axiom	ax-mulcom 9467	Multiplication of complex numbers is commutative. Axiom 8 of 22 for real and complex numbers, justified by theorem axmulcom 9443. Proofs should normally use mulcom 9489 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 9468	Addition of complex numbers is associative. Axiom 9 of 22 for real and complex numbers, justified by theorem axaddass 9444. Proofs should normally use addass 9490 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 9469	Multiplication of complex numbers is associative. Axiom 10 of 22 for real and complex numbers, justified by theorem axmulass 9445. Proofs should normally use mulass 9491 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 9470	Distributive law for complex numbers (left-distributivity). Axiom 11 of 22 for real and complex numbers, justified by theorem axdistr 9446. Proofs should normally use adddi 9492 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 9471	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom 12 of 22 for real and complex numbers, justified by theorem axi2m1 9447. (Contributed by NM, 29-Jan-1995.)
|- ( ( _i x. _i ) + 1 ) = 0
Axiom	ax-1ne0 9472	1 and 0 are distinct. Axiom 13 of 22 for real and complex numbers, justified by theorem ax1ne0 9448. (Contributed by NM, 29-Jan-1995.)
|- 1 =/= 0
Axiom	ax-1rid 9473	1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, justified by theorem ax1rid 9449. Weakened from the original axiom in the form of statement in mulid1 9504, based on ideas by Eric Schmidt. (Contributed by NM, 29-Jan-1995.)
|- ( A e. RR -> ( A x. 1 ) = A )
Axiom	ax-rnegex 9474*	Existence of negative of real number. Axiom 15 of 22 for real and complex numbers, justified by theorem axrnegex 9450. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Axiom	ax-rrecex 9475*	Existence of reciprocal of nonzero real number. Axiom 16 of 22 for real and complex numbers, justified by theorem axrrecex 9451. (Contributed by Eric Schmidt, 11-Apr-2007.)
|- ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )
Axiom	ax-cnre 9476*	A complex number can be expressed in terms of two reals. Definition 10-1.1(v) of [Gleason] p. 130. Axiom 17 of 22 for real and complex numbers, justified by theorem axcnre 9452. For naming consistency, use cnre 9503 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-lttri 9477	Ordering on reals satisfies strict trichotomy. Axiom 18 of 22 for real and complex numbers, justified by theorem axpre-lttri 9453. Note: The more general version for extended reals is axlttri 9567. Normally new proofs would use xrlttri 11266. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <RR B <-> -. ( A = B \/ B <RR A ) ) )
Axiom	ax-pre-lttrn 9478	Ordering on reals is transitive. Axiom 19 of 22 for real and complex numbers, justified by theorem axpre-lttrn 9454. Note: The more general version for extended reals is axlttrn 9568. Normally new proofs would use lttr 9572. (New usage is discouraged.) (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-ltadd 9479	Ordering property of addition on reals. Axiom 20 of 22 for real and complex numbers, justified by theorem axpre-ltadd 9455. Normally new proofs would use axltadd 9569. (New usage is discouraged.) (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 9480	The product of two positive reals is positive. Axiom 21 of 22 for real and complex numbers, justified by theorem axpre-mulgt0 9456. Normally new proofs would use axmulgt0 9570. (New usage is discouraged.) (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-sup 9481*	A nonempty, bounded-above set of reals has a supremum. Axiom 22 of 22 for real and complex numbers, justified by theorem axpre-sup 9457. Note: Normally new proofs would use axsup 9571. (New usage is discouraged.) (Contributed by NM, 13-Oct-2005.)
|- ( ( A C_ RR /\ A =/= (/) /\ E. x e. RR A. y e. A y <RR x ) -> E. x e. RR ( A. y e. A -. x <RR y /\ A. y e. RR ( y <RR x -> E. z e. A y <RR z ) ) )
Axiom	ax-addf 9482	Addition is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see http://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific addcl 9485 should be used. Note that uses of ax-addf 9482 can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x + y ) ) in place of +, from which this axiom (with the defined operation in place of +) follows as a theorem. This axiom is justified by theorem axaddf 9433. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 9483	Multiplication is an operation on the complex numbers. This deprecated axiom is provided for historical compatibility but is not a bona fide axiom for complex numbers (independent of set theory) since it cannot be interpreted as a first- or second-order statement (see http://us.metamath.org/downloads/schmidt-cnaxioms.pdf). It may be deleted in the future and should be avoided for new theorems. Instead, the less specific ax-mulcl 9465 should be used. Note that uses of ax-mulf 9483 can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x x. y ) ) in place of x., from which this axiom (with the defined operation in place of x.) follows as a theorem. This axiom is justified by theorem axmulf 9434. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- x. : ( CC X. CC ) --> CC
5.2  Derive the basic properties from the field axioms
5.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 9484	Alias for ax-cnex 9459. See also cnexALT 11135. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 9485	Alias for ax-addcl 9463, for naming consistency with addcli 9511. Use this theorem instead of ax-addcl 9463 or axaddcl 9439. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 9486	Alias for ax-addrcl 9464, for naming consistency with readdcli 9520. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 9487	Alias for ax-mulcl 9465, for naming consistency with mulcli 9512. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 9488	Alias for ax-mulrcl 9466, for naming consistency with remulcli 9521. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 9489	Alias for ax-mulcom 9467, for naming consistency with mulcomi 9513. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 9490	Alias for ax-addass 9468, for naming consistency with addassi 9515. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 9491	Alias for ax-mulass 9469, for naming consistency with mulassi 9516. (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 9492	Alias for ax-distr 9470, for naming consistency with adddii 9517. (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 9493	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 9494	The real numbers form a set. See also reexALT 11133. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 9495	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 9496	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	elimne0 9497	Hypothesis for weak deduction theorem to eliminate A =/= 0. (Contributed by NM, 15-May-1999.)
|- if ( A =/= 0 , A , 1 ) =/= 0
Theorem	adddir 9498	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 9499	0 is a complex number. See also 0cnALT 9722. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 9500	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )