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	distrlem5prl 7901	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 7902	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 7903	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 7904	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 7905	Lemma for 1idpr 7907. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- ( A e. P. -> ( 1st ` ( A .P. 1P ) ) = ( 1st ` A ) )
Theorem	1idpru 7906	Lemma for 1idpr 7907. (Contributed by Jim Kingdon, 13-Dec-2019.)
|- ( A e. P. -> ( 2nd ` ( A .P. 1P ) ) = ( 2nd ` A ) )
Theorem	1idpr 7907	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 7908*	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 7909*	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 7910	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 7911. (Contributed by Jim Kingdon, 15-Dec-2019.)
|- <P Po P.
Theorem	ltsopr 7911	Positive real 'less than' is a weak linear order (in the sense of df-iso 4418). Proposition 11.2.3 of [HoTT], p. (varies). (Contributed by Jim Kingdon, 16-Dec-2019.)
|- <P Or P.
Theorem	ltaddpr 7912	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 7913*	Element in lower cut of the constructed difference. Lemma for ltexpri 7928. (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 7914*	Element in upper cut of the constructed difference. Lemma for ltexpri 7928. (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 7915*	Our constructed difference is inhabited. Lemma for ltexpri 7928. (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 7916*	The lower cut of our constructed difference is open. Lemma for ltexpri 7928. (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 7917*	The lower cut of our constructed difference is lower. Lemma for ltexpri 7928. (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 7918*	The upper cut of our constructed difference is open. Lemma for ltexpri 7928. (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 7919*	The upper cut of our constructed difference is upper. Lemma for ltexpri 7928. (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 7920*	Our constructed difference is rounded. Lemma for ltexpri 7928. (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 7921*	Our constructed difference is disjoint. Lemma for ltexpri 7928. (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 7922*	Our constructed difference is located. Lemma for ltexpri 7928. (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 7923*	Our constructed difference is a positive real. Lemma for ltexpri 7928. (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 7924*	Lemma for ltexpri 7928. 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 7925*	Lemma for ltexpri 7928. 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 7926*	Lemma for ltexpri 7928. 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 7927*	Lemma for ltexpri 7928. 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 7928*	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 7929	Lemma for addcanprg 7931. (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 7930	Lemma for addcanprg 7931. (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 7931	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 7932*	The difference from ltexpri 7928 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.)
|- ( A <P B -> E! x e. P. ( A +P. x ) = B )
Theorem	ltaprlem 7933	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 7934	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 7935*	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 7936	Strong extensionality of addition (ordering version). This is similar to addext 8884 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 7937*	Membership in the lower cut of B. Lemma for recexpr 7953. (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 7938*	Membership in the upper cut of B. Lemma for recexpr 7953. (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 7939*	B is inhabited. Lemma for recexpr 7953. (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 7940*	The lower cut of B is open. Lemma for recexpr 7953. (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 7941*	The lower cut of B is lower. Lemma for recexpr 7953. (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 7942*	The upper cut of B is open. Lemma for recexpr 7953. (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 7943*	The upper cut of B is upper. Lemma for recexpr 7953. (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 7944*	B is rounded. Lemma for recexpr 7953. (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 7945*	B is disjoint. Lemma for recexpr 7953. (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 7946*	B is located. Lemma for recexpr 7953. (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 7947*	B is a positive real. Lemma for recexpr 7953. (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 7948*	The lower cut of one is a subset of the lower cut of A .P. B. Lemma for recexpr 7953. (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 7949*	The upper cut of one is a subset of the upper cut of A .P. B. Lemma for recexpr 7953. (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 7950*	The lower cut of A .P. B is a subset of the lower cut of one. Lemma for recexpr 7953. (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 7951*	The upper cut of A .P. B is a subset of the upper cut of one. Lemma for recexpr 7953. (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 7952*	B is the reciprocal of A. Lemma for recexpr 7953. (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 7953*	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 7954	Lemma for aptipr 7956. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. B <P A ) -> ( 1st ` A ) C_ ( 1st ` B ) )
Theorem	aptiprlemu 7955	Lemma for aptipr 7956. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. B <P A ) -> ( 2nd ` B ) C_ ( 2nd ` A ) )
Theorem	aptipr 7956	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 7957	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 7958*	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 7868. (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 } >. )
Theorem	caucvgprlemcanl 7959*	Lemma for cauappcvgprlemladdrl 7972. Cancelling a term from both sides. (Contributed by Jim Kingdon, 15-Aug-2020.)
|- ( ph -> L e. P. )   &    |- ( ph -> S e. Q. )   &    |- ( ph -> R e. Q. )   &    |- ( ph -> Q e. Q. )   =>    |- ( ph -> ( ( R +Q Q ) e. ( 1st ` ( L +P. <. { l | l <Q ( S +Q Q ) } , { u | ( S +Q Q ) <Q u } >. ) ) <-> R e. ( 1st ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) ) )
Theorem	cauappcvgprlemm 7960*	Lemma for cauappcvgpr 7977. The putative limit is inhabited. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ph -> ( E. s e. Q. s e. ( 1st ` L ) /\ E. r e. Q. r e. ( 2nd ` L ) ) )
Theorem	cauappcvgprlemopl 7961*	Lemma for cauappcvgpr 7977. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ( ph /\ s e. ( 1st ` L ) ) -> E. r e. Q. ( s <Q r /\ r e. ( 1st ` L ) ) )
Theorem	cauappcvgprlemlol 7962*	Lemma for cauappcvgpr 7977. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ( ph /\ s <Q r /\ r e. ( 1st ` L ) ) -> s e. ( 1st ` L ) )
Theorem	cauappcvgprlemopu 7963*	Lemma for cauappcvgpr 7977. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ( ph /\ r e. ( 2nd ` L ) ) -> E. s e. Q. ( s <Q r /\ s e. ( 2nd ` L ) ) )
Theorem	cauappcvgprlemupu 7964*	Lemma for cauappcvgpr 7977. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 4-Aug-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ( ph /\ s <Q r /\ s e. ( 2nd ` L ) ) -> r e. ( 2nd ` L ) )
Theorem	cauappcvgprlemrnd 7965*	Lemma for cauappcvgpr 7977. The putative limit is rounded. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ph -> ( A. s e. Q. ( s e. ( 1st ` L ) <-> E. r e. Q. ( s <Q r /\ r e. ( 1st ` L ) ) ) /\ A. r e. Q. ( r e. ( 2nd ` L ) <-> E. s e. Q. ( s <Q r /\ s e. ( 2nd ` L ) ) ) ) )
Theorem	cauappcvgprlemdisj 7966*	Lemma for cauappcvgpr 7977. The putative limit is disjoint. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )
Theorem	cauappcvgprlemloc 7967*	Lemma for cauappcvgpr 7977. The putative limit is located. (Contributed by Jim Kingdon, 18-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ph -> A. s e. Q. A. r e. Q. ( s <Q r -> ( s e. ( 1st ` L ) \/ r e. ( 2nd ` L ) ) ) )
Theorem	cauappcvgprlemcl 7968*	Lemma for cauappcvgpr 7977. The putative limit is a positive real. (Contributed by Jim Kingdon, 20-Jun-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ph -> L e. P. )
Theorem	cauappcvgprlemladdfu 7969*	Lemma for cauappcvgprlemladd 7973. The forward subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> ( 2nd ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) C_ ( 2nd ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( ( F ` q ) +Q S ) } , { u e. Q. | E. q e. Q. ( ( ( F ` q ) +Q q ) +Q S ) <Q u } >. ) )
Theorem	cauappcvgprlemladdfl 7970*	Lemma for cauappcvgprlemladd 7973. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> ( 1st ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) C_ ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( ( F ` q ) +Q S ) } , { u e. Q. | E. q e. Q. ( ( ( F ` q ) +Q q ) +Q S ) <Q u } >. ) )
Theorem	cauappcvgprlemladdru 7971*	Lemma for cauappcvgprlemladd 7973. The reverse subset relationship for the upper cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> ( 2nd ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( ( F ` q ) +Q S ) } , { u e. Q. | E. q e. Q. ( ( ( F ` q ) +Q q ) +Q S ) <Q u } >. ) C_ ( 2nd ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) )
Theorem	cauappcvgprlemladdrl 7972*	Lemma for cauappcvgprlemladd 7973. The forward subset relationship for the lower cut. (Contributed by Jim Kingdon, 11-Jul-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> ( 1st ` <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( ( F ` q ) +Q S ) } , { u e. Q. | E. q e. Q. ( ( ( F ` q ) +Q q ) +Q S ) <Q u } >. ) C_ ( 1st ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) )
Theorem	cauappcvgprlemladd 7973*	Lemma for cauappcvgpr 7977. This takes L and offsets it by the positive fraction S. (Contributed by Jim Kingdon, 23-Jun-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( ( F ` q ) +Q S ) } , { u e. Q. | E. q e. Q. ( ( ( F ` q ) +Q q ) +Q S ) <Q u } >. )
Theorem	cauappcvgprlem1 7974*	Lemma for cauappcvgpr 7977. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> Q e. Q. )   &    |- ( ph -> R e. Q. )   =>    |- ( ph -> <. { l | l <Q ( F ` Q ) } , { u | ( F ` Q ) <Q u } >. <P ( L +P. <. { l | l <Q ( Q +Q R ) } , { u | ( Q +Q R ) <Q u } >. ) )
Theorem	cauappcvgprlem2 7975*	Lemma for cauappcvgpr 7977. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 23-Jun-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   &    |- ( ph -> Q e. Q. )   &    |- ( ph -> R e. Q. )   =>    |- ( ph -> L <P <. { l | l <Q ( ( F ` Q ) +Q ( Q +Q R ) ) } , { u | ( ( F ` Q ) +Q ( Q +Q R ) ) <Q u } >. )
Theorem	cauappcvgprlemlim 7976*	Lemma for cauappcvgpr 7977. The putative limit is a limit. (Contributed by Jim Kingdon, 20-Jun-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   &    |- L = <. { l e. Q. | E. q e. Q. ( l +Q q ) <Q ( F ` q ) } , { u e. Q. | E. q e. Q. ( ( F ` q ) +Q q ) <Q u } >.   =>    |- ( ph -> A. q e. Q. A. r e. Q. ( <. { l | l <Q ( F ` q ) } , { u | ( F ` q ) <Q u } >. <P ( L +P. <. { l | l <Q ( q +Q r ) } , { u | ( q +Q r ) <Q u } >. ) /\ L <P <. { l | l <Q ( ( F ` q ) +Q ( q +Q r ) ) } , { u | ( ( F ` q ) +Q ( q +Q r ) ) <Q u } >. ) )
Theorem	cauappcvgpr 7977*	A Cauchy approximation has a limit. A Cauchy approximation, here F, is similar to a Cauchy sequence but is indexed by the desired tolerance (that is, how close together terms needs to be) rather than by natural numbers. This is basically Theorem 11.2.12 of [HoTT], p. (varies) with a few differences such as that we are proving the existence of a limit without anything about how fast it converges (that is, mere existence instead of existence, in HoTT terms), and that the codomain of F is Q. rather than P.. We also specify that every term needs to be larger than a fraction A, to avoid the case where we have positive terms which "converge" to zero (which is not a positive real). This proof (including its lemmas) is similar to the proofs of caucvgpr 7997 and caucvgprpr 8027 but is somewhat simpler, so reading this one first may help understanding the other two. (Contributed by Jim Kingdon, 19-Jun-2020.)
|- ( ph -> F : Q. --> Q. )   &    |- ( ph -> A. p e. Q. A. q e. Q. ( ( F ` p ) <Q ( ( F ` q ) +Q ( p +Q q ) ) /\ ( F ` q ) <Q ( ( F ` p ) +Q ( p +Q q ) ) ) )   &    |- ( ph -> A. p e. Q. A <Q ( F ` p ) )   =>    |- ( ph -> E. y e. P. A. q e. Q. A. r e. Q. ( <. { l | l <Q ( F ` q ) } , { u | ( F ` q ) <Q u } >. <P ( y +P. <. { l | l <Q ( q +Q r ) } , { u | ( q +Q r ) <Q u } >. ) /\ y <P <. { l | l <Q ( ( F ` q ) +Q ( q +Q r ) ) } , { u | ( ( F ` q ) +Q ( q +Q r ) ) <Q u } >. ) )
Theorem	archrecnq 7978*	Archimedean principle for fractions (reciprocal version). (Contributed by Jim Kingdon, 27-Sep-2020.)
|- ( A e. Q. -> E. j e. N. ( *Q ` [ <. j , 1o >. ] ~Q ) <Q A )
Theorem	archrecpr 7979*	Archimedean principle for positive reals (reciprocal version). (Contributed by Jim Kingdon, 25-Nov-2020.)
|- ( A e. P. -> E. j e. N. <. { l | l <Q ( *Q ` [ <. j , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. j , 1o >. ] ~Q ) <Q u } >. <P A )
Theorem	caucvgprlemk 7980	Lemma for caucvgpr 7997. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 9-Oct-2020.)
|- ( ph -> J <N K )   &    |- ( ph -> ( *Q ` [ <. J , 1o >. ] ~Q ) <Q Q )   =>    |- ( ph -> ( *Q ` [ <. K , 1o >. ] ~Q ) <Q Q )
Theorem	caucvgprlemnkj 7981*	Lemma for caucvgpr 7997. Part of disjointness. (Contributed by Jim Kingdon, 23-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> K e. N. )   &    |- ( ph -> J e. N. )   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> -. ( ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) <Q ( F ` K ) /\ ( ( F ` J ) +Q ( *Q ` [ <. J , 1o >. ] ~Q ) ) <Q S ) )
Theorem	caucvgprlemnbj 7982*	Lemma for caucvgpr 7997. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 18-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> B e. N. )   &    |- ( ph -> J e. N. )   =>    |- ( ph -> -. ( ( ( F ` B ) +Q ( *Q ` [ <. B , 1o >. ] ~Q ) ) +Q ( *Q ` [ <. J , 1o >. ] ~Q ) ) <Q ( F ` J ) )
Theorem	caucvgprlemm 7983*	Lemma for caucvgpr 7997. The putative limit is inhabited. (Contributed by Jim Kingdon, 27-Sep-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ph -> ( E. s e. Q. s e. ( 1st ` L ) /\ E. r e. Q. r e. ( 2nd ` L ) ) )
Theorem	caucvgprlemopl 7984*	Lemma for caucvgpr 7997. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ( ph /\ s e. ( 1st ` L ) ) -> E. r e. Q. ( s <Q r /\ r e. ( 1st ` L ) ) )
Theorem	caucvgprlemlol 7985*	Lemma for caucvgpr 7997. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 20-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ( ph /\ s <Q r /\ r e. ( 1st ` L ) ) -> s e. ( 1st ` L ) )
Theorem	caucvgprlemopu 7986*	Lemma for caucvgpr 7997. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 20-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ( ph /\ r e. ( 2nd ` L ) ) -> E. s e. Q. ( s <Q r /\ s e. ( 2nd ` L ) ) )
Theorem	caucvgprlemupu 7987*	Lemma for caucvgpr 7997. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 20-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ( ph /\ s <Q r /\ s e. ( 2nd ` L ) ) -> r e. ( 2nd ` L ) )
Theorem	caucvgprlemrnd 7988*	Lemma for caucvgpr 7997. The putative limit is rounded. (Contributed by Jim Kingdon, 27-Sep-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ph -> ( A. s e. Q. ( s e. ( 1st ` L ) <-> E. r e. Q. ( s <Q r /\ r e. ( 1st ` L ) ) ) /\ A. r e. Q. ( r e. ( 2nd ` L ) <-> E. s e. Q. ( s <Q r /\ s e. ( 2nd ` L ) ) ) ) )
Theorem	caucvgprlemdisj 7989*	Lemma for caucvgpr 7997. The putative limit is disjoint. (Contributed by Jim Kingdon, 27-Sep-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ph -> A. s e. Q. -. ( s e. ( 1st ` L ) /\ s e. ( 2nd ` L ) ) )
Theorem	caucvgprlemloc 7990*	Lemma for caucvgpr 7997. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ph -> A. s e. Q. A. r e. Q. ( s <Q r -> ( s e. ( 1st ` L ) \/ r e. ( 2nd ` L ) ) ) )
Theorem	caucvgprlemcl 7991*	Lemma for caucvgpr 7997. The putative limit is a positive real. (Contributed by Jim Kingdon, 26-Sep-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ph -> L e. P. )
Theorem	caucvgprlemladdfu 7992*	Lemma for caucvgpr 7997. Adding S after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 9-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> ( 2nd ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) C_ { u e. Q. | E. j e. N. ( ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) +Q S ) <Q u } )
Theorem	caucvgprlemladdrl 7993*	Lemma for caucvgpr 7997. Adding S after embedding in positive reals, or adding it as a rational. (Contributed by Jim Kingdon, 8-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( ( F ` j ) +Q S ) } C_ ( 1st ` ( L +P. <. { l | l <Q S } , { u | S <Q u } >. ) ) )
Theorem	caucvgprlem1 7994*	Lemma for caucvgpr 7997. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   &    |- ( ph -> Q e. Q. )   &    |- ( ph -> J <N K )   &    |- ( ph -> ( *Q ` [ <. J , 1o >. ] ~Q ) <Q Q )   =>    |- ( ph -> <. { l | l <Q ( F ` K ) } , { u | ( F ` K ) <Q u } >. <P ( L +P. <. { l | l <Q Q } , { u | Q <Q u } >. ) )
Theorem	caucvgprlem2 7995*	Lemma for caucvgpr 7997. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 3-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   &    |- ( ph -> Q e. Q. )   &    |- ( ph -> J <N K )   &    |- ( ph -> ( *Q ` [ <. J , 1o >. ] ~Q ) <Q Q )   =>    |- ( ph -> L <P <. { l | l <Q ( ( F ` K ) +Q Q ) } , { u | ( ( F ` K ) +Q Q ) <Q u } >. )
Theorem	caucvgprlemlim 7996*	Lemma for caucvgpr 7997. The putative limit is a limit. (Contributed by Jim Kingdon, 1-Oct-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   &    |- L = <. { l e. Q. | E. j e. N. ( l +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q ( F ` j ) } , { u e. Q. | E. j e. N. ( ( F ` j ) +Q ( *Q ` [ <. j , 1o >. ] ~Q ) ) <Q u } >.   =>    |- ( ph -> A. x e. Q. E. j e. N. A. k e. N. ( j <N k -> ( <. { l | l <Q ( F ` k ) } , { u | ( F ` k ) <Q u } >. <P ( L +P. <. { l | l <Q x } , { u | x <Q u } >. ) /\ L <P <. { l | l <Q ( ( F ` k ) +Q x ) } , { u | ( ( F ` k ) +Q x ) <Q u } >. ) ) )
Theorem	caucvgpr 7997*	A Cauchy sequence of positive fractions with a modulus of convergence converges to a positive real. This is basically Corollary 11.2.13 of [HoTT], p. (varies) (one key difference being that this is for positive reals rather than signed reals). Also, the HoTT book theorem has a modulus of convergence (that is, a rate of convergence) specified by (11.2.9) in HoTT whereas this theorem fixes the rate of convergence to say that all terms after the nth term must be within 1 / n of the nth term (it should later be able to prove versions of this theorem with a different fixed rate or a modulus of convergence supplied as a hypothesis). We also specify that every term needs to be larger than a fraction A, to avoid the case where we have positive terms which "converge" to zero (which is not a positive real). This proof (including its lemmas) is similar to the proofs of cauappcvgpr 7977 and caucvgprpr 8027. Reading cauappcvgpr 7977 first (the simplest of the three) might help understanding the other two. (Contributed by Jim Kingdon, 18-Jun-2020.)
|- ( ph -> F : N. --> Q. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <Q ( ( F ` k ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) /\ ( F ` k ) <Q ( ( F ` n ) +Q ( *Q ` [ <. n , 1o >. ] ~Q ) ) ) ) )   &    |- ( ph -> A. j e. N. A <Q ( F ` j ) )   =>    |- ( ph -> E. y e. P. A. x e. Q. E. j e. N. A. k e. N. ( j <N k -> ( <. { l | l <Q ( F ` k ) } , { u | ( F ` k ) <Q u } >. <P ( y +P. <. { l | l <Q x } , { u | x <Q u } >. ) /\ y <P <. { l | l <Q ( ( F ` k ) +Q x ) } , { u | ( ( F ` k ) +Q x ) <Q u } >. ) ) )
Theorem	caucvgprprlemk 7998*	Lemma for caucvgprpr 8027. Reciprocals of positive integers decrease as the positive integers increase. (Contributed by Jim Kingdon, 28-Nov-2020.)
|- ( ph -> J <N K )   &    |- ( ph -> <. { l | l <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q u } >. <P Q )   =>    |- ( ph -> <. { l | l <Q ( *Q ` [ <. K , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. K , 1o >. ] ~Q ) <Q u } >. <P Q )
Theorem	caucvgprprlemloccalc 7999*	Lemma for caucvgprpr 8027. Rearranging some expressions for caucvgprprlemloc 8018. (Contributed by Jim Kingdon, 8-Feb-2021.)
|- ( ph -> S <Q T )   &    |- ( ph -> Y e. Q. )   &    |- ( ph -> ( S +Q Y ) = T )   &    |- ( ph -> X e. Q. )   &    |- ( ph -> ( X +Q X ) <Q Y )   &    |- ( ph -> M e. N. )   &    |- ( ph -> ( *Q ` [ <. M , 1o >. ] ~Q ) <Q X )   =>    |- ( ph -> ( <. { l | l <Q ( S +Q ( *Q ` [ <. M , 1o >. ] ~Q ) ) } , { u | ( S +Q ( *Q ` [ <. M , 1o >. ] ~Q ) ) <Q u } >. +P. <. { l | l <Q ( *Q ` [ <. M , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. M , 1o >. ] ~Q ) <Q u } >. ) <P <. { l | l <Q T } , { u | T <Q u } >. )
Theorem	caucvgprprlemell 8000*	Lemma for caucvgprpr 8027. Membership in the lower cut of the putative limit. (Contributed by Jim Kingdon, 21-Jan-2021.)
|- L = <. { l e. Q. | E. r e. N. <. { p | p <Q ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) } , { q | ( l +Q ( *Q ` [ <. r , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` r ) } , { u e. Q. | E. r e. N. ( ( F ` r ) +P. <. { p | p <Q ( *Q ` [ <. r , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. r , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q u } , { q | u <Q q } >. } >.   =>    |- ( X e. ( 1st ` L ) <-> ( X e. Q. /\ E. b e. N. <. { p | p <Q ( X +Q ( *Q ` [ <. b , 1o >. ] ~Q ) ) } , { q | ( X +Q ( *Q ` [ <. b , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` b ) ) )