HomeHome Intuitionistic Logic Explorer
Theorem List (p. 75 of 131)
< Previous  Next >
Browser slow? Try the
Unicode version.

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

Theorem List for Intuitionistic Logic Explorer - 7401-7500   *Has distinct variable group(s)
TypeLabelDescription
Statement
 
Theoremrecexprlemrnd 7401*  B is rounded. Lemma for recexpr 7410. (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 ) ) ) ) )
 
Theoremrecexprlemdisj 7402*  B is disjoint. Lemma for recexpr 7410. (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 ) ) )
 
Theoremrecexprlemloc 7403*  B is located. Lemma for recexpr 7410. (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 ) ) ) )
 
Theoremrecexprlempr 7404*  B is a positive real. Lemma for recexpr 7410. (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. )
 
Theoremrecexprlem1ssl 7405* The lower cut of one is a subset of the lower cut of  A  .P.  B. Lemma for recexpr 7410. (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 ) ) )
 
Theoremrecexprlem1ssu 7406* The upper cut of one is a subset of the upper cut of  A  .P.  B. Lemma for recexpr 7410. (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 ) ) )
 
Theoremrecexprlemss1l 7407* The lower cut of  A  .P.  B is a subset of the lower cut of one. Lemma for recexpr 7410. (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 ) )
 
Theoremrecexprlemss1u 7408* The upper cut of  A  .P.  B is a subset of the upper cut of one. Lemma for recexpr 7410. (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 ) )
 
Theoremrecexprlemex 7409*  B is the reciprocal of  A. Lemma for recexpr 7410. (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 )
 
Theoremrecexpr 7410* 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 )
 
Theoremaptiprleml 7411 Lemma for aptipr 7413. (Contributed by Jim Kingdon, 28-Jan-2020.)
 |-  ( ( A  e.  P. 
 /\  B  e.  P.  /\ 
 -.  B  <P  A ) 
 ->  ( 1st `  A )  C_  ( 1st `  B ) )
 
Theoremaptiprlemu 7412 Lemma for aptipr 7413. (Contributed by Jim Kingdon, 28-Jan-2020.)
 |-  ( ( A  e.  P. 
 /\  B  e.  P.  /\ 
 -.  B  <P  A ) 
 ->  ( 2nd `  B )  C_  ( 2nd `  A ) )
 
Theoremaptipr 7413 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 )
 
Theoremltmprr 7414 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 ) )
 
Theoremarchpr 7415* 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 7325. (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 } >. )
 
Theoremcaucvgprlemcanl 7416* Lemma for cauappcvgprlemladdrl 7429. 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 } >. ) ) ) )
 
Theoremcauappcvgprlemm 7417* Lemma for cauappcvgpr 7434. 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 ) ) )
 
Theoremcauappcvgprlemopl 7418* Lemma for cauappcvgpr 7434. 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 ) ) )
 
Theoremcauappcvgprlemlol 7419* Lemma for cauappcvgpr 7434. 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 ) )
 
Theoremcauappcvgprlemopu 7420* Lemma for cauappcvgpr 7434. 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 ) ) )
 
Theoremcauappcvgprlemupu 7421* Lemma for cauappcvgpr 7434. 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 ) )
 
Theoremcauappcvgprlemrnd 7422* Lemma for cauappcvgpr 7434. 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 ) ) ) ) )
 
Theoremcauappcvgprlemdisj 7423* Lemma for cauappcvgpr 7434. 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 ) ) )
 
Theoremcauappcvgprlemloc 7424* Lemma for cauappcvgpr 7434. 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 ) ) ) )
 
Theoremcauappcvgprlemcl 7425* Lemma for cauappcvgpr 7434. 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. )
 
Theoremcauappcvgprlemladdfu 7426* Lemma for cauappcvgprlemladd 7430. 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 } >. ) )
 
Theoremcauappcvgprlemladdfl 7427* Lemma for cauappcvgprlemladd 7430. 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 } >. ) )
 
Theoremcauappcvgprlemladdru 7428* Lemma for cauappcvgprlemladd 7430. 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 } >. ) ) )
 
Theoremcauappcvgprlemladdrl 7429* Lemma for cauappcvgprlemladd 7430. 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 } >. ) ) )
 
Theoremcauappcvgprlemladd 7430* Lemma for cauappcvgpr 7434. 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 } >. )
 
Theoremcauappcvgprlem1 7431* Lemma for cauappcvgpr 7434. 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 } >. ) )
 
Theoremcauappcvgprlem2 7432* Lemma for cauappcvgpr 7434. 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 } >. )
 
Theoremcauappcvgprlemlim 7433* Lemma for cauappcvgpr 7434. 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 } >. ) )
 
Theoremcauappcvgpr 7434* 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 7454 and caucvgprpr 7484 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 } >. ) )
 
Theoremarchrecnq 7435* 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 )
 
Theoremarchrecpr 7436* 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 )
 
Theoremcaucvgprlemk 7437 Lemma for caucvgpr 7454. 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 )
 
Theoremcaucvgprlemnkj 7438* Lemma for caucvgpr 7454. 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 ) )
 
Theoremcaucvgprlemnbj 7439* Lemma for caucvgpr 7454. 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 ) )
 
Theoremcaucvgprlemm 7440* Lemma for caucvgpr 7454. 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 ) ) )
 
Theoremcaucvgprlemopl 7441* Lemma for caucvgpr 7454. 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 ) ) )
 
Theoremcaucvgprlemlol 7442* Lemma for caucvgpr 7454. 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 ) )
 
Theoremcaucvgprlemopu 7443* Lemma for caucvgpr 7454. 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 ) ) )
 
Theoremcaucvgprlemupu 7444* Lemma for caucvgpr 7454. 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 ) )
 
Theoremcaucvgprlemrnd 7445* Lemma for caucvgpr 7454. 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 ) ) ) ) )
 
Theoremcaucvgprlemdisj 7446* Lemma for caucvgpr 7454. 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 ) ) )
 
Theoremcaucvgprlemloc 7447* Lemma for caucvgpr 7454. 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 ) ) ) )
 
Theoremcaucvgprlemcl 7448* Lemma for caucvgpr 7454. 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. )
 
Theoremcaucvgprlemladdfu 7449* Lemma for caucvgpr 7454. 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 } )
 
Theoremcaucvgprlemladdrl 7450* Lemma for caucvgpr 7454. 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 } >. ) ) )
 
Theoremcaucvgprlem1 7451* Lemma for caucvgpr 7454. 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 } >. ) )
 
Theoremcaucvgprlem2 7452* Lemma for caucvgpr 7454. 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 } >. )
 
Theoremcaucvgprlemlim 7453* Lemma for caucvgpr 7454. 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 } >. ) ) )
 
Theoremcaucvgpr 7454* 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 7434 and caucvgprpr 7484. Reading cauappcvgpr 7434 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 } >. ) ) )
 
Theoremcaucvgprprlemk 7455* Lemma for caucvgprpr 7484. 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 )
 
Theoremcaucvgprprlemloccalc 7456* Lemma for caucvgprpr 7484. Rearranging some expressions for caucvgprprlemloc 7475. (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 } >. )
 
Theoremcaucvgprprlemell 7457* Lemma for caucvgprpr 7484. 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
 ) ) )
 
Theoremcaucvgprprlemelu 7458* Lemma for caucvgprpr 7484. 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 } >. ) )
 
Theoremcaucvgprprlemcbv 7459* Lemma for caucvgprpr 7484. 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 } >. ) ) ) )
 
Theoremcaucvgprprlemval 7460* Lemma for caucvgprpr 7484. 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 } >. ) ) )
 
Theoremcaucvgprprlemnkltj 7461* Lemma for caucvgprpr 7484. 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 } >. ) )
 
Theoremcaucvgprprlemnkeqj 7462* Lemma for caucvgprpr 7484. 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 } >. ) )
 
Theoremcaucvgprprlemnjltk 7463* Lemma for caucvgprpr 7484. 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 } >. ) )
 
Theoremcaucvgprprlemnkj 7464* Lemma for caucvgprpr 7484. 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 } >. ) )
 
Theoremcaucvgprprlemnbj 7465* Lemma for caucvgprpr 7484. 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 ) )
 
Theoremcaucvgprprlemml 7466* Lemma for caucvgprpr 7484. 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 ) )
 
Theoremcaucvgprprlemmu 7467* Lemma for caucvgprpr 7484. 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 ) )
 
Theoremcaucvgprprlemm 7468* Lemma for caucvgprpr 7484. 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 ) ) )
 
Theoremcaucvgprprlemopl 7469* Lemma for caucvgprpr 7484. 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 ) ) )
 
Theoremcaucvgprprlemlol 7470* Lemma for caucvgprpr 7484. 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 ) )
 
Theoremcaucvgprprlemopu 7471* Lemma for caucvgprpr 7484. 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 ) ) )
 
Theoremcaucvgprprlemupu 7472* Lemma for caucvgprpr 7484. 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 ) )
 
Theoremcaucvgprprlemrnd 7473* Lemma for caucvgprpr 7484. 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 ) ) ) ) )
 
Theoremcaucvgprprlemdisj 7474* Lemma for caucvgprpr 7484. The putative limit is disjoint. (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 )  /\  s  e.  ( 2nd `  L ) ) )
 
Theoremcaucvgprprlemloc 7475* Lemma for caucvgprpr 7484. The putative limit is located. (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.  A. t  e. 
 Q.  ( s  <Q  t 
 ->  ( s  e.  ( 1st `  L )  \/  t  e.  ( 2nd `  L ) ) ) )
 
Theoremcaucvgprprlemcl 7476* Lemma for caucvgprpr 7484. The putative limit is a positive real. (Contributed by Jim Kingdon, 21-Nov-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  ->  L  e.  P. )
 
Theoremcaucvgprprlemclphr 7477* Lemma for caucvgprpr 7484. The putative limit is a positive real. Like caucvgprprlemcl 7476 but without a distinct variable constraint between  ph and  r. (Contributed by Jim Kingdon, 19-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  ->  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  ->  L  e.  P. )
 
Theoremcaucvgprprlemexbt 7478* Lemma for caucvgprpr 7484. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 16-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  ->  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  ->  Q  e.  Q. )   &    |-  ( ph  ->  T  e.  P. )   &    |-  ( ph  ->  ( L  +P.  <. { p  |  p  <Q  Q } ,  {
 q  |  Q  <Q  q } >. )  <P  T )   =>    |-  ( ph  ->  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  Q } ,  { q  |  Q  <Q  q } >. )  <P  T )
 
Theoremcaucvgprprlemexb 7479* Lemma for caucvgprpr 7484. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 15-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  ->  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  ->  Q  e.  P. )   &    |-  ( ph  ->  R  e.  N. )   =>    |-  ( ph  ->  ( ( ( L  +P.  Q )  +P.  <. { p  |  p  <Q  ( *Q ` 
 [ <. R ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. R ,  1o >. ]  ~Q  )  <Q  q } >. )  <P  ( ( F `  R )  +P.  Q )  ->  E. b  e.  N.  ( ( ( F `
  b )  +P.  <. { p  |  p  <Q  ( *Q `  [ <. b ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. b ,  1o >. ]  ~Q  )  <Q  q } >. ) 
 +P.  ( Q  +P.  <. { p  |  p  <Q  ( *Q `  [ <. R ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. R ,  1o >. ]  ~Q  )  <Q  q } >. ) )  <P  ( ( F `  R )  +P.  Q ) ) )
 
Theoremcaucvgprprlemaddq 7480* Lemma for caucvgprpr 7484. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 5-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  ->  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  ->  X  e.  P. )   &    |-  ( ph  ->  Q  e.  P. )   &    |-  ( ph  ->  E. r  e.  N.  ( X  +P.  <. { p  |  p  <Q  ( *Q ` 
 [ <. r ,  1o >. ]  ~Q  ) } ,  { q  |  ( *Q `  [ <. r ,  1o >. ]  ~Q  )  <Q  q } >. )  <P  ( ( F `  r
 )  +P.  Q )
 )   =>    |-  ( ph  ->  X  <P  ( L  +P.  Q ) )
 
Theoremcaucvgprprlem1 7481* Lemma for caucvgprpr 7484. Part of showing the putative limit to be a limit. (Contributed by Jim Kingdon, 25-Nov-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  |  (