ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  caucvgprlemloc Unicode version

Theorem caucvgprlemloc 7503
Description: Lemma for caucvgpr 7510. The putative limit is located. (Contributed by Jim Kingdon, 27-Sep-2020.)
Hypotheses
Ref Expression
caucvgpr.f  |-  ( ph  ->  F : N. --> Q. )
caucvgpr.cau  |-  ( 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  )
) ) ) )
caucvgpr.bnd  |-  ( ph  ->  A. j  e.  N.  A  <Q  ( F `  j ) )
caucvgpr.lim  |-  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 } >.
Assertion
Ref Expression
caucvgprlemloc  |-  ( ph  ->  A. s  e.  Q.  A. r  e.  Q.  (
s  <Q  r  ->  (
s  e.  ( 1st `  L )  \/  r  e.  ( 2nd `  L
) ) ) )
Distinct variable groups:    A, j    j, F, l    u, F    ph, j,
r, s    s, l    u, j, r
Allowed substitution hints:    ph( u, k, n, l)    A( u, k, n, s, r, l)    F( k, n, s, r)    L( u, j, k, n, s, r, l)

Proof of Theorem caucvgprlemloc
Dummy variables  f  g  h  m  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ltexnqi 7237 . . . . 5  |-  ( s 
<Q  r  ->  E. y  e.  Q.  ( s  +Q  y )  =  r )
21adantl 275 . . . 4  |-  ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  ->  E. y  e.  Q.  ( s  +Q  y )  =  r )
3 subhalfnqq 7242 . . . . . 6  |-  ( y  e.  Q.  ->  E. x  e.  Q.  ( x  +Q  x )  <Q  y
)
43ad2antrl 482 . . . . 5  |-  ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  ->  E. x  e.  Q.  ( x  +Q  x
)  <Q  y )
5 archrecnq 7491 . . . . . . 7  |-  ( x  e.  Q.  ->  E. m  e.  N.  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x )
65ad2antrl 482 . . . . . 6  |-  ( ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  ->  E. m  e.  N.  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x )
7 simprr 522 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x )
8 nnnq 7250 . . . . . . . . . . . . . . 15  |-  ( m  e.  N.  ->  [ <. m ,  1o >. ]  ~Q  e.  Q. )
9 recclnq 7220 . . . . . . . . . . . . . . 15  |-  ( [
<. m ,  1o >. ]  ~Q  e.  Q.  ->  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )
108, 9syl 14 . . . . . . . . . . . . . 14  |-  ( m  e.  N.  ->  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )
1110ad2antrl 482 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )
12 simplrl 525 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  x  e.  Q. )
13 lt2addnq 7232 . . . . . . . . . . . . 13  |-  ( ( ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e. 
Q.  /\  x  e.  Q. )  /\  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q.  /\  x  e.  Q. )
)  ->  ( (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
)  ->  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
( x  +Q  x
) ) )
1411, 12, 11, 12, 13syl22anc 1218 . . . . . . . . . . . 12  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x )  ->  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( x  +Q  x ) ) )
157, 7, 14mp2and 430 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( x  +Q  x ) )
16 simplrr 526 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
x  +Q  x ) 
<Q  y )
17 ltsonq 7226 . . . . . . . . . . . 12  |-  <Q  Or  Q.
18 ltrelnq 7193 . . . . . . . . . . . 12  |-  <Q  C_  ( Q.  X.  Q. )
1917, 18sotri 4938 . . . . . . . . . . 11  |-  ( ( ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
( x  +Q  x
)  /\  ( x  +Q  x )  <Q  y
)  ->  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
y )
2015, 16, 19syl2anc 409 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  y )
21 simplrl 525 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  ->  s  e.  Q. )
2221ad3antrrr 484 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  s  e.  Q. )
23 ltanqi 7230 . . . . . . . . . 10  |-  ( ( ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
y  /\  s  e.  Q. )  ->  ( s  +Q  ( ( *Q
`  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( s  +Q  y
) )
2420, 22, 23syl2anc 409 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  <Q  ( s  +Q  y ) )
25 simprr 522 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  ->  ( s  +Q  y )  =  r )
2625ad2antrr 480 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
s  +Q  y )  =  r )
2724, 26breqtrd 3958 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  <Q  r )
28 addclnq 7203 . . . . . . . . . . 11  |-  ( ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )  ->  ( ( *Q
`  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  e. 
Q. )
2911, 11, 28syl2anc 409 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )
30 addclnq 7203 . . . . . . . . . 10  |-  ( ( s  e.  Q.  /\  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  e. 
Q. )  ->  (
s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  e.  Q. )
3122, 29, 30syl2anc 409 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  e.  Q. )
32 simplrr 526 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  ->  r  e.  Q. )
3332ad3antrrr 484 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  r  e.  Q. )
34 caucvgpr.f . . . . . . . . . . . 12  |-  ( ph  ->  F : N. --> Q. )
3534ad5antr 488 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  F : N. --> Q. )
36 simprl 521 . . . . . . . . . . 11  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  m  e.  N. )
3735, 36ffvelrnd 5560 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  ( F `  m )  e.  Q. )
38 addclnq 7203 . . . . . . . . . 10  |-  ( ( ( F `  m
)  e.  Q.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )  ->  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )
3937, 11, 38syl2anc 409 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( F `  m
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )
40 sowlin 4246 . . . . . . . . . 10  |-  ( ( 
<Q  Or  Q.  /\  (
( s  +Q  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  e.  Q.  /\  r  e.  Q.  /\  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )
)  ->  ( (
s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  <Q  r  ->  ( ( s  +Q  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  <Q  (
( F `  m
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  \/  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) 
<Q  r ) ) )
4117, 40mpan 421 . . . . . . . . 9  |-  ( ( ( s  +Q  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  e.  Q.  /\  r  e.  Q.  /\  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )  ->  ( ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  r  ->  ( ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  <Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  \/  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  r ) ) )
4231, 33, 39, 41syl3anc 1217 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( s  +Q  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  <Q  r  ->  ( ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  \/  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) 
<Q  r ) ) )
4327, 42mpd 13 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( s  +Q  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  <Q  (
( F `  m
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  \/  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) 
<Q  r ) )
4422adantr 274 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  s  e.  Q. )
45 simplrl 525 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  m  e.  N. )
46 simpr 109 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )  <Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )
4711adantr 274 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )
48 addassnqg 7210 . . . . . . . . . . . . . . 15  |-  ( ( s  e.  Q.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )  ->  (
( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  =  ( s  +Q  ( ( *Q
`  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) )
4944, 47, 47, 48syl3anc 1217 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  =  ( s  +Q  ( ( *Q
`  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) )
5049breq1d 3943 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
( ( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <->  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) ) )
5146, 50mpbird 166 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( ( F `
 m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )
52 ltanqg 7228 . . . . . . . . . . . . . 14  |-  ( ( f  e.  Q.  /\  g  e.  Q.  /\  h  e.  Q. )  ->  (
f  <Q  g  <->  ( h  +Q  f )  <Q  (
h  +Q  g ) ) )
5352adantl 275 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  /\  (
f  e.  Q.  /\  g  e.  Q.  /\  h  e.  Q. ) )  -> 
( f  <Q  g  <->  ( h  +Q  f ) 
<Q  ( h  +Q  g
) ) )
54 addclnq 7203 . . . . . . . . . . . . . 14  |-  ( ( s  e.  Q.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  e.  Q. )  ->  ( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )
5544, 47, 54syl2anc 409 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
s  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  e.  Q. )
5637adantr 274 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  ( F `  m )  e.  Q. )
57 addcomnqg 7209 . . . . . . . . . . . . . 14  |-  ( ( f  e.  Q.  /\  g  e.  Q. )  ->  ( f  +Q  g
)  =  ( g  +Q  f ) )
5857adantl 275 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  /\  (
f  e.  Q.  /\  g  e.  Q. )
)  ->  ( f  +Q  g )  =  ( g  +Q  f ) )
5953, 55, 56, 47, 58caovord2d 5944 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( F `  m )  <->  ( (
s  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( ( F `
 m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) )
6051, 59mpbird 166 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  (
s  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( F `  m ) )
61 opeq1 3709 . . . . . . . . . . . . . . . 16  |-  ( j  =  m  ->  <. j ,  1o >.  =  <. m ,  1o >. )
6261eceq1d 6469 . . . . . . . . . . . . . . 15  |-  ( j  =  m  ->  [ <. j ,  1o >. ]  ~Q  =  [ <. m ,  1o >. ]  ~Q  )
6362fveq2d 5429 . . . . . . . . . . . . . 14  |-  ( j  =  m  ->  ( *Q `  [ <. j ,  1o >. ]  ~Q  )  =  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )
6463oveq2d 5794 . . . . . . . . . . . . 13  |-  ( j  =  m  ->  (
s  +Q  ( *Q
`  [ <. j ,  1o >. ]  ~Q  )
)  =  ( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )
65 fveq2 5425 . . . . . . . . . . . . 13  |-  ( j  =  m  ->  ( F `  j )  =  ( F `  m ) )
6664, 65breq12d 3946 . . . . . . . . . . . 12  |-  ( j  =  m  ->  (
( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  ( F `  j )  <->  ( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
( F `  m
) ) )
6766rspcev 2790 . . . . . . . . . . 11  |-  ( ( m  e.  N.  /\  ( s  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  ( F `  m ) )  ->  E. j  e.  N.  ( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  ( F `  j ) )
6845, 60, 67syl2anc 409 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  E. j  e.  N.  ( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
( F `  j
) )
69 oveq1 5785 . . . . . . . . . . . . 13  |-  ( l  =  s  ->  (
l  +Q  ( *Q
`  [ <. j ,  1o >. ]  ~Q  )
)  =  ( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) ) )
7069breq1d 3943 . . . . . . . . . . . 12  |-  ( l  =  s  ->  (
( l  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  ( F `  j )  <->  ( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
( F `  j
) ) )
7170rexbidv 2439 . . . . . . . . . . 11  |-  ( l  =  s  ->  ( E. j  e.  N.  ( l  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  ( F `  j )  <->  E. j  e.  N.  ( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
( F `  j
) ) )
72 caucvgpr.lim . . . . . . . . . . . . 13  |-  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 } >.
7372fveq2i 5428 . . . . . . . . . . . 12  |-  ( 1st `  L )  =  ( 1st `  <. { 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 } >. )
74 nqex 7191 . . . . . . . . . . . . . 14  |-  Q.  e.  _V
7574rabex 4076 . . . . . . . . . . . . 13  |-  { l  e.  Q.  |  E. j  e.  N.  (
l  +Q  ( *Q
`  [ <. j ,  1o >. ]  ~Q  )
)  <Q  ( F `  j ) }  e.  _V
7674rabex 4076 . . . . . . . . . . . . 13  |-  { u  e.  Q.  |  E. j  e.  N.  ( ( F `
 j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q  u }  e.  _V
7775, 76op1st 6048 . . . . . . . . . . . 12  |-  ( 1st `  <. { 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 } >. )  =  { l  e. 
Q.  |  E. j  e.  N.  ( l  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
( F `  j
) }
7873, 77eqtri 2161 . . . . . . . . . . 11  |-  ( 1st `  L )  =  {
l  e.  Q.  |  E. j  e.  N.  ( l  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  ( F `  j ) }
7971, 78elrab2 2844 . . . . . . . . . 10  |-  ( s  e.  ( 1st `  L
)  <->  ( s  e. 
Q.  /\  E. j  e.  N.  ( s  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
( F `  j
) ) )
8044, 68, 79sylanbrc 414 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  ->  s  e.  ( 1st `  L
) )
8180ex 114 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( s  +Q  (
( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
) )  <Q  (
( F `  m
)  +Q  ( *Q
`  [ <. m ,  1o >. ]  ~Q  )
)  ->  s  e.  ( 1st `  L ) ) )
8233adantr 274 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( ( F `
 m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
r )  ->  r  e.  Q. )
8365, 63oveq12d 5796 . . . . . . . . . . . . 13  |-  ( j  =  m  ->  (
( F `  j
)  +Q  ( *Q
`  [ <. j ,  1o >. ]  ~Q  )
)  =  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) )
8483breq1d 3943 . . . . . . . . . . . 12  |-  ( j  =  m  ->  (
( ( F `  j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  r  <->  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
r ) )
8584rspcev 2790 . . . . . . . . . . 11  |-  ( ( m  e.  N.  /\  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  r )  ->  E. j  e.  N.  ( ( F `  j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  r )
8636, 85sylan 281 . . . . . . . . . 10  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( ( F `
 m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
r )  ->  E. j  e.  N.  ( ( F `
 j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
r )
87 breq2 3937 . . . . . . . . . . . 12  |-  ( u  =  r  ->  (
( ( F `  j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  u  <->  ( ( F `  j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
r ) )
8887rexbidv 2439 . . . . . . . . . . 11  |-  ( u  =  r  ->  ( E. j  e.  N.  ( ( F `  j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  u  <->  E. j  e.  N.  ( ( F `
 j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
r ) )
8972fveq2i 5428 . . . . . . . . . . . 12  |-  ( 2nd `  L )  =  ( 2nd `  <. { 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 } >. )
9075, 76op2nd 6049 . . . . . . . . . . . 12  |-  ( 2nd `  <. { 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 } >. )  =  { u  e. 
Q.  |  E. j  e.  N.  ( ( F `
 j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q  u }
9189, 90eqtri 2161 . . . . . . . . . . 11  |-  ( 2nd `  L )  =  {
u  e.  Q.  |  E. j  e.  N.  ( ( F `  j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  )
)  <Q  u }
9288, 91elrab2 2844 . . . . . . . . . 10  |-  ( r  e.  ( 2nd `  L
)  <->  ( r  e. 
Q.  /\  E. j  e.  N.  ( ( F `
 j )  +Q  ( *Q `  [ <. j ,  1o >. ]  ~Q  ) )  <Q 
r ) )
9382, 86, 92sylanbrc 414 . . . . . . . . 9  |-  ( ( ( ( ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  /\  (
m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x ) )  /\  ( ( F `
 m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) )  <Q 
r )  ->  r  e.  ( 2nd `  L
) )
9493ex 114 . . . . . . . 8  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  <Q  r  ->  r  e.  ( 2nd `  L
) ) )
9581, 94orim12d 776 . . . . . . 7  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
( ( s  +Q  ( ( *Q `  [ <. m ,  1o >. ]  ~Q  )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) ) 
<Q  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  )
)  \/  ( ( F `  m )  +Q  ( *Q `  [ <. m ,  1o >. ]  ~Q  ) ) 
<Q  r )  ->  (
s  e.  ( 1st `  L )  \/  r  e.  ( 2nd `  L
) ) ) )
9643, 95mpd 13 . . . . . 6  |-  ( ( ( ( ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  ( s  +Q  y
)  =  r ) )  /\  ( x  e.  Q.  /\  (
x  +Q  x ) 
<Q  y ) )  /\  ( m  e.  N.  /\  ( *Q `  [ <. m ,  1o >. ]  ~Q  )  <Q  x
) )  ->  (
s  e.  ( 1st `  L )  \/  r  e.  ( 2nd `  L
) ) )
976, 96rexlimddv 2555 . . . . 5  |-  ( ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  /\  ( x  e. 
Q.  /\  ( x  +Q  x )  <Q  y
) )  ->  (
s  e.  ( 1st `  L )  \/  r  e.  ( 2nd `  L
) ) )
984, 97rexlimddv 2555 . . . 4  |-  ( ( ( ( ph  /\  ( s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  /\  ( y  e.  Q.  /\  (
s  +Q  y )  =  r ) )  ->  ( s  e.  ( 1st `  L
)  \/  r  e.  ( 2nd `  L
) ) )
992, 98rexlimddv 2555 . . 3  |-  ( ( ( ph  /\  (
s  e.  Q.  /\  r  e.  Q. )
)  /\  s  <Q  r )  ->  ( s  e.  ( 1st `  L
)  \/  r  e.  ( 2nd `  L
) ) )
10099ex 114 . 2  |-  ( (
ph  /\  ( s  e.  Q.  /\  r  e. 
Q. ) )  -> 
( s  <Q  r  ->  ( s  e.  ( 1st `  L )  \/  r  e.  ( 2nd `  L ) ) ) )
101100ralrimivva 2515 1  |-  ( ph  ->  A. s  e.  Q.  A. r  e.  Q.  (
s  <Q  r  ->  (
s  e.  ( 1st `  L )  \/  r  e.  ( 2nd `  L
) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    <-> wb 104    \/ wo 698    /\ w3a 963    = wceq 1332    e. wcel 1481   A.wral 2417   E.wrex 2418   {crab 2421   <.cop 3531   class class class wbr 3933    Or wor 4221   -->wf 5123   ` cfv 5127  (class class class)co 5778   1stc1st 6040   2ndc2nd 6041   1oc1o 6310   [cec 6431   N.cnpi 7100    <N clti 7103    ~Q ceq 7107   Q.cnq 7108    +Q cplq 7110   *Qcrq 7112    <Q cltq 7113
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4047  ax-sep 4050  ax-nul 4058  ax-pow 4102  ax-pr 4135  ax-un 4359  ax-setind 4456  ax-iinf 4506
This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-ral 2422  df-rex 2423  df-reu 2424  df-rab 2426  df-v 2689  df-sbc 2911  df-csb 3005  df-dif 3074  df-un 3076  df-in 3078  df-ss 3085  df-nul 3365  df-pw 3513  df-sn 3534  df-pr 3535  df-op 3537  df-uni 3741  df-int 3776  df-iun 3819  df-br 3934  df-opab 3994  df-mpt 3995  df-tr 4031  df-eprel 4215  df-id 4219  df-po 4222  df-iso 4223  df-iord 4292  df-on 4294  df-suc 4297  df-iom 4509  df-xp 4549  df-rel 4550  df-cnv 4551  df-co 4552  df-dm 4553  df-rn 4554  df-res 4555  df-ima 4556  df-iota 5092  df-fun 5129  df-fn 5130  df-f 5131  df-f1 5132  df-fo 5133  df-f1o 5134  df-fv 5135  df-ov 5781  df-oprab 5782  df-mpo 5783  df-1st 6042  df-2nd 6043  df-recs 6206  df-irdg 6271  df-1o 6317  df-oadd 6321  df-omul 6322  df-er 6433  df-ec 6435  df-qs 6439  df-ni 7132  df-pli 7133  df-mi 7134  df-lti 7135  df-plpq 7172  df-mpq 7173  df-enq 7175  df-nqqs 7176  df-plqqs 7177  df-mqqs 7178  df-1nqqs 7179  df-rq 7180  df-ltnqqs 7181
This theorem is referenced by:  caucvgprlemcl  7504
  Copyright terms: Public domain W3C validator