Metamath Proof Explorer

Theorem pntlemp

Description: Lemma for pnt . Wrapping up more quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypotheses pntlem3.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem3.a 
|- ( ph -> A e. RR+ )
pntlem3.A 
|- ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
pntlemp.b 
|- ( ph -> B e. RR+ )
pntlemp.l 
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlemp.d 
|- D = ( A + 1 )
pntlemp.f 
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlemp.K 
|- ( ph -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / 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 ) )
pntlemp.u 
|- ( ph -> U e. RR+ )
pntlemp.u2 
|- ( ph -> U <_ A )
pntlemp.e 
|- E = ( U / D )
pntlemp.k 
|- K = ( exp ` ( B / E ) )
pntlemp.y 
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlemp.U 
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
Assertion pntlemp 
|- ( ph -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 pntlem3.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem3.a 
 |-  ( ph -> A e. RR+ )
3 pntlem3.A 
 |-  ( ph -> A. x e. RR+ ( abs ` ( ( R ` x ) / x ) ) <_ A )
4 pntlemp.b 
 |-  ( ph -> B e. RR+ )
5 pntlemp.l 
 |-  ( ph -> L e. ( 0 (,) 1 ) )
6 pntlemp.d 
 |-  D = ( A + 1 )
7 pntlemp.f 
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
8 pntlemp.K 
 |-  ( ph -> A. e e. ( 0 (,) 1 ) E. x e. RR+ A. k e. ( ( exp ` ( B / 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 ) )
9 pntlemp.u 
 |-  ( ph -> U e. RR+ )
10 pntlemp.u2 
 |-  ( ph -> U <_ A )
11 pntlemp.e 
 |-  E = ( U / D )
12 pntlemp.k 
 |-  K = ( exp ` ( B / E ) )
13 pntlemp.y 
 |-  ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
14 pntlemp.U 
 |-  ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
15 oveq2 
 |-  ( e = E -> ( B / e ) = ( B / E ) )
16 15 fveq2d 
 |-  ( e = E -> ( exp ` ( B / e ) ) = ( exp ` ( B / E ) ) )
17 16 12 eqtr4di 
 |-  ( e = E -> ( exp ` ( B / e ) ) = K )
18 17 oveq1d 
 |-  ( e = E -> ( ( exp ` ( B / e ) ) [,) +oo ) = ( K [,) +oo ) )
19 oveq2 
 |-  ( e = E -> ( L x. e ) = ( L x. E ) )
20 19 oveq2d 
 |-  ( e = E -> ( 1 + ( L x. e ) ) = ( 1 + ( L x. E ) ) )
21 20 oveq1d 
 |-  ( e = E -> ( ( 1 + ( L x. e ) ) x. z ) = ( ( 1 + ( L x. E ) ) x. z ) )
22 21 breq1d 
 |-  ( e = E -> ( ( ( 1 + ( L x. e ) ) x. z ) < ( k x. y ) <-> ( ( 1 + ( L x. E ) ) x. z ) < ( k x. y ) ) )
23 22 anbi2d 
 |-  ( e = E -> ( ( y < z /\ ( ( 1 + ( L x. e ) ) x. z ) < ( k x. y ) ) <-> ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( k x. y ) ) ) )
24 21 oveq2d 
 |-  ( e = E -> ( z [,] ( ( 1 + ( L x. e ) ) x. z ) ) = ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) )
25 breq2 
 |-  ( e = E -> ( ( abs ` ( ( R ` u ) / u ) ) <_ e <-> ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
26 24 25 raleqbidv 
 |-  ( e = E -> ( A. u e. ( z [,] ( ( 1 + ( L x. e ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ e <-> A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
27 23 26 anbi12d 
 |-  ( e = E -> ( ( ( 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 + ( L x. E ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
28 27 rexbidv 
 |-  ( e = E -> ( 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 + ( L x. E ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
29 28 ralbidv 
 |-  ( e = E -> ( 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 + ( L x. E ) ) x. z ) < ( k x. y ) ) /\ A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
30 18 29 raleqbidv 
 |-  ( e = E -> ( A. k e. ( ( exp ` ( B / 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. ( K [,) +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 ) ) )
31 30 rexbidv 
 |-  ( e = E -> ( E. x e. RR+ A. k e. ( ( exp ` ( B / 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. ( K [,) +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 ) ) )
32 oveq1 
 |-  ( x = t -> ( x (,) +oo ) = ( t (,) +oo ) )
33 32 raleqdv 
 |-  ( x = t -> ( 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. ( t (,) +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 ) ) )
34 33 ralbidv 
 |-  ( x = t -> ( A. k e. ( K [,) +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. ( K [,) +oo ) A. y e. ( t (,) +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 ) ) )
35 34 cbvrexvw 
 |-  ( E. x e. RR+ A. k e. ( K [,) +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. t e. RR+ A. k e. ( K [,) +oo ) A. y e. ( t (,) +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 ) )
36 31 35 bitrdi 
 |-  ( e = E -> ( E. x e. RR+ A. k e. ( ( exp ` ( B / 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. t e. RR+ A. k e. ( K [,) +oo ) A. y e. ( t (,) +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 ) ) )
37 1 2 4 5 6 7 9 10 11 12 pntlemc 
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
38 37 simp3d 
 |-  ( ph -> ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) )
39 38 simp1d 
 |-  ( ph -> E e. ( 0 (,) 1 ) )
40 36 8 39 rspcdva 
 |-  ( ph -> E. t e. RR+ A. k e. ( K [,) +oo ) A. y e. ( t (,) +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 ) )
41 13 simpld 
 |-  ( ph -> Y e. RR+ )
42 41 rpred 
 |-  ( ph -> Y e. RR )
43 13 simprd 
 |-  ( ph -> 1 <_ Y )
44 1 pntrlog2bnd 
 |-  ( ( Y e. RR /\ 1 <_ Y ) -> E. c e. RR+ A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c )
45 42 43 44 syl2anc 
 |-  ( ph -> E. c e. RR+ A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c )
46 reeanv 
 |-  ( E. t e. RR+ E. c e. RR+ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) <-> ( E. t e. RR+ A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. c e. RR+ A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) )
47 2 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> A e. RR+ )
48 4 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> B e. RR+ )
49 5 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> L e. ( 0 (,) 1 ) )
50 9 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> U e. RR+ )
51 10 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> U <_ A )
52 13 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> ( Y e. RR+ /\ 1 <_ Y ) )
53 simpl 
 |-  ( ( t e. RR+ /\ c e. RR+ ) -> t e. RR+ )
54 rpaddcl 
 |-  ( ( Y e. RR+ /\ t e. RR+ ) -> ( Y + t ) e. RR+ )
55 41 53 54 syl2an 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> ( Y + t ) e. RR+ )
56 ltaddrp 
 |-  ( ( Y e. RR /\ t e. RR+ ) -> Y < ( Y + t ) )
57 42 53 56 syl2an 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> Y < ( Y + t ) )
58 55 57 jca 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> ( ( Y + t ) e. RR+ /\ Y < ( Y + t ) ) )
59 58 adantrr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> ( ( Y + t ) e. RR+ /\ Y < ( Y + t ) ) )
60 simprlr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> c e. RR+ )
61 eqid 
 |-  ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( ( Y + t ) x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + c ) ) ) ) ) = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( ( Y + t ) x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + c ) ) ) ) )
62 14 adantr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
63 rpxr 
 |-  ( t e. RR+ -> t e. RR* )
64 63 ad2antrl 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> t e. RR* )
65 rpre 
 |-  ( t e. RR+ -> t e. RR )
66 65 ad2antrl 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> t e. RR )
67 55 rpred 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> ( Y + t ) e. RR )
68 41 adantr 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> Y e. RR+ )
69 66 68 ltaddrp2d 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> t < ( Y + t ) )
70 66 67 69 ltled 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> t <_ ( Y + t ) )
71 iooss1 
 |-  ( ( t e. RR* /\ t <_ ( Y + t ) ) -> ( ( Y + t ) (,) +oo ) C_ ( t (,) +oo ) )
72 64 70 71 syl2anc 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> ( ( Y + t ) (,) +oo ) C_ ( t (,) +oo ) )
73 72 adantrr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> ( ( Y + t ) (,) +oo ) C_ ( t (,) +oo ) )
74 simprrl 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> A. k e. ( K [,) +oo ) A. y e. ( t (,) +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 ) )
75 ssralv 
 |-  ( ( ( Y + t ) (,) +oo ) C_ ( t (,) +oo ) -> ( A. y e. ( t (,) +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. ( ( Y + t ) (,) +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 ) ) )
76 75 ralimdv 
 |-  ( ( ( Y + t ) (,) +oo ) C_ ( t (,) +oo ) -> ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. ( K [,) +oo ) A. y e. ( ( Y + t ) (,) +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 ) ) )
77 73 74 76 sylc 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> A. k e. ( K [,) +oo ) A. y e. ( ( Y + t ) (,) +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 ) )
78 simprrr 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c )
79 1 47 48 49 6 7 50 51 11 12 52 59 60 61 62 77 78 pntleme 
 |-  ( ( ph /\ ( ( t e. RR+ /\ c e. RR+ ) /\ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) ) ) -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
80 79 expr 
 |-  ( ( ph /\ ( t e. RR+ /\ c e. RR+ ) ) -> ( ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) ) )
81 80 rexlimdvva 
 |-  ( ph -> ( E. t e. RR+ E. c e. RR+ ( A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) ) )
82 46 81 biimtrrid 
 |-  ( ph -> ( ( E. t e. RR+ A. k e. ( K [,) +oo ) A. y e. ( t (,) +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. c e. RR+ A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ n e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / n ) ) ) x. ( log ` n ) ) ) ) / z ) <_ c ) -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) ) )
83 40 45 82 mp2and 
 |-  ( ph -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )