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

Theorem cvg1nlemres 9584
Description: Lemma for cvg1n 9585. The original sequence  F has a limit (turns out it is the same as the limit of the modified sequence  G). (Contributed by Jim Kingdon, 1-Aug-2021.)
Hypotheses
Ref Expression
cvg1n.f  |-  ( ph  ->  F : NN --> RR )
cvg1n.c  |-  ( ph  ->  C  e.  RR+ )
cvg1n.cau  |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( F `  n )  <  ( ( F `
 k )  +  ( C  /  n
) )  /\  ( F `  k )  <  ( ( F `  n )  +  ( C  /  n ) ) ) )
cvg1nlem.g  |-  G  =  ( j  e.  NN  |->  ( F `  ( j  x.  Z ) ) )
cvg1nlem.z  |-  ( ph  ->  Z  e.  NN )
cvg1nlem.start  |-  ( ph  ->  C  <  Z )
Assertion
Ref Expression
cvg1nlemres  |-  ( ph  ->  E. y  e.  RR  A. x  e.  RR+  E. j  e.  NN  A. i  e.  ( ZZ>= `  j )
( ( F `  i )  <  (
y  +  x )  /\  y  <  (
( F `  i
)  +  x ) ) )
Distinct variable groups:    C, i, k    C, n, k    j, F, k, n    i, G, y, k    n, G   
x, G, i, y   
i, Z, j, k   
n, Z    ph, i, x, y, j    ph, k, n    x, j, y
Allowed substitution hints:    C( x, y, j)    F( x, y, i)    G( j)    Z( x, y)

Proof of Theorem cvg1nlemres
Dummy variables  e  a  b  c  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvg1n.f . . . 4  |-  ( ph  ->  F : NN --> RR )
2 cvg1n.c . . . 4  |-  ( ph  ->  C  e.  RR+ )
3 cvg1n.cau . . . 4  |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( F `  n )  <  ( ( F `
 k )  +  ( C  /  n
) )  /\  ( F `  k )  <  ( ( F `  n )  +  ( C  /  n ) ) ) )
4 cvg1nlem.g . . . 4  |-  G  =  ( j  e.  NN  |->  ( F `  ( j  x.  Z ) ) )
5 cvg1nlem.z . . . 4  |-  ( ph  ->  Z  e.  NN )
6 cvg1nlem.start . . . 4  |-  ( ph  ->  C  <  Z )
71, 2, 3, 4, 5, 6cvg1nlemf 9582 . . 3  |-  ( ph  ->  G : NN --> RR )
81, 2, 3, 4, 5, 6cvg1nlemcau 9583 . . 3  |-  ( ph  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( G `  n )  <  ( ( G `
 k )  +  ( 1  /  n
) )  /\  ( G `  k )  <  ( ( G `  n )  +  ( 1  /  n ) ) ) )
97, 8caucvgre 9580 . 2  |-  ( ph  ->  E. y  e.  RR  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )
10 fveq2 5178 . . . . . . . . . . 11  |-  ( a  =  w  ->  ( ZZ>=
`  a )  =  ( ZZ>= `  w )
)
1110raleqdv 2511 . . . . . . . . . 10  |-  ( a  =  w  ->  ( A. b  e.  ( ZZ>=
`  a ) ( ( G `  b
)  <  ( y  +  c )  /\  y  <  ( ( G `
 b )  +  c ) )  <->  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) ) )
1211cbvrexv 2534 . . . . . . . . 9  |-  ( E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) )  <->  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )
1312ralbii 2330 . . . . . . . 8  |-  ( A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) )  <->  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )
1413anbi2i 430 . . . . . . 7  |-  ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  <->  ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) ) )
1514anbi1i 431 . . . . . 6  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  <->  ( (
( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ ) )
16 simpr 103 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  ->  x  e.  RR+ )
1716rphalfcld 8635 . . . . . . . . 9  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  -> 
( x  /  2
)  e.  RR+ )
18 simplr 482 . . . . . . . . 9  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  ->  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )
19 oveq2 5520 . . . . . . . . . . . . 13  |-  ( c  =  ( x  / 
2 )  ->  (
y  +  c )  =  ( y  +  ( x  /  2
) ) )
2019breq2d 3776 . . . . . . . . . . . 12  |-  ( c  =  ( x  / 
2 )  ->  (
( G `  b
)  <  ( y  +  c )  <->  ( G `  b )  <  (
y  +  ( x  /  2 ) ) ) )
21 oveq2 5520 . . . . . . . . . . . . 13  |-  ( c  =  ( x  / 
2 )  ->  (
( G `  b
)  +  c )  =  ( ( G `
 b )  +  ( x  /  2
) ) )
2221breq2d 3776 . . . . . . . . . . . 12  |-  ( c  =  ( x  / 
2 )  ->  (
y  <  ( ( G `  b )  +  c )  <->  y  <  ( ( G `  b
)  +  ( x  /  2 ) ) ) )
2320, 22anbi12d 442 . . . . . . . . . . 11  |-  ( c  =  ( x  / 
2 )  ->  (
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) )  <->  ( ( G `
 b )  < 
( y  +  ( x  /  2 ) )  /\  y  < 
( ( G `  b )  +  ( x  /  2 ) ) ) ) )
2423rexralbidv 2350 . . . . . . . . . 10  |-  ( c  =  ( x  / 
2 )  ->  ( E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) )  <->  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  ( x  /  2 ) )  /\  y  <  (
( G `  b
)  +  ( x  /  2 ) ) ) ) )
2524rspcv 2652 . . . . . . . . 9  |-  ( ( x  /  2 )  e.  RR+  ->  ( A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) )  ->  E. a  e.  NN  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  ( x  /  2 ) )  /\  y  <  (
( G `  b
)  +  ( x  /  2 ) ) ) ) )
2617, 18, 25sylc 56 . . . . . . . 8  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  ->  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) )
2715, 26sylbir 125 . . . . . . 7  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  ->  E. a  e.  NN  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) )
282rpred 8622 . . . . . . . . . . . . . 14  |-  ( ph  ->  C  e.  RR )
2928ad4antr 463 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  C  e.  RR )
30 2re 7985 . . . . . . . . . . . . . 14  |-  2  e.  RR
3130a1i 9 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  2  e.  RR )
3229, 31remulcld 7056 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  ( C  x.  2 )  e.  RR )
33 simplr 482 . . . . . . . . . . . 12  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  x  e.  RR+ )
3432, 33rerpdivcld 8654 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  ( ( C  x.  2 )  /  x )  e.  RR )
355ad4antr 463 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  Z  e.  NN )
3634, 35nndivred 7963 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  ( (
( C  x.  2 )  /  x )  /  Z )  e.  RR )
37 simprl 483 . . . . . . . . . . 11  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  a  e.  NN )
3837nnred 7927 . . . . . . . . . 10  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  a  e.  RR )
3936, 38readdcld 7055 . . . . . . . . 9  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  ( (
( ( C  x.  2 )  /  x
)  /  Z )  +  a )  e.  RR )
40 arch 8178 . . . . . . . . 9  |-  ( ( ( ( ( C  x.  2 )  /  x )  /  Z
)  +  a )  e.  RR  ->  E. e  e.  NN  ( ( ( ( C  x.  2 )  /  x )  /  Z )  +  a )  <  e
)
4139, 40syl 14 . . . . . . . 8  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  E. e  e.  NN  ( ( ( ( C  x.  2 )  /  x )  /  Z )  +  a )  <  e
)
42 simprl 483 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  -> 
e  e.  NN )
4335adantr 261 . . . . . . . . . 10  |-  ( ( ( ( ( (
ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  ->  Z  e.  NN )
4442, 43nnmulcld 7962 . . . . . . . . 9  |-  ( ( ( ( ( (
ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  -> 
( e  x.  Z
)  e.  NN )
451ad6antr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  F : NN --> RR )
46 simplrl 487 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
e  e.  NN )
475ad6antr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  Z  e.  NN )
4846, 47nnmulcld 7962 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( e  x.  Z
)  e.  NN )
49 eluznn 8538 . . . . . . . . . . . . . . . 16  |-  ( ( ( e  x.  Z
)  e.  NN  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
i  e.  NN )
5048, 49sylancom 397 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
i  e.  NN )
5145, 50ffvelrnd 5303 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  i
)  e.  RR )
5245, 48ffvelrnd 5303 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  (
e  x.  Z ) )  e.  RR )
5333ad2antrr 457 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  x  e.  RR+ )
5453rpred 8622 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  x  e.  RR )
5554rehalfcld 8171 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( x  /  2
)  e.  RR )
5652, 55readdcld 7055 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  ( e  x.  Z
) )  +  ( x  /  2 ) )  e.  RR )
57 simpllr 486 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  -> 
y  e.  RR )
5857ad3antrrr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
y  e.  RR )
5958, 55readdcld 7055 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( y  +  ( x  /  2 ) )  e.  RR )
6059, 55readdcld 7055 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( y  +  ( x  /  2
) )  +  ( x  /  2 ) )  e.  RR )
6128ad6antr 467 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  C  e.  RR )
6261, 48nndivred 7963 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( C  /  (
e  x.  Z ) )  e.  RR )
6352, 62readdcld 7055 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  ( e  x.  Z
) )  +  ( C  /  ( e  x.  Z ) ) )  e.  RR )
64 simpr 103 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
i  e.  ( ZZ>= `  ( e  x.  Z
) ) )
653ad6antr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( F `  n )  <  ( ( F `
 k )  +  ( C  /  n
) )  /\  ( F `  k )  <  ( ( F `  n )  +  ( C  /  n ) ) ) )
66 fveq2 5178 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( e  x.  Z )  ->  ( ZZ>=
`  n )  =  ( ZZ>= `  ( e  x.  Z ) ) )
67 fveq2 5178 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( e  x.  Z )  ->  ( F `  n )  =  ( F `  ( e  x.  Z
) ) )
68 oveq2 5520 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  ( e  x.  Z )  ->  ( C  /  n )  =  ( C  /  (
e  x.  Z ) ) )
6968oveq2d 5528 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( e  x.  Z )  ->  (
( F `  k
)  +  ( C  /  n ) )  =  ( ( F `
 k )  +  ( C  /  (
e  x.  Z ) ) ) )
7067, 69breq12d 3777 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  ( e  x.  Z )  ->  (
( F `  n
)  <  ( ( F `  k )  +  ( C  /  n ) )  <->  ( F `  ( e  x.  Z
) )  <  (
( F `  k
)  +  ( C  /  ( e  x.  Z ) ) ) ) )
7167, 68oveq12d 5530 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( e  x.  Z )  ->  (
( F `  n
)  +  ( C  /  n ) )  =  ( ( F `
 ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) ) )
7271breq2d 3776 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  ( e  x.  Z )  ->  (
( F `  k
)  <  ( ( F `  n )  +  ( C  /  n ) )  <->  ( F `  k )  <  (
( F `  (
e  x.  Z ) )  +  ( C  /  ( e  x.  Z ) ) ) ) )
7370, 72anbi12d 442 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( e  x.  Z )  ->  (
( ( F `  n )  <  (
( F `  k
)  +  ( C  /  n ) )  /\  ( F `  k )  <  (
( F `  n
)  +  ( C  /  n ) ) )  <->  ( ( F `
 ( e  x.  Z ) )  < 
( ( F `  k )  +  ( C  /  ( e  x.  Z ) ) )  /\  ( F `
 k )  < 
( ( F `  ( e  x.  Z
) )  +  ( C  /  ( e  x.  Z ) ) ) ) ) )
7466, 73raleqbidv 2517 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( e  x.  Z )  ->  ( A. k  e.  ( ZZ>=
`  n ) ( ( F `  n
)  <  ( ( F `  k )  +  ( C  /  n ) )  /\  ( F `  k )  <  ( ( F `
 n )  +  ( C  /  n
) ) )  <->  A. k  e.  ( ZZ>= `  ( e  x.  Z ) ) ( ( F `  (
e  x.  Z ) )  <  ( ( F `  k )  +  ( C  / 
( e  x.  Z
) ) )  /\  ( F `  k )  <  ( ( F `
 ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) ) ) ) )
7574rspcv 2652 . . . . . . . . . . . . . . . . . 18  |-  ( ( e  x.  Z )  e.  NN  ->  ( A. n  e.  NN  A. k  e.  ( ZZ>= `  n ) ( ( F `  n )  <  ( ( F `
 k )  +  ( C  /  n
) )  /\  ( F `  k )  <  ( ( F `  n )  +  ( C  /  n ) ) )  ->  A. k  e.  ( ZZ>= `  ( e  x.  Z ) ) ( ( F `  (
e  x.  Z ) )  <  ( ( F `  k )  +  ( C  / 
( e  x.  Z
) ) )  /\  ( F `  k )  <  ( ( F `
 ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) ) ) ) )
7648, 65, 75sylc 56 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  A. k  e.  ( ZZ>=
`  ( e  x.  Z ) ) ( ( F `  (
e  x.  Z ) )  <  ( ( F `  k )  +  ( C  / 
( e  x.  Z
) ) )  /\  ( F `  k )  <  ( ( F `
 ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) ) ) )
77 fveq2 5178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  i  ->  ( F `  k )  =  ( F `  i ) )
7877oveq1d 5527 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  i  ->  (
( F `  k
)  +  ( C  /  ( e  x.  Z ) ) )  =  ( ( F `
 i )  +  ( C  /  (
e  x.  Z ) ) ) )
7978breq2d 3776 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  i  ->  (
( F `  (
e  x.  Z ) )  <  ( ( F `  k )  +  ( C  / 
( e  x.  Z
) ) )  <->  ( F `  ( e  x.  Z
) )  <  (
( F `  i
)  +  ( C  /  ( e  x.  Z ) ) ) ) )
8077breq1d 3774 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  i  ->  (
( F `  k
)  <  ( ( F `  ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) )  <->  ( F `  i )  <  (
( F `  (
e  x.  Z ) )  +  ( C  /  ( e  x.  Z ) ) ) ) )
8179, 80anbi12d 442 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  i  ->  (
( ( F `  ( e  x.  Z
) )  <  (
( F `  k
)  +  ( C  /  ( e  x.  Z ) ) )  /\  ( F `  k )  <  (
( F `  (
e  x.  Z ) )  +  ( C  /  ( e  x.  Z ) ) ) )  <->  ( ( F `
 ( e  x.  Z ) )  < 
( ( F `  i )  +  ( C  /  ( e  x.  Z ) ) )  /\  ( F `
 i )  < 
( ( F `  ( e  x.  Z
) )  +  ( C  /  ( e  x.  Z ) ) ) ) ) )
8281rspcv 2652 . . . . . . . . . . . . . . . . 17  |-  ( i  e.  ( ZZ>= `  (
e  x.  Z ) )  ->  ( A. k  e.  ( ZZ>= `  ( e  x.  Z
) ) ( ( F `  ( e  x.  Z ) )  <  ( ( F `
 k )  +  ( C  /  (
e  x.  Z ) ) )  /\  ( F `  k )  <  ( ( F `  ( e  x.  Z
) )  +  ( C  /  ( e  x.  Z ) ) ) )  ->  (
( F `  (
e  x.  Z ) )  <  ( ( F `  i )  +  ( C  / 
( e  x.  Z
) ) )  /\  ( F `  i )  <  ( ( F `
 ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) ) ) ) )
8364, 76, 82sylc 56 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  ( e  x.  Z
) )  <  (
( F `  i
)  +  ( C  /  ( e  x.  Z ) ) )  /\  ( F `  i )  <  (
( F `  (
e  x.  Z ) )  +  ( C  /  ( e  x.  Z ) ) ) ) )
8483simprd 107 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  i
)  <  ( ( F `  ( e  x.  Z ) )  +  ( C  /  (
e  x.  Z ) ) ) )
85 simpr 103 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  ->  x  e.  RR+ )
8685ad3antrrr 461 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  x  e.  RR+ )
8786rpred 8622 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  x  e.  RR )
8887rehalfcld 8171 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( x  /  2
)  e.  RR )
892ad6antr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  C  e.  RR+ )
9037ad2antrr 457 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
a  e.  NN )
91 simplrr 488 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( ( ( C  x.  2 )  /  x )  /  Z )  +  a )  <  e )
9289, 86, 47, 46, 90, 91cvg1nlemcxze 9581 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( C  /  (
e  x.  Z ) )  <  ( x  /  2 ) )
9362, 88, 92ltled 7135 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( C  /  (
e  x.  Z ) )  <_  ( x  /  2 ) )
9462, 55, 52, 93leadd2dd 7551 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  ( e  x.  Z
) )  +  ( C  /  ( e  x.  Z ) ) )  <_  ( ( F `  ( e  x.  Z ) )  +  ( x  /  2
) ) )
9551, 63, 56, 84, 94ltletrd 7420 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  i
)  <  ( ( F `  ( e  x.  Z ) )  +  ( x  /  2
) ) )
9690nnred 7927 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
a  e.  RR )
9746nnred 7927 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
e  e.  RR )
98 2rp 8588 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  2  e.  RR+
9998a1i 9 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
2  e.  RR+ )
10089, 99rpmulcld 8639 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( C  x.  2 )  e.  RR+ )
101100, 86rpdivcld 8640 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( C  x.  2 )  /  x
)  e.  RR+ )
10247nnrpd 8621 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  Z  e.  RR+ )
103101, 102rpdivcld 8640 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( ( C  x.  2 )  /  x )  /  Z
)  e.  RR+ )
104103rpred 8622 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( ( C  x.  2 )  /  x )  /  Z
)  e.  RR )
105104, 96readdcld 7055 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( ( ( C  x.  2 )  /  x )  /  Z )  +  a )  e.  RR )
10696, 103ltaddrp2d 8657 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
a  <  ( (
( ( C  x.  2 )  /  x
)  /  Z )  +  a ) )
10796, 105, 97, 106, 91lttrd 7140 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
a  <  e )
10896, 97, 107ltled 7135 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
a  <_  e )
10990nnzd 8359 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
a  e.  ZZ )
11046nnzd 8359 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
e  e.  ZZ )
111 eluz 8486 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( a  e.  ZZ  /\  e  e.  ZZ )  ->  ( e  e.  (
ZZ>= `  a )  <->  a  <_  e ) )
112109, 110, 111syl2anc 391 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( e  e.  (
ZZ>= `  a )  <->  a  <_  e ) )
113108, 112mpbird 156 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
e  e.  ( ZZ>= `  a ) )
114 simprr 484 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w ) ( ( G `  b )  <  ( y  +  c )  /\  y  <  ( ( G `  b )  +  c ) ) )  /\  x  e.  RR+ )  /\  ( a  e.  NN  /\ 
A. b  e.  (
ZZ>= `  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) ) )  ->  A. b  e.  ( ZZ>= `  a )
( ( G `  b )  <  (
y  +  ( x  /  2 ) )  /\  y  <  (
( G `  b
)  +  ( x  /  2 ) ) ) )
115114ad2antrr 457 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  A. b  e.  ( ZZ>=
`  a ) ( ( G `  b
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 b )  +  ( x  /  2
) ) ) )
116 fveq2 5178 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  e  ->  ( G `  b )  =  ( G `  e ) )
117116breq1d 3774 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  e  ->  (
( G `  b
)  <  ( y  +  ( x  / 
2 ) )  <->  ( G `  e )  <  (
y  +  ( x  /  2 ) ) ) )
118116oveq1d 5527 . . . . . . . . . . . . . . . . . . . . 21  |-  ( b  =  e  ->  (
( G `  b
)  +  ( x  /  2 ) )  =  ( ( G `
 e )  +  ( x  /  2
) ) )
119118breq2d 3776 . . . . . . . . . . . . . . . . . . . 20  |-  ( b  =  e  ->  (
y  <  ( ( G `  b )  +  ( x  / 
2 ) )  <->  y  <  ( ( G `  e
)  +  ( x  /  2 ) ) ) )
120117, 119anbi12d 442 . . . . . . . . . . . . . . . . . . 19  |-  ( b  =  e  ->  (
( ( G `  b )  <  (
y  +  ( x  /  2 ) )  /\  y  <  (
( G `  b
)  +  ( x  /  2 ) ) )  <->  ( ( G `
 e )  < 
( y  +  ( x  /  2 ) )  /\  y  < 
( ( G `  e )  +  ( x  /  2 ) ) ) ) )
121120rspcv 2652 . . . . . . . . . . . . . . . . . 18  |-  ( e  e.  ( ZZ>= `  a
)  ->  ( A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) )  ->  (
( G `  e
)  <  ( y  +  ( x  / 
2 ) )  /\  y  <  ( ( G `
 e )  +  ( x  /  2
) ) ) ) )
122113, 115, 121sylc 56 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( G `  e )  <  (
y  +  ( x  /  2 ) )  /\  y  <  (
( G `  e
)  +  ( x  /  2 ) ) ) )
123 oveq1 5519 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  e  ->  (
j  x.  Z )  =  ( e  x.  Z ) )
124123fveq2d 5182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  e  ->  ( F `  ( j  x.  Z ) )  =  ( F `  (
e  x.  Z ) ) )
125124, 4fvmptg 5248 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( e  e.  NN  /\  ( F `  ( e  x.  Z ) )  e.  RR )  -> 
( G `  e
)  =  ( F `
 ( e  x.  Z ) ) )
12646, 52, 125syl2anc 391 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( G `  e
)  =  ( F `
 ( e  x.  Z ) ) )
127126breq1d 3774 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( G `  e )  <  (
y  +  ( x  /  2 ) )  <-> 
( F `  (
e  x.  Z ) )  <  ( y  +  ( x  / 
2 ) ) ) )
128126oveq1d 5527 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( G `  e )  +  ( x  /  2 ) )  =  ( ( F `  ( e  x.  Z ) )  +  ( x  / 
2 ) ) )
129128breq2d 3776 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( y  <  (
( G `  e
)  +  ( x  /  2 ) )  <-> 
y  <  ( ( F `  ( e  x.  Z ) )  +  ( x  /  2
) ) ) )
130127, 129anbi12d 442 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( ( G `
 e )  < 
( y  +  ( x  /  2 ) )  /\  y  < 
( ( G `  e )  +  ( x  /  2 ) ) )  <->  ( ( F `  ( e  x.  Z ) )  < 
( y  +  ( x  /  2 ) )  /\  y  < 
( ( F `  ( e  x.  Z
) )  +  ( x  /  2 ) ) ) ) )
131122, 130mpbid 135 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  ( e  x.  Z
) )  <  (
y  +  ( x  /  2 ) )  /\  y  <  (
( F `  (
e  x.  Z ) )  +  ( x  /  2 ) ) ) )
132131simpld 105 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  (
e  x.  Z ) )  <  ( y  +  ( x  / 
2 ) ) )
13352, 59, 55, 132ltadd1dd 7547 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  ( e  x.  Z
) )  +  ( x  /  2 ) )  <  ( ( y  +  ( x  /  2 ) )  +  ( x  / 
2 ) ) )
13451, 56, 60, 95, 133lttrd 7140 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  i
)  <  ( (
y  +  ( x  /  2 ) )  +  ( x  / 
2 ) ) )
13558recnd 7054 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
y  e.  CC )
13655recnd 7054 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( x  /  2
)  e.  CC )
137135, 136, 136addassd 7049 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( y  +  ( x  /  2
) )  +  ( x  /  2 ) )  =  ( y  +  ( ( x  /  2 )  +  ( x  /  2
) ) ) )
138134, 137breqtrd 3788 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  i
)  <  ( y  +  ( ( x  /  2 )  +  ( x  /  2
) ) ) )
13953rpcnd 8624 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  ->  x  e.  CC )
1401392halvesd 8170 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( x  / 
2 )  +  ( x  /  2 ) )  =  x )
141140oveq2d 5528 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( y  +  ( ( x  /  2
)  +  ( x  /  2 ) ) )  =  ( y  +  x ) )
142138, 141breqtrd 3788 . . . . . . . . . . 11  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( F `  i
)  <  ( y  +  x ) )
14351, 55readdcld 7055 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( F `  i )  +  ( x  /  2 ) )  e.  RR )
144143, 55readdcld 7055 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (
a  e.  NN  /\  A. b  e.  ( ZZ>= `  a ) ( ( G `  b )  <  ( y  +  ( x  /  2
) )  /\  y  <  ( ( G `  b )  +  ( x  /  2 ) ) ) ) )  /\  ( e  e.  NN  /\  ( ( ( ( C  x.  2 )  /  x
)  /  Z )  +  a )  < 
e ) )  /\  i  e.  ( ZZ>= `  ( e  x.  Z
) ) )  -> 
( ( ( F `
 i )  +  ( x  /  2
) )  +  ( x  /  2 ) )  e.  RR )
145131simprd 107 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( ( ph  /\  y  e.  RR )  /\  A. c  e.  RR+  E. w  e.  NN  A. b  e.  ( ZZ>= `  w )
( ( G `  b )  <  (
y  +  c )  /\  y  <  (
( G `  b
)  +  c ) ) )  /\  x  e.  RR+ )  /\  (