Metamath Proof Explorer

Theorem pntlemn

Description: Lemma for pnt . The "naive" base bound, which we will slightly improve. (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 )
Assertion pntlemn 
|- ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) x. ( log ` J ) ) )

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 7 adantr 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> U e. RR+ )
20 19 rpred 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> U e. RR )
21 simprl 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. NN )
22 20 21 nndivred 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( U / J ) e. RR )
23 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 pntlemb 
 |-  ( ph -> ( Z e. RR+ /\ ( 1 < Z /\ _e <_ ( sqrt ` Z ) /\ ( sqrt ` Z ) <_ ( Z / Y ) ) /\ ( ( 4 / ( L x. E ) ) <_ ( sqrt ` Z ) /\ ( ( ( log ` X ) / ( log ` K ) ) + 2 ) <_ ( ( ( log ` Z ) / ( log ` K ) ) / 4 ) /\ ( ( U x. 3 ) + C ) <_ ( ( ( U - E ) x. ( ( L x. ( E ^ 2 ) ) / ( ; 3 2 x. B ) ) ) x. ( log ` Z ) ) ) ) )
24 23 simp1d 
 |-  ( ph -> Z e. RR+ )
25 24 adantr 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Z e. RR+ )
26 21 nnrpd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. RR+ )
27 25 26 rpdivcld 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z / J ) e. RR+ )
28 1 pntrf 
 |-  R : RR+ --> RR
29 28 ffvelcdmi 
 |-  ( ( Z / J ) e. RR+ -> ( R ` ( Z / J ) ) e. RR )
30 27 29 syl 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( R ` ( Z / J ) ) e. RR )
31 30 25 rerpdivcld 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / Z ) e. RR )
32 31 recnd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / Z ) e. CC )
33 32 abscld 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) e. RR )
34 22 33 resubcld 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) e. RR )
35 26 relogcld 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( log ` J ) e. RR )
36 30 recnd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( R ` ( Z / J ) ) e. CC )
37 25 rpcnne0d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z e. CC /\ Z =/= 0 ) )
38 26 rpcnne0d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( J e. CC /\ J =/= 0 ) )
39 divdiv2 
 |-  ( ( ( R ` ( Z / J ) ) e. CC /\ ( Z e. CC /\ Z =/= 0 ) /\ ( J e. CC /\ J =/= 0 ) ) -> ( ( R ` ( Z / J ) ) / ( Z / J ) ) = ( ( ( R ` ( Z / J ) ) x. J ) / Z ) )
40 36 37 38 39 syl3anc 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / ( Z / J ) ) = ( ( ( R ` ( Z / J ) ) x. J ) / Z ) )
41 21 nncnd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. CC )
42 div23 
 |-  ( ( ( R ` ( Z / J ) ) e. CC /\ J e. CC /\ ( Z e. CC /\ Z =/= 0 ) ) -> ( ( ( R ` ( Z / J ) ) x. J ) / Z ) = ( ( ( R ` ( Z / J ) ) / Z ) x. J ) )
43 36 41 37 42 syl3anc 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( ( R ` ( Z / J ) ) x. J ) / Z ) = ( ( ( R ` ( Z / J ) ) / Z ) x. J ) )
44 40 43 eqtrd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( R ` ( Z / J ) ) / ( Z / J ) ) = ( ( ( R ` ( Z / J ) ) / Z ) x. J ) )
45 44 fveq2d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) = ( abs ` ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) )
46 32 41 absmuld 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( ( R ` ( Z / J ) ) / Z ) x. J ) ) = ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. ( abs ` J ) ) )
47 26 rprege0d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( J e. RR /\ 0 <_ J ) )
48 absid 
 |-  ( ( J e. RR /\ 0 <_ J ) -> ( abs ` J ) = J )
49 47 48 syl 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` J ) = J )
50 49 oveq2d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. ( abs ` J ) ) = ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) )
51 45 46 50 3eqtrd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) = ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) )
52 fveq2 
 |-  ( z = ( Z / J ) -> ( R ` z ) = ( R ` ( Z / J ) ) )
53 id 
 |-  ( z = ( Z / J ) -> z = ( Z / J ) )
54 52 53 oveq12d 
 |-  ( z = ( Z / J ) -> ( ( R ` z ) / z ) = ( ( R ` ( Z / J ) ) / ( Z / J ) ) )
55 54 fveq2d 
 |-  ( z = ( Z / J ) -> ( abs ` ( ( R ` z ) / z ) ) = ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) )
56 55 breq1d 
 |-  ( z = ( Z / J ) -> ( ( abs ` ( ( R ` z ) / z ) ) <_ U <-> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) <_ U ) )
57 18 adantr 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> A. z e. ( Y [,) +oo ) ( abs ` ( ( R ` z ) / z ) ) <_ U )
58 27 rpred 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z / J ) e. RR )
59 simprr 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J <_ ( Z / Y ) )
60 26 rpred 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> J e. RR )
61 25 rpred 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Z e. RR )
62 11 simpld 
 |-  ( ph -> Y e. RR+ )
63 62 adantr 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Y e. RR+ )
64 60 61 63 lemuldiv2d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( Y x. J ) <_ Z <-> J <_ ( Z / Y ) ) )
65 59 64 mpbird 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Y x. J ) <_ Z )
66 63 rpred 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Y e. RR )
67 66 61 26 lemuldivd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( Y x. J ) <_ Z <-> Y <_ ( Z / J ) ) )
68 65 67 mpbid 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> Y <_ ( Z / J ) )
69 elicopnf 
 |-  ( Y e. RR -> ( ( Z / J ) e. ( Y [,) +oo ) <-> ( ( Z / J ) e. RR /\ Y <_ ( Z / J ) ) ) )
70 66 69 syl 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( Z / J ) e. ( Y [,) +oo ) <-> ( ( Z / J ) e. RR /\ Y <_ ( Z / J ) ) ) )
71 58 68 70 mpbir2and 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( Z / J ) e. ( Y [,) +oo ) )
72 56 57 71 rspcdva 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / ( Z / J ) ) ) <_ U )
73 51 72 eqbrtrrd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) <_ U )
74 33 20 26 lemuldivd 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( ( ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) x. J ) <_ U <-> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) <_ ( U / J ) ) )
75 73 74 mpbid 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) <_ ( U / J ) )
76 22 33 subge0d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( 0 <_ ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) <-> ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) <_ ( U / J ) ) )
77 75 76 mpbird 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) )
78 log1 
 |-  ( log ` 1 ) = 0
79 nnge1 
 |-  ( J e. NN -> 1 <_ J )
80 79 ad2antrl 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 1 <_ J )
81 1rp 
 |-  1 e. RR+
82 logleb 
 |-  ( ( 1 e. RR+ /\ J e. RR+ ) -> ( 1 <_ J <-> ( log ` 1 ) <_ ( log ` J ) ) )
83 81 26 82 sylancr 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( 1 <_ J <-> ( log ` 1 ) <_ ( log ` J ) ) )
84 80 83 mpbid 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> ( log ` 1 ) <_ ( log ` J ) )
85 78 84 eqbrtrrid 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( log ` J ) )
86 34 35 77 85 mulge0d 
 |-  ( ( ph /\ ( J e. NN /\ J <_ ( Z / Y ) ) ) -> 0 <_ ( ( ( U / J ) - ( abs ` ( ( R ` ( Z / J ) ) / Z ) ) ) x. ( log ` J ) ) )