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	addcomnq 9401	Addition of positive fractions is commutative. (Contributed by NM, 30-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A +Q B ) = ( B +Q A )
Theorem	mulcompq 9402	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A .pQ B ) = ( B .pQ A )
Theorem	mulcomnq 9403	Multiplication of positive fractions is commutative. (Contributed by NM, 31-Aug-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A .Q B ) = ( B .Q A )
Theorem	adderpqlem 9404	Lemma for adderpq 9406. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( A +pQ C ) ~Q ( B +pQ C ) ) )
Theorem	mulerpqlem 9405	Lemma for mulerpq 9407. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) /\ C e. ( N. X. N. ) ) -> ( A ~Q B <-> ( A .pQ C ) ~Q ( B .pQ C ) ) )
Theorem	adderpq 9406	Addition is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( /Q ` A ) +Q ( /Q ` B ) ) = ( /Q ` ( A +pQ B ) )
Theorem	mulerpq 9407	Multiplication is compatible with the equivalence relation. (Contributed by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( /Q ` A ) .Q ( /Q ` B ) ) = ( /Q ` ( A .pQ B ) )
Theorem	addassnq 9408	Addition of positive fractions is associative. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( ( A +Q B ) +Q C ) = ( A +Q ( B +Q C ) )
Theorem	mulassnq 9409	Multiplication of positive fractions is associative. (Contributed by NM, 1-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A .Q B ) .Q C ) = ( A .Q ( B .Q C ) )
Theorem	mulcanenq 9410	Lemma for distributive law: cancellation of common factor. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( ( A e. N. /\ B e. N. /\ C e. N. ) -> <. ( A .N B ) , ( A .N C ) >. ~Q <. B , C >. )
Theorem	distrnq 9411	Multiplication of positive fractions is distributive. (Contributed by NM, 2-Sep-1995.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A .Q ( B +Q C ) ) = ( ( A .Q B ) +Q ( A .Q C ) )
Theorem	1nqenq 9412	The equivalence class of ratio 1. (Contributed by NM, 4-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A e. N. -> 1Q ~Q <. A , A >. )
Theorem	mulidnq 9413	Multiplication identity element for positive fractions. (Contributed by NM, 3-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( A .Q 1Q ) = A )
Theorem	recmulnq 9414	Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 28-Apr-2015.) (New usage is discouraged.)
|- ( A e. Q. -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) )
Theorem	recidnq 9415	A positive fraction times its reciprocal is 1. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( A .Q ( *Q ` A ) ) = 1Q )
Theorem	recclnq 9416	Closure law for positive fraction reciprocal. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 8-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( *Q ` A ) e. Q. )
Theorem	recrecnq 9417	Reciprocal of reciprocal of positive fraction. (Contributed by NM, 26-Apr-1996.) (Revised by Mario Carneiro, 29-Apr-2013.) (New usage is discouraged.)
|- ( A e. Q. -> ( *Q ` ( *Q ` A ) ) = A )
Theorem	dmrecnq 9418	Domain of reciprocal on positive fractions. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
|- dom *Q = Q.
Theorem	ltsonq 9419	'Less than' is a strict ordering on positive fractions. (Contributed by NM, 19-Feb-1996.) (Revised by Mario Carneiro, 4-May-2013.) (New usage is discouraged.)
|- <Q Or Q.
Theorem	lterpq 9420	Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013.) (New usage is discouraged.)
|- ( A <pQ B <-> ( /Q ` A ) <Q ( /Q ` B ) )
Theorem	ltanq 9421	Ordering property of addition for positive fractions. Proposition 9-2.6(ii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( C e. Q. -> ( A <Q B <-> ( C +Q A ) <Q ( C +Q B ) ) )
Theorem	ltmnq 9422	Ordering property of multiplication for positive fractions. Proposition 9-2.6(iii) of [Gleason] p. 120. (Contributed by NM, 6-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( C e. Q. -> ( A <Q B <-> ( C .Q A ) <Q ( C .Q B ) ) )
Theorem	1lt2nq 9423	One is less than two (one plus one). (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- 1Q <Q ( 1Q +Q 1Q )
Theorem	ltaddnq 9424	The sum of two fractions is greater than one of them. (Contributed by NM, 14-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( ( A e. Q. /\ B e. Q. ) -> A <Q ( A +Q B ) )
Theorem	ltexnq 9425*	Ordering on positive fractions in terms of existence of sum. Definition in Proposition 9-2.6 of [Gleason] p. 119. (Contributed by NM, 24-Apr-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( B e. Q. -> ( A <Q B <-> E. x ( A +Q x ) = B ) )
Theorem	halfnq 9426*	One-half of any positive fraction exists. Lemma for Proposition 9-2.6(i) of [Gleason] p. 120. (Contributed by NM, 16-Mar-1996.) (Revised by Mario Carneiro, 10-May-2013.) (New usage is discouraged.)
|- ( A e. Q. -> E. x ( x +Q x ) = A )
Theorem	nsmallnq 9427*	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 9428*	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 9429	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 9430*	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 9431*	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 9570, 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 9432	Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 9570, 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 9433*	Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9570, 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 9434*	Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9570, 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 9435*	Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 9570, 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 9436	The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
|- P. e. _V
Theorem	elnp 9437*	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 9438*	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 9439	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 9440	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 9441	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 9442	The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.)
|- -. (/) e. P.
Theorem	prcdnq 9443	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 9444	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 9445*	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 9446	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 9443 and nsmallnq 9427). (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 9447*	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 9448	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 9449*	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 9450*	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 9451*	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 9452*	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 9453*	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 9454*	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 9455*	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 9456*	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 9457*	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 9458*	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 9459*	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 9460*	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 9461*	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 9462	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom +P. = ( P. X. P. )
Theorem	dmmp 9463	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom .P. = ( P. X. P. )
Theorem	nqpr 9464*	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 9465	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 9466	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 9467*	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 9468	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 9469*	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 9470	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 9471	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 9472	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 9473	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 9474	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 9475	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 9476*	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 9477	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 9478	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 9479	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 9480	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 9481	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 9482	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 9483*	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 9484	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 9485	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 9486*	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 9487*	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 9488*	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 9489*	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 9490*	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 9491*	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 9492*	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 9493*	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 9494	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 9495	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 9496	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 9497*	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 9498*	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 9499*	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 9500*	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 )