HomeHome Intuitionistic Logic Explorer
Theorem List (p. 75 of 132)
< 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
 
Theoremrecexprlemopl 7401* The lower cut of  B is open. Lemma for recexpr 7414. (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 ) ) )
 
Theoremrecexprlemlol 7402* The lower cut of  B is lower. Lemma for recexpr 7414. (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 ) ) )
 
Theoremrecexprlemopu 7403* The upper cut of  B is open. Lemma for recexpr 7414. (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 ) ) )
 
Theoremrecexprlemupu 7404* The upper cut of  B is upper. Lemma for recexpr 7414. (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 ) ) )
 
Theoremrecexprlemrnd 7405*  B is rounded. Lemma for recexpr 7414. (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 7406*  B is disjoint. Lemma for recexpr 7414. (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 7407*  B is located. Lemma for recexpr 7414. (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 7408*  B is a positive real. Lemma for recexpr 7414. (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 7409* The lower cut of one is a subset of the lower cut of  A  .P.  B. Lemma for recexpr 7414. (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 7410* The upper cut of one is a subset of the upper cut of  A  .P.  B. Lemma for recexpr 7414. (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 7411* The lower cut of  A  .P.  B is a subset of the lower cut of one. Lemma for recexpr 7414. (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 7412* The upper cut of  A  .P.  B is a subset of the upper cut of one. Lemma for recexpr 7414. (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 7413*  B is the reciprocal of  A. Lemma for recexpr 7414. (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 7414* 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 7415 Lemma for aptipr 7417. (Contributed by Jim Kingdon, 28-Jan-2020.)
 |-  ( ( A  e.  P. 
 /\  B  e.  P.  /\ 
 -.  B  <P  A ) 
 ->  ( 1st `  A )  C_  ( 1st `  B ) )
 
Theoremaptiprlemu 7416 Lemma for aptipr 7417. (Contributed by Jim Kingdon, 28-Jan-2020.)
 |-  ( ( A  e.  P. 
 /\  B  e.  P.  /\ 
 -.  B  <P  A ) 
 ->  ( 2nd `  B )  C_  ( 2nd `  A ) )
 
Theoremaptipr 7417 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 7418 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 7419* 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 7329. (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 7420* Lemma for cauappcvgprlemladdrl 7433. 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 7421* Lemma for cauappcvgpr 7438. 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 7422* Lemma for cauappcvgpr 7438. 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 7423* Lemma for cauappcvgpr 7438. 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 7424* Lemma for cauappcvgpr 7438. 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 7425* Lemma for cauappcvgpr 7438. 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 7426* Lemma for cauappcvgpr 7438. 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 7427* Lemma for cauappcvgpr 7438. 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 7428* Lemma for cauappcvgpr 7438. 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 7429* Lemma for cauappcvgpr 7438. 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 7430* Lemma for cauappcvgprlemladd 7434. 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 7431* Lemma for cauappcvgprlemladd 7434. 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 7432* Lemma for cauappcvgprlemladd 7434. 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 7433* Lemma for cauappcvgprlemladd 7434. 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 7434* Lemma for cauappcvgpr 7438. 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 7435* Lemma for cauappcvgpr 7438. 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 7436* Lemma for cauappcvgpr 7438. 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 7437* Lemma for cauappcvgpr 7438. 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 7438* 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 7458 and caucvgprpr 7488 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 7439* 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 7440* 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 7441 Lemma for caucvgpr 7458. 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 7442* Lemma for caucvgpr 7458. 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 7443* Lemma for caucvgpr 7458. 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 7444* Lemma for caucvgpr 7458. 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 7445* Lemma for caucvgpr 7458. 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 7446* Lemma for caucvgpr 7458. 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 7447* Lemma for caucvgpr 7458. 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 7448* Lemma for caucvgpr 7458. 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 7449* Lemma for caucvgpr 7458. 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 7450* Lemma for caucvgpr 7458. 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 7451* Lemma for caucvgpr 7458. 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 7452* Lemma for caucvgpr 7458. 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 7453* Lemma for caucvgpr 7458. 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 7454* Lemma for caucvgpr 7458. 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 7455* Lemma for caucvgpr 7458. 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 7456* Lemma for caucvgpr 7458. 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 7457* Lemma for caucvgpr 7458. 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 7458* 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 7438 and caucvgprpr 7488. Reading cauappcvgpr 7438 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 7459* Lemma for caucvgprpr 7488. 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 7460* Lemma for caucvgprpr 7488. Rearranging some expressions for caucvgprprlemloc 7479. (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 7461* Lemma for caucvgprpr 7488. 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 7462* Lemma for caucvgprpr 7488. 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 7463* Lemma for caucvgprpr 7488. 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 7464* Lemma for caucvgprpr 7488. 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 7465* Lemma for caucvgprpr 7488. 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 7466* Lemma for caucvgprpr 7488. 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 7467* Lemma for caucvgprpr 7488. 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 7468* Lemma for caucvgprpr 7488. 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 7469* Lemma for caucvgprpr 7488. 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 7470* Lemma for caucvgprpr 7488. 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 7471* Lemma for caucvgprpr 7488. 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 7472* Lemma for caucvgprpr 7488. 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 7473* Lemma for caucvgprpr 7488. 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 7474* Lemma for caucvgprpr 7488. 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 7475* Lemma for caucvgprpr 7488. 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 7476* Lemma for caucvgprpr 7488. 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 7477* Lemma for caucvgprpr 7488. 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 7478* Lemma for caucvgprpr 7488. 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 7479* Lemma for caucvgprpr 7488. 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 7480* Lemma for caucvgprpr 7488. 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 7481* Lemma for caucvgprpr 7488. The putative limit is a positive real. Like caucvgprprlemcl 7480 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 7482* Lemma for caucvgprpr 7488. 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 7483* Lemma for caucvgprpr 7488. 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 7484* Lemma for caucvgprpr 7488. 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 7485* Lemma for caucvgprpr 7488. 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  |  ( *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  ->  J 
 <N  K )   &    |-  ( ph  ->  <. { l  |  l  <Q  ( *Q `  [ <. J ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. J ,  1o >. ]  ~Q  )  <Q  u } >.  <P  Q )   =>    |-  ( ph  ->  ( F `  K )  <P  ( L  +P.  Q ) )
 
Theoremcaucvgprprlem2 7486* Lemma for caucvgprpr 7488. 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  |  ( *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  ->  J 
 <N  K )   &    |-  ( ph  ->  <. { l  |  l  <Q  ( *Q `  [ <. J ,  1o >. ]  ~Q  ) } ,  { u  |  ( *Q `  [ <. J ,  1o >. ]  ~Q  )  <Q  u } >.  <P  Q )   =>    |-  ( ph  ->  L  <P  ( ( F `  K )  +P.  Q ) )
 
Theoremcaucvgprprlemlim 7487* Lemma for caucvgprpr 7488. The putative limit is a limit. (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  ->  A. x  e.  P.  E. j  e. 
 N.  A. k  e.  N.  ( j  <N  k  ->  ( ( F `  k )  <P  ( L 
 +P.  x )  /\  L  <P  ( ( F `
  k )  +P.  x ) ) ) )
 
Theoremcaucvgprpr 7488* A Cauchy sequence of positive reals 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 given value  A, to avoid the case where we have positive terms which "converge" to zero (which is not a positive real).

This is similar to caucvgpr 7458 except that values of the sequence are positive reals rather than positive fractions. Reading that proof first (or cauappcvgpr 7438) might help in understanding this one, as they are slightly simpler but similarly structured. (Contributed by Jim Kingdon, 14-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 ) )   =>    |-  ( ph  ->  E. y  e.  P.  A. x  e. 
 P.  E. j  e.  N.  A. k  e.  N.  (
 j  <N  k  ->  (
 ( F `  k
 )  <P  ( y  +P.  x )  /\  y  <P  ( ( F `  k
 )  +P.  x )
 ) ) )
 
Theoremsuplocexprlemell 7489* Lemma for suplocexpr 7501. Membership in the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
 |-  ( B  e.  U. ( 1st " A )  <->  E. x  e.  A  B  e.  ( 1st `  x ) )
 
Theoremsuplocexprlem2b 7490 Lemma for suplocexpr 7501. Expression for the lower cut of the putative supremum. (Contributed by Jim Kingdon, 9-Jan-2024.)
 |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( A  C_  P.  ->  ( 2nd `  B )  =  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u }
 )
 
Theoremsuplocexprlemss 7491* Lemma for suplocexpr 7501. 
A is a set of positive reals. (Contributed by Jim Kingdon, 7-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   =>    |-  ( ph  ->  A  C_  P. )
 
Theoremsuplocexprlemml 7492* Lemma for suplocexpr 7501. The lower cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   =>    |-  ( ph  ->  E. s  e.  Q.  s  e.  U. ( 1st " A ) )
 
Theoremsuplocexprlemrl 7493* Lemma for suplocexpr 7501. The lower cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   =>    |-  ( ph  ->  A. q  e. 
 Q.  ( q  e. 
 U. ( 1st " A ) 
 <-> 
 E. r  e.  Q.  ( q  <Q  r  /\  r  e.  U. ( 1st " A ) ) ) )
 
Theoremsuplocexprlemmu 7494* Lemma for suplocexpr 7501. The upper cut of the putative supremum is inhabited. (Contributed by Jim Kingdon, 7-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  E. s  e.  Q.  s  e.  ( 2nd `  B ) )
 
Theoremsuplocexprlemru 7495* Lemma for suplocexpr 7501. The upper cut of the putative supremum is rounded. (Contributed by Jim Kingdon, 9-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  A. r  e. 
 Q.  ( r  e.  ( 2nd `  B ) 
 <-> 
 E. q  e.  Q.  ( q  <Q  r  /\  q  e.  ( 2nd `  B ) ) ) )
 
Theoremsuplocexprlemdisj 7496* Lemma for suplocexpr 7501. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  A. q  e. 
 Q.  -.  ( q  e.  U. ( 1st " A )  /\  q  e.  ( 2nd `  B ) ) )
 
Theoremsuplocexprlemloc 7497* Lemma for suplocexpr 7501. The putative supremum is located. (Contributed by Jim Kingdon, 9-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  A. q  e. 
 Q.  A. r  e.  Q.  ( q  <Q  r  ->  ( q  e.  U. ( 1st " A )  \/  r  e.  ( 2nd `  B ) ) ) )
 
Theoremsuplocexprlemex 7498* Lemma for suplocexpr 7501. The putative supremum is a positive real. (Contributed by Jim Kingdon, 7-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  B  e.  P. )
 
Theoremsuplocexprlemub 7499* Lemma for suplocexpr 7501. The putative supremum is an upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  A. y  e.  A  -.  B  <P  y )
 
Theoremsuplocexprlemlub 7500* Lemma for suplocexpr 7501. The putative supremum is a least upper bound. (Contributed by Jim Kingdon, 14-Jan-2024.)
 |-  ( ph  ->  E. x  x  e.  A )   &    |-  ( ph  ->  E. x  e.  P.  A. y  e.  A  y 
 <P  x )   &    |-  ( ph  ->  A. x  e.  P.  A. y  e.  P.  ( x  <P  y  ->  ( E. z  e.  A  x  <P  z  \/  A. z  e.  A  z  <P  y ) ) )   &    |-  B  =  <. U. ( 1st " A ) ,  { u  e.  Q.  |  E. w  e.  |^| ( 2nd " A ) w  <Q  u } >.   =>    |-  ( ph  ->  ( y  <P  B  ->  E. z  e.  A  y  <P  z ) )
    < Previous  Next >

Page List
Jump to page: Contents  1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000 71 7001-7100 72 7101-7200 73 7201-7300 74 7301-7400 75 7401-7500 76 7501-7600 77 7601-7700 78 7701-7800 79 7801-7900 80 7901-8000 81 8001-8100 82 8101-8200 83 8201-8300 84 8301-8400 85 8401-8500 86 8501-8600 87 8601-8700 88 8701-8800 89 8801-8900 90 8901-9000 91 9001-9100 92 9101-9200 93 9201-9300 94 9301-9400 95 9401-9500 96 9501-9600 97 9601-9700 98 9701-9800 99 9801-9900 100 9901-10000 101 10001-10100 102 10101-10200 103 10201-10300 104 10301-10400 105 10401-10500 106 10501-10600 107 10601-10700 108 10701-10800 109 10801-10900 110 10901-11000 111 11001-11100 112 11101-11200 113 11201-11300 114 11301-11400 115 11401-11500 116 11501-11600 117 11601-11700 118 11701-11800 119 11801-11900 120 11901-12000 121 12001-12100 122 12101-12200 123 12201-12300 124 12301-12400 125 12401-12500 126 12501-12600 127 12601-12700 128 12701-12800 129 12801-12900 130 12901-13000 131 13001-13100 132 13101-13177
  Copyright terms: Public domain < Previous  Next >