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

Theorem resqrexlemglsq 10801
Description: Lemma for resqrex 10805. The sequence formed by squaring each term of  F converges to  ( L ^
2 ). (Contributed by Mario Carneiro and Jim Kingdon, 8-Aug-2021.)
Hypotheses
Ref Expression
resqrexlemex.seq  |-  F  =  seq 1 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y ) )  /  2 ) ) ,  ( NN  X.  { ( 1  +  A ) } ) )
resqrexlemex.a  |-  ( ph  ->  A  e.  RR )
resqrexlemex.agt0  |-  ( ph  ->  0  <_  A )
resqrexlemgt0.rr  |-  ( ph  ->  L  e.  RR )
resqrexlemgt0.lim  |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) ) )
resqrexlemsqa.g  |-  G  =  ( x  e.  NN  |->  ( ( F `  x ) ^ 2 ) )
Assertion
Ref Expression
resqrexlemglsq  |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( G `  k )  <  ( ( L ^ 2 )  +  e )  /\  ( L ^ 2 )  < 
( ( G `  k )  +  e ) ) )
Distinct variable groups:    y, A, z   
e, F, j, k, i, y, z    x, F, k    e, L, j, k, i, y, z    ph, e, i, j, k, y, z
Allowed substitution hints:    ph( x)    A( x, e, i, j, k)    G( x, y, z, e, i, j, k)    L( x)

Proof of Theorem resqrexlemglsq
Dummy variable  f is distinct from all other variables.
StepHypRef Expression
1 oveq2 5782 . . . . . . 7  |-  ( f  =  ( e  / 
( ( F ` 
1 )  +  L
) )  ->  ( L  +  f )  =  ( L  +  ( e  /  (
( F `  1
)  +  L ) ) ) )
21breq2d 3941 . . . . . 6  |-  ( f  =  ( e  / 
( ( F ` 
1 )  +  L
) )  ->  (
( F `  k
)  <  ( L  +  f )  <->  ( F `  k )  <  ( L  +  ( e  /  ( ( F `
 1 )  +  L ) ) ) ) )
3 oveq2 5782 . . . . . . 7  |-  ( f  =  ( e  / 
( ( F ` 
1 )  +  L
) )  ->  (
( F `  k
)  +  f )  =  ( ( F `
 k )  +  ( e  /  (
( F `  1
)  +  L ) ) ) )
43breq2d 3941 . . . . . 6  |-  ( f  =  ( e  / 
( ( F ` 
1 )  +  L
) )  ->  ( L  <  ( ( F `
 k )  +  f )  <->  L  <  ( ( F `  k
)  +  ( e  /  ( ( F `
 1 )  +  L ) ) ) ) )
52, 4anbi12d 464 . . . . 5  |-  ( f  =  ( e  / 
( ( F ` 
1 )  +  L
) )  ->  (
( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) )  <-> 
( ( F `  k )  <  ( L  +  ( e  /  ( ( F `
 1 )  +  L ) ) )  /\  L  <  (
( F `  k
)  +  ( e  /  ( ( F `
 1 )  +  L ) ) ) ) ) )
65rexralbidv 2461 . . . 4  |-  ( f  =  ( e  / 
( ( F ` 
1 )  +  L
) )  ->  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) )  <->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  ( e  /  ( ( F `
 1 )  +  L ) ) )  /\  L  <  (
( F `  k
)  +  ( e  /  ( ( F `
 1 )  +  L ) ) ) ) ) )
7 resqrexlemgt0.lim . . . . . . 7  |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) ) )
8 fveq2 5421 . . . . . . . . . . . 12  |-  ( i  =  k  ->  ( F `  i )  =  ( F `  k ) )
98breq1d 3939 . . . . . . . . . . 11  |-  ( i  =  k  ->  (
( F `  i
)  <  ( L  +  e )  <->  ( F `  k )  <  ( L  +  e )
) )
108oveq1d 5789 . . . . . . . . . . . 12  |-  ( i  =  k  ->  (
( F `  i
)  +  e )  =  ( ( F `
 k )  +  e ) )
1110breq2d 3941 . . . . . . . . . . 11  |-  ( i  =  k  ->  ( L  <  ( ( F `
 i )  +  e )  <->  L  <  ( ( F `  k
)  +  e ) ) )
129, 11anbi12d 464 . . . . . . . . . 10  |-  ( i  =  k  ->  (
( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) )  <-> 
( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) ) ) )
1312cbvralv 2654 . . . . . . . . 9  |-  ( A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) )  <->  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) ) )
1413rexbii 2442 . . . . . . . 8  |-  ( E. j  e.  NN  A. i  e.  ( ZZ>= `  j ) ( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) )  <->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) ) )
1514ralbii 2441 . . . . . . 7  |-  ( A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j )
( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) )  <->  A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) ) )
167, 15sylib 121 . . . . . 6  |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) ) )
17 oveq2 5782 . . . . . . . . . 10  |-  ( e  =  f  ->  ( L  +  e )  =  ( L  +  f ) )
1817breq2d 3941 . . . . . . . . 9  |-  ( e  =  f  ->  (
( F `  k
)  <  ( L  +  e )  <->  ( F `  k )  <  ( L  +  f )
) )
19 oveq2 5782 . . . . . . . . . 10  |-  ( e  =  f  ->  (
( F `  k
)  +  e )  =  ( ( F `
 k )  +  f ) )
2019breq2d 3941 . . . . . . . . 9  |-  ( e  =  f  ->  ( L  <  ( ( F `
 k )  +  e )  <->  L  <  ( ( F `  k
)  +  f ) ) )
2118, 20anbi12d 464 . . . . . . . 8  |-  ( e  =  f  ->  (
( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) )  <-> 
( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) ) ) )
2221rexralbidv 2461 . . . . . . 7  |-  ( e  =  f  ->  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) )  <->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) ) ) )
2322cbvralv 2654 . . . . . 6  |-  ( A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  e )  /\  L  <  ( ( F `  k )  +  e ) )  <->  A. f  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) ) )
2416, 23sylib 121 . . . . 5  |-  ( ph  ->  A. f  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) ) )
2524adantr 274 . . . 4  |-  ( (
ph  /\  e  e.  RR+ )  ->  A. f  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  f )  /\  L  <  ( ( F `  k )  +  f ) ) )
26 simpr 109 . . . . 5  |-  ( (
ph  /\  e  e.  RR+ )  ->  e  e.  RR+ )
27 resqrexlemex.seq . . . . . . . . . . 11  |-  F  =  seq 1 ( ( y  e.  RR+ ,  z  e.  RR+  |->  ( ( y  +  ( A  /  y ) )  /  2 ) ) ,  ( NN  X.  { ( 1  +  A ) } ) )
28 resqrexlemex.a . . . . . . . . . . 11  |-  ( ph  ->  A  e.  RR )
29 resqrexlemex.agt0 . . . . . . . . . . 11  |-  ( ph  ->  0  <_  A )
3027, 28, 29resqrexlemf 10786 . . . . . . . . . 10  |-  ( ph  ->  F : NN --> RR+ )
3130adantr 274 . . . . . . . . 9  |-  ( (
ph  /\  e  e.  RR+ )  ->  F : NN
--> RR+ )
32 1nn 8738 . . . . . . . . . 10  |-  1  e.  NN
3332a1i 9 . . . . . . . . 9  |-  ( (
ph  /\  e  e.  RR+ )  ->  1  e.  NN )
3431, 33ffvelrnd 5556 . . . . . . . 8  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( F `  1 )  e.  RR+ )
3534rpred 9490 . . . . . . 7  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( F `  1 )  e.  RR )
36 resqrexlemgt0.rr . . . . . . . 8  |-  ( ph  ->  L  e.  RR )
3736adantr 274 . . . . . . 7  |-  ( (
ph  /\  e  e.  RR+ )  ->  L  e.  RR )
3835, 37readdcld 7802 . . . . . 6  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( ( F `  1 )  +  L )  e.  RR )
3934rpgt0d 9493 . . . . . . 7  |-  ( (
ph  /\  e  e.  RR+ )  ->  0  <  ( F `  1 ) )
4027, 28, 29, 36, 7resqrexlemgt0 10799 . . . . . . . 8  |-  ( ph  ->  0  <_  L )
4140adantr 274 . . . . . . 7  |-  ( (
ph  /\  e  e.  RR+ )  ->  0  <_  L )
42 addgtge0 8219 . . . . . . 7  |-  ( ( ( ( F ` 
1 )  e.  RR  /\  L  e.  RR )  /\  ( 0  < 
( F `  1
)  /\  0  <_  L ) )  ->  0  <  ( ( F ` 
1 )  +  L
) )
4335, 37, 39, 41, 42syl22anc 1217 . . . . . 6  |-  ( (
ph  /\  e  e.  RR+ )  ->  0  <  ( ( F `  1
)  +  L ) )
4438, 43elrpd 9488 . . . . 5  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( ( F `  1 )  +  L )  e.  RR+ )
4526, 44rpdivcld 9508 . . . 4  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( e  /  ( ( F `
 1 )  +  L ) )  e.  RR+ )
466, 25, 45rspcdva 2794 . . 3  |-  ( (
ph  /\  e  e.  RR+ )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  ( e  /  ( ( F `
 1 )  +  L ) ) )  /\  L  <  (
( F `  k
)  +  ( e  /  ( ( F `
 1 )  +  L ) ) ) ) )
47 simpllr 523 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
j  e.  NN )
48 simplr 519 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
k  e.  ( ZZ>= `  j ) )
49 eluznn 9401 . . . . . . . . . 10  |-  ( ( j  e.  NN  /\  k  e.  ( ZZ>= `  j ) )  -> 
k  e.  NN )
5047, 48, 49syl2anc 408 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
k  e.  NN )
5131ad3antrrr 483 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  ->  F : NN --> RR+ )
5251, 50ffvelrnd 5556 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( F `  k
)  e.  RR+ )
53 2z 9089 . . . . . . . . . . 11  |-  2  e.  ZZ
5453a1i 9 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
2  e.  ZZ )
5552, 54rpexpcld 10455 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k ) ^ 2 )  e.  RR+ )
56 fveq2 5421 . . . . . . . . . . 11  |-  ( x  =  k  ->  ( F `  x )  =  ( F `  k ) )
5756oveq1d 5789 . . . . . . . . . 10  |-  ( x  =  k  ->  (
( F `  x
) ^ 2 )  =  ( ( F `
 k ) ^
2 ) )
58 resqrexlemsqa.g . . . . . . . . . 10  |-  G  =  ( x  e.  NN  |->  ( ( F `  x ) ^ 2 ) )
5957, 58fvmptg 5497 . . . . . . . . 9  |-  ( ( k  e.  NN  /\  ( ( F `  k ) ^ 2 )  e.  RR+ )  ->  ( G `  k
)  =  ( ( F `  k ) ^ 2 ) )
6050, 55, 59syl2anc 408 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( G `  k
)  =  ( ( F `  k ) ^ 2 ) )
6152rpred 9490 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( F `  k
)  e.  RR )
6261recnd 7801 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( F `  k
)  e.  CC )
6337ad3antrrr 483 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  ->  L  e.  RR )
6463recnd 7801 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  ->  L  e.  CC )
65 subsq 10406 . . . . . . . . . . 11  |-  ( ( ( F `  k
)  e.  CC  /\  L  e.  CC )  ->  ( ( ( F `
 k ) ^
2 )  -  ( L ^ 2 ) )  =  ( ( ( F `  k )  +  L )  x.  ( ( F `  k )  -  L
) ) )
6662, 64, 65syl2anc 408 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 k ) ^
2 )  -  ( L ^ 2 ) )  =  ( ( ( F `  k )  +  L )  x.  ( ( F `  k )  -  L
) ) )
6761, 63readdcld 7802 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k )  +  L
)  e.  RR )
6861, 63resubcld 8150 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k )  -  L
)  e.  RR )
6967, 68remulcld 7803 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 k )  +  L )  x.  (
( F `  k
)  -  L ) )  e.  RR )
7038ad3antrrr 483 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F ` 
1 )  +  L
)  e.  RR )
7170, 68remulcld 7803 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 1 )  +  L )  x.  (
( F `  k
)  -  L ) )  e.  RR )
7226ad3antrrr 483 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
e  e.  RR+ )
7372rpred 9490 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
e  e.  RR )
7428ad4antr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  ->  A  e.  RR )
7529ad4antr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
0  <_  A )
767ad4antr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  ->  A. e  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j )
( ( F `  i )  <  ( L  +  e )  /\  L  <  ( ( F `  i )  +  e ) ) )
7727, 74, 75, 63, 76, 50resqrexlemoverl 10800 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  ->  L  <_  ( F `  k ) )
7861, 63subge0d 8304 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( 0  <_  (
( F `  k
)  -  L )  <-> 
L  <_  ( F `  k ) ) )
7977, 78mpbird 166 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
0  <_  ( ( F `  k )  -  L ) )
80 fveq2 5421 . . . . . . . . . . . . . . 15  |-  ( k  =  1  ->  ( F `  k )  =  ( F ` 
1 ) )
8180oveq1d 5789 . . . . . . . . . . . . . 14  |-  ( k  =  1  ->  (
( F `  k
)  +  L )  =  ( ( F `
 1 )  +  L ) )
82 eqle 7862 . . . . . . . . . . . . . 14  |-  ( ( ( ( F `  k )  +  L
)  e.  RR  /\  ( ( F `  k )  +  L
)  =  ( ( F `  1 )  +  L ) )  ->  ( ( F `
 k )  +  L )  <_  (
( F `  1
)  +  L ) )
8367, 81, 82syl2an 287 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  k  =  1 )  ->  ( ( F `
 k )  +  L )  <_  (
( F `  1
)  +  L ) )
8461adantr 274 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
( F `  k
)  e.  RR )
8535ad4antr 485 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
( F `  1
)  e.  RR )
8663adantr 274 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  ->  L  e.  RR )
8728ad5antr 487 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  ->  A  e.  RR )
8829ad5antr 487 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
0  <_  A )
8932a1i 9 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
1  e.  NN )
9050adantr 274 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
k  e.  NN )
91 simpr 109 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
1  <  k )
9227, 87, 88, 89, 90, 91resqrexlemdecn 10791 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
( F `  k
)  <  ( F `  1 ) )
9384, 85, 92ltled 7888 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
( F `  k
)  <_  ( F `  1 ) )
9484, 85, 86, 93leadd1dd 8328 . . . . . . . . . . . . 13  |-  ( ( ( ( ( (
ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>= `  j )
)  /\  ( ( F `  k )  <  ( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  /\  1  <  k )  -> 
( ( F `  k )  +  L
)  <_  ( ( F `  1 )  +  L ) )
95 nn1gt1 8761 . . . . . . . . . . . . . 14  |-  ( k  e.  NN  ->  (
k  =  1  \/  1  <  k ) )
9650, 95syl 14 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( k  =  1  \/  1  <  k
) )
9783, 94, 96mpjaodan 787 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k )  +  L
)  <_  ( ( F `  1 )  +  L ) )
9867, 70, 68, 79, 97lemul1ad 8704 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 k )  +  L )  x.  (
( F `  k
)  -  L ) )  <_  ( (
( F `  1
)  +  L )  x.  ( ( F `
 k )  -  L ) ) )
99 simprl 520 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( F `  k
)  <  ( L  +  ( e  / 
( ( F ` 
1 )  +  L
) ) ) )
10045ad3antrrr 483 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( e  /  (
( F `  1
)  +  L ) )  e.  RR+ )
101100rpred 9490 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( e  /  (
( F `  1
)  +  L ) )  e.  RR )
10261, 63, 101ltsubadd2d 8312 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 k )  -  L )  <  (
e  /  ( ( F `  1 )  +  L ) )  <-> 
( F `  k
)  <  ( L  +  ( e  / 
( ( F ` 
1 )  +  L
) ) ) ) )
10399, 102mpbird 166 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k )  -  L
)  <  ( e  /  ( ( F `
 1 )  +  L ) ) )
10444ad3antrrr 483 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F ` 
1 )  +  L
)  e.  RR+ )
10568, 73, 104ltmuldiv2d 9539 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( ( F `  1 )  +  L )  x.  ( ( F `  k )  -  L
) )  <  e  <->  ( ( F `  k
)  -  L )  <  ( e  / 
( ( F ` 
1 )  +  L
) ) ) )
106103, 105mpbird 166 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 1 )  +  L )  x.  (
( F `  k
)  -  L ) )  <  e )
10769, 71, 73, 98, 106lelttrd 7894 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 k )  +  L )  x.  (
( F `  k
)  -  L ) )  <  e )
10866, 107eqbrtrd 3950 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( F `
 k ) ^
2 )  -  ( L ^ 2 ) )  <  e )
10961resqcld 10457 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k ) ^ 2 )  e.  RR )
11063resqcld 10457 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( L ^ 2 )  e.  RR )
111109, 110, 73ltsubadd2d 8312 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( ( ( F `  k ) ^ 2 )  -  ( L ^ 2 ) )  <  e  <->  ( ( F `  k ) ^ 2 )  < 
( ( L ^
2 )  +  e ) ) )
112108, 111mpbid 146 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( F `  k ) ^ 2 )  <  ( ( L ^ 2 )  +  e ) )
11360, 112eqbrtrd 3950 . . . . . . 7  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( G `  k
)  <  ( ( L ^ 2 )  +  e ) )
11460, 109eqeltrd 2216 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( G `  k
)  e.  RR )
115114, 73readdcld 7802 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( G `  k )  +  e )  e.  RR )
11641ad3antrrr 483 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
0  <_  L )
117 le2sq2 10375 . . . . . . . . . 10  |-  ( ( ( L  e.  RR  /\  0  <_  L )  /\  ( ( F `  k )  e.  RR  /\  L  <_  ( F `  k ) ) )  ->  ( L ^
2 )  <_  (
( F `  k
) ^ 2 ) )
11863, 116, 61, 77, 117syl22anc 1217 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( L ^ 2 )  <_  ( ( F `  k ) ^ 2 ) )
119118, 60breqtrrd 3956 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( L ^ 2 )  <_  ( G `  k ) )
120114, 72ltaddrpd 9524 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( G `  k
)  <  ( ( G `  k )  +  e ) )
121110, 114, 115, 119, 120lelttrd 7894 . . . . . . 7  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( L ^ 2 )  <  ( ( G `  k )  +  e ) )
122113, 121jca 304 . . . . . 6  |-  ( ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  (
ZZ>= `  j ) )  /\  ( ( F `
 k )  < 
( L  +  ( e  /  ( ( F `  1 )  +  L ) ) )  /\  L  < 
( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) ) )  -> 
( ( G `  k )  <  (
( L ^ 2 )  +  e )  /\  ( L ^
2 )  <  (
( G `  k
)  +  e ) ) )
123122ex 114 . . . . 5  |-  ( ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  /\  k  e.  ( ZZ>=
`  j ) )  ->  ( ( ( F `  k )  <  ( L  +  ( e  /  (
( F `  1
)  +  L ) ) )  /\  L  <  ( ( F `  k )  +  ( e  /  ( ( F `  1 )  +  L ) ) ) )  ->  (
( G `  k
)  <  ( ( L ^ 2 )  +  e )  /\  ( L ^ 2 )  < 
( ( G `  k )  +  e ) ) ) )
124123ralimdva 2499 . . . 4  |-  ( ( ( ph  /\  e  e.  RR+ )  /\  j  e.  NN )  ->  ( A. k  e.  ( ZZ>=
`  j ) ( ( F `  k
)  <  ( L  +  ( e  / 
( ( F ` 
1 )  +  L
) ) )  /\  L  <  ( ( F `
 k )  +  ( e  /  (
( F `  1
)  +  L ) ) ) )  ->  A. k  e.  ( ZZ>=
`  j ) ( ( G `  k
)  <  ( ( L ^ 2 )  +  e )  /\  ( L ^ 2 )  < 
( ( G `  k )  +  e ) ) ) )
125124reximdva 2534 . . 3  |-  ( (
ph  /\  e  e.  RR+ )  ->  ( E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( F `  k )  <  ( L  +  ( e  /  ( ( F `
 1 )  +  L ) ) )  /\  L  <  (
( F `  k
)  +  ( e  /  ( ( F `
 1 )  +  L ) ) ) )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( G `  k )  <  (
( L ^ 2 )  +  e )  /\  ( L ^
2 )  <  (
( G `  k
)  +  e ) ) ) )
12646, 125mpd 13 . 2  |-  ( (
ph  /\  e  e.  RR+ )  ->  E. j  e.  NN  A. k  e.  ( ZZ>= `  j )
( ( G `  k )  <  (
( L ^ 2 )  +  e )  /\  ( L ^
2 )  <  (
( G `  k
)  +  e ) ) )
127126ralrimiva 2505 1  |-  ( ph  ->  A. e  e.  RR+  E. j  e.  NN  A. k  e.  ( ZZ>= `  j ) ( ( G `  k )  <  ( ( L ^ 2 )  +  e )  /\  ( L ^ 2 )  < 
( ( G `  k )  +  e ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    \/ wo 697    = wceq 1331    e. wcel 1480   A.wral 2416   E.wrex 2417   {csn 3527   class class class wbr 3929    |-> cmpt 3989    X. cxp 4537   -->wf 5119   ` cfv 5123  (class class class)co 5774    e. cmpo 5776   CCcc 7625   RRcr 7626   0cc0 7627   1c1 7628    + caddc 7630    x. cmul 7632    < clt 7807    <_ cle 7808    - cmin 7940    / cdiv 8439   NNcn 8727   2c2 8778   ZZcz 9061   ZZ>=cuz 9333   RR+crp 9448    seqcseq 10225   ^cexp 10299
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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502  ax-cnex 7718  ax-resscn 7719  ax-1cn 7720  ax-1re 7721  ax-icn 7722  ax-addcl 7723  ax-addrcl 7724  ax-mulcl 7725  ax-mulrcl 7726  ax-addcom 7727  ax-mulcom 7728  ax-addass 7729  ax-mulass 7730  ax-distr 7731  ax-i2m1 7732  ax-0lt1 7733  ax-1rid 7734  ax-0id 7735  ax-rnegex 7736  ax-precex 7737  ax-cnre 7738  ax-pre-ltirr 7739  ax-pre-ltwlin 7740  ax-pre-lttrn 7741  ax-pre-apti 7742  ax-pre-ltadd 7743  ax-pre-mulgt0 7744  ax-pre-mulext 7745
This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-po 4218  df-iso 4219  df-iord 4288  df-on 4290  df-ilim 4291  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-1st 6038  df-2nd 6039  df-recs 6202  df-frec 6288  df-pnf 7809  df-mnf 7810  df-xr 7811  df-ltxr 7812  df-le 7813  df-sub 7942  df-neg 7943  df-reap 8344  df-ap 8351  df-div 8440  df-inn 8728  df-2 8786  df-3 8787  df-4 8788  df-n0 8985  df-z 9062  df-uz 9334  df-rp 9449  df-seqfrec 10226  df-exp 10300
This theorem is referenced by:  resqrexlemsqa  10803
  Copyright terms: Public domain W3C validator