P. 95 of Theorem List - Metamath Proof Explorer

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

Type	Label	Description
Statement
Theorem	ltprord 9401	Positive real 'less than' in terms of proper subset. (Contributed by NM, 20-Feb-1996.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> ( A <P B <-> A C. B ) )
Theorem	psslinpr 9402	Proper subset is a linear ordering on positive reals. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> ( A C. B \/ A = B \/ B C. A ) )
Theorem	ltsopr 9403	Positive real 'less than' is a strict ordering. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
|- <P Or P.
Theorem	prlem934 9404*	Lemma 9-3.4 of [Gleason] p. 122. (Contributed by NM, 25-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- B e. _V   =>    |- ( A e. P. -> E. x e. A -. ( x +Q B ) e. A )
Theorem	ltaddpr 9405	The sum of two positive reals is greater than one of them. Proposition 9-3.5(iii) of [Gleason] p. 123. (Contributed by NM, 26-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> A <P ( A +P. B ) )
Theorem	ltaddpr2 9406	The sum of two positive reals is greater than one of them. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- ( C e. P. -> ( ( A +P. B ) = C -> A <P C ) )
Theorem	ltexprlem1 9407*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( B e. P. -> ( A C. B -> C =/= (/) ) )
Theorem	ltexprlem2 9408*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 3-Apr-1996.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( B e. P. -> C C. Q. )
Theorem	ltexprlem3 9409*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( B e. P. -> ( x e. C -> A. z ( z <Q x -> z e. C ) ) )
Theorem	ltexprlem4 9410*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( B e. P. -> ( x e. C -> E. z ( z e. C /\ x <Q z ) ) )
Theorem	ltexprlem5 9411*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 6-Apr-1996.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( ( B e. P. /\ A C. B ) -> C e. P. )
Theorem	ltexprlem6 9412*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> ( A +P. C ) C_ B )
Theorem	ltexprlem7 9413*	Lemma for Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }   =>    |- ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> B C_ ( A +P. C ) )
Theorem	ltexpri 9414*	Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
|- ( A <P B -> E. x e. P. ( A +P. x ) = B )
Theorem	ltaprlem 9415	Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.)
|- ( C e. P. -> ( A <P B -> ( C +P. A ) <P ( C +P. B ) ) )
Theorem	ltapr 9416	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.) (New usage is discouraged.)
|- ( C e. P. -> ( A <P B <-> ( C +P. A ) <P ( C +P. B ) ) )
Theorem	addcanpr 9417	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by NM, 9-Apr-1996.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) )
Theorem	prlem936 9418*	Lemma 9-3.6 of [Gleason] p. 124. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ 1Q <Q B ) -> E. x e. A -. ( x .Q B ) e. A )
Theorem	reclem2pr 9419*	Lemma for Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- B = { x | E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) }   =>    |- ( A e. P. -> B e. P. )
Theorem	reclem3pr 9420*	Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- B = { x | E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) }   =>    |- ( A e. P. -> 1P C_ ( A .P. B ) )
Theorem	reclem4pr 9421*	Lemma for Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 30-Apr-1996.) (New usage is discouraged.)
|- B = { x | E. y ( x <Q y /\ -. ( *Q ` y ) e. A ) }   =>    |- ( A e. P. -> ( A .P. B ) = 1P )
Theorem	recexpr 9422*	The reciprocal of a positive real exists. Part of Proposition 9-3.7(v) of [Gleason] p. 124. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- ( A e. P. -> E. x e. P. ( A .P. x ) = 1P )
Theorem	suplem1pr 9423*	The union of a nonempty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- ( ( A =/= (/) /\ E. x e. P. A. y e. A y <P x ) -> U. A e. P. )
Theorem	suplem2pr 9424*	The union of a set of positive reals (if a positive real) is its supremum (the least upper bound). Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- ( A C_ P. -> ( ( y e. A -> -. U. A <P y ) /\ ( y <P U. A -> E. z e. A y <P z ) ) )
Theorem	supexpr 9425*	The union of a nonempty, bounded set of positive reals has a supremum. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (New usage is discouraged.)
|- ( ( A =/= (/) /\ E. x e. P. A. y e. A y <P x ) -> E. x e. P. ( A. y e. A -. x <P y /\ A. y e. P. ( y <P x -> E. z e. A y <P z ) ) )
Definition	df-enr 9426*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
|- ~R = { <. x , y >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. z E. w E. v E. u ( ( x = <. z , w >. /\ y = <. v , u >. ) /\ ( z +P. u ) = ( w +P. v ) ) ) }
Definition	df-nr 9427	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
|- R. = ( ( P. X. P. ) /. ~R )
Definition	df-plr 9428*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
|- +R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. f ) >. ] ~R ) ) }
Definition	df-mr 9429*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
|- .R = { <. <. x , y >. , z >. | ( ( x e. R. /\ y e. R. ) /\ E. w E. v E. u E. f ( ( x = [ <. w , v >. ] ~R /\ y = [ <. u , f >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ] ~R ) ) }
Definition	df-ltr 9430*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.4 of [Gleason] p. 127. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
|- <R = { <. x , y >. | ( ( x e. R. /\ y e. R. ) /\ E. z E. w E. v E. u ( ( x = [ <. z , w >. ] ~R /\ y = [ <. v , u >. ] ~R ) /\ ( z +P. u ) <P ( w +P. v ) ) ) }
Definition	df-0r 9431	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- 0R = [ <. 1P , 1P >. ] ~R
Definition	df-1r 9432	Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. From Proposition 9-4.2 of [Gleason] p. 126. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- 1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
Definition	df-m1r 9433	Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 9491, and is intended to be used only by the construction. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- -1R = [ <. 1P , ( 1P +P. 1P ) >. ] ~R
Theorem	enrbreq 9434	Equivalence relation for signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( <. A , B >. ~R <. C , D >. <-> ( A +P. D ) = ( B +P. C ) ) )
Theorem	enrer 9435	The equivalence relation for signed reals is an equivalence relation. Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 6-Jul-2015.) (New usage is discouraged.)
|- ~R Er ( P. X. P. )
Theorem	enreceq 9436	Equivalence class equality of positive fractions in terms of positive integers. (Contributed by NM, 29-Nov-1995.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R = [ <. C , D >. ] ~R <-> ( A +P. D ) = ( B +P. C ) ) )
Theorem	enrex 9437	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
|- ~R e. _V
Theorem	ltrelsr 9438	Signed real 'less than' is a relation on signed reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
|- <R C_ ( R. X. R. )
Theorem	addcmpblnr 9439	Lemma showing compatibility of addition. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( A +P. F ) , ( B +P. G ) >. ~R <. ( C +P. R ) , ( D +P. S ) >. ) )
Theorem	mulcmpblnrlem 9440	Lemma used in lemma showing compatibility of multiplication. (Contributed by NM, 4-Sep-1995.) (New usage is discouraged.)
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) )
Theorem	mulcmpblnr 9441	Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995.) (New usage is discouraged.)
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( ( A .P. F ) +P. ( B .P. G ) ) , ( ( A .P. G ) +P. ( B .P. F ) ) >. ~R <. ( ( C .P. R ) +P. ( D .P. S ) ) , ( ( C .P. S ) +P. ( D .P. R ) ) >. ) )
Theorem	prsrlem1 9442*	Decomposing signed reals into positive reals. Lemma for addsrpr 9445 and mulsrpr 9446. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ( ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) /\ ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ ( A = [ <. s , f >. ] ~R /\ B = [ <. g , h >. ] ~R ) ) ) -> ( ( ( ( w e. P. /\ v e. P. ) /\ ( s e. P. /\ f e. P. ) ) /\ ( ( u e. P. /\ t e. P. ) /\ ( g e. P. /\ h e. P. ) ) ) /\ ( ( w +P. f ) = ( v +P. s ) /\ ( u +P. h ) = ( t +P. g ) ) ) )
Theorem	addsrmo 9443*	There is at most one result from adding signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( w +P. u ) , ( v +P. t ) >. ] ~R ) )
Theorem	mulsrmo 9444*	There is at most one result from multiplying signed reals. (Contributed by Jim Kingdon, 30-Dec-2019.)
|- ( ( A e. ( ( P. X. P. ) /. ~R ) /\ B e. ( ( P. X. P. ) /. ~R ) ) -> E* z E. w E. v E. u E. t ( ( A = [ <. w , v >. ] ~R /\ B = [ <. u , t >. ] ~R ) /\ z = [ <. ( ( w .P. u ) +P. ( v .P. t ) ) , ( ( w .P. t ) +P. ( v .P. u ) ) >. ] ~R ) )
Theorem	addsrpr 9445	Addition of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R +R [ <. C , D >. ] ~R ) = [ <. ( A +P. C ) , ( B +P. D ) >. ] ~R )
Theorem	mulsrpr 9446	Multiplication of signed reals in terms of positive reals. (Contributed by NM, 3-Sep-1995.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( [ <. A , B >. ] ~R .R [ <. C , D >. ] ~R ) = [ <. ( ( A .P. C ) +P. ( B .P. D ) ) , ( ( A .P. D ) +P. ( B .P. C ) ) >. ] ~R )
Theorem	ltsrpr 9447	Ordering of signed reals in terms of positive reals. (Contributed by NM, 20-Feb-1996.) (Revised by Mario Carneiro, 12-Aug-2015.) (New usage is discouraged.)
|- ( [ <. A , B >. ] ~R <R [ <. C , D >. ] ~R <-> ( A +P. D ) <P ( B +P. C ) )
Theorem	gt0srpr 9448	Greater than zero in terms of positive reals. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- ( 0R <R [ <. A , B >. ] ~R <-> B <P A )
Theorem	0nsr 9449	The empty set is not a signed real. (Contributed by NM, 25-Aug-1995.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
|- -. (/) e. R.
Theorem	0r 9450	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- 0R e. R.
Theorem	1sr 9451	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- 1R e. R.
Theorem	m1r 9452	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- -1R e. R.
Theorem	addclsr 9453	Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
|- ( ( A e. R. /\ B e. R. ) -> ( A +R B ) e. R. )
Theorem	mulclsr 9454	Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995.) (New usage is discouraged.)
|- ( ( A e. R. /\ B e. R. ) -> ( A .R B ) e. R. )
Theorem	dmaddsr 9455	Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
|- dom +R = ( R. X. R. )
Theorem	dmmulsr 9456	Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
|- dom .R = ( R. X. R. )
Theorem	addcomsr 9457	Addition of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
|- ( A +R B ) = ( B +R A )
Theorem	addasssr 9458	Addition of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
|- ( ( A +R B ) +R C ) = ( A +R ( B +R C ) )
Theorem	mulcomsr 9459	Multiplication of signed reals is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
|- ( A .R B ) = ( B .R A )
Theorem	mulasssr 9460	Multiplication of signed reals is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
|- ( ( A .R B ) .R C ) = ( A .R ( B .R C ) )
Theorem	distrsr 9461	Multiplication of signed reals is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
|- ( A .R ( B +R C ) ) = ( ( A .R B ) +R ( A .R C ) )
Theorem	m1p1sr 9462	Minus one plus one is zero for signed reals. (Contributed by NM, 5-May-1996.) (New usage is discouraged.)
|- ( -1R +R 1R ) = 0R
Theorem	m1m1sr 9463	Minus one times minus one is plus one for signed reals. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
|- ( -1R .R -1R ) = 1R
Theorem	ltsosr 9464	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.) (New usage is discouraged.)
|- <R Or R.
Theorem	0lt1sr 9465	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
|- 0R <R 1R
Theorem	1ne0sr 9466	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
|- -. 1R = 0R
Theorem	0idsr 9467	The signed real number 0 is an identity element for addition of signed reals. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.)
|- ( A e. R. -> ( A +R 0R ) = A )
Theorem	1idsr 9468	1 is an identity element for multiplication. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
|- ( A e. R. -> ( A .R 1R ) = A )
Theorem	00sr 9469	A signed real times 0 is 0. (Contributed by NM, 10-Apr-1996.) (New usage is discouraged.)
|- ( A e. R. -> ( A .R 0R ) = 0R )
Theorem	ltasr 9470	Ordering property of addition. (Contributed by NM, 10-May-1996.) (New usage is discouraged.)
|- ( C e. R. -> ( A <R B <-> ( C +R A ) <R ( C +R B ) ) )
Theorem	pn0sr 9471	A signed real plus its negative is zero. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
|- ( A e. R. -> ( A +R ( A .R -1R ) ) = 0R )
Theorem	negexsr 9472*	Existence of negative signed real. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
|- ( A e. R. -> E. x e. R. ( A +R x ) = 0R )
Theorem	recexsrlem 9473*	The reciprocal of a positive signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( 0R <R A -> E. x e. R. ( A .R x ) = 1R )
Theorem	addgt0sr 9474	The sum of two positive signed reals is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
|- ( ( 0R <R A /\ 0R <R B ) -> 0R <R ( A +R B ) )
Theorem	mulgt0sr 9475	The product of two positive signed reals is positive. (Contributed by NM, 13-May-1996.) (New usage is discouraged.)
|- ( ( 0R <R A /\ 0R <R B ) -> 0R <R ( A .R B ) )
Theorem	sqgt0sr 9476	The square of a nonzero signed real is positive. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
|- ( ( A e. R. /\ A =/= 0R ) -> 0R <R ( A .R A ) )
Theorem	recexsr 9477*	The reciprocal of a nonzero signed real exists. Part of Proposition 9-4.3 of [Gleason] p. 126. (Contributed by NM, 15-May-1996.) (New usage is discouraged.)
|- ( ( A e. R. /\ A =/= 0R ) -> E. x e. R. ( A .R x ) = 1R )
Theorem	mappsrpr 9478	Mapping from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
|- C e. R.   =>    |- ( ( C +R -1R ) <R ( C +R [ <. A , 1P >. ] ~R ) <-> A e. P. )
Theorem	ltpsrpr 9479	Mapping of order from positive signed reals to positive reals. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
|- C e. R.   =>    |- ( ( C +R [ <. A , 1P >. ] ~R ) <R ( C +R [ <. B , 1P >. ] ~R ) <-> A <P B )
Theorem	map2psrpr 9480*	Equivalence for positive signed real. (Contributed by NM, 17-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
|- C e. R.   =>    |- ( ( C +R -1R ) <R A <-> E. x e. P. ( C +R [ <. x , 1P >. ] ~R ) = A )
Theorem	supsrlem 9481*	Lemma for supremum theorem. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
|- B = { w | ( C +R [ <. w , 1P >. ] ~R ) e. A }   &    |- C e. R.   =>    |- ( ( C e. A /\ E. x e. R. A. y e. A y <R x ) -> 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	supsr 9482*	A nonempty, bounded set of signed reals has a supremum. (Contributed by NM, 21-May-1996.) (Revised by Mario Carneiro, 15-Jun-2013.) (New usage is discouraged.)
|- ( ( A =/= (/) /\ E. x e. R. A. y e. A y <R x ) -> 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 9483	Class of complex numbers.
class CC
Syntax	cr 9484	Class of real numbers.
class RR
Syntax	cc0 9485	Extend class notation to include the complex number 0.
class 0
Syntax	c1 9486	Extend class notation to include the complex number 1.
class 1
Syntax	ci 9487	Extend class notation to include the complex number i.
class _i
Syntax	caddc 9488	Addition on complex numbers.
class +
Syntax	cltrr 9489	'Less than' predicate (defined over real subset of complex numbers).
class <RR
Syntax	cmul 9490	Multiplication on complex numbers. The token x. is a center dot.
class x.
Definition	df-c 9491	Define the set of complex numbers. The 23 axioms for complex numbers start at axresscn 9518. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- CC = ( R. X. R. )
Definition	df-0 9492	Define the complex number 0. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- 0 = <. 0R , 0R >.
Definition	df-1 9493	Define the complex number 1. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- 1 = <. 1R , 0R >.
Definition	df-i 9494	Define the complex number _i (the imaginary unit). (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- _i = <. 0R , 1R >.
Definition	df-r 9495	Define the set of real numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- RR = ( R. X. { 0R } )
Definition	df-add 9496*	Define addition over complex numbers. (Contributed by NM, 28-May-1995.) (New usage is discouraged.)
|- + = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +R u ) , ( v +R f ) >. ) ) }
Definition	df-mul 9497*	Define multiplication over complex numbers. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- x. = { <. <. x , y >. , z >. | ( ( x e. CC /\ y e. CC ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .R u ) +R ( -1R .R ( v .R f ) ) ) , ( ( v .R u ) +R ( w .R f ) ) >. ) ) }
Definition	df-lt 9498*	Define 'less than' on the real subset of complex numbers. Proofs should typically use < instead; see df-ltxr 9626. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- <RR = { <. x , y >. | ( ( x e. RR /\ y e. RR ) /\ E. z E. w ( ( x = <. z , 0R >. /\ y = <. w , 0R >. ) /\ z <R w ) ) }
Theorem	opelcn 9499	Ordered pair membership in the class of complex numbers. (Contributed by NM, 14-May-1996.) (New usage is discouraged.)
|- ( <. A , B >. e. CC <-> ( A e. R. /\ B e. R. ) )
Theorem	opelreal 9500	Ordered pair membership in class of real subset of complex numbers. (Contributed by NM, 22-Feb-1996.) (New usage is discouraged.)
|- ( <. A , 0R >. e. RR <-> A e. R. )