Metamath Proof Explorer

Theorem pntleme

Description: Lemma for pnt . Package up pntlemo in quantifiers. (Contributed by Mario Carneiro, 14-Apr-2016)

Ref Expression
Hypotheses pntlem1.r 
|- R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
pntlem1.a 
|- ( ph -> A e. RR+ )
pntlem1.b 
|- ( ph -> B e. RR+ )
pntlem1.l 
|- ( ph -> L e. ( 0 (,) 1 ) )
pntlem1.d 
|- D = ( A + 1 )
pntlem1.f 
|- F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
pntlem1.u 
|- ( ph -> U e. RR+ )
pntlem1.u2 
|- ( ph -> U <_ A )
pntlem1.e 
|- E = ( U / D )
pntlem1.k 
|- K = ( exp ` ( B / E ) )
pntlem1.y 
|- ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
pntlem1.x 
|- ( ph -> ( X e. RR+ /\ Y < X ) )
pntlem1.c 
|- ( ph -> C e. RR+ )
pntlem1.w 
|- W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
pntleme.U 
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
pntleme.K 
|- ( ph -> 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 ) )
pntleme.C 
|- ( ph -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )
Assertion pntleme 
|- ( 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 pntlem1.r 
 |-  R = ( a e. RR+ |-> ( ( psi ` a ) - a ) )
2 pntlem1.a 
 |-  ( ph -> A e. RR+ )
3 pntlem1.b 
 |-  ( ph -> B e. RR+ )
4 pntlem1.l 
 |-  ( ph -> L e. ( 0 (,) 1 ) )
5 pntlem1.d 
 |-  D = ( A + 1 )
6 pntlem1.f 
 |-  F = ( ( 1 - ( 1 / D ) ) x. ( ( L / ( ; 3 2 x. B ) ) / ( D ^ 2 ) ) )
7 pntlem1.u 
 |-  ( ph -> U e. RR+ )
8 pntlem1.u2 
 |-  ( ph -> U <_ A )
9 pntlem1.e 
 |-  E = ( U / D )
10 pntlem1.k 
 |-  K = ( exp ` ( B / E ) )
11 pntlem1.y 
 |-  ( ph -> ( Y e. RR+ /\ 1 <_ Y ) )
12 pntlem1.x 
 |-  ( ph -> ( X e. RR+ /\ Y < X ) )
13 pntlem1.c 
 |-  ( ph -> C e. RR+ )
14 pntlem1.w 
 |-  W = ( ( ( Y + ( 4 / ( L x. E ) ) ) ^ 2 ) + ( ( ( X x. ( K ^ 2 ) ) ^ 4 ) + ( exp ` ( ( ( ; 3 2 x. B ) / ( ( U - E ) x. ( L x. ( E ^ 2 ) ) ) ) x. ( ( U x. 3 ) + C ) ) ) ) )
15 pntleme.U 
 |-  ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
16 pntleme.K 
 |-  ( ph -> 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 ) )
17 pntleme.C 
 |-  ( ph -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )
18 1 2 3 4 5 6 7 8 9 10 11 12 13 14 pntlema 
 |-  ( ph -> W e. RR+ )
19 2 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> A e. RR+ )
20 3 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> B e. RR+ )
21 4 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> L e. ( 0 (,) 1 ) )
22 7 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> U e. RR+ )
23 8 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> U <_ A )
24 11 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> ( Y e. RR+ /\ 1 <_ Y ) )
25 12 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> ( X e. RR+ /\ Y < X ) )
26 13 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> C e. RR+ )
27 simpr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> v e. ( W [,) +oo ) )
28 eqid 
 |-  ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 ) = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
29 eqid 
 |-  ( |_ ` ( ( ( log ` v ) / ( log ` K ) ) / 2 ) ) = ( |_ ` ( ( ( log ` v ) / ( log ` K ) ) / 2 ) )
30 15 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
31 oveq1 
 |-  ( k = K -> ( k x. y ) = ( K x. y ) )
32 31 breq2d 
 |-  ( k = K -> ( ( ( 1 + ( L x. E ) ) x. z ) < ( k x. y ) <-> ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) )
33 32 anbi2d 
 |-  ( k = K -> ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( k x. y ) ) <-> ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) ) )
34 33 anbi1d 
 |-  ( k = K -> ( ( ( 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 ) ) )
35 34 rexbidv 
 |-  ( k = K -> ( 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 ) ) )
36 35 ralbidv 
 |-  ( k = K -> ( 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 ) ) )
37 1 2 3 4 5 6 7 8 9 10 pntlemc 
 |-  ( ph -> ( E e. RR+ /\ K e. RR+ /\ ( E e. ( 0 (,) 1 ) /\ 1 < K /\ ( U - E ) e. RR+ ) ) )
38 37 simp2d 
 |-  ( ph -> K e. RR+ )
39 38 rpxrd 
 |-  ( ph -> K e. RR* )
40 pnfxr 
 |-  +oo e. RR*
41 40 a1i 
 |-  ( ph -> +oo e. RR* )
42 38 rpred 
 |-  ( ph -> K e. RR )
43 42 ltpnfd 
 |-  ( ph -> K < +oo )
44 lbico1 
 |-  ( ( K e. RR* /\ +oo e. RR* /\ K < +oo ) -> K e. ( K [,) +oo ) )
45 39 41 43 44 syl3anc 
 |-  ( ph -> K e. ( K [,) +oo ) )
46 36 16 45 rspcdva 
 |-  ( ph -> 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 ) )
47 46 adantr 
 |-  ( ( ph /\ v e. ( W [,) +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 ) )
48 17 adantr 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> A. z e. ( 1 (,) +oo ) ( ( ( ( abs ` ( R ` z ) ) x. ( log ` z ) ) - ( ( 2 / ( log ` z ) ) x. sum_ i e. ( 1 ... ( |_ ` ( z / Y ) ) ) ( ( abs ` ( R ` ( z / i ) ) ) x. ( log ` i ) ) ) ) / z ) <_ C )
49 1 19 20 21 5 6 22 23 9 10 24 25 26 14 27 28 29 30 47 48 pntlemo 
 |-  ( ( ph /\ v e. ( W [,) +oo ) ) -> ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
50 49 ralrimiva 
 |-  ( ph -> A. v e. ( W [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
51 oveq1 
 |-  ( w = W -> ( w [,) +oo ) = ( W [,) +oo ) )
52 51 raleqdv 
 |-  ( w = W -> ( A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) <-> A. v e. ( W [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) ) )
53 52 rspcev 
 |-  ( ( W e. RR+ /\ A. v e. ( W [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) ) -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )
54 18 50 53 syl2anc 
 |-  ( ph -> E. w e. RR+ A. v e. ( w [,) +oo ) ( abs ` ( ( R ` v ) / v ) ) <_ ( U - ( F x. ( U ^ 3 ) ) ) )