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	caucvgsrlemcl 7901*	Lemma for caucvgsr 7914. Terms of the sequence from caucvgsrlemgt1 7907 can be mapped to positive reals. (Contributed by Jim Kingdon, 2-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   =>    |- ( ( ph /\ A e. N. ) -> ( iota_ y e. P. ( F ` A ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) e. P. )
Theorem	caucvgsrlemasr 7902*	Lemma for caucvgsr 7914. The lower bound is a signed real. (Contributed by Jim Kingdon, 4-Jul-2021.)
|- ( ph -> A. m e. N. A <R ( F ` m ) )   =>    |- ( ph -> A e. R. )
Theorem	caucvgsrlemfv 7903*	Lemma for caucvgsr 7914. Coercing sequence value from a positive real to a signed real. (Contributed by Jim Kingdon, 29-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ( ph /\ A e. N. ) -> [ <. ( ( G ` A ) +P. 1P ) , 1P >. ] ~R = ( F ` A ) )
Theorem	caucvgsrlemf 7904*	Lemma for caucvgsr 7914. Defining the sequence in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ph -> G : N. --> P. )
Theorem	caucvgsrlemcau 7905*	Lemma for caucvgsr 7914. Defining the Cauchy condition in terms of positive reals. (Contributed by Jim Kingdon, 23-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( G ` n ) <P ( ( G ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( G ` k ) <P ( ( G ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )
Theorem	caucvgsrlembound 7906*	Lemma for caucvgsr 7914. Defining the boundedness condition in terms of positive reals. (Contributed by Jim Kingdon, 25-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   &    |- G = ( x e. N. |-> ( iota_ y e. P. ( F ` x ) = [ <. ( y +P. 1P ) , 1P >. ] ~R ) )   =>    |- ( ph -> A. m e. N. 1P <P ( G ` m ) )
Theorem	caucvgsrlemgt1 7907*	Lemma for caucvgsr 7914. A Cauchy sequence whose terms are greater than one converges. (Contributed by Jim Kingdon, 22-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. 1R <R ( F ` m ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. i e. N. ( j <N i -> ( ( F ` i ) <R ( y +R x ) /\ y <R ( ( F ` i ) +R x ) ) ) ) )
Theorem	caucvgsrlemoffval 7908*	Lemma for caucvgsr 7914. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ( ph /\ J e. N. ) -> ( ( G ` J ) +R A ) = ( ( F ` J ) +R 1R ) )
Theorem	caucvgsrlemofff 7909*	Lemma for caucvgsr 7914. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> G : N. --> R. )
Theorem	caucvgsrlemoffcau 7910*	Lemma for caucvgsr 7914. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( 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	caucvgsrlemoffgt1 7911*	Lemma for caucvgsr 7914. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> A. m e. N. 1R <R ( G ` m ) )
Theorem	caucvgsrlemoffres 7912*	Lemma for caucvgsr 7914. Offsetting the values of the sequence so they are greater than one. (Contributed by Jim Kingdon, 3-Jul-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   &    |- G = ( a e. N. |-> ( ( ( F ` a ) +R 1R ) +R ( A .R -1R ) ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )
Theorem	caucvgsrlembnd 7913*	Lemma for caucvgsr 7914. A Cauchy sequence with a lower bound converges. (Contributed by Jim Kingdon, 19-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   &    |- ( ph -> A. m e. N. A <R ( F ` m ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )
Theorem	caucvgsr 7914*	A Cauchy sequence of signed reals with a modulus of convergence converges to a signed real. 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). This is similar to caucvgprpr 7824 but is for signed reals rather than positive reals. Here is an outline of how we prove it: 1. Choose a lower bound for the sequence (see caucvgsrlembnd 7913). 2. Offset each element of the sequence so that each element of the resulting sequence is greater than one (greater than zero would not suffice, because the limit as well as the elements of the sequence need to be positive) (see caucvgsrlemofff 7909). 3. Since a signed real (element of R.) which is greater than zero can be mapped to a positive real (element of P.), perform that mapping on each element of the sequence and invoke caucvgprpr 7824 to get a limit (see caucvgsrlemgt1 7907). 4. Map the resulting limit from positive reals back to signed reals (see caucvgsrlemgt1 7907). 5. Offset that limit so that we get the limit of the original sequence rather than the limit of the offsetted sequence (see caucvgsrlemoffres 7912). (Contributed by Jim Kingdon, 20-Jun-2021.)
|- ( ph -> F : N. --> R. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <R ( ( F ` k ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) /\ ( F ` k ) <R ( ( F ` n ) +R [ <. ( <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. +P. 1P ) , 1P >. ] ~R ) ) ) )   =>    |- ( ph -> E. y e. R. A. x e. R. ( 0R <R x -> E. j e. N. A. k e. N. ( j <N k -> ( ( F ` k ) <R ( y +R x ) /\ y <R ( ( F ` k ) +R x ) ) ) ) )
Theorem	ltpsrprg 7915	Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
|- ( ( A e. P. /\ B e. P. /\ C e. R. ) -> ( ( C +R [ <. A , 1P >. ] ~R ) <R ( C +R [ <. B , 1P >. ] ~R ) <-> A <P B ) )
Theorem	mappsrprg 7916	Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
|- ( ( A e. P. /\ C e. R. ) -> ( C +R -1R ) <R ( C +R [ <. A , 1P >. ] ~R ) )
Theorem	map2psrprg 7917*	Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.)
|- ( C e. R. -> ( ( C +R -1R ) <R A <-> E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A ) )
Theorem	suplocsrlemb 7918*	Lemma for suplocsr 7921. The set B is located. (Contributed by Jim Kingdon, 18-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> A. u e. P. A. v e. P. ( u <P v -> ( E. q e. B u <P q \/ A. q e. B q <P v ) ) )
Theorem	suplocsrlempr 7919*	Lemma for suplocsr 7921. The set B has a least upper bound. (Contributed by Jim Kingdon, 19-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. v e. P. ( A. w e. B -. v <P w /\ A. w e. P. ( w <P v -> E. u e. B w <P u ) ) )
Theorem	suplocsrlem 7920*	Lemma for suplocsr 7921. The set A has a least upper bound. (Contributed by Jim Kingdon, 16-Jan-2024.)
|- B = { w e. P. | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- ( ph -> A C_ R. )   &    |- ( ph -> C e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
Theorem	suplocsr 7921*	An inhabited, bounded, located set of signed reals has a supremum. (Contributed by Jim Kingdon, 22-Jan-2024.)
|- ( ph -> E. x x e. A )   &    |- ( ph -> E. x e. R. A. y e. A y <R x )   &    |- ( ph -> A. x e. R. A. y e. R. ( x <R y -> ( E. z e. A x <R z \/ A. z e. A z <R y ) ) )   =>    |- ( ph -> E. x e. R. ( A. y e. A -. x <R y /\ A. y e. R. ( y <R x -> E. z e. A y <R z ) ) )
Syntax	cc 7922	Class of complex numbers.
class CC
Syntax	cr 7923	Class of real numbers.
class RR
Syntax	cc0 7924	Extend class notation to include the complex number 0.
class 0
Syntax	c1 7925	Extend class notation to include the complex number 1.
class 1
Syntax	ci 7926	Extend class notation to include the complex number i.
class _i
Syntax	caddc 7927	Addition on complex numbers.
class +
Syntax	cltrr 7928	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 7929	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 7930	Define the set of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- CC = ( R. X. R. )
Definition	df-0 7931	Define the complex number 0. (Contributed by NM, 22-Feb-1996.)
|- 0 = <. 0R , 0R >.
Definition	df-1 7932	Define the complex number 1. (Contributed by NM, 22-Feb-1996.)
|- 1 = <. 1R , 0R >.
Definition	df-i 7933	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.)
|- _i = <. 0R , 1R >.
Definition	df-r 7934	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.)
|- RR = ( R. X. { 0R } )
Definition	df-add 7935*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.)
|- + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
Definition	df-mul 7936*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.)
|- x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) }
Definition	df-lt 7937*	Define 'less than' on the real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
Theorem	opelcn 7938	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.)
|- ( <. A , B >. e. CC <-> ( A e. R. /\ B e. R. ) )
Theorem	opelreal 7939	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.)
|- ( <. A , 0R >. e. RR <-> A e. R. )
Theorem	elreal 7940*	Membership in class of real numbers. (Contributed by NM, 31-Mar-1996.)
|- ( A e. RR <-> E. x e. R. <. x , 0R >. = A )
Theorem	elrealeu 7941*	The real number mapping in elreal 7940 is unique. (Contributed by Jim Kingdon, 11-Jul-2021.)
|- ( A e. RR <-> E! x e. R. <. x , 0R >. = A )
Theorem	elreal2 7942	Ordered pair membership in the class of complex numbers. (Contributed by Mario Carneiro, 15-Jun-2013.)
|- ( A e. RR <-> ( ( 1st ` A ) e. R. /\ A = <. ( 1st ` A ) , 0R >. ) )
Theorem	0ncn 7943	The empty set is not a complex number. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. See also cnm 7944 which is a related property. (Contributed by NM, 2-May-1996.)
|- -. (/) e. CC
Theorem	cnm 7944*	A complex number is an inhabited set. Note: do not use this after the real number axioms are developed, since it is a construction-dependent property. (Contributed by Jim Kingdon, 23-Oct-2023.) (New usage is discouraged.)
|- ( A e. CC -> E. x x e. A )
Theorem	ltrelre 7945	'Less than' is a relation on real numbers. (Contributed by NM, 22-Feb-1996.)
|- <RR C_ ( RR X. RR )
Theorem	addcnsr 7946	Addition of complex numbers in terms of signed reals. (Contributed by NM, 28-May-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. + <. C , D >. ) = <. ( A +R C ) , ( B +R D ) >. )
Theorem	mulcnsr 7947	Multiplication of complex numbers in terms of signed reals. (Contributed by NM, 9-Aug-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( <. A , B >. x. <. C , D >. ) = <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. )
Theorem	eqresr 7948	Equality of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- A e. _V   =>    |- ( <. A , 0R >. = <. B , 0R >. <-> A = B )
Theorem	addresr 7949	Addition of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. + <. B , 0R >. ) = <. ( A +R B ) , 0R >. )
Theorem	mulresr 7950	Multiplication of real numbers in terms of intermediate signed reals. (Contributed by NM, 10-May-1996.)
|- ( ( A e. R. /\ B e. R. ) -> ( <. A , 0R >. x. <. B , 0R >. ) = <. ( A .R B ) , 0R >. )
Theorem	ltresr 7951	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
|- ( <. A , 0R >. <RR <. B , 0R >. <-> A <R B )
Theorem	ltresr2 7952	Ordering of real subset of complex numbers in terms of signed reals. (Contributed by NM, 22-Feb-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A <RR B <-> ( 1st ` A ) <R ( 1st ` B ) ) )
Theorem	dfcnqs 7953	Technical trick to permit reuse of previous lemmas to prove arithmetic operation laws in CC from those in R.. The trick involves qsid 6686, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) acts as an identity divisor for the quotient set operation. This lets us "pretend" that CC is a quotient set, even though it is not (compare df-c 7930), and allows us to reuse some of the equivalence class lemmas we developed for the transition from positive reals to signed reals, etc. (Contributed by NM, 13-Aug-1995.)
|- CC = ( ( R. X. R. ) /. `' _E )
Theorem	addcnsrec 7954	Technical trick to permit re-use of some equivalence class lemmas for operation laws. See dfcnqs 7953 and mulcnsrec 7955. (Contributed by NM, 13-Aug-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E + [ <. C , D >. ] `' _E ) = [ <. ( A +R C ) , ( B +R D ) >. ] `' _E )
Theorem	mulcnsrec 7955	Technical trick to permit re-use of some equivalence class lemmas for operation laws. The trick involves ecidg 6685, which shows that the coset of the converse epsilon relation (which is not an equivalence relation) leaves a set unchanged. See also dfcnqs 7953. (Contributed by NM, 13-Aug-1995.)
|- ( ( ( A e. R. /\ B e. R. ) /\ ( C e. R. /\ D e. R. ) ) -> ( [ <. A , B >. ] `' _E x. [ <. C , D >. ] `' _E ) = [ <. ( ( A .R C ) +R ( -1R .R ( B .R D ) ) ) , ( ( B .R C ) +R ( A .R D ) ) >. ] `' _E )
Theorem	addvalex 7956	Existence of a sum. This is dependent on how we define + so once we proceed to real number axioms we will replace it with theorems such as addcl 8049. (Contributed by Jim Kingdon, 14-Jul-2021.)
|- ( ( A e. V /\ B e. W ) -> ( A + B ) e. _V )
Theorem	pitonnlem1 7957*	Lemma for pitonn 7960. Two ways to write the number one. (Contributed by Jim Kingdon, 24-Apr-2020.)
|- <. [ <. ( <. { l | l <Q [ <. 1o , 1o >. ] ~Q } , { u | [ <. 1o , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. = 1
Theorem	pitonnlem1p1 7958	Lemma for pitonn 7960. Simplifying an expression involving signed reals. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- ( A e. P. -> [ <. ( A +P. ( 1P +P. 1P ) ) , ( 1P +P. 1P ) >. ] ~R = [ <. ( A +P. 1P ) , 1P >. ] ~R )
Theorem	pitonnlem2 7959*	Lemma for pitonn 7960. Two ways to add one to a number. (Contributed by Jim Kingdon, 24-Apr-2020.)
|- ( K e. N. -> ( <. [ <. ( <. { l | l <Q [ <. K , 1o >. ] ~Q } , { u | [ <. K , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. + 1 ) = <. [ <. ( <. { l | l <Q [ <. ( K +N 1o ) , 1o >. ] ~Q } , { u | [ <. ( K +N 1o ) , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	pitonn 7960*	Mapping from N. to NN. (Contributed by Jim Kingdon, 22-Apr-2020.)
|- ( N e. N. -> <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. e. |^| { x | ( 1 e. x /\ A. y e. x ( y + 1 ) e. x ) } )
Theorem	pitoregt0 7961*	Embedding from N. to RR yields a number greater than zero. (Contributed by Jim Kingdon, 15-Jul-2021.)
|- ( N e. N. -> 0 <RR <. [ <. ( <. { l | l <Q [ <. N , 1o >. ] ~Q } , { u | [ <. N , 1o >. ] ~Q <Q u } >. +P. 1P ) , 1P >. ] ~R , 0R >. )
Theorem	pitore 7962*	Embedding from N. to RR. Similar to pitonn 7960 but separate in the sense that we have not proved nnssre 9039 yet. (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 >. e. RR )
Theorem	recnnre 7963*	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 7964*	One is an element of NN. This is a counterpart to 1nn 9046 designed for real number axioms which involve natural numbers (notably, axcaucvg 8012). (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 7965*	A successor of a positive integer is a positive integer. This is a counterpart to peano2nn 9047 designed for real number axioms which involve to natural numbers (notably, axcaucvg 8012). (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 7966*	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 7967*	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 7968*	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 7969	Lemma for recidpirq 7970. 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 7970*	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 7971	The complex numbers form a set. Use cnex 8048 instead. (Contributed by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- CC e. _V
Theorem	axresscn 7972	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 8016. (Contributed by NM, 1-Mar-1995.) (Proof shortened by Andrew Salmon, 12-Aug-2011.) (New usage is discouraged.)
|- RR C_ CC
Theorem	ax1cn 7973	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 8017. (Contributed by NM, 12-Apr-2007.) (New usage is discouraged.)
|- 1 e. CC
Theorem	ax1re 7974	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 8018. In the Metamath Proof Explorer, this is not a complex number axiom but is proved from ax-1cn 8017 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 7975	_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 8019. (Contributed by NM, 23-Feb-1996.) (New usage is discouraged.)
|- _i e. CC
Theorem	axaddcl 7976	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 8020 be used later. Instead, in most cases use addcl 8049. (Contributed by NM, 14-Jun-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
Theorem	axaddrcl 7977	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 8021 be used later. Instead, in most cases use readdcl 8050. (Contributed by NM, 31-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. RR /\ B e. RR ) -> ( A + B ) e. RR )
Theorem	axmulcl 7978	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 8022 be used later. Instead, in most cases use mulcl 8051. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) e. CC )
Theorem	axmulrcl 7979	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 8023 be used later. Instead, in most cases use remulcl 8052. (New usage is discouraged.) (Contributed by NM, 31-Mar-1996.)
|- ( ( A e. RR /\ B e. RR ) -> ( A x. B ) e. RR )
Theorem	axaddf 7980	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 7976. This construction-dependent theorem should not be referenced directly; instead, use ax-addf 8046. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- + : ( CC X. CC ) --> CC
Theorem	axmulf 7981	Multiplication is an operation on the complex numbers. This is the construction-dependent version of ax-mulf 8047 and it should not be referenced outside the construction. We generally prefer to develop our theory using the less specific mulcl 8051. (Contributed by NM, 8-Feb-2005.) (New usage is discouraged.)
|- x. : ( CC X. CC ) --> CC
Theorem	axaddcom 7982	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 8024 be used later. Instead, use addcom 8208. 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 7983	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 8025 be used later. Instead, use mulcom 8053. (Contributed by NM, 31-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. CC /\ B e. CC ) -> ( A x. B ) = ( B x. A ) )
Theorem	axaddass 7984	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 8026 be used later. Instead, use addass 8054. (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 7985	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 8027. (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 7986	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 8028 be used later. Instead, use adddi 8056. (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 7987	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 8029. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( ( _i x. _i ) + 1 ) = 0
Theorem	ax0lt1 7988	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 8030. 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 7989	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 8031. (Contributed by Scott Fenton, 3-Jan-2013.) (New usage is discouraged.)
|- ( A e. RR -> ( A x. 1 ) = A )
Theorem	ax0id 7990	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 8032. 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 7991*	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 8033. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( A e. RR -> E. x e. RR ( A + x ) = 0 )
Theorem	axprecex 7992*	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 8034. 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 7993*	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 8035. (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 7994	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 8036. (Contributed by Jim Kingdon, 12-Jan-2020.) (New usage is discouraged.)
|- ( A e. RR -> -. A <RR A )
Theorem	axpre-ltwlin 7995	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 8037. (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 7996	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 8038. (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 7997	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 8039. (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 7998	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 8040. (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 7999	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 8041. (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 8000	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 8042. (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 ) ) )