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	mpv 9401*	Value of multiplication on positive reals. (Contributed by NM, 28-Feb-1996.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) = { x | E. y e. A E. z e. B x = ( y .Q z ) } )
Theorem	dmplp 9402	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom +P. = ( P. X. P. )
Theorem	dmmp 9403	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom .P. = ( P. X. P. )
Theorem	nqpr 9404*	The canonical embedding of the rationals into the reals. (Contributed by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- ( A e. Q. -> { x | x <Q A } e. P. )
Theorem	1pr 9405	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- 1P e. P.
Theorem	addclprlem1 9406	Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ g e. A ) /\ x e. Q. ) -> ( x <Q ( g +Q h ) -> ( ( x .Q ( *Q ` ( g +Q h ) ) ) .Q g ) e. A ) )
Theorem	addclprlem2 9407*	Lemma to prove downward closure in positive real addition. Part of proof of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
|- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x <Q ( g +Q h ) -> x e. ( A +P. B ) ) )
Theorem	addclpr 9408	Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )
Theorem	mulclprlem 9409*	Lemma to prove downward closure in positive real multiplication. Part of proof of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 14-Mar-1996.) (New usage is discouraged.)
|- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x <Q ( g .Q h ) -> x e. ( A .P. B ) ) )
Theorem	mulclpr 9410	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) e. P. )
Theorem	addcompr 9411	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.)
|- ( A +P. B ) = ( B +P. A )
Theorem	addasspr 9412	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
|- ( ( A +P. B ) +P. C ) = ( A +P. ( B +P. C ) )
Theorem	mulcompr 9413	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by NM, 19-Nov-1995.) (New usage is discouraged.)
|- ( A .P. B ) = ( B .P. A )
Theorem	mulasspr 9414	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by NM, 18-Mar-1996.) (New usage is discouraged.)
|- ( ( A .P. B ) .P. C ) = ( A .P. ( B .P. C ) )
Theorem	distrlem1pr 9415	Lemma for distributive law for positive reals. (Contributed by NM, 1-May-1996.) (Revised by Mario Carneiro, 13-Jun-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A .P. ( B +P. C ) ) C_ ( ( A .P. B ) +P. ( A .P. C ) ) )
Theorem	distrlem4pr 9416*	Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) )
Theorem	distrlem5pr 9417	Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A .P. B ) +P. ( A .P. C ) ) C_ ( A .P. ( B +P. C ) ) )
Theorem	distrpr 9418	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by NM, 2-May-1996.) (New usage is discouraged.)
|- ( A .P. ( B +P. C ) ) = ( ( A .P. B ) +P. ( A .P. C ) )
Theorem	1idpr 9419	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.) (New usage is discouraged.)
|- ( A e. P. -> ( A .P. 1P ) = A )
Theorem	ltprord 9420	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 9421	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 9422	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 9423*	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 9424	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 9425	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 9426*	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 9427*	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 9428*	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 9429*	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 9430*	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 9431*	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 9432*	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 9433*	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 9434	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 9435	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 9436	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 9437*	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 9438*	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 9439*	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 9440*	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 9441*	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 9442*	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 9443*	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 9444*	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 9445*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9446	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9447*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9448*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9449*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9450	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9451	Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9452	Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 9510, 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 9453	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 9454	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 9455	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 9456	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
|- ~R e. _V
Theorem	ltrelsr 9457	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 9458	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 9459	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 9460	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 9461*	Decomposing signed reals into positive reals. Lemma for addsrpr 9464 and mulsrpr 9465. (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 9462*	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 9463*	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 9464	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 9465	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 9466	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 9467	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 9468	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 9469	The constant 0R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- 0R e. R.
Theorem	1sr 9470	The constant 1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- 1R e. R.
Theorem	m1r 9471	The constant -1R is a signed real. (Contributed by NM, 9-Aug-1995.) (New usage is discouraged.)
|- -1R e. R.
Theorem	addclsr 9472	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 9473	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 9474	Domain of addition on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
|- dom +R = ( R. X. R. )
Theorem	dmmulsr 9475	Domain of multiplication on signed reals. (Contributed by NM, 25-Aug-1995.) (New usage is discouraged.)
|- dom .R = ( R. X. R. )
Theorem	addcomsr 9476	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 9477	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 9478	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 9479	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 9480	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 9481	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 9482	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 9483	Signed real 'less than' is a strict ordering. (Contributed by NM, 19-Feb-1996.) (New usage is discouraged.)
|- <R Or R.
Theorem	0lt1sr 9484	0 is less than 1 for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
|- 0R <R 1R
Theorem	1ne0sr 9485	1 and 0 are distinct for signed reals. (Contributed by NM, 26-Mar-1996.) (New usage is discouraged.)
|- -. 1R = 0R
Theorem	0idsr 9486	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 9487	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 9488	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 9489	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 9490	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 9491*	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 9492*	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 9493	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 9494	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 9495	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 9496*	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 9497	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 9498	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 9499*	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 9500*	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 ) ) )