P. 80 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	axaddass 7901	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 7943 be used later. Instead, use addass 7971. (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 7902	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 7944. (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 7903	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 7945 be used later. Instead, use adddi 7973. (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 7904	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 7946. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( ( _i x. _i ) + 1 ) = 0
Theorem	ax0lt1 7905	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 7947. 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 7906	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 7948. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- ( A e. RR -> ( A x. 1 ) = A )
Theorem	ax0id 7907	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 7949. 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 7908*	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 7950. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Theorem	axprecex 7909*	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 7951. 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 7910*	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 7952. (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 7911	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 7953. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ( A e. RR -> -. A <RR A )
Theorem	axpre-ltwlin 7912	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 7954. (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 7913	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 7955. (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 7914	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 7956. (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 7915	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 7957. (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 7916	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 7958. (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 7917	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 7959. (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 7918*	The reciprocal from axprecex 7909 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 7919*	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 7920*	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 8951 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 7960. (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 7921*	Peano's inductive postulate. This is a counterpart to peano5nni 8952 designed for real number axioms which involve natural numbers (notably, axcaucvg 7929). (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 7922*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 8965 designed for real number axioms which involve natural numbers (notably, axcaucvg 7929). (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 7923*	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 7924*	Lemma for axcaucvg 7929. 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 7925*	Lemma for axcaucvg 7929. 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 7926*	Lemma for axcaucvg 7929. 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 7927*	Lemma for axcaucvg 7929. 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 7928*	Lemma for axcaucvg 7929. 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 7929*	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 7961. (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 7930*	Lemma for axpre-suploc 7931. 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 7838. (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 7931*	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 7962. (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 7932	The complex numbers form a set. Proofs should normally use cnex 7965 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 7933	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 7889. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 7934	1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 7890. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-1re 7935	1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 7891. Proofs should use 1re 7986 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 7936	_i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 7892. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 7937	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 7893. Proofs should normally use addcl 7966 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 7938	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 7894. Proofs should normally use readdcl 7967 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Axiom	ax-mulcl 7939	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 7895. Proofs should normally use mulcl 7968 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 7940	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 7896. Proofs should normally use remulcl 7969 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 7941	Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 7899. Proofs should normally use addcom 8124 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 7942	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 7900. Proofs should normally use mulcom 7970 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 7943	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 7901. Proofs should normally use addass 7971 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 7944	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 7902. Proofs should normally use mulass 7972 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 7945	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 7903. Proofs should normally use adddi 7973 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 7946	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 7904. (Contributed by NM, 29-Jan-1995.)
|- ( ( _i x. _i ) + 1 ) = 0
Axiom	ax-0lt1 7947	0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 7905. Proofs should normally use 0lt1 8114 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 7948	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 7906. (Contributed by NM, 29-Jan-1995.)
|- ( A e. RR -> ( A x. 1 ) = A )
Axiom	ax-0id 7949	0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 7907. Proofs should normally use addrid 8125 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Axiom	ax-rnegex 7950*	Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 7908. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Axiom	ax-precex 7951*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 7909. (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 7952*	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 7910. For naming consistency, use cnre 7983 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 7953	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 7953. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ( A e. RR -> -. A <RR A )
Axiom	ax-pre-ltwlin 7954	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 7912. (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 7955	Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 7913. (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 7956	Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 7914. (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 7957	Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 7915. (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 7958	The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 7916. (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 7959	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by Theorem axpre-mulext 7917 (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 7960*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 7920. This axiom should not be used directly; instead use arch 9203 (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 7961*	Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 7929. 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 11022 (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 7962*	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 7961 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 7961. (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 7963	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 7966 should be used. Note that uses of ax-addf 7963 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 7897. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 7964	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 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 ax-mulcl 7939 should be used. Note that uses of ax-mulf 7964 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 7898. (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 7965	Alias for ax-cnex 7932. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 7966	Alias for ax-addcl 7937, for naming consistency with addcli 7991. Use this theorem instead of ax-addcl 7937 or axaddcl 7893. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 7967	Alias for ax-addrcl 7938, for naming consistency with readdcli 8000. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 7968	Alias for ax-mulcl 7939, for naming consistency with mulcli 7992. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 7969	Alias for ax-mulrcl 7940, for naming consistency with remulcli 8001. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 7970	Alias for ax-mulcom 7942, for naming consistency with mulcomi 7993. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 7971	Alias for ax-addass 7943, for naming consistency with addassi 7995. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 7972	Alias for ax-mulass 7944, for naming consistency with mulassi 7996. (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 7973	Alias for ax-distr 7945, for naming consistency with adddii 7997. (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 7974	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 7975	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 7976	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 7977	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 7978	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 7979	0 is a complex number. (Contributed by NM, 19-Feb-2005.)
|- 0 e. CC
Theorem	0cnd 7980	0 is a complex number, deductive form. (Contributed by David A. Wheeler, 8-Dec-2018.)
|- ( ph -> 0 e. CC )
Theorem	c0ex 7981	0 is a set (common case). (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 0 e. _V
Theorem	1ex 7982	1 is a set. Common special case. (Contributed by David A. Wheeler, 7-Jul-2016.)
|- 1 e. _V
Theorem	cnre 7983*	Alias for ax-cnre 7952, 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 7984	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 7985	Identity law for multiplication. Note: see mulrid 7984 for commuted version. (Contributed by NM, 8-Oct-1999.)
|- ( A e. CC -> ( 1 x. A ) = A )
Theorem	1re 7986	1 is a real number. (Contributed by Jim Kingdon, 13-Jan-2020.)
|- 1 e. RR
Theorem	0re 7987	0 is a real number. (Contributed by Eric Schmidt, 21-May-2007.) (Revised by Scott Fenton, 3-Jan-2013.)
|- 0 e. RR
Theorem	0red 7988	0 is a real number, deductive form. (Contributed by David A. Wheeler, 6-Dec-2018.)
|- ( ph -> 0 e. RR )
Theorem	mulid1i 7989	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( A x. 1 ) = A
Theorem	mullidi 7990	Identity law for multiplication. (Contributed by NM, 14-Feb-1995.)
|- A e. CC   =>    |- ( 1 x. A ) = A
Theorem	addcli 7991	Closure law for addition. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A + B ) e. CC
Theorem	mulcli 7992	Closure law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) e. CC
Theorem	mulcomi 7993	Commutative law for multiplication. (Contributed by NM, 23-Nov-1994.)
|- A e. CC   &    |- B e. CC   =>    |- ( A x. B ) = ( B x. A )
Theorem	mulcomli 7994	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 7995	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 7996	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 7997	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 7998	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 7999	A real number is a complex number. (Contributed by NM, 1-Mar-1995.)
|- A e. RR   =>    |- A e. CC
Theorem	readdcli 8000	Closure law for addition of reals. (Contributed by NM, 17-Jan-1997.)
|- A e. RR   &    |- B e. RR   =>    |- ( A + B ) e. RR