P. 67 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 6601-6700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	prarloc 6601*	A Dedekind cut is arithmetically located. Part of Proposition 11.15 of [BauerTaylor], p. 52, slightly modified. It states that given a tolerance P, there are elements of the lower and upper cut which are within that tolerance of each other. Usually, proofs will be shorter if they use prarloc2 6602 instead. (Contributed by Jim Kingdon, 22-Oct-2019.)
|- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. a e. L E. b e. U b <Q ( a +Q P ) )
Theorem	prarloc2 6602*	A Dedekind cut is arithmetically located. This is a variation of prarloc 6601 which only constructs one (named) point and is therefore often easier to work with. It states that given a tolerance P, there are elements of the lower and upper cut which are exactly that tolerance from each other. (Contributed by Jim Kingdon, 26-Dec-2019.)
|- ( ( <. L , U >. e. P. /\ P e. Q. ) -> E. a e. L ( a +Q P ) e. U )
Theorem	ltrelpr 6603	Positive real 'less than' is a relation on positive reals. (Contributed by NM, 14-Feb-1996.)
|- <P C_ ( P. X. P. )
Theorem	ltdfpr 6604*	More convenient form of df-iltp 6568. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A <P B <-> E. q e. Q. ( q e. ( 2nd ` A ) /\ q e. ( 1st ` B ) ) ) )
Theorem	genpdflem 6605*	Simplification of upper or lower cut expression. Lemma for genpdf 6606. (Contributed by Jim Kingdon, 30-Sep-2019.)
|- ( ( ph /\ r e. A ) -> r e. Q. )   &    |- ( ( ph /\ s e. B ) -> s e. Q. )   =>    |- ( ph -> { q e. Q. | E. r e. Q. E. s e. Q. ( r e. A /\ s e. B /\ q = ( r G s ) ) } = { q e. Q. | E. r e. A E. s e. B q = ( r G s ) } )
Theorem	genpdf 6606*	Simplified definition of addition or multiplication on positive reals. (Contributed by Jim Kingdon, 30-Sep-2019.)
|- F = ( w e. P. , v e. P. |-> <. { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 1st ` w ) /\ s e. ( 1st ` v ) /\ q = ( r G s ) ) } , { q e. Q. | E. r e. Q. E. s e. Q. ( r e. ( 2nd ` w ) /\ s e. ( 2nd ` v ) /\ q = ( r G s ) ) } >. )   =>    |- F = ( w e. P. , v e. P. |-> <. { q e. Q. | E. r e. ( 1st ` w ) E. s e. ( 1st ` v ) q = ( r G s ) } , { q e. Q. | E. r e. ( 2nd ` w ) E. s e. ( 2nd ` v ) q = ( r G s ) } >. )
Theorem	genipv 6607*	Value of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingon, 3-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` 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 ) = <. { q e. Q. | E. r e. ( 1st ` A ) E. s e. ( 1st ` B ) q = ( r G s ) } , { q e. Q. | E. r e. ( 2nd ` A ) E. s e. ( 2nd ` B ) q = ( r G s ) } >. )
Theorem	genplt2i 6608*	Operating on both sides of two inequalities, when the operation is consistent with <Q. (Contributed by Jim Kingdon, 6-Oct-2019.)
|- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   =>    |- ( ( A <Q B /\ C <Q D ) -> ( A G C ) <Q ( B G D ) )
Theorem	genpelxp 6609*	Set containing the result of adding or multiplying positive reals. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( A F B ) e. ( ~P Q. X. ~P Q. ) )
Theorem	genpelvl 6610*	Membership in lower cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( C e. ( 1st ` ( A F B ) ) <-> E. g e. ( 1st ` A ) E. h e. ( 1st ` B ) C = ( g G h ) ) )
Theorem	genpelvu 6611*	Membership in upper cut of general operation (addition or multiplication) on positive reals. (Contributed by Jim Kingdon, 15-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( C e. ( 2nd ` ( A F B ) ) <-> E. g e. ( 2nd ` A ) E. h e. ( 2nd ` B ) C = ( g G h ) ) )
Theorem	genpprecll 6612*	Pre-closure law for general operation on lower cuts. (Contributed by Jim Kingdon, 2-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( ( C e. ( 1st ` A ) /\ D e. ( 1st ` B ) ) -> ( C G D ) e. ( 1st ` ( A F B ) ) ) )
Theorem	genppreclu 6613*	Pre-closure law for general operation on upper cuts. (Contributed by Jim Kingdon, 7-Nov-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( ( C e. ( 2nd ` A ) /\ D e. ( 2nd ` B ) ) -> ( C G D ) e. ( 2nd ` ( A F B ) ) ) )
Theorem	genipdm 6614*	Domain of general operation on positive reals. (Contributed by Jim Kingdon, 2-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- dom F = ( P. X. P. )
Theorem	genpml 6615*	The lower cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> E. q e. Q. q e. ( 1st ` ( A F B ) ) )
Theorem	genpmu 6616*	The upper cut produced by addition or multiplication on positive reals is inhabited. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   =>    |- ( ( A e. P. /\ B e. P. ) -> E. q e. Q. q e. ( 2nd ` ( A F B ) ) )
Theorem	genpcdl 6617*	Downward closure of an operation on positive reals. (Contributed by Jim Kingdon, 14-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( ( ( A e. P. /\ g e. ( 1st ` A ) ) /\ ( B e. P. /\ h e. ( 1st ` B ) ) ) /\ x e. Q. ) -> ( x <Q ( g G h ) -> x e. ( 1st ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( f e. ( 1st ` ( A F B ) ) -> ( x <Q f -> x e. ( 1st ` ( A F B ) ) ) ) )
Theorem	genpcuu 6618*	Upward closure of an operation on positive reals. (Contributed by Jim Kingdon, 8-Nov-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( ( ( A e. P. /\ g e. ( 2nd ` A ) ) /\ ( B e. P. /\ h e. ( 2nd ` B ) ) ) /\ x e. Q. ) -> ( ( g G h ) <Q x -> x e. ( 2nd ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> ( f e. ( 2nd ` ( A F B ) ) -> ( f <Q x -> x e. ( 2nd ` ( A F B ) ) ) ) )
Theorem	genprndl 6619*	The lower cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ( ( A e. P. /\ g e. ( 1st ` A ) ) /\ ( B e. P. /\ h e. ( 1st ` B ) ) ) /\ x e. Q. ) -> ( x <Q ( g G h ) -> x e. ( 1st ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> A. q e. Q. ( q e. ( 1st ` ( A F B ) ) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` ( A F B ) ) ) ) )
Theorem	genprndu 6620*	The upper cut produced by addition or multiplication on positive reals is rounded. (Contributed by Jim Kingdon, 7-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   &    |- ( ( ( ( A e. P. /\ g e. ( 2nd ` A ) ) /\ ( B e. P. /\ h e. ( 2nd ` B ) ) ) /\ x e. Q. ) -> ( ( g G h ) <Q x -> x e. ( 2nd ` ( A F B ) ) ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> A. r e. Q. ( r e. ( 2nd ` ( A F B ) ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` ( A F B ) ) ) ) )
Theorem	genpdisj 6621*	The lower and upper cuts produced by addition or multiplication on positive reals are disjoint. (Contributed by Jim Kingdon, 15-Oct-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` v ) /\ x = ( y G z ) ) } >. )   &    |- ( ( y e. Q. /\ z e. Q. ) -> ( y G z ) e. Q. )   &    |- ( ( x e. Q. /\ y e. Q. /\ z e. Q. ) -> ( x <Q y <-> ( z G x ) <Q ( z G y ) ) )   &    |- ( ( x e. Q. /\ y e. Q. ) -> ( x G y ) = ( y G x ) )   =>    |- ( ( A e. P. /\ B e. P. ) -> A. q e. Q. -. ( q e. ( 1st ` ( A F B ) ) /\ q e. ( 2nd ` ( A F B ) ) ) )
Theorem	genpassl 6622*	Associativity of lower cuts. Lemma for genpassg 6624. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` 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 e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f G g ) G h ) = ( f G ( g G h ) ) )   =>    |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 1st ` ( ( A F B ) F C ) ) = ( 1st ` ( A F ( B F C ) ) ) )
Theorem	genpassu 6623*	Associativity of upper cuts. Lemma for genpassg 6624. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` 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 e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f G g ) G h ) = ( f G ( g G h ) ) )   =>    |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 2nd ` ( ( A F B ) F C ) ) = ( 2nd ` ( A F ( B F C ) ) ) )
Theorem	genpassg 6624*	Associativity of an operation on reals. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- F = ( w e. P. , v e. P. |-> <. { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 1st ` w ) /\ z e. ( 1st ` v ) /\ x = ( y G z ) ) } , { x e. Q. | E. y e. Q. E. z e. Q. ( y e. ( 2nd ` w ) /\ z e. ( 2nd ` 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 e. Q. /\ g e. Q. /\ h e. Q. ) -> ( ( f G g ) G h ) = ( f G ( g G h ) ) )   =>    |- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A F B ) F C ) = ( A F ( B F C ) ) )
Theorem	addnqprllem 6625	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ( ( <. L , U >. e. P. /\ G e. L ) /\ X e. Q. ) -> ( X <Q S -> ( ( X .Q ( *Q ` S ) ) .Q G ) e. L ) )
Theorem	addnqprulem 6626	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ( ( <. L , U >. e. P. /\ G e. U ) /\ X e. Q. ) -> ( S <Q X -> ( ( X .Q ( *Q ` S ) ) .Q G ) e. U ) )
Theorem	addnqprl 6627	Lemma to prove downward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ( ( ( ( A e. P. /\ G e. ( 1st ` A ) ) /\ ( B e. P. /\ H e. ( 1st ` B ) ) ) /\ X e. Q. ) -> ( X <Q ( G +Q H ) -> X e. ( 1st ` ( A +P. B ) ) ) )
Theorem	addnqpru 6628	Lemma to prove upward closure in positive real addition. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ( ( ( ( A e. P. /\ G e. ( 2nd ` A ) ) /\ ( B e. P. /\ H e. ( 2nd ` B ) ) ) /\ X e. Q. ) -> ( ( G +Q H ) <Q X -> X e. ( 2nd ` ( A +P. B ) ) ) )
Theorem	addlocprlemlt 6629	Lemma for addlocpr 6634. The Q <Q ( D +Q E ) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( Q <Q ( D +Q E ) -> Q e. ( 1st ` ( A +P. B ) ) ) )
Theorem	addlocprlemeqgt 6630	Lemma for addlocpr 6634. This is a step used in both the Q = ( D +Q E ) and ( D +Q E ) <Q Q cases. (Contributed by Jim Kingdon, 7-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( U +Q T ) <Q ( ( D +Q E ) +Q ( P +Q P ) ) )
Theorem	addlocprlemeq 6631	Lemma for addlocpr 6634. The Q = ( D +Q E ) case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( Q = ( D +Q E ) -> R e. ( 2nd ` ( A +P. B ) ) ) )
Theorem	addlocprlemgt 6632	Lemma for addlocpr 6634. The ( D +Q E ) <Q Q case. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( ( D +Q E ) <Q Q -> R e. ( 2nd ` ( A +P. B ) ) ) )
Theorem	addlocprlem 6633	Lemma for addlocpr 6634. The result, in deduction form. (Contributed by Jim Kingdon, 6-Dec-2019.)
|- ( ph -> A e. P. )   &    |- ( ph -> B e. P. )   &    |- ( ph -> Q <Q R )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> ( Q +Q ( P +Q P ) ) = R )   &    |- ( ph -> D e. ( 1st ` A ) )   &    |- ( ph -> U e. ( 2nd ` A ) )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> E e. ( 1st ` B ) )   &    |- ( ph -> T e. ( 2nd ` B ) )   &    |- ( ph -> T <Q ( E +Q P ) )   =>    |- ( ph -> ( Q e. ( 1st ` ( A +P. B ) ) \/ R e. ( 2nd ` ( A +P. B ) ) ) )
Theorem	addlocpr 6634*	Locatedness of addition on positive reals. Lemma 11.16 in [BauerTaylor], p. 53. The proof in BauerTaylor relies on signed rationals, so we replace it with another proof which applies prarloc 6601 to both A and B, and uses nqtri3or 6494 rather than prloc 6589 to decide whether q is too big to be in the lower cut of A +P. B (and deduce that if it is, then r must be in the upper cut). What the two proofs have in common is that they take the difference between q and r to determine how tight a range they need around the real numbers. (Contributed by Jim Kingdon, 5-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` ( A +P. B ) ) \/ r e. ( 2nd ` ( A +P. B ) ) ) ) )
Theorem	addclpr 6635	Closure of addition on positive reals. First statement of Proposition 9-3.5 of [Gleason] p. 123. Combination of Lemma 11.13 and Lemma 11.16 in [BauerTaylor], p. 53. (Contributed by NM, 13-Mar-1996.)
|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) e. P. )
Theorem	plpvlu 6636*	Value of addition on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = <. { x e. Q. | E. y e. ( 1st ` A ) E. z e. ( 1st ` B ) x = ( y +Q z ) } , { x e. Q. | E. y e. ( 2nd ` A ) E. z e. ( 2nd ` B ) x = ( y +Q z ) } >. )
Theorem	mpvlu 6637*	Value of multiplication on positive reals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) = <. { x e. Q. | E. y e. ( 1st ` A ) E. z e. ( 1st ` B ) x = ( y .Q z ) } , { x e. Q. | E. y e. ( 2nd ` A ) E. z e. ( 2nd ` B ) x = ( y .Q z ) } >. )
Theorem	dmplp 6638	Domain of addition on positive reals. (Contributed by NM, 18-Nov-1995.)
|- dom +P. = ( P. X. P. )
Theorem	dmmp 6639	Domain of multiplication on positive reals. (Contributed by NM, 18-Nov-1995.)
|- dom .P. = ( P. X. P. )
Theorem	nqprm 6640*	A cut produced from a rational is inhabited. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( A e. Q. -> ( E. q e. Q. q e. { x | x <Q A } /\ E. r e. Q. r e. { x | A <Q x } ) )
Theorem	nqprrnd 6641*	A cut produced from a rational is rounded. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( A e. Q. -> ( A. q e. Q. ( q e. { x | x <Q A } <-> E. r e. Q. ( q <Q r /\ r e. { x | x <Q A } ) ) /\ A. r e. Q. ( r e. { x | A <Q x } <-> E. q e. Q. ( q <Q r /\ q e. { x | A <Q x } ) ) ) )
Theorem	nqprdisj 6642*	A cut produced from a rational is disjoint. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( A e. Q. -> A. q e. Q. -. ( q e. { x | x <Q A } /\ q e. { x | A <Q x } ) )
Theorem	nqprloc 6643*	A cut produced from a rational is located. Lemma for nqprlu 6645. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( A e. Q. -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. { x | x <Q A } \/ r e. { x | A <Q x } ) ) )
Theorem	nqprxx 6644*	The canonical embedding of the rationals into the reals, expressed with the same variable for the lower and upper cuts. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( A e. Q. -> <. { x | x <Q A } , { x | A <Q x } >. e. P. )
Theorem	nqprlu 6645*	The canonical embedding of the rationals into the reals. (Contributed by Jim Kingdon, 24-Jun-2020.)
|- ( A e. Q. -> <. { l | l <Q A } , { u | A <Q u } >. e. P. )
Theorem	recnnpr 6646*	The reciprocal of a positive integer, as a positive real. (Contributed by Jim Kingdon, 27-Feb-2021.)
|- ( A e. N. -> <. { l | l <Q ( *Q ` [ <. A , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. A , 1o >. ] ~Q ) <Q u } >. e. P. )
Theorem	ltnqex 6647	The class of rationals less than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- { x | x <Q A } e. _V
Theorem	gtnqex 6648	The class of rationals greater than a given rational is a set. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- { x | A <Q x } e. _V
Theorem	nqprl 6649*	Comparing a fraction to a real can be done by whether it is an element of the lower cut, or by <P. (Contributed by Jim Kingdon, 8-Jul-2020.)
|- ( ( A e. Q. /\ B e. P. ) -> ( A e. ( 1st ` B ) <-> <. { l | l <Q A } , { u | A <Q u } >. <P B ) )
Theorem	nqpru 6650*	Comparing a fraction to a real can be done by whether it is an element of the upper cut, or by <P. (Contributed by Jim Kingdon, 29-Nov-2020.)
|- ( ( A e. Q. /\ B e. P. ) -> ( A e. ( 2nd ` B ) <-> B <P <. { l | l <Q A } , { u | A <Q u } >. ) )
Theorem	nnprlu 6651*	The canonical embedding of positive integers into the positive reals. (Contributed by Jim Kingdon, 23-Apr-2020.)
|- ( A e. N. -> <. { l | l <Q [ <. A , 1o >. ] ~Q } , { u | [ <. A , 1o >. ] ~Q <Q u } >. e. P. )
Theorem	1pr 6652	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
|- 1P e. P.
Theorem	1prl 6653	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( 1st ` 1P ) = { x | x <Q 1Q }
Theorem	1pru 6654	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( 2nd ` 1P ) = { x | 1Q <Q x }
Theorem	addnqprlemrl 6655*	Lemma for addnqpr 6659. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 1st ` ( <. { l | l <Q A } , { u | A <Q u } >. +P. <. { l | l <Q B } , { u | B <Q u } >. ) ) C_ ( 1st ` <. { l | l <Q ( A +Q B ) } , { u | ( A +Q B ) <Q u } >. ) )
Theorem	addnqprlemru 6656*	Lemma for addnqpr 6659. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 2nd ` ( <. { l | l <Q A } , { u | A <Q u } >. +P. <. { l | l <Q B } , { u | B <Q u } >. ) ) C_ ( 2nd ` <. { l | l <Q ( A +Q B ) } , { u | ( A +Q B ) <Q u } >. ) )
Theorem	addnqprlemfl 6657*	Lemma for addnqpr 6659. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 1st ` <. { l | l <Q ( A +Q B ) } , { u | ( A +Q B ) <Q u } >. ) C_ ( 1st ` ( <. { l | l <Q A } , { u | A <Q u } >. +P. <. { l | l <Q B } , { u | B <Q u } >. ) ) )
Theorem	addnqprlemfu 6658*	Lemma for addnqpr 6659. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 2nd ` <. { l | l <Q ( A +Q B ) } , { u | ( A +Q B ) <Q u } >. ) C_ ( 2nd ` ( <. { l | l <Q A } , { u | A <Q u } >. +P. <. { l | l <Q B } , { u | B <Q u } >. ) ) )
Theorem	addnqpr 6659*	Addition of fractions embedded into positive reals. One can either add the fractions as fractions, or embed them into positive reals and add them as positive reals, and get the same result. (Contributed by Jim Kingdon, 19-Aug-2020.)
|- ( ( A e. Q. /\ B e. Q. ) -> <. { l | l <Q ( A +Q B ) } , { u | ( A +Q B ) <Q u } >. = ( <. { l | l <Q A } , { u | A <Q u } >. +P. <. { l | l <Q B } , { u | B <Q u } >. ) )
Theorem	addnqpr1 6660*	Addition of one to a fraction embedded into a positive real. One can either add the fraction one to the fraction, or the positive real one to the positive real, and get the same result. Special case of addnqpr 6659. (Contributed by Jim Kingdon, 26-Apr-2020.)
|- ( A e. Q. -> <. { l | l <Q ( A +Q 1Q ) } , { u | ( A +Q 1Q ) <Q u } >. = ( <. { l | l <Q A } , { u | A <Q u } >. +P. 1P ) )
Theorem	appdivnq 6661*	Approximate division for positive rationals. Proposition 12.7 of [BauerTaylor], p. 55 (a special case where A and B are positive, as well as C). Our proof is simpler than the one in BauerTaylor because we have reciprocals. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( ( A <Q B /\ C e. Q. ) -> E. m e. Q. ( A <Q ( m .Q C ) /\ ( m .Q C ) <Q B ) )
Theorem	appdiv0nq 6662*	Approximate division for positive rationals. This can be thought of as a variation of appdivnq 6661 in which A is zero, although it can be stated and proved in terms of positive rationals alone, without zero as such. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ( ( B e. Q. /\ C e. Q. ) -> E. m e. Q. ( m .Q C ) <Q B )
Theorem	prmuloclemcalc 6663	Calculations for prmuloc 6664. (Contributed by Jim Kingdon, 9-Dec-2019.)
|- ( ph -> R <Q U )   &    |- ( ph -> U <Q ( D +Q P ) )   &    |- ( ph -> ( A +Q X ) = B )   &    |- ( ph -> ( P .Q B ) <Q ( R .Q X ) )   &    |- ( ph -> A e. Q. )   &    |- ( ph -> B e. Q. )   &    |- ( ph -> D e. Q. )   &    |- ( ph -> P e. Q. )   &    |- ( ph -> X e. Q. )   =>    |- ( ph -> ( U .Q A ) <Q ( D .Q B ) )
Theorem	prmuloc 6664*	Positive reals are multiplicatively located. Lemma 12.8 of [BauerTaylor], p. 56. (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( ( <. L , U >. e. P. /\ A <Q B ) -> E. d e. Q. E. u e. Q. ( d e. L /\ u e. U /\ ( u .Q A ) <Q ( d .Q B ) ) )
Theorem	prmuloc2 6665*	Positive reals are multiplicatively located. This is a variation of prmuloc 6664 which only constructs one (named) point and is therefore often easier to work with. It states that given a ratio B, there are elements of the lower and upper cut which have exactly that ratio between them. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( ( <. L , U >. e. P. /\ 1Q <Q B ) -> E. x e. L ( x .Q B ) e. U )
Theorem	mulnqprl 6666	Lemma to prove downward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
|- ( ( ( ( A e. P. /\ G e. ( 1st ` A ) ) /\ ( B e. P. /\ H e. ( 1st ` B ) ) ) /\ X e. Q. ) -> ( X <Q ( G .Q H ) -> X e. ( 1st ` ( A .P. B ) ) ) )
Theorem	mulnqpru 6667	Lemma to prove upward closure in positive real multiplication. (Contributed by Jim Kingdon, 10-Dec-2019.)
|- ( ( ( ( A e. P. /\ G e. ( 2nd ` A ) ) /\ ( B e. P. /\ H e. ( 2nd ` B ) ) ) /\ X e. Q. ) -> ( ( G .Q H ) <Q X -> X e. ( 2nd ` ( A .P. B ) ) ) )
Theorem	mullocprlem 6668	Calculations for mullocpr 6669. (Contributed by Jim Kingdon, 10-Dec-2019.)
|- ( ph -> ( A e. P. /\ B e. P. ) )   &    |- ( ph -> ( U .Q Q ) <Q ( E .Q ( D .Q U ) ) )   &    |- ( ph -> ( E .Q ( D .Q U ) ) <Q ( T .Q ( D .Q U ) ) )   &    |- ( ph -> ( T .Q ( D .Q U ) ) <Q ( D .Q R ) )   &    |- ( ph -> ( Q e. Q. /\ R e. Q. ) )   &    |- ( ph -> ( D e. Q. /\ U e. Q. ) )   &    |- ( ph -> ( D e. ( 1st ` A ) /\ U e. ( 2nd ` A ) ) )   &    |- ( ph -> ( E e. Q. /\ T e. Q. ) )   =>    |- ( ph -> ( Q e. ( 1st ` ( A .P. B ) ) \/ R e. ( 2nd ` ( A .P. B ) ) ) )
Theorem	mullocpr 6669*	Locatedness of multiplication on positive reals. Lemma 12.9 in [BauerTaylor], p. 56 (but where both A and B are positive, not just A). (Contributed by Jim Kingdon, 8-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` ( A .P. B ) ) \/ r e. ( 2nd ` ( A .P. B ) ) ) ) )
Theorem	mulclpr 6670	Closure of multiplication on positive reals. First statement of Proposition 9-3.7 of [Gleason] p. 124. (Contributed by NM, 13-Mar-1996.)
|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) e. P. )
Theorem	mulnqprlemrl 6671*	Lemma for mulnqpr 6675. The reverse subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 1st ` ( <. { l | l <Q A } , { u | A <Q u } >. .P. <. { l | l <Q B } , { u | B <Q u } >. ) ) C_ ( 1st ` <. { l | l <Q ( A .Q B ) } , { u | ( A .Q B ) <Q u } >. ) )
Theorem	mulnqprlemru 6672*	Lemma for mulnqpr 6675. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 2nd ` ( <. { l | l <Q A } , { u | A <Q u } >. .P. <. { l | l <Q B } , { u | B <Q u } >. ) ) C_ ( 2nd ` <. { l | l <Q ( A .Q B ) } , { u | ( A .Q B ) <Q u } >. ) )
Theorem	mulnqprlemfl 6673*	Lemma for mulnqpr 6675. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 1st ` <. { l | l <Q ( A .Q B ) } , { u | ( A .Q B ) <Q u } >. ) C_ ( 1st ` ( <. { l | l <Q A } , { u | A <Q u } >. .P. <. { l | l <Q B } , { u | B <Q u } >. ) ) )
Theorem	mulnqprlemfu 6674*	Lemma for mulnqpr 6675. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 18-Jul-2021.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( 2nd ` <. { l | l <Q ( A .Q B ) } , { u | ( A .Q B ) <Q u } >. ) C_ ( 2nd ` ( <. { l | l <Q A } , { u | A <Q u } >. .P. <. { l | l <Q B } , { u | B <Q u } >. ) ) )
Theorem	mulnqpr 6675*	Multiplication of fractions embedded into positive reals. One can either multiply the fractions as fractions, or embed them into positive reals and multiply them as positive reals, and get the same result. (Contributed by Jim Kingdon, 18-Jul-2021.)
|- ( ( A e. Q. /\ B e. Q. ) -> <. { l | l <Q ( A .Q B ) } , { u | ( A .Q B ) <Q u } >. = ( <. { l | l <Q A } , { u | A <Q u } >. .P. <. { l | l <Q B } , { u | B <Q u } >. ) )
Theorem	addcomprg 6676	Addition of positive reals is commutative. Proposition 9-3.5(ii) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A +P. B ) = ( B +P. A ) )
Theorem	addassprg 6677	Addition of positive reals is associative. Proposition 9-3.5(i) of [Gleason] p. 123. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A +P. B ) +P. C ) = ( A +P. ( B +P. C ) ) )
Theorem	mulcomprg 6678	Multiplication of positive reals is commutative. Proposition 9-3.7(ii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) = ( B .P. A ) )
Theorem	mulassprg 6679	Multiplication of positive reals is associative. Proposition 9-3.7(i) of [Gleason] p. 124. (Contributed by Jim Kingdon, 11-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A .P. B ) .P. C ) = ( A .P. ( B .P. C ) ) )
Theorem	distrlem1prl 6680	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 1st ` ( A .P. ( B +P. C ) ) ) C_ ( 1st ` ( ( A .P. B ) +P. ( A .P. C ) ) ) )
Theorem	distrlem1pru 6681	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 2nd ` ( A .P. ( B +P. C ) ) ) C_ ( 2nd ` ( ( A .P. B ) +P. ( A .P. C ) ) ) )
Theorem	distrlem4prl 6682*	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. ( 1st ` A ) /\ y e. ( 1st ` B ) ) /\ ( f e. ( 1st ` A ) /\ z e. ( 1st ` C ) ) ) ) -> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( 1st ` ( A .P. ( B +P. C ) ) ) )
Theorem	distrlem4pru 6683*	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. ( 2nd ` A ) /\ y e. ( 2nd ` B ) ) /\ ( f e. ( 2nd ` A ) /\ z e. ( 2nd ` C ) ) ) ) -> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( 2nd ` ( A .P. ( B +P. C ) ) ) )
Theorem	distrlem5prl 6684	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 1st ` ( ( A .P. B ) +P. ( A .P. C ) ) ) C_ ( 1st ` ( A .P. ( B +P. C ) ) ) )
Theorem	distrlem5pru 6685	Lemma for distributive law for positive reals. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( 2nd ` ( ( A .P. B ) +P. ( A .P. C ) ) ) C_ ( 2nd ` ( A .P. ( B +P. C ) ) ) )
Theorem	distrprg 6686	Multiplication of positive reals is distributive. Proposition 9-3.7(iii) of [Gleason] p. 124. (Contributed by Jim Kingdon, 12-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A .P. ( B +P. C ) ) = ( ( A .P. B ) +P. ( A .P. C ) ) )
Theorem	ltprordil 6687	If a positive real is less than a second positive real, its lower cut is a subset of the second's lower cut. (Contributed by Jim Kingdon, 23-Dec-2019.)
|- ( A <P B -> ( 1st ` A ) C_ ( 1st ` B ) )
Theorem	1idprl 6688	Lemma for 1idpr 6690. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- ( A e. P. -> ( 1st ` ( A .P. 1P ) ) = ( 1st ` A ) )
Theorem	1idpru 6689	Lemma for 1idpr 6690. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- ( A e. P. -> ( 2nd ` ( A .P. 1P ) ) = ( 2nd ` A ) )
Theorem	1idpr 6690	1 is an identity element for positive real multiplication. Theorem 9-3.7(iv) of [Gleason] p. 124. (Contributed by NM, 2-Apr-1996.)
|- ( A e. P. -> ( A .P. 1P ) = A )
Theorem	ltnqpr 6691*	We can order fractions via <Q or <P. (Contributed by Jim Kingdon, 19-Jun-2021.)
|- ( ( A e. Q. /\ B e. Q. ) -> ( A <Q B <-> <. { l | l <Q A } , { u | A <Q u } >. <P <. { l | l <Q B } , { u | B <Q u } >. ) )
Theorem	ltnqpri 6692*	We can order fractions via <Q or <P. (Contributed by Jim Kingdon, 8-Jan-2021.)
|- ( A <Q B -> <. { l | l <Q A } , { u | A <Q u } >. <P <. { l | l <Q B } , { u | B <Q u } >. )
Theorem	ltpopr 6693	Positive real 'less than' is a partial ordering. Remark ("< is transitive and irreflexive") preceding Proposition 11.2.3 of [HoTT], p. (varies). Lemma for ltsopr 6694. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- <P Po P.
Theorem	ltsopr 6694	Positive real 'less than' is a weak linear order (in the sense of df-iso 4034). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
|- <P Or P.
Theorem	ltaddpr 6695	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.)
|- ( ( A e. P. /\ B e. P. ) -> A <P ( A +P. B ) )
Theorem	ltexprlemell 6696*	Element in lower cut of the constructed difference. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. { x e. Q. | E. y ( y e. ( 2nd ` A ) /\ ( y +Q x ) e. ( 1st ` B ) ) } , { x e. Q. | E. y ( y e. ( 1st ` A ) /\ ( y +Q x ) e. ( 2nd ` B ) ) } >.   =>    |- ( q e. ( 1st ` C ) <-> ( q e. Q. /\ E. y ( y e. ( 2nd ` A ) /\ ( y +Q q ) e. ( 1st ` B ) ) ) )
Theorem	ltexprlemelu 6697*	Element in upper cut of the constructed difference. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. { x e. Q. | E. y ( y e. ( 2nd ` A ) /\ ( y +Q x ) e. ( 1st ` B ) ) } , { x e. Q. | E. y ( y e. ( 1st ` A ) /\ ( y +Q x ) e. ( 2nd ` B ) ) } >.   =>    |- ( r e. ( 2nd ` C ) <-> ( r e. Q. /\ E. y ( y e. ( 1st ` A ) /\ ( y +Q r ) e. ( 2nd ` B ) ) ) )
Theorem	ltexprlemm 6698*	Our constructed difference is inhabited. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 17-Dec-2019.)
|- C = <. { x e. Q. | E. y ( y e. ( 2nd ` A ) /\ ( y +Q x ) e. ( 1st ` B ) ) } , { x e. Q. | E. y ( y e. ( 1st ` A ) /\ ( y +Q x ) e. ( 2nd ` B ) ) } >.   =>    |- ( A <P B -> ( E. q e. Q. q e. ( 1st ` C ) /\ E. r e. Q. r e. ( 2nd ` C ) ) )
Theorem	ltexprlemopl 6699*	The lower cut of our constructed difference is open. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. { x e. Q. | E. y ( y e. ( 2nd ` A ) /\ ( y +Q x ) e. ( 1st ` B ) ) } , { x e. Q. | E. y ( y e. ( 1st ` A ) /\ ( y +Q x ) e. ( 2nd ` B ) ) } >.   =>    |- ( ( A <P B /\ q e. Q. /\ q e. ( 1st ` C ) ) -> E. r e. Q. ( q <Q r /\ r e. ( 1st ` C ) ) )
Theorem	ltexprlemlol 6700*	The lower cut of our constructed difference is lower. Lemma for ltexpri 6711. (Contributed by Jim Kingdon, 21-Dec-2019.)
|- C = <. { x e. Q. | E. y ( y e. ( 2nd ` A ) /\ ( y +Q x ) e. ( 1st ` B ) ) } , { x e. Q. | E. y ( y e. ( 1st ` A ) /\ ( y +Q x ) e. ( 2nd ` B ) ) } >.   =>    |- ( ( A <P B /\ q e. Q. ) -> ( E. r e. Q. ( q <Q r /\ r e. ( 1st ` C ) ) -> q e. ( 1st ` C ) ) )