P. 83 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8201-8300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axaddcom 8201	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 8243 be used later. Instead, use addcom 8426. 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 8202	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 8244 be used later. Instead, use mulcom 8272. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	axaddass 8203	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 8245 be used later. Instead, use addass 8273. (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 8204	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 8246. (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 8205	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 8247 be used later. Instead, use adddi 8275. (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 8206	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 8248. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( ( _i x. _i ) + 1 ) = 0
Theorem	ax0lt1 8207	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 8249. 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 8208	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 8250. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- ( A e. RR -> ( A x. 1 ) = A )
Theorem	ax0id 8209	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 8251. 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 8210*	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 8252. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Theorem	axprecex 8211*	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 8253. 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 8212*	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 8254. (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 8213	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 8255. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ( A e. RR -> -. A <RR A )
Theorem	axpre-ltwlin 8214	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 8256. (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 8215	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 8257. (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 8216	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 8258. (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 8217	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 8259. (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 8218	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 8260. (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 8219	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 8261. (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	rereceu 8220*	The reciprocal from axprecex 8211 is unique. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( ( A e. RR /\ 0 <RR A ) -> E! x e. RR ( A x. x ) = 1 )
Theorem	recriota 8221*	Two ways to express the reciprocal of a natural number. (Contributed by Jim Kingdon, 11-Jul-2021.)
|- ( N e. N. -> ( iota_ r e. RR ( <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. x. r ) = 1 ) = <. [ <. ( <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	axarch 8222*	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 9256 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 8262. (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 )
Theorem	peano5nnnn 8223*	Peano's inductive postulate. This is a counterpart to peano5nni 9257 designed for real number axioms which involve natural numbers (notably, axcaucvg 8231). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   =>    |- ( ( 1 e. A /\ A. z e. A ( z + 1 ) e. A ) -> N C_ A )
Theorem	nnindnn 8224*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 9270 designed for real number axioms which involve natural numbers (notably, axcaucvg 8231). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( z = 1 -> ( ph <-> ps ) )   &    |- ( z = k -> ( ph <-> ch ) )   &    |- ( z = ( k + 1 ) -> ( ph <-> th ) )   &    |- ( z = A -> ( ph <-> ta ) )   &    |- ps   &    |- ( k e. N -> ( ch -> th ) )   =>    |- ( A e. N -> ta )
Theorem	nntopi 8225*	Mapping from NN to N.. (Contributed by Jim Kingdon, 13-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   =>    |- ( A e. N -> E. z e. N. <. [ <. ( <. { l | l <Q [ <. z , 1o >. ] ~Q } , { u | [ <. z , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. = A )
Theorem	axcaucvglemcl 8226*	Lemma for axcaucvg 8231. Mapping to N. and R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   =>    |- ( ( ph /\ J e. N. ) -> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) e. R. )
Theorem	axcaucvglemf 8227*	Lemma for axcaucvg 8231. Mapping to N. and R. yields a sequence. (Contributed by Jim Kingdon, 9-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ph -> G : N. --> R. )
Theorem	axcaucvglemval 8228*	Lemma for axcaucvg 8231. Value of sequence when mapping to N. and R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ( ph /\ J e. N. ) -> ( F ` <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. ( G ` J ) , 0R >. )
Theorem	axcaucvglemcau 8229*	Lemma for axcaucvg 8231. The result of mapping to N. and R. satisfies the Cauchy condition. (Contributed by Jim Kingdon, 9-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( G ` n ) <R ( ( G ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( G ` k ) <R ( ( G ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )
Theorem	axcaucvglemres 8230*	Lemma for axcaucvg 8231. Mapping the limit from N. and R.. (Contributed by Jim Kingdon, 10-Jul-2021.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   &    |- G = ( j e. N. |-> ( iota_ z e. R. ( F ` <. [ <. ( <. { l | l <Q [ <. j , 1o >. ] ~Q } , { u | [ <. j , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = <. z , 0R >. ) )   =>    |- ( ph -> E. y e. RR A. x e. RR ( 0 <RR x -> E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) ) ) )
Theorem	axcaucvg 8231*	Real number completeness axiom. A Cauchy sequence with a modulus of convergence converges. This is basically Corollary 11.2.13 of [HoTT], p. (varies). The HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / n of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis). Because we are stating this axiom before we have introduced notations for NN or division, we use N for the natural numbers and express a reciprocal in terms of iota_. This construction-dependent theorem should not be referenced directly; instead, use ax-caucvg 8263. (Contributed by Jim Kingdon, 8-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   =>    |- ( ph -> E. y e. RR A. x e. RR ( 0 <RR x -> E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) ) ) )
Theorem	axpre-suploclemres 8232*	Lemma for axpre-suploc 8233. The result. The proof just needs to define B as basically the same set as A (but expressed as a subset of R. rather than a subset of RR), and apply suplocsr 8140. (Contributed by Jim Kingdon, 24-Jan-2024.)
|- ( ph -> A C_ RR )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. RR A. y e. A y <RR x )   &    |- ( ph -> A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) )   &    |- B = { w e. R. | <. w , 0R >. e. A }   =>    |- ( ph -> 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	axpre-suploc 8233*	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound. This construction-dependent theorem should not be referenced directly; instead, use ax-pre-suploc 8264. (Contributed by Jim Kingdon, 23-Jan-2024.) (New usage is discouraged.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> 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 ) ) )
4.1.3  Real and complex number postulates restated as axioms
Axiom	ax-cnex 8234	The complex numbers form a set. Proofs should normally use cnex 8267 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 8235	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 8191. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 8236	1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 8192. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-1re 8237	1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 8193. Proofs should use 1re 8289 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 8238	_i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8194. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 8239	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 8195. Proofs should normally use addcl 8268 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 8240	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 8196. Proofs should normally use readdcl 8269 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Axiom	ax-mulcl 8241	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 8197. Proofs should normally use mulcl 8270 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 8242	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 8198. Proofs should normally use remulcl 8271 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 8243	Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 8201. Proofs should normally use addcom 8426 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 8244	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 8202. Proofs should normally use mulcom 8272 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 8245	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 8203. Proofs should normally use addass 8273 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 8246	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 8204. Proofs should normally use mulass 8274 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 8247	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 8205. Proofs should normally use adddi 8275 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 8248	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 8206. (Contributed by NM, 29-Jan-1995.)
|- ( ( _i x. _i ) + 1 ) = 0
Axiom	ax-0lt1 8249	0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 8207. Proofs should normally use 0lt1 8416 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 8250	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 8208. (Contributed by NM, 29-Jan-1995.)
|- ( A e. RR -> ( A x. 1 ) = A )
Axiom	ax-0id 8251	0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 8209. Proofs should normally use addrid 8427 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Axiom	ax-rnegex 8252*	Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 8210. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Axiom	ax-precex 8253*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 8211. (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 8254*	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 8212. For naming consistency, use cnre 8286 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 8255	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 8255. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ( A e. RR -> -. A <RR A )
Axiom	ax-pre-ltwlin 8256	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 8214. (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 8257	Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 8215. (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 8258	Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 8216. (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 8259	Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 8217. (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 8260	The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 8218. (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 8261	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by Theorem axpre-mulext 8219 (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 8262*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 8222. This axiom should not be used directly; instead use arch 9510 (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 )
Axiom	ax-caucvg 8263*	Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 8231. A Cauchy sequence (as defined here, which has a rate convergence built in) of real numbers converges to a real number. Specifically on rate of convergence, all terms after the nth term must be within 1 / n of the nth term. This axiom should not be used directly; instead use caucvgre 11691 (which is the same, but stated in terms of the NN and 1 / n notations). (Contributed by Jim Kingdon, 19-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   &    |- ( ph -> F : N --> RR )   &    |- ( ph -> A. n e. N A. k e. N ( n <RR k -> ( ( F ` n ) <RR ( ( F ` k ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) /\ ( F ` k ) <RR ( ( F ` n ) + ( iota_ r e. RR ( n x. r ) = 1 ) ) ) ) )   =>    |- ( ph -> E. y e. RR A. x e. RR ( 0 <RR x -> E. j e. N A. k e. N ( j <RR k -> ( ( F ` k ) <RR ( y + x ) /\ y <RR ( ( F ` k ) + x ) ) ) ) )
Axiom	ax-pre-suploc 8264*	An inhabited, bounded-above, located set of reals has a supremum. Locatedness here means that given x < y, either there is an element of the set greater than x, or y is an upper bound. Although this and ax-caucvg 8263 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8263. (Contributed by Jim Kingdon, 23-Jan-2024.)
|- ( ( ( A C_ RR /\ E. x x e. A ) /\ ( E. x e. RR A. y e. A y <RR x /\ A. x e. RR A. y e. RR ( x <RR y -> ( E. z e. A x <RR z \/ A. z e. A z <RR y ) ) ) ) -> 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 8265	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 https://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 8268 should be used. Note that uses of ax-addf 8265 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 8199. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 8266	Multiplication is an operation on the complex numbers. This axiom tells us that x. is defined only on complex numbers which is analogous to the way that other operations are defined, for example see subf 8491 or eff 12374. However, while Metamath can handle this axiom, if we wish to work with weaker complex number axioms, we can avoid it by using the less specific mulcl 8270. Note that uses of ax-mulf 8266 can be eliminated by using the defined operation ( x e. CC , y e. CC |-> ( x x. y ) ) in place of x., as seen in mpomulf 8280. This axiom is justified by Theorem axmulf 8200. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- x. : ( CC X. CC ) --> CC
4.2  Derive the basic properties from the field axioms
4.2.1  Some deductions from the field axioms for complex numbers
Theorem	cnex 8267	Alias for ax-cnex 8234. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 8268	Alias for ax-addcl 8239, for naming consistency with addcli 8294. Use this theorem instead of ax-addcl 8239 or axaddcl 8195. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 8269	Alias for ax-addrcl 8240, for naming consistency with readdcli 8303. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 8270	Alias for ax-mulcl 8241, for naming consistency with mulcli 8295. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 8271	Alias for ax-mulrcl 8242, for naming consistency with remulcli 8304. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 8272	Alias for ax-mulcom 8244, for naming consistency with mulcomi 8296. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 8273	Alias for ax-addass 8245, for naming consistency with addassi 8298. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 8274	Alias for ax-mulass 8246, for naming consistency with mulassi 8299. (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 8275	Alias for ax-distr 8247, for naming consistency with adddii 8300. (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 8276	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 8277	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 8278	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 8279	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	mpomulf 8280*	Multiplication is an operation on complex numbers. Version of ax-mulf 8266 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8241. (Contributed by GG, 16-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
Theorem	adddir 8281	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 8282	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 8283	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )
Theorem	c0ex 8284	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 8285	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 8286*	Alias for ax-cnre 8254, 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	mulrid 8287	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	mullid 8288	Identity law for multiplication. Note: see mulrid 8287 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- ( A e. CC -> ( 1 x. A ) = A )
Theorem	1re 8289	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
Theorem	0re 8290	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 8291	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 0 e. RR )
Theorem	mulridi 8292	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( A x. 1 ) = A
Theorem	mullidi 8293	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( 1 x. A ) = A
Theorem	addcli 8294	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) e. CC
Theorem	mulcli 8295	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) e. CC
Theorem	mulcomi 8296	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) = ( B x. A )
Theorem	mulcomli 8297	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 8298	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 8299	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 8300	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 ) )