Metamath Proof Explorer

Theorem chebbnd1

Description: The Chebyshev bound: The function ppi ( x ) is eventually lower bounded by a positive constant times x / log ( x ) . Alternatively stated, the function ( x / log ( x ) ) / ppi ( x ) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chebbnd1 
|- ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 2re 
 |-  2 e. RR
2 pnfxr 
 |-  +oo e. RR*
3 icossre 
 |-  ( ( 2 e. RR /\ +oo e. RR* ) -> ( 2 [,) +oo ) C_ RR )
4 1 2 3 mp2an 
 |-  ( 2 [,) +oo ) C_ RR
5 4 a1i 
 |-  ( T. -> ( 2 [,) +oo ) C_ RR )
6 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
7 1 6 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
8 7 simplbi 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
9 0red 
 |-  ( x e. ( 2 [,) +oo ) -> 0 e. RR )
10 1re 
 |-  1 e. RR
11 10 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 1 e. RR )
12 0lt1 
 |-  0 < 1
13 12 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < 1 )
14 1 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 2 e. RR )
15 1lt2 
 |-  1 < 2
16 15 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 1 < 2 )
17 7 simprbi 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
18 11 14 8 16 17 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 1 < x )
19 9 11 8 13 18 lttrd 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < x )
20 8 19 elrpd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
21 8 18 rplogcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. RR+ )
22 20 21 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( x / ( log ` x ) ) e. RR+ )
23 ppinncl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. NN )
24 7 23 sylbi 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. NN )
25 24 nnrpd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. RR+ )
26 22 25 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ )
27 26 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. CC )
28 27 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. CC )
29 8re 
 |-  8 e. RR
30 29 a1i 
 |-  ( T. -> 8 e. RR )
31 2rp 
 |-  2 e. RR+
32 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
33 31 32 ax-mp 
 |-  ( log ` 2 ) e. RR
34 ere 
 |-  _e e. RR
35 1 34 remulcli 
 |-  ( 2 x. _e ) e. RR
36 2pos 
 |-  0 < 2
37 epos 
 |-  0 < _e
38 1 34 36 37 mulgt0ii 
 |-  0 < ( 2 x. _e )
39 35 38 gt0ne0ii 
 |-  ( 2 x. _e ) =/= 0
40 35 39 rereccli 
 |-  ( 1 / ( 2 x. _e ) ) e. RR
41 33 40 resubcli 
 |-  ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR
42 2t1e2 
 |-  ( 2 x. 1 ) = 2
43 egt2lt3 
 |-  ( 2 < _e /\ _e < 3 )
44 43 simpli 
 |-  2 < _e
45 10 1 34 lttri 
 |-  ( ( 1 < 2 /\ 2 < _e ) -> 1 < _e )
46 15 44 45 mp2an 
 |-  1 < _e
47 10 34 1 ltmul2i 
 |-  ( 0 < 2 -> ( 1 < _e <-> ( 2 x. 1 ) < ( 2 x. _e ) ) )
48 36 47 ax-mp 
 |-  ( 1 < _e <-> ( 2 x. 1 ) < ( 2 x. _e ) )
49 46 48 mpbi 
 |-  ( 2 x. 1 ) < ( 2 x. _e )
50 42 49 eqbrtrri 
 |-  2 < ( 2 x. _e )
51 1 35 36 38 ltrecii 
 |-  ( 2 < ( 2 x. _e ) <-> ( 1 / ( 2 x. _e ) ) < ( 1 / 2 ) )
52 50 51 mpbi 
 |-  ( 1 / ( 2 x. _e ) ) < ( 1 / 2 )
53 43 simpri 
 |-  _e < 3
54 3lt4 
 |-  3 < 4
55 3re 
 |-  3 e. RR
56 4re 
 |-  4 e. RR
57 34 55 56 lttri 
 |-  ( ( _e < 3 /\ 3 < 4 ) -> _e < 4 )
58 53 54 57 mp2an 
 |-  _e < 4
59 epr 
 |-  _e e. RR+
60 4pos 
 |-  0 < 4
61 56 60 elrpii 
 |-  4 e. RR+
62 logltb 
 |-  ( ( _e e. RR+ /\ 4 e. RR+ ) -> ( _e < 4 <-> ( log ` _e ) < ( log ` 4 ) ) )
63 59 61 62 mp2an 
 |-  ( _e < 4 <-> ( log ` _e ) < ( log ` 4 ) )
64 58 63 mpbi 
 |-  ( log ` _e ) < ( log ` 4 )
65 loge 
 |-  ( log ` _e ) = 1
66 sq2 
 |-  ( 2 ^ 2 ) = 4
67 66 fveq2i 
 |-  ( log ` ( 2 ^ 2 ) ) = ( log ` 4 )
68 2z 
 |-  2 e. ZZ
69 relogexp 
 |-  ( ( 2 e. RR+ /\ 2 e. ZZ ) -> ( log ` ( 2 ^ 2 ) ) = ( 2 x. ( log ` 2 ) ) )
70 31 68 69 mp2an 
 |-  ( log ` ( 2 ^ 2 ) ) = ( 2 x. ( log ` 2 ) )
71 67 70 eqtr3i 
 |-  ( log ` 4 ) = ( 2 x. ( log ` 2 ) )
72 64 65 71 3brtr3i 
 |-  1 < ( 2 x. ( log ` 2 ) )
73 1 36 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
74 ltdivmul 
 |-  ( ( 1 e. RR /\ ( log ` 2 ) e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 1 / 2 ) < ( log ` 2 ) <-> 1 < ( 2 x. ( log ` 2 ) ) ) )
75 10 33 73 74 mp3an 
 |-  ( ( 1 / 2 ) < ( log ` 2 ) <-> 1 < ( 2 x. ( log ` 2 ) ) )
76 72 75 mpbir 
 |-  ( 1 / 2 ) < ( log ` 2 )
77 halfre 
 |-  ( 1 / 2 ) e. RR
78 40 77 33 lttri 
 |-  ( ( ( 1 / ( 2 x. _e ) ) < ( 1 / 2 ) /\ ( 1 / 2 ) < ( log ` 2 ) ) -> ( 1 / ( 2 x. _e ) ) < ( log ` 2 ) )
79 52 76 78 mp2an 
 |-  ( 1 / ( 2 x. _e ) ) < ( log ` 2 )
80 40 33 posdifi 
 |-  ( ( 1 / ( 2 x. _e ) ) < ( log ` 2 ) <-> 0 < ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) )
81 79 80 mpbi 
 |-  0 < ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) )
82 41 81 elrpii 
 |-  ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR+
83 rerpdivcl 
 |-  ( ( 2 e. RR /\ ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. RR+ ) -> ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) e. RR )
84 1 82 83 mp2an 
 |-  ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) e. RR
85 84 a1i 
 |-  ( T. -> ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) e. RR )
86 rpre 
 |-  ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR )
87 rpge0 
 |-  ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ -> 0 <_ ( ( x / ( log ` x ) ) / ( ppi ` x ) ) )
88 86 87 absidd 
 |-  ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ -> ( abs ` ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( ( x / ( log ` x ) ) / ( ppi ` x ) ) )
89 26 88 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( abs ` ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( ( x / ( log ` x ) ) / ( ppi ` x ) ) )
90 89 adantr 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( abs ` ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( ( x / ( log ` x ) ) / ( ppi ` x ) ) )
91 eqid 
 |-  ( |_ ` ( x / 2 ) ) = ( |_ ` ( x / 2 ) )
92 91 chebbnd1lem3 
 |-  ( ( x e. RR /\ 8 <_ x ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ppi ` x ) x. ( ( log ` x ) / x ) ) )
93 8 92 sylan 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) < ( ( ppi ` x ) x. ( ( log ` x ) / x ) ) )
94 1 recni 
 |-  2 e. CC
95 2ne0 
 |-  2 =/= 0
96 41 recni 
 |-  ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. CC
97 41 81 gt0ne0ii 
 |-  ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) =/= 0
98 recdiv 
 |-  ( ( ( 2 e. CC /\ 2 =/= 0 ) /\ ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) e. CC /\ ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) =/= 0 ) ) -> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) = ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) )
99 94 95 96 97 98 mp4an 
 |-  ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) = ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 )
100 99 a1i 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) = ( ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) / 2 ) )
101 22 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( x / ( log ` x ) ) e. CC )
102 24 nncnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. CC )
103 22 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( x / ( log ` x ) ) =/= 0 )
104 24 nnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) =/= 0 )
105 101 102 103 104 recdivd 
 |-  ( x e. ( 2 [,) +oo ) -> ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( ( ppi ` x ) / ( x / ( log ` x ) ) ) )
106 102 101 103 divrecd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) = ( ( ppi ` x ) x. ( 1 / ( x / ( log ` x ) ) ) ) )
107 20 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( x e. CC /\ x =/= 0 ) )
108 21 rpcnne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( log ` x ) e. CC /\ ( log ` x ) =/= 0 ) )
109 recdiv 
 |-  ( ( ( x e. CC /\ x =/= 0 ) /\ ( ( log ` x ) e. CC /\ ( log ` x ) =/= 0 ) ) -> ( 1 / ( x / ( log ` x ) ) ) = ( ( log ` x ) / x ) )
110 107 108 109 syl2anc 
 |-  ( x e. ( 2 [,) +oo ) -> ( 1 / ( x / ( log ` x ) ) ) = ( ( log ` x ) / x ) )
111 110 oveq2d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( 1 / ( x / ( log ` x ) ) ) ) = ( ( ppi ` x ) x. ( ( log ` x ) / x ) ) )
112 105 106 111 3eqtrd 
 |-  ( x e. ( 2 [,) +oo ) -> ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( ( ppi ` x ) x. ( ( log ` x ) / x ) ) )
113 112 adantr 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( ( ppi ` x ) x. ( ( log ` x ) / x ) ) )
114 93 100 113 3brtr4d 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) < ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) )
115 26 adantr 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ )
116 elrp 
 |-  ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ <-> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR /\ 0 < ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) )
117 1 41 36 81 divgt0ii 
 |-  0 < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) )
118 ltrec 
 |-  ( ( ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR /\ 0 < ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) /\ ( ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) e. RR /\ 0 < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) ) -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) <-> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) < ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) ) )
119 84 117 118 mpanr12 
 |-  ( ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR /\ 0 < ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) <-> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) < ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) ) )
120 116 119 sylbi 
 |-  ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR+ -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) <-> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) < ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) ) )
121 115 120 syl 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) <-> ( 1 / ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) < ( 1 / ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) ) )
122 114 121 mpbird 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) )
123 115 rpred 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR )
124 ltle 
 |-  ( ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) e. RR /\ ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) e. RR ) -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) <_ ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) )
125 123 84 124 sylancl 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( ( x / ( log ` x ) ) / ( ppi ` x ) ) < ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) <_ ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) ) )
126 122 125 mpd 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) <_ ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) )
127 90 126 eqbrtrd 
 |-  ( ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) -> ( abs ` ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) <_ ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) )
128 127 adantl 
 |-  ( ( T. /\ ( x e. ( 2 [,) +oo ) /\ 8 <_ x ) ) -> ( abs ` ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) <_ ( 2 / ( ( log ` 2 ) - ( 1 / ( 2 x. _e ) ) ) ) )
129 5 28 30 85 128 elo1d 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1) )
130 129 mptru 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1)