P. 89 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 8801-8900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dmrecnq 8801	Domain of reciprocal on positive fractions. (Contributed by Mario Carneiro, 6-Mar-1996.) (Revised by Mario Carneiro, 10-Jul-2014.) (New usage is discouraged.)
|- dom *Q = Q.
Theorem	ltsonq 8802	'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 8803	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 8804	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 8805	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 8806	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 8807	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 8808*	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 8809*	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 8810*	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 8811*	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 8812	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 8813*	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 8814*	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 8952, 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 8815	Define the positive real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8816*	Define addition on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8817*	Define multiplication on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8818*	Define ordering on positive reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8819	The class of positive reals is a set. (Contributed by NM, 31-Oct-1995.) (New usage is discouraged.)
|- P. e. _V
Theorem	elnp 8820*	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 8821*	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 8822	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 8823	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 8824	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 8825	The empty set is not a positive real. (Contributed by NM, 15-Nov-1995.) (New usage is discouraged.)
|- -. (/) e. P.
Theorem	prcdnq 8826	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 8827	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 8828*	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 8829	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 8826 and nsmallnq 8810). (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 8830*	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 8831	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 8832*	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 8833*	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 8834*	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 8835*	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 8836*	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 8837*	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 8838*	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 8839*	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 8840*	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 8841*	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 8842*	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 8843*	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 8844*	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 8845	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom +P. = ( P. X. P. )
Theorem	dmmp 8846	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.) (New usage is discouraged.)
|- dom .P. = ( P. X. P. )
Theorem	nqpr 8847*	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 8848	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 8849	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 8850*	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 8851	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 8852*	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 8853	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 8854	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 8855	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 8856	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 8857	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 8858	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 8859*	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 8860	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 8861	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 8862	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 8863	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 8864	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 8865	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 8866*	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 8867	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 8868	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 8869*	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 8870*	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 8871*	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 8872*	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 8873*	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 8874*	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 8875*	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 8876*	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 8877	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 8878	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 8879	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 8880*	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 8881*	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 8882*	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 8883*	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 8884*	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 8885*	The union of a non-empty, 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 8886*	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 8887*	The union of a non-empty, 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-plpr 8888*	Define pre-addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- +pR = { <. <. x , y >. , z >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( w +P. u ) , ( v +P. f ) >. ) ) }
Definition	df-mpr 8889*	Define pre-multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, and is intended to be used only by the construction. From Proposition 9-4.1 of [Gleason] p. 126. (Contributed by NM, 3-Sep-1995.) (New usage is discouraged.)
|- .pR = { <. <. x , y >. , z >. | ( ( x e. ( P. X. P. ) /\ y e. ( P. X. P. ) ) /\ E. w E. v E. u E. f ( ( x = <. w , v >. /\ y = <. u , f >. ) /\ z = <. ( ( w .P. u ) +P. ( v .P. f ) ) , ( ( w .P. f ) +P. ( v .P. u ) ) >. ) ) }
Definition	df-enr 8890*	Define equivalence relation for signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8891	Define class of signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8892*	Define addition on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 , v >. +pR <. u , f >. ) ] ~R ) ) }
Definition	df-mr 8893*	Define multiplication on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 , v >. .pR <. u , f >. ) ] ~R ) ) }
Definition	df-ltr 8894*	Define ordering relation on signed reals. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8895	Define signed real constant 0. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8896	Define signed real constant 1. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8897	Define signed real constant -1. This is a "temporary" set used in the construction of complex numbers df-c 8952, 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 8898	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 8899	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 8900	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 ) ) )