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	nsmallnq 9401*	The is no smallest positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> E. x x <Q A )
Theorem	ltbtwnnq 9402*	There exists a number between any two positive fractions. Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 17-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( A <Q B <-> E. x ( A <Q x /\ x <Q B ) )
Theorem	ltrnq 9403	Ordering property of reciprocal for positive fractions. Proposition 9-2.6(iv) of [Gleason] p. 120. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( A <Q B <-> ( *Q ` B ) <Q ( *Q ` A ) )
Theorem	archnq 9404*	For any fraction, there is an integer that is greater than it. This is also known as the "archimedean property". (Contributed by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> E. x e. N. A <Q <. x , 1o >. )
Definition	df-np 9405*	Define the set of positive reals. A "Dedekind cut" is a partition of the positive rational numbers into two classes such that all the numbers of one class are less than all the numbers of the other. A positive real is defined as the lower class of a Dedekind cut. Definition 9-3.1 of [Gleason] p. 121. (Note: This is a "temporary" definition used in the construction of complex numbers df-c 9544, and is intended to be used only by the construction.) (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
|- P. = { x | ( ( (/) C. x /\ x C. Q. ) /\ A. y e. x ( A. z ( z <Q y -> z e. x ) /\ E. z e. x y <Q z ) ) }
Definition	df-1p 9406	Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9544, and is intended to be used only by the construction. Definition of [Gleason] p. 122. (Contributed by NM, 13-Mar-1996.) (New usage is discouraged.)
|- 1P = { x | x <Q 1Q }
Definition	df-plp 9407*	Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, and is intended to be used only by the construction. From Proposition 9-3.5 of [Gleason] p. 123. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- +P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v +Q u ) } )
Definition	df-mp 9408*	Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, and is intended to be used only by the construction. From Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- .P. = ( x e. P. , y e. P. |-> { w | E. v e. x E. u e. y w = ( v .Q u ) } )
Definition	df-ltp 9409*	Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, and is intended to be used only by the construction. From Proposition 9-3.2 of [Gleason] p. 122. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
|- <P = { <. x , y >. | ( ( x e. P. /\ y e. P. ) /\ x C. y ) }
Theorem	npex 9410	The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
|- P. e. _V
Theorem	elnp 9411*	Membership in positive reals. (Contributed by NM, 16-Feb-1996.) (New usage is discouraged.)
|- ( A e. P. <-> ( ( (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y <Q x -> y e. A ) /\ E. y e. A x <Q y ) ) )
Theorem	elnpi 9412*	Membership in positive reals. (Contributed by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( A e. P. <-> ( ( A e. _V /\ (/) C. A /\ A C. Q. ) /\ A. x e. A ( A. y ( y <Q x -> y e. A ) /\ E. y e. A x <Q y ) ) )
Theorem	prn0 9413	A positive real is not empty. (Contributed by NM, 15-May-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( A e. P. -> A =/= (/) )
Theorem	prpssnq 9414	A positive real is a subset of the positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( A e. P. -> A C. Q. )
Theorem	elprnq 9415	A positive real is a set of positive fractions. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. A ) -> B e. Q. )
Theorem	0npr 9416	The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.)
|- -. (/) e. P.
Theorem	prcdnq 9417	A positive real is closed downwards under the positive fractions. Definition 9-3.1 (ii) of [Gleason] p. 121. (Contributed by NM, 25-Feb-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. A ) -> ( C <Q B -> C e. A ) )
Theorem	prub 9418	A positive fraction not in a positive real is an upper bound. Remark (1) of [Gleason] p. 122. (Contributed by NM, 25-Feb-1996.) (New usage is discouraged.)
|- ( ( ( A e. P. /\ B e. A ) /\ C e. Q. ) -> ( -. C e. A -> B <Q C ) )
Theorem	prnmax 9419*	A positive real has no largest member. Definition 9-3.1(iii) of [Gleason] p. 121. (Contributed by NM, 9-Mar-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. A ) -> E. x e. A B <Q x )
Theorem	npomex 9420	A simplifying observation, and an indication of why any attempt to develop a theory of the real numbers without the Axiom of Infinity is doomed to failure: since every member of P. is an infinite set, the negation of Infinity implies that P., and hence RR, is empty. (Note that this proof, which used the fact that Dedekind cuts have no maximum, could just as well have used that they have no minimum, since they are downward-closed by prcdnq 9417 and nsmallnq 9401). (Contributed by Mario Carneiro, 11-May-2013.) (Revised by Mario Carneiro, 16-Nov-2014.) (New usage is discouraged.)
|- ( A e. P. -> om e. _V )
Theorem	prnmadd 9421*	A positive real has no largest member. Addition version. (Contributed by NM, 7-Apr-1996.) (Revised by Mario Carneiro, 11-May-2013.) (New usage is discouraged.)
|- ( ( A e. P. /\ B e. A ) -> E. x ( B +Q x ) e. A )
Theorem	ltrelpr 9422	Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.) (New usage is discouraged.)
|- <P C_ ( P. X. P. )
Theorem	genpv 9423*	Value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) = { f | E. g e. A E. h e. B f = ( g G h ) } )
Theorem	genpelv 9424*	Membership in value of general operation (addition or multiplication) on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( C e. ( A F B ) <-> E. g e. A E. h e. B C = ( g G h ) ) )
Theorem	genpprecl 9425*	Pre-closure law for general operation on positive reals. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( ( C e. A /\ D e. B ) -> ( C G D ) e. ( A F B ) ) )
Theorem	genpdm 9426*	Domain of general operation on positive reals. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- dom F = ( P. X. P. )
Theorem	genpn0 9427*	The result of an operation on positive reals is not empty. (Contributed by NM, 28-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> (/) C. ( A F B ) )
Theorem	genpss 9428*	The result of an operation on positive reals is a subset of the positive fractions. (Contributed by NM, 18-Nov-1995.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) C_ Q. )
Theorem	genpnnp 9429*	The result of an operation on positive reals is different from the set of positive fractions. (Contributed by NM, 29-Feb-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( z e. Q. -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( x G y ) = ( y G x )   =>    |- ( ( A e. P. /\ B e. P. ) -> -. ( A F B ) = Q. )
Theorem	genpcd 9430*	Downward closure of an operation on positive reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x <Q ( g G h ) -> x e. ( A F B ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> ( x <Q f -> x e. ( A F B ) ) ) )
Theorem	genpnmax 9431*	An operation on positive reals has no largest member. (Contributed by NM, 10-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( v e. Q. -> ( z <Q w <-> ( v G z ) <Q ( v G w ) ) )   &    |- ( z G w ) = ( w G z )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( f e. ( A F B ) -> E. x e. ( A F B ) f <Q x ) )
Theorem	genpcl 9432*	Closure of an operation on reals. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 17-Nov-2014.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( h e. Q. -> ( f <Q g <-> ( h G f ) <Q ( h G g ) ) )   &    |- ( x G y ) = ( y G x )   &    |- ( ( ( ( A e. P. /\ g e. A ) /\ ( B e. P. /\ h e. B ) ) /\ x e. Q. ) -> ( x <Q ( g G h ) -> x e. ( A F B ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. P. )
Theorem	genpass 9433*	Associativity of an operation on reals. (Contributed by NM, 18-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)
|- F = ( w e. P. , v e. P. |-> { x | E. y e. w E. z e. v x = ( y G z ) } )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- dom F = ( P. X. P. )   &    |- ( ( f e. P. /\ g e. P. ) -> ( f F g ) e. P. )   &    |- ( ( f G g ) G h ) = ( f G ( g G h ) )   =>    |- ( ( A F B ) F C ) = ( A F ( B F C ) )
Theorem	plpv 9434*	Value of addition 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	mpv 9435*	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 9436	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom +P. = ( P. X. P. )
Theorem	dmmp 9437	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom .P. = ( P. X. P. )
Theorem	nqpr 9438*	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 9439	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 9440	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 9441*	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 9442	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 9443*	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 9444	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 9445	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 9446	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 9447	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 9448	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 9449	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 9450*	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 9451	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 9452	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 9453	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 9454	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 9455	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 9456	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 9457*	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 9458	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 9459	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 9460*	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 9461*	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 9462*	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 9463*	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 9464*	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 9465*	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 9466*	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 9467*	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 9468	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 9469	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 9470	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 9471*	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 9472*	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 9473*	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 9474*	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 9475*	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 9476*	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 9477*	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 9478*	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 9479*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9480	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9481*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9482*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9483*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9484	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9485	Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9486	Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 9544, 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 9487	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 9488	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 9489	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 9490	The equivalence relation for signed reals exists. (Contributed by NM, 25-Jul-1995.) (New usage is discouraged.)
|- ~R e. _V
Theorem	ltrelsr 9491	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 9492	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 9493	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 9494	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 9495*	Decomposing signed reals into positive reals. Lemma for addsrpr 9498 and mulsrpr 9499. (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 9496*	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 9497*	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 9498	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 9499	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 9500	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 ) )