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
|
syl5bir |
|- ( 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 ) ) ) ) |