Metamath Proof Explorer

Theorem pntibnd

Description: Lemma for pnt . Establish smallness of R on an interval. Lemma 10.6.2 in Shapiro, p. 436. (Contributed by Mario Carneiro, 10-Apr-2016)

Ref Expression
Hypothesis pntlem1.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
Assertion pntibnd 
|- E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e )

Proof

Step Hyp Ref Expression
1 pntlem1.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 1 pntrmax 
 |-  E. d e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d
3 1 pntpbnd 
 |-  E. b e. RR+ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f )
4 reeanv 
 |-  ( E. d e. RR+ E. b e. RR+ ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) <-> ( E. d e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ E. b e. RR+ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) )
5 2rp 
 |-  2 e. RR+
6 rpmulcl 
 |-  ( ( 2 e. RR+ /\ b e. RR+ ) -> ( 2 x. b ) e. RR+ )
7 5 6 mpan 
 |-  ( b e. RR+ -> ( 2 x. b ) e. RR+ )
8 2re 
 |-  2 e. RR
9 1lt2 
 |-  1 < 2
10 rplogcl 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
11 8 9 10 mp2an 
 |-  ( log ` 2 ) e. RR+
12 rpaddcl 
 |-  ( ( ( 2 x. b ) e. RR+ /\ ( log ` 2 ) e. RR+ ) -> ( ( 2 x. b ) + ( log ` 2 ) ) e. RR+ )
13 7 11 12 sylancl 
 |-  ( b e. RR+ -> ( ( 2 x. b ) + ( log ` 2 ) ) e. RR+ )
14 13 ad2antlr 
 |-  ( ( ( d e. RR+ /\ b e. RR+ ) /\ ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) ) -> ( ( 2 x. b ) + ( log ` 2 ) ) e. RR+ )
15 id 
 |-  ( d e. RR+ -> d e. RR+ )
16 eqid 
 |-  ( ( 1 / 4 ) / ( d + 3 ) ) = ( ( 1 / 4 ) / ( d + 3 ) )
17 1 15 16 pntibndlem1 
 |-  ( d e. RR+ -> ( ( 1 / 4 ) / ( d + 3 ) ) e. ( 0 (,) 1 ) )
18 17 ad2antrr 
 |-  ( ( ( d e. RR+ /\ b e. RR+ ) /\ ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) ) -> ( ( 1 / 4 ) / ( d + 3 ) ) e. ( 0 (,) 1 ) )
19 elioore 
 |-  ( e e. ( 0 (,) 1 ) -> e e. RR )
20 eliooord 
 |-  ( e e. ( 0 (,) 1 ) -> ( 0 < e /\ e < 1 ) )
21 20 simpld 
 |-  ( e e. ( 0 (,) 1 ) -> 0 < e )
22 19 21 elrpd 
 |-  ( e e. ( 0 (,) 1 ) -> e e. RR+ )
23 22 rphalfcld 
 |-  ( e e. ( 0 (,) 1 ) -> ( e / 2 ) e. RR+ )
24 23 rpred 
 |-  ( e e. ( 0 (,) 1 ) -> ( e / 2 ) e. RR )
25 23 rpgt0d 
 |-  ( e e. ( 0 (,) 1 ) -> 0 < ( e / 2 ) )
26 1red 
 |-  ( e e. ( 0 (,) 1 ) -> 1 e. RR )
27 rphalflt 
 |-  ( e e. RR+ -> ( e / 2 ) < e )
28 22 27 syl 
 |-  ( e e. ( 0 (,) 1 ) -> ( e / 2 ) < e )
29 20 simprd 
 |-  ( e e. ( 0 (,) 1 ) -> e < 1 )
30 24 19 26 28 29 lttrd 
 |-  ( e e. ( 0 (,) 1 ) -> ( e / 2 ) < 1 )
31 0xr 
 |-  0 e. RR*
32 1xr 
 |-  1 e. RR*
33 elioo2 
 |-  ( ( 0 e. RR* /\ 1 e. RR* ) -> ( ( e / 2 ) e. ( 0 (,) 1 ) <-> ( ( e / 2 ) e. RR /\ 0 < ( e / 2 ) /\ ( e / 2 ) < 1 ) ) )
34 31 32 33 mp2an 
 |-  ( ( e / 2 ) e. ( 0 (,) 1 ) <-> ( ( e / 2 ) e. RR /\ 0 < ( e / 2 ) /\ ( e / 2 ) < 1 ) )
35 24 25 30 34 syl3anbrc 
 |-  ( e e. ( 0 (,) 1 ) -> ( e / 2 ) e. ( 0 (,) 1 ) )
36 35 adantl 
 |-  ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( e / 2 ) e. ( 0 (,) 1 ) )
37 oveq2 
 |-  ( f = ( e / 2 ) -> ( b / f ) = ( b / ( e / 2 ) ) )
38 37 fveq2d 
 |-  ( f = ( e / 2 ) -> ( exp ` ( b / f ) ) = ( exp ` ( b / ( e / 2 ) ) ) )
39 38 oveq1d 
 |-  ( f = ( e / 2 ) -> ( ( exp ` ( b / f ) ) [,) +oo ) = ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) )
40 breq2 
 |-  ( f = ( e / 2 ) -> ( ( abs ` ( ( R ` n ) / n ) ) <_ f <-> ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) )
41 40 anbi2d 
 |-  ( f = ( e / 2 ) -> ( ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) <-> ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
42 41 rexbidv 
 |-  ( f = ( e / 2 ) -> ( E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) <-> E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
43 42 ralbidv 
 |-  ( f = ( e / 2 ) -> ( A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) <-> A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
44 39 43 raleqbidv 
 |-  ( f = ( e / 2 ) -> ( A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) <-> A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
45 44 rexbidv 
 |-  ( f = ( e / 2 ) -> ( E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) <-> E. g e. RR+ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
46 45 rspcv 
 |-  ( ( e / 2 ) e. ( 0 (,) 1 ) -> ( A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) -> E. g e. RR+ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
47 36 46 syl 
 |-  ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) -> E. g e. RR+ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) )
48 simp-4l 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> d e. RR+ )
49 simpllr 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d )
50 simplr 
 |-  ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) -> b e. RR+ )
51 50 ad2antrr 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> b e. RR+ )
52 eqid 
 |-  ( exp ` ( b / ( e / 2 ) ) ) = ( exp ` ( b / ( e / 2 ) ) )
53 eqid 
 |-  ( ( 2 x. b ) + ( log ` 2 ) ) = ( ( 2 x. b ) + ( log ` 2 ) )
54 simplr 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> e e. ( 0 (,) 1 ) )
55 simprl 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> g e. RR+ )
56 simprr 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) )
57 1 48 16 49 51 52 53 54 55 56 pntibndlem3 
 |-  ( ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) /\ ( g e. RR+ /\ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
58 57 rexlimdvaa 
 |-  ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( E. g e. RR+ A. m e. ( ( exp ` ( b / ( e / 2 ) ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ ( e / 2 ) ) -> E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
59 47 58 syld 
 |-  ( ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) /\ e e. ( 0 (,) 1 ) ) -> ( A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) -> E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
60 59 ralrimdva 
 |-  ( ( ( d e. RR+ /\ b e. RR+ ) /\ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d ) -> ( A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
61 60 impr 
 |-  ( ( ( d e. RR+ /\ b e. RR+ ) /\ ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) ) -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
62 fvoveq1 
 |-  ( c = ( ( 2 x. b ) + ( log ` 2 ) ) -> ( exp ` ( c / e ) ) = ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) )
63 62 oveq1d 
 |-  ( c = ( ( 2 x. b ) + ( log ` 2 ) ) -> ( ( exp ` ( c / e ) ) [,) +oo ) = ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) )
64 63 raleqdv 
 |-  ( c = ( ( 2 x. b ) + ( log ` 2 ) ) -> ( A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
65 64 rexbidv 
 |-  ( c = ( ( 2 x. b ) + ( log ` 2 ) ) -> ( E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
66 65 ralbidv 
 |-  ( c = ( ( 2 x. b ) + ( log ` 2 ) ) -> ( A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
67 oveq1 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( l x. e ) = ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) )
68 67 oveq2d 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( 1 + ( l x. e ) ) = ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) )
69 68 oveq1d 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( ( 1 + ( l x. e ) ) x. z ) = ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) )
70 69 breq1d 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) <-> ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) )
71 70 anbi2d 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) <-> ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) ) )
72 69 oveq2d 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) = ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) )
73 72 raleqdv 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e <-> A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
74 71 73 anbi12d 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
75 74 rexbidv 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
76 75 ralbidv 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
77 76 rexralbidv 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
78 77 ralbidv 
 |-  ( l = ( ( 1 / 4 ) / ( d + 3 ) ) -> ( A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) <-> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
79 66 78 rspc2ev 
 |-  ( ( ( ( 2 x. b ) + ( log ` 2 ) ) e. RR+ /\ ( ( 1 / 4 ) / ( d + 3 ) ) e. ( 0 (,) 1 ) /\ A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( ( ( 2 x. b ) + ( log ` 2 ) ) / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( ( ( 1 / 4 ) / ( d + 3 ) ) x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) -> E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
80 14 18 61 79 syl3anc 
 |-  ( ( ( d e. RR+ /\ b e. RR+ ) /\ ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) ) -> E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
81 80 ex 
 |-  ( ( d e. RR+ /\ b e. RR+ ) -> ( ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) -> E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) ) )
82 81 rexlimivv 
 |-  ( E. d e. RR+ E. b e. RR+ ( A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) -> E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
83 4 82 sylbir 
 |-  ( ( E. d e. RR+ A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ d /\ E. b e. RR+ A. f e. ( 0 (,) 1 ) E. g e. RR+ A. m e. ( ( exp ` ( b / f ) ) [,) +oo ) A. v e. ( g (,) +oo ) E. n e. NN ( ( v < n /\ n <_ ( m x. v ) ) /\ ( abs ` ( ( R ` n ) / n ) ) <_ f ) ) -> E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e ) )
84 2 3 83 mp2an 
 |-  E. c e. RR+ E. l e. ( 0 (,) 1 ) A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( c / e ) ) [,) +oo ) A. y e. ( x (,) +oo ) E. z e. RR+ ( ( y < z /\ ( ( 1 + ( l x. e ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( l x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e )