Metamath Proof Explorer

Theorem pntlemi

Description: Lemma for pnt . Eliminate some assumptions from pntlemj . (Contributed by Mario Carneiro, 13-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 ) ) ) ) )
pntlem1.z 
|- ( ph -> Z e. ( W [,) +oo ) )
pntlem1.m 
|- M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
pntlem1.n 
|- N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
pntlem1.U 
|- ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
pntlem1.K 
|- ( 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 ) )
pntlem1.o 
|- O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )
Assertion pntlemi 
|- ( ( ph /\ J e. ( M ..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )

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 pntlem1.z 
 |-  ( ph -> Z e. ( W [,) +oo ) )
16 pntlem1.m 
 |-  M = ( ( |_ ` ( ( log ` X ) / ( log ` K ) ) ) + 1 )
17 pntlem1.n 
 |-  N = ( |_ ` ( ( ( log ` Z ) / ( log ` K ) ) / 2 ) )
18 pntlem1.U 
 |-  ( ph -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
19 pntlem1.K 
 |-  ( 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 ) )
20 pntlem1.o 
 |-  O = ( ( ( |_ ` ( Z / ( K ^ ( J + 1 ) ) ) ) + 1 ) ... ( |_ ` ( Z / ( K ^ J ) ) ) )
21 breq2 
 |-  ( z = x -> ( y < z <-> y < x ) )
22 oveq2 
 |-  ( z = x -> ( ( 1 + ( L x. E ) ) x. z ) = ( ( 1 + ( L x. E ) ) x. x ) )
23 22 breq1d 
 |-  ( z = x -> ( ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) <-> ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) )
24 21 23 anbi12d 
 |-  ( z = x -> ( ( y < z /\ ( ( 1 + ( L x. E ) ) x. z ) < ( K x. y ) ) <-> ( y < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) ) )
25 id 
 |-  ( z = x -> z = x )
26 25 22 oveq12d 
 |-  ( z = x -> ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) = ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) )
27 26 raleqdv 
 |-  ( z = x -> ( A. u e. ( z [,] ( ( 1 + ( L x. E ) ) x. z ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E <-> A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
28 24 27 anbi12d 
 |-  ( z = x -> ( ( ( 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 < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
29 28 cbvrexvw 
 |-  ( 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+ ( ( y < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
30 breq1 
 |-  ( y = ( K ^ J ) -> ( y < x <-> ( K ^ J ) < x ) )
31 oveq2 
 |-  ( y = ( K ^ J ) -> ( K x. y ) = ( K x. ( K ^ J ) ) )
32 31 breq2d 
 |-  ( y = ( K ^ J ) -> ( ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) <-> ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) )
33 30 32 anbi12d 
 |-  ( y = ( K ^ J ) -> ( ( y < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) <-> ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) ) )
34 33 anbi1d 
 |-  ( y = ( K ^ J ) -> ( ( ( y < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) <-> ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
35 34 rexbidv 
 |-  ( y = ( K ^ J ) -> ( E. x e. RR+ ( ( y < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. y ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) <-> E. x e. RR+ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
36 29 35 bitrid 
 |-  ( y = ( K ^ J ) -> ( 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+ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) )
37 19 adantr 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> 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 ) )
38 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+ ) ) )
39 38 simp2d 
 |-  ( ph -> K e. RR+ )
40 elfzoelz 
 |-  ( J e. ( M ..^ N ) -> J e. ZZ )
41 rpexpcl 
 |-  ( ( K e. RR+ /\ J e. ZZ ) -> ( K ^ J ) e. RR+ )
42 39 40 41 syl2an 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> ( K ^ J ) e. RR+ )
43 42 rpred 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> ( K ^ J ) e. RR )
44 elfzofz 
 |-  ( J e. ( M ..^ N ) -> J e. ( M ... N ) )
45 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 pntlemh 
 |-  ( ( ph /\ J e. ( M ... N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) )
46 44 45 sylan2 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> ( X < ( K ^ J ) /\ ( K ^ J ) <_ ( sqrt ` Z ) ) )
47 46 simpld 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> X < ( K ^ J ) )
48 12 simpld 
 |-  ( ph -> X e. RR+ )
49 48 adantr 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> X e. RR+ )
50 rpxr 
 |-  ( X e. RR+ -> X e. RR* )
51 elioopnf 
 |-  ( X e. RR* -> ( ( K ^ J ) e. ( X (,) +oo ) <-> ( ( K ^ J ) e. RR /\ X < ( K ^ J ) ) ) )
52 49 50 51 3syl 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> ( ( K ^ J ) e. ( X (,) +oo ) <-> ( ( K ^ J ) e. RR /\ X < ( K ^ J ) ) ) )
53 43 47 52 mpbir2and 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> ( K ^ J ) e. ( X (,) +oo ) )
54 36 37 53 rspcdva 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> E. x e. RR+ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
55 2 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> A e. RR+ )
56 3 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> B e. RR+ )
57 4 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> L e. ( 0 (,) 1 ) )
58 7 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> U e. RR+ )
59 8 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> U <_ A )
60 11 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> ( Y e. RR+ /\ 1 <_ Y ) )
61 12 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> ( X e. RR+ /\ Y < X ) )
62 13 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> C e. RR+ )
63 15 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> Z e. ( W [,) +oo ) )
64 18 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
65 19 ad2antrr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( 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 ) )
66 simprl 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> x e. RR+ )
67 simprr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) )
68 simplr 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> J e. ( M ..^ N ) )
69 eqid 
 |-  ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. x ) ) ) + 1 ) ... ( |_ ` ( Z / x ) ) ) = ( ( ( |_ ` ( Z / ( ( 1 + ( L x. E ) ) x. x ) ) ) + 1 ) ... ( |_ ` ( Z / x ) ) )
70 1 55 56 57 5 6 58 59 9 10 60 61 62 14 63 16 17 64 65 20 66 67 68 69 pntlemj 
 |-  ( ( ( ph /\ J e. ( M ..^ N ) ) /\ ( x e. RR+ /\ ( ( ( K ^ J ) < x /\ ( ( 1 + ( L x. E ) ) x. x ) < ( K x. ( K ^ J ) ) ) /\ A. u e. ( x [,] ( ( 1 + ( L x. E ) ) x. x ) ) ( abs ` ( ( R ` u ) / u ) ) <_ E ) ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )
71 54 70 rexlimddv 
 |-  ( ( ph /\ J e. ( M ..^ N ) ) -> ( ( U - E ) x. ( ( ( L x. E ) / 8 ) x. ( log ` Z ) ) ) <_ sum_ n e. O ( ( ( U / n ) - ( abs ` ( ( R ` ( Z / n ) ) / Z ) ) ) x. ( log ` n ) ) )