P. 81 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 8001-8100   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	recnnre 8001*	Embedding the reciprocal of a natural number into RR. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> <. [ <. ( <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. e. RR )
Theorem	peano1nnnn 8002*	One is an element of NN. This is a counterpart to 1nn 9084 designed for real number axioms which involve natural numbers (notably, axcaucvg 8050). (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. N
Theorem	peano2nnnn 8003*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 9085 designed for real number axioms which involve to natural numbers (notably, axcaucvg 8050). (Contributed by Jim Kingdon, 14-Jul-2021.) (New usage is discouraged.)
|- N = |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) }   =>    |- ( A e. N -> ( A + 1 ) e. N )
Theorem	ltrennb 8004*	Ordering of natural numbers with <N or <RR. (Contributed by Jim Kingdon, 13-Jul-2021.)
|- ( ( J e. N. /\ K e. N. ) -> ( J <N K <-> <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. <RR <. [ <. ( <. { l | l <Q [ <. K , 1o >. ] ~Q } , { u | [ <. K , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) )
Theorem	ltrenn 8005*	Ordering of natural numbers with <N or <RR. (Contributed by Jim Kingdon, 12-Jul-2021.)
|- ( J <N K -> <. [ <. ( <. { l | l <Q [ <. J , 1o >. ] ~Q } , { u | [ <. J , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. <RR <. [ <. ( <. { l | l <Q [ <. K , 1o >. ] ~Q } , { u | [ <. K , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	recidpipr 8006*	Another way of saying that a number times its reciprocal is one. (Contributed by Jim Kingdon, 17-Jul-2021.)
|- ( N e. N. -> ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. .P. <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. ) = 1P )
Theorem	recidpirqlemcalc 8007	Lemma for recidpirq 8008. Rearranging some of the expressions. (Contributed by Jim Kingdon, 17-Jul-2021.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> ( A .P. B ) = 1P )   =>    |- ( ph -> ( ( ( ( A +P. 1P ) .P. ( B +P. 1P ) ) +P. ( 1P .P. 1P ) ) +P. 1P ) = ( ( ( ( A +P. 1P ) .P. 1P ) +P. ( 1P .P. ( B +P. 1P ) ) ) +P. ( 1P +P. 1P ) ) )
Theorem	recidpirq 8008*	A real number times its reciprocal is one, where reciprocal is expressed with *Q. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> ( <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. x. <. [ <. ( <. { l | l <Q ( *Q ` [ <. N , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. N , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. ) = 1 )
4.1.2  Final derivation of real and complex number postulates
Theorem	axcnex 8009	The complex numbers form a set. Use cnex 8086 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 8010	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-resscn 8054. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 8011	1 is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1cn 8055. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	ax1re 8012	1 is a real number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-1re 8056. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 8055 and the other axioms. It is not known whether we can do so here, but the Metamath Proof Explorer proof (accessed 13-Jan-2020) uses excluded middle. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Theorem	axicn 8013	_i is a complex number. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly; instead, use ax-icn 8057. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 8014	Closure law for addition of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addcl 8058 be used later. Instead, in most cases use addcl 8087. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	axaddrcl 8015	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-addrcl 8059 be used later. Instead, in most cases use readdcl 8088. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	axmulcl 8016	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulcl 8060 be used later. Instead, in most cases use mulcl 8089. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	axmulrcl 8017	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, derived from set theory. This construction-dependent theorem should not be referenced directly, nor should the proven axiom ax-mulrcl 8061 be used later. Instead, in most cases use remulcl 8090. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	axaddf 8018	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 8014. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 8084. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- + : ( CC X. CC ) --> CC
Theorem	axmulf 8019	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 8085 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 8089. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- x. : ( CC X. CC ) --> CC
Theorem	axaddcom 8020	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 8062 be used later. Instead, use addcom 8246. 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 8021	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 8063 be used later. Instead, use mulcom 8091. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	axaddass 8022	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 8064 be used later. Instead, use addass 8092. (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 8023	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 8065. (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 8024	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 8066 be used later. Instead, use adddi 8094. (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 8025	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 8067. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( ( _i x. _i ) + 1 ) = 0
Theorem	ax0lt1 8026	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 8068. 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 8027	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 8069. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- ( A e. RR -> ( A x. 1 ) = A )
Theorem	ax0id 8028	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 8070. 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 8029*	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 8071. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Theorem	axprecex 8030*	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 8072. 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 8031*	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 8073. (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 8032	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 8074. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ( A e. RR -> -. A <RR A )
Theorem	axpre-ltwlin 8033	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 8075. (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 8034	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 8076. (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 8035	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 8077. (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 8036	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 8078. (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 8037	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 8079. (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 8038	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 8080. (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 8039*	The reciprocal from axprecex 8030 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 8040*	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 8041*	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 9075 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 8081. (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 8042*	Peano's inductive postulate. This is a counterpart to peano5nni 9076 designed for real number axioms which involve natural numbers (notably, axcaucvg 8050). (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 8043*	Principle of Mathematical Induction (inference schema). This is a counterpart to nnind 9089 designed for real number axioms which involve natural numbers (notably, axcaucvg 8050). (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 8044*	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 8045*	Lemma for axcaucvg 8050. 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 8046*	Lemma for axcaucvg 8050. 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 8047*	Lemma for axcaucvg 8050. 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 8048*	Lemma for axcaucvg 8050. 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 8049*	Lemma for axcaucvg 8050. 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 8050*	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 8082. (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 8051*	Lemma for axpre-suploc 8052. 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 7959. (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 8052*	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 8083. (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 8053	The complex numbers form a set. Proofs should normally use cnex 8086 instead. (New usage is discouraged.) (Contributed by NM, 1-Mar-1995.)
|- CC e. _V
Axiom	ax-resscn 8054	The real numbers are a subset of the complex numbers. Axiom for real and complex numbers, justified by Theorem axresscn 8010. (Contributed by NM, 1-Mar-1995.)
|- RR C_ CC
Axiom	ax-1cn 8055	1 is a complex number. Axiom for real and complex numbers, justified by Theorem ax1cn 8011. (Contributed by NM, 1-Mar-1995.)
|- 1 e. CC
Axiom	ax-1re 8056	1 is a real number. Axiom for real and complex numbers, justified by Theorem ax1re 8012. Proofs should use 1re 8108 instead. (Contributed by Jim Kingdon, 13-Jan-2020.) (New usage is discouraged.)
|- 1 e. RR
Axiom	ax-icn 8057	_i is a complex number. Axiom for real and complex numbers, justified by Theorem axicn 8013. (Contributed by NM, 1-Mar-1995.)
|- _i e. CC
Axiom	ax-addcl 8058	Closure law for addition of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddcl 8014. Proofs should normally use addcl 8087 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 8059	Closure law for addition in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axaddrcl 8015. Proofs should normally use readdcl 8088 instead. (New usage is discouraged.) (Contributed by NM, 22-Nov-1994.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Axiom	ax-mulcl 8060	Closure law for multiplication of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulcl 8016. Proofs should normally use mulcl 8089 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 8061	Closure law for multiplication in the real subfield of complex numbers. Axiom for real and complex numbers, justified by Theorem axmulrcl 8017. Proofs should normally use remulcl 8090 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 8062	Addition commutes. Axiom for real and complex numbers, justified by Theorem axaddcom 8020. Proofs should normally use addcom 8246 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 8063	Multiplication of complex numbers is commutative. Axiom for real and complex numbers, justified by Theorem axmulcom 8021. Proofs should normally use mulcom 8091 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 8064	Addition of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axaddass 8022. Proofs should normally use addass 8092 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 8065	Multiplication of complex numbers is associative. Axiom for real and complex numbers, justified by Theorem axmulass 8023. Proofs should normally use mulass 8093 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 8066	Distributive law for complex numbers (left-distributivity). Axiom for real and complex numbers, justified by Theorem axdistr 8024. Proofs should normally use adddi 8094 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 8067	i-squared equals -1 (expressed as i-squared plus 1 is 0). Axiom for real and complex numbers, justified by Theorem axi2m1 8025. (Contributed by NM, 29-Jan-1995.)
|- ( ( _i x. _i ) + 1 ) = 0
Axiom	ax-0lt1 8068	0 is less than 1. Axiom for real and complex numbers, justified by Theorem ax0lt1 8026. Proofs should normally use 0lt1 8236 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 12-Jan-2020.)
|- 0 <RR 1
Axiom	ax-1rid 8069	1 is an identity element for real multiplication. Axiom for real and complex numbers, justified by Theorem ax1rid 8027. (Contributed by NM, 29-Jan-1995.)
|- ( A e. RR -> ( A x. 1 ) = A )
Axiom	ax-0id 8070	0 is an identity element for real addition. Axiom for real and complex numbers, justified by Theorem ax0id 8028. Proofs should normally use addrid 8247 instead. (New usage is discouraged.) (Contributed by Jim Kingdon, 16-Jan-2020.)
|- ( A e. CC -> ( A + 0 ) = A )
Axiom	ax-rnegex 8071*	Existence of negative of real number. Axiom for real and complex numbers, justified by Theorem axrnegex 8029. (Contributed by Eric Schmidt, 21-May-2007.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Axiom	ax-precex 8072*	Existence of reciprocal of positive real number. Axiom for real and complex numbers, justified by Theorem axprecex 8030. (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 8073*	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 8031. For naming consistency, use cnre 8105 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 8074	Real number less-than is irreflexive. Axiom for real and complex numbers, justified by Theorem ax-pre-ltirr 8074. (Contributed by Jim Kingdon, 12-Jan-2020.)
|- ( A e. RR -> -. A <RR A )
Axiom	ax-pre-ltwlin 8075	Real number less-than is weakly linear. Axiom for real and complex numbers, justified by Theorem axpre-ltwlin 8033. (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 8076	Ordering on reals is transitive. Axiom for real and complex numbers, justified by Theorem axpre-lttrn 8034. (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 8077	Apartness of reals is tight. Axiom for real and complex numbers, justified by Theorem axpre-apti 8035. (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 8078	Ordering property of addition on reals. Axiom for real and complex numbers, justified by Theorem axpre-ltadd 8036. (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 8079	The product of two positive reals is positive. Axiom for real and complex numbers, justified by Theorem axpre-mulgt0 8037. (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 8080	Strong extensionality of multiplication (expressed in terms of <RR). Axiom for real and complex numbers, justified by Theorem axpre-mulext 8038 (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 8081*	Archimedean axiom. Definition 3.1(2) of [Geuvers], p. 9. Axiom for real and complex numbers, justified by Theorem axarch 8041. This axiom should not be used directly; instead use arch 9329 (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 8082*	Completeness. Axiom for real and complex numbers, justified by Theorem axcaucvg 8050. 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 11453 (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 8083*	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 8082 are both completeness properties, countable choice would probably be needed to derive this from ax-caucvg 8082. (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 8084	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 8087 should be used. Note that uses of ax-addf 8084 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 8018. (New usage is discouraged.) (Contributed by NM, 19-Oct-2004.)
|- + : ( CC X. CC ) --> CC
Axiom	ax-mulf 8085	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 8311 or eff 12135. 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 8089. Note that uses of ax-mulf 8085 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 8099. This axiom is justified by Theorem axmulf 8019. (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 8086	Alias for ax-cnex 8053. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- CC e. _V
Theorem	addcl 8087	Alias for ax-addcl 8058, for naming consistency with addcli 8113. Use this theorem instead of ax-addcl 8058 or axaddcl 8014. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	readdcl 8088	Alias for ax-addrcl 8059, for naming consistency with readdcli 8122. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	mulcl 8089	Alias for ax-mulcl 8060, for naming consistency with mulcli 8114. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	remulcl 8090	Alias for ax-mulrcl 8061, for naming consistency with remulcli 8123. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	mulcom 8091	Alias for ax-mulcom 8063, for naming consistency with mulcomi 8115. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	addass 8092	Alias for ax-addass 8064, for naming consistency with addassi 8117. (Contributed by NM, 10-Mar-2008.)
|- ( ( A e. CC /\ B e. CC /\ C e. CC ) -> ( ( A + B ) + C ) = ( A + ( B + C ) ) )
Theorem	mulass 8093	Alias for ax-mulass 8065, for naming consistency with mulassi 8118. (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 8094	Alias for ax-distr 8066, for naming consistency with adddii 8119. (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 8095	A real number is a complex number. (Contributed by NM, 10-Aug-1999.)
|- ( A e. RR -> A e. CC )
Theorem	reex 8096	The real numbers form a set. (Contributed by Mario Carneiro, 17-Nov-2014.)
|- RR e. _V
Theorem	reelprrecn 8097	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 8098	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 8099*	Multiplication is an operation on complex numbers. Version of ax-mulf 8085 using maps-to notation, proved from the axioms of set theory and ax-mulcl 8060. (Contributed by GG, 16-Mar-2025.)
|- ( x e. CC , y e. CC |-> ( x x. y ) ) : ( CC X. CC ) --> CC
Theorem	adddir 8100	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 ) ) )