P. 77 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 7601-7700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ltexprlemlol 7601*	The lower cut of our constructed difference is lower. Lemma for ltexpri 7612. (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 7602*	The upper cut of our constructed difference is open. Lemma for ltexpri 7612. (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 7603*	The upper cut of our constructed difference is upper. Lemma for ltexpri 7612. (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 7604*	Our constructed difference is rounded. Lemma for ltexpri 7612. (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 7605*	Our constructed difference is disjoint. Lemma for ltexpri 7612. (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 7606*	Our constructed difference is located. Lemma for ltexpri 7612. (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 7607*	Our constructed difference is a positive real. Lemma for ltexpri 7612. (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 7608*	Lemma for ltexpri 7612. 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 7609*	Lemma for ltexpri 7612. 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 7610*	Lemma for ltexpri 7612. 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 7611*	Lemma for ltexpri 7612. 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 7612*	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 7613	Lemma for addcanprg 7615. (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 7614	Lemma for addcanprg 7615. (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 7615	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 7616*	The difference from ltexpri 7612 is unique. (Contributed by Jim Kingdon, 7-Jul-2021.)
|- ( A <P B -> E! x e. P. ( A +P. x ) = B )
Theorem	ltaprlem 7617	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 7618	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 7619*	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 7620	Strong extensionality of addition (ordering version). This is similar to addext 8567 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 7621*	Membership in the lower cut of B. Lemma for recexpr 7637. (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 7622*	Membership in the upper cut of B. Lemma for recexpr 7637. (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 7623*	B is inhabited. Lemma for recexpr 7637. (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 7624*	The lower cut of B is open. Lemma for recexpr 7637. (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 7625*	The lower cut of B is lower. Lemma for recexpr 7637. (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 7626*	The upper cut of B is open. Lemma for recexpr 7637. (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 7627*	The upper cut of B is upper. Lemma for recexpr 7637. (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 7628*	B is rounded. Lemma for recexpr 7637. (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 7629*	B is disjoint. Lemma for recexpr 7637. (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 7630*	B is located. Lemma for recexpr 7637. (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 7631*	B is a positive real. Lemma for recexpr 7637. (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 7632*	The lower cut of one is a subset of the lower cut of A .P. B. Lemma for recexpr 7637. (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 7633*	The upper cut of one is a subset of the upper cut of A .P. B. Lemma for recexpr 7637. (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 7634*	The lower cut of A .P. B is a subset of the lower cut of one. Lemma for recexpr 7637. (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 7635*	The upper cut of A .P. B is a subset of the upper cut of one. Lemma for recexpr 7637. (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 7636*	B is the reciprocal of A. Lemma for recexpr 7637. (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 7637*	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 7638	Lemma for aptipr 7640. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. B <P A ) -> ( 1st ` A ) C_ ( 1st ` B ) )
Theorem	aptiprlemu 7639	Lemma for aptipr 7640. (Contributed by Jim Kingdon, 28-Jan-2020.)
|- ( ( A e. P. /\ B e. P. /\ -. B <P A ) -> ( 2nd ` B ) C_ ( 2nd ` A ) )
Theorem	aptipr 7640	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 7641	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 7642*	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 7552. (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 7643*	Lemma for cauappcvgprlemladdrl 7656. 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 7644*	Lemma for cauappcvgpr 7661. 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 7645*	Lemma for cauappcvgpr 7661. 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 7646*	Lemma for cauappcvgpr 7661. 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 7647*	Lemma for cauappcvgpr 7661. 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 7648*	Lemma for cauappcvgpr 7661. 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 7649*	Lemma for cauappcvgpr 7661. 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 7650*	Lemma for cauappcvgpr 7661. 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 7651*	Lemma for cauappcvgpr 7661. 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 7652*	Lemma for cauappcvgpr 7661. 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 7653*	Lemma for cauappcvgprlemladd 7657. 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 7654*	Lemma for cauappcvgprlemladd 7657. 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 7655*	Lemma for cauappcvgprlemladd 7657. 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 7656*	Lemma for cauappcvgprlemladd 7657. 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 7657*	Lemma for cauappcvgpr 7661. 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 7658*	Lemma for cauappcvgpr 7661. 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 7659*	Lemma for cauappcvgpr 7661. 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 7660*	Lemma for cauappcvgpr 7661. 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 7661*	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 7681 and caucvgprpr 7711 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 7662*	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 7663*	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 7664	Lemma for caucvgpr 7681. 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 7665*	Lemma for caucvgpr 7681. 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 7666*	Lemma for caucvgpr 7681. 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 7667*	Lemma for caucvgpr 7681. 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 7668*	Lemma for caucvgpr 7681. 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 7669*	Lemma for caucvgpr 7681. 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 7670*	Lemma for caucvgpr 7681. 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 7671*	Lemma for caucvgpr 7681. 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 7672*	Lemma for caucvgpr 7681. 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 7673*	Lemma for caucvgpr 7681. 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 7674*	Lemma for caucvgpr 7681. 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 7675*	Lemma for caucvgpr 7681. 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 7676*	Lemma for caucvgpr 7681. 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 7677*	Lemma for caucvgpr 7681. 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 7678*	Lemma for caucvgpr 7681. 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 7679*	Lemma for caucvgpr 7681. 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 7680*	Lemma for caucvgpr 7681. 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 7681*	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 7661 and caucvgprpr 7711. Reading cauappcvgpr 7661 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 7682*	Lemma for caucvgprpr 7711. 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 7683*	Lemma for caucvgprpr 7711. Rearranging some expressions for caucvgprprlemloc 7702. (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 7684*	Lemma for caucvgprpr 7711. 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 ) ) )
Theorem	caucvgprprlemelu 7685*	Lemma for caucvgprpr 7711. Membership in the upper cut of the putative limit. (Contributed by Jim Kingdon, 28-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. ( 2nd ` L ) <-> ( X e. Q. /\ E. b e. N. ( ( F ` b ) +P. <. { p | p <Q ( *Q ` [ <. b , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. b , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q X } , { q | X <Q q } >. ) )
Theorem	caucvgprprlemcbv 7686*	Lemma for caucvgprpr 7711. Change bound variables in Cauchy condition. (Contributed by Jim Kingdon, 12-Feb-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   =>    |- ( ph -> A. a e. N. A. b e. N. ( a <N b -> ( ( F ` a ) <P ( ( F ` b ) +P. <. { l | l <Q ( *Q ` [ <. a , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. a , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` b ) <P ( ( F ` a ) +P. <. { l | l <Q ( *Q ` [ <. a , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. a , 1o >. ] ~Q ) <Q u } >. ) ) ) )
Theorem	caucvgprprlemval 7687*	Lemma for caucvgprpr 7711. Cauchy condition expressed in terms of classes. (Contributed by Jim Kingdon, 3-Mar-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   =>    |- ( ( ph /\ A <N B ) -> ( ( F ` A ) <P ( ( F ` B ) +P. <. { p | p <Q ( *Q ` [ <. A , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. A , 1o >. ] ~Q ) <Q q } >. ) /\ ( F ` B ) <P ( ( F ` A ) +P. <. { p | p <Q ( *Q ` [ <. A , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. A , 1o >. ] ~Q ) <Q q } >. ) ) )
Theorem	caucvgprprlemnkltj 7688*	Lemma for caucvgprpr 7711. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> K e. N. )   &    |- ( ph -> J e. N. )   &    |- ( ph -> S e. Q. )   =>    |- ( ( ph /\ K <N J ) -> -. ( <. { p | p <Q ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) } , { q | ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` K ) /\ ( ( F ` J ) +P. <. { p | p <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q S } , { q | S <Q q } >. ) )
Theorem	caucvgprprlemnkeqj 7689*	Lemma for caucvgprpr 7711. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> K e. N. )   &    |- ( ph -> J e. N. )   &    |- ( ph -> S e. Q. )   =>    |- ( ( ph /\ K = J ) -> -. ( <. { p | p <Q ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) } , { q | ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` K ) /\ ( ( F ` J ) +P. <. { p | p <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q S } , { q | S <Q q } >. ) )
Theorem	caucvgprprlemnjltk 7690*	Lemma for caucvgprpr 7711. Part of disjointness. (Contributed by Jim Kingdon, 12-Feb-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> K e. N. )   &    |- ( ph -> J e. N. )   &    |- ( ph -> S e. Q. )   =>    |- ( ( ph /\ J <N K ) -> -. ( <. { p | p <Q ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) } , { q | ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` K ) /\ ( ( F ` J ) +P. <. { p | p <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q S } , { q | S <Q q } >. ) )
Theorem	caucvgprprlemnkj 7691*	Lemma for caucvgprpr 7711. Part of disjointness. (Contributed by Jim Kingdon, 20-Jan-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> K e. N. )   &    |- ( ph -> J e. N. )   &    |- ( ph -> S e. Q. )   =>    |- ( ph -> -. ( <. { p | p <Q ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) } , { q | ( S +Q ( *Q ` [ <. K , 1o >. ] ~Q ) ) <Q q } >. <P ( F ` K ) /\ ( ( F ` J ) +P. <. { p | p <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { q | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q q } >. ) <P <. { p | p <Q S } , { q | S <Q q } >. ) )
Theorem	caucvgprprlemnbj 7692*	Lemma for caucvgprpr 7711. Non-existence of two elements of the sequence which are too far from each other. (Contributed by Jim Kingdon, 17-Jun-2021.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> B e. N. )   &    |- ( ph -> J e. N. )   =>    |- ( ph -> -. ( ( ( F ` B ) +P. <. { l | l <Q ( *Q ` [ <. B , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. B , 1o >. ] ~Q ) <Q u } >. ) +P. <. { l | l <Q ( *Q ` [ <. J , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. J , 1o >. ] ~Q ) <Q u } >. ) <P ( F ` J ) )
Theorem	caucvgprprlemml 7693*	Lemma for caucvgprpr 7711. The lower cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ph -> E. s e. Q. s e. ( 1st ` L ) )
Theorem	caucvgprprlemmu 7694*	Lemma for caucvgprpr 7711. The upper cut of the putative limit is inhabited. (Contributed by Jim Kingdon, 29-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ph -> E. t e. Q. t e. ( 2nd ` L ) )
Theorem	caucvgprprlemm 7695*	Lemma for caucvgprpr 7711. The putative limit is inhabited. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ph -> ( E. s e. Q. s e. ( 1st ` L ) /\ E. t e. Q. t e. ( 2nd ` L ) ) )
Theorem	caucvgprprlemopl 7696*	Lemma for caucvgprpr 7711. The lower cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ( ph /\ s e. ( 1st ` L ) ) -> E. t e. Q. ( s <Q t /\ t e. ( 1st ` L ) ) )
Theorem	caucvgprprlemlol 7697*	Lemma for caucvgprpr 7711. The lower cut of the putative limit is lower. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ( ph /\ s <Q t /\ t e. ( 1st ` L ) ) -> s e. ( 1st ` L ) )
Theorem	caucvgprprlemopu 7698*	Lemma for caucvgprpr 7711. The upper cut of the putative limit is open. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ( ph /\ t e. ( 2nd ` L ) ) -> E. s e. Q. ( s <Q t /\ s e. ( 2nd ` L ) ) )
Theorem	caucvgprprlemupu 7699*	Lemma for caucvgprpr 7711. The upper cut of the putative limit is upper. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ( ph /\ s <Q t /\ s e. ( 2nd ` L ) ) -> t e. ( 2nd ` L ) )
Theorem	caucvgprprlemrnd 7700*	Lemma for caucvgprpr 7711. The putative limit is rounded. (Contributed by Jim Kingdon, 21-Dec-2020.)
|- ( ph -> F : N. --> P. )   &    |- ( ph -> A. n e. N. A. k e. N. ( n <N k -> ( ( F ` n ) <P ( ( F ` k ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) /\ ( F ` k ) <P ( ( F ` n ) +P. <. { l | l <Q ( *Q ` [ <. n , 1o >. ] ~Q ) } , { u | ( *Q ` [ <. n , 1o >. ] ~Q ) <Q u } >. ) ) ) )   &    |- ( ph -> A. m e. N. A <P ( F ` m ) )   &    |- 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 } >. } >.   =>    |- ( ph -> ( A. s e. Q. ( s e. ( 1st ` L ) <-> E. t e. Q. ( s <Q t /\ t e. ( 1st ` L ) ) ) /\ A. t e. Q. ( t e. ( 2nd ` L ) <-> E. s e. Q. ( s <Q t /\ s e. ( 2nd ` L ) ) ) ) )