P. 80 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7901-8000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	nqprdisj 7901*	A cut produced from a rational is disjoint. Lemma for nqprlu 7904. (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 7902*	A cut produced from a rational is located. Lemma for nqprlu 7904. (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 7903*	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 7904*	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 7905*	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 7906	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 7907	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 7908*	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 7909*	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 7910*	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 7911	The positive real number 'one'. (Contributed by NM, 13-Mar-1996.) (Revised by Mario Carneiro, 12-Jun-2013.)
|- 1P e. P.
Theorem	1prl 7912	The lower cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( 1st ` 1P ) = { x | x <Q 1Q }
Theorem	1pru 7913	The upper cut of the positive real number 'one'. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- ( 2nd ` 1P ) = { x | 1Q <Q x }
Theorem	addnqprlemrl 7914*	Lemma for addnqpr 7918. 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 7915*	Lemma for addnqpr 7918. 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 7916*	Lemma for addnqpr 7918. 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 7917*	Lemma for addnqpr 7918. 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 7918*	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 7919*	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 7918. (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 7920*	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 7921*	Approximate division for positive rationals. This can be thought of as a variation of appdivnq 7920 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 7922	Calculations for prmuloc 7923. (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 7923*	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 7924*	Positive reals are multiplicatively located. This is a variation of prmuloc 7923 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 7925	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 7926	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 7927	Calculations for mullocpr 7928. (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 7928*	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 7929	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 7930*	Lemma for mulnqpr 7934. 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 7931*	Lemma for mulnqpr 7934. 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 7932*	Lemma for mulnqpr 7934. 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 7933*	Lemma for mulnqpr 7934. 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 7934*	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 7935	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 7936	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 7937	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 7938	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 7939	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 7940	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 7941*	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 7942*	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 7943	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 7944	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 7945	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 7946	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 7947	Lemma for 1idpr 7949. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- ( A e. P. -> ( 1st ` ( A .P. 1P ) ) = ( 1st ` A ) )
Theorem	1idpru 7948	Lemma for 1idpr 7949. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- ( A e. P. -> ( 2nd ` ( A .P. 1P ) ) = ( 2nd ` A ) )
Theorem	1idpr 7949	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 7950*	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 7951*	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 7952	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 7953. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- <P Po P.
Theorem	ltsopr 7953	Positive real 'less than' is a weak linear order (in the sense of df-iso 4437). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
|- <P Or P.
Theorem	ltaddpr 7954	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 7955*	Element in lower cut of the constructed difference. Lemma for ltexpri 7970. (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 7956*	Element in upper cut of the constructed difference. Lemma for ltexpri 7970. (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 7957*	Our constructed difference is inhabited. Lemma for ltexpri 7970. (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 7958*	The lower cut of our constructed difference is open. Lemma for ltexpri 7970. (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 7959*	The lower cut of our constructed difference is lower. Lemma for ltexpri 7970. (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 ) ) )
Theorem	ltexprlemopu 7960*	The upper cut of our constructed difference is open. Lemma for ltexpri 7970. (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 /\ r e. Q. /\ r e. ( 2nd ` C ) ) -> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` C ) ) )
Theorem	ltexprlemupu 7961*	The upper cut of our constructed difference is upper. Lemma for ltexpri 7970. (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 /\ r e. Q. ) -> ( E. q e. Q. ( q <Q r /\ q e. ( 2nd ` C ) ) -> r e. ( 2nd ` C ) ) )
Theorem	ltexprlemrnd 7962*	Our constructed difference is rounded. Lemma for ltexpri 7970. (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 -> ( A. q e. Q. ( q e. ( 1st ` C ) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` C ) ) ) /\ A. r e. Q. ( r e. ( 2nd ` C ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` C ) ) ) ) )
Theorem	ltexprlemdisj 7963*	Our constructed difference is disjoint. Lemma for ltexpri 7970. (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 -> A. q e. Q. -. ( q e. ( 1st ` C ) /\ q e. ( 2nd ` C ) ) )
Theorem	ltexprlemloc 7964*	Our constructed difference is located. Lemma for ltexpri 7970. (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 -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` C ) \/ r e. ( 2nd ` C ) ) ) )
Theorem	ltexprlempr 7965*	Our constructed difference is a positive real. Lemma for ltexpri 7970. (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 -> C e. P. )
Theorem	ltexprlemfl 7966*	Lemma for ltexpri 7970. One direction of our result for lower cuts. (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 -> ( 1st ` ( A +P. C ) ) C_ ( 1st ` B ) )
Theorem	ltexprlemrl 7967*	Lemma for ltexpri 7970. Reverse direction of our result for lower cuts. (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 -> ( 1st ` B ) C_ ( 1st ` ( A +P. C ) ) )
Theorem	ltexprlemfu 7968*	Lemma for ltexpri 7970. One direction of our result for upper cuts. (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 -> ( 2nd ` ( A +P. C ) ) C_ ( 2nd ` B ) )
Theorem	ltexprlemru 7969*	Lemma for ltexpri 7970. One direction of our result for upper cuts. (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 -> ( 2nd ` B ) C_ ( 2nd ` ( A +P. C ) ) )
Theorem	ltexpri 7970*	Proposition 9-3.5(iv) of [Gleason] p. 123. (Contributed by NM, 13-May-1996.) (Revised by Mario Carneiro, 14-Jun-2013.)
|- ( A <P B -> E. x e. P. ( A +P. x ) = B )
Theorem	addcanprleml 7971	Lemma for addcanprg 7973. (Contributed by Jim Kingdon, 25-Dec-2019.)
|- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) -> ( 1st ` B ) C_ ( 1st ` C ) )
Theorem	addcanprlemu 7972	Lemma for addcanprg 7973. (Contributed by Jim Kingdon, 25-Dec-2019.)
|- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( A +P. B ) = ( A +P. C ) ) -> ( 2nd ` B ) C_ ( 2nd ` C ) )
Theorem	addcanprg 7973	Addition cancellation law for positive reals. Proposition 9-3.5(vi) of [Gleason] p. 123. (Contributed by Jim Kingdon, 24-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A +P. B ) = ( A +P. C ) -> B = C ) )
Theorem	lteupri 7974*	The difference from ltexpri 7970 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.)
|- ( A <P B -> E! x e. P. ( A +P. x ) = B )
Theorem	ltaprlem 7975	Lemma for Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by NM, 8-Apr-1996.)
|- ( C e. P. -> ( A <P B -> ( C +P. A ) <P ( C +P. B ) ) )
Theorem	ltaprg 7976	Ordering property of addition. Proposition 9-3.5(v) of [Gleason] p. 123. (Contributed by Jim Kingdon, 26-Dec-2019.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A <P B <-> ( C +P. A ) <P ( C +P. B ) ) )
Theorem	prplnqu 7977*	Membership in the upper cut of a sum of a positive real and a fraction. (Contributed by Jim Kingdon, 16-Jun-2021.)
|- ( ph -> X e. P. )   &    |- ( ph -> Q e. Q. )   &    |- ( ph -> A e. ( 2nd ` ( X +P. <. { l | l <Q Q } , { u | Q <Q u } >. ) ) )   =>    |- ( ph -> E. y e. ( 2nd ` X ) ( y +Q Q ) = A )
Theorem	addextpr 7978	Strong extensionality of addition (ordering version). This is similar to addext 8928 but for positive reals and based on less-than rather than apartness. (Contributed by Jim Kingdon, 17-Feb-2020.)
|- ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) -> ( ( A +P. B ) <P ( C +P. D ) -> ( A <P C \/ B <P D ) ) )
Theorem	recexprlemell 7979*	Membership in the lower cut of B. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( C e. ( 1st ` B ) <-> E. y ( C <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) )
Theorem	recexprlemelu 7980*	Membership in the upper cut of B. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( C e. ( 2nd ` B ) <-> E. y ( y <Q C /\ ( *Q ` y ) e. ( 1st ` A ) ) )
Theorem	recexprlemm 7981*	B is inhabited. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( E. q e. Q. q e. ( 1st ` B ) /\ E. r e. Q. r e. ( 2nd ` B ) ) )
Theorem	recexprlemopl 7982*	The lower cut of B is open. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( ( A e. P. /\ q e. Q. /\ q e. ( 1st ` B ) ) -> E. r e. Q. ( q <Q r /\ r e. ( 1st ` B ) ) )
Theorem	recexprlemlol 7983*	The lower cut of B is lower. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( ( A e. P. /\ q e. Q. ) -> ( E. r e. Q. ( q <Q r /\ r e. ( 1st ` B ) ) -> q e. ( 1st ` B ) ) )
Theorem	recexprlemopu 7984*	The upper cut of B is open. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( ( A e. P. /\ r e. Q. /\ r e. ( 2nd ` B ) ) -> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B ) ) )
Theorem	recexprlemupu 7985*	The upper cut of B is upper. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 28-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( ( A e. P. /\ r e. Q. ) -> ( E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B ) ) -> r e. ( 2nd ` B ) ) )
Theorem	recexprlemrnd 7986*	B is rounded. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( A. q e. Q. ( q e. ( 1st ` B ) <-> E. r e. Q. ( q <Q r /\ r e. ( 1st ` B ) ) ) /\ A. r e. Q. ( r e. ( 2nd ` B ) <-> E. q e. Q. ( q <Q r /\ q e. ( 2nd ` B ) ) ) ) )
Theorem	recexprlemdisj 7987*	B is disjoint. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> A. q e. Q. -. ( q e. ( 1st ` B ) /\ q e. ( 2nd ` B ) ) )
Theorem	recexprlemloc 7988*	B is located. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> A. q e. Q. A. r e. Q. ( q <Q r -> ( q e. ( 1st ` B ) \/ r e. ( 2nd ` B ) ) ) )
Theorem	recexprlempr 7989*	B is a positive real. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> B e. P. )
Theorem	recexprlem1ssl 7990*	The lower cut of one is a subset of the lower cut of A .P. B. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( 1st ` 1P ) C_ ( 1st ` ( A .P. B ) ) )
Theorem	recexprlem1ssu 7991*	The upper cut of one is a subset of the upper cut of A .P. B. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( 2nd ` 1P ) C_ ( 2nd ` ( A .P. B ) ) )
Theorem	recexprlemss1l 7992*	The lower cut of A .P. B is a subset of the lower cut of one. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( 1st ` ( A .P. B ) ) C_ ( 1st ` 1P ) )
Theorem	recexprlemss1u 7993*	The upper cut of A .P. B is a subset of the upper cut of one. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( 2nd ` ( A .P. B ) ) C_ ( 2nd ` 1P ) )
Theorem	recexprlemex 7994*	B is the reciprocal of A. Lemma for recexpr 7995. (Contributed by Jim Kingdon, 27-Dec-2019.)
|- B = <. { x | E. y ( x <Q y /\ ( *Q ` y ) e. ( 2nd ` A ) ) } , { x | E. y ( y <Q x /\ ( *Q ` y ) e. ( 1st ` A ) ) } >.   =>    |- ( A e. P. -> ( A .P. B ) = 1P )
Theorem	recexpr 7995*	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.)
|- ( A e. P. -> E. x e. P. ( A .P. x ) = 1P )
Theorem	aptiprleml 7996	Lemma for aptipr 7998. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. B <P A ) -> ( 1st ` A ) C_ ( 1st ` B ) )
Theorem	aptiprlemu 7997	Lemma for aptipr 7998. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. B <P A ) -> ( 2nd ` B ) C_ ( 2nd ` A ) )
Theorem	aptipr 7998	Apartness of positive reals is tight. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. ( A <P B \/ B <P A ) ) -> A = B )
Theorem	ltmprr 7999	Ordering property of multiplication. (Contributed by Jim Kingdon, 18-Feb-2020.)
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( C .P. A ) <P ( C .P. B ) -> A <P B ) )
Theorem	archpr 8000*	For any positive real, there is an integer that is greater than it. This is also known as the "archimedean property". The integer x is embedded into the reals as described at nnprlu 7910. (Contributed by Jim Kingdon, 22-Apr-2020.)
|- ( A e. P. -> E. x e. N. A <P <. { l | l <Q [ <. x , 1o >. ] ~Q } , { u | [ <. x , 1o >. ] ~Q <Q u } >. )