Metamath Proof Explorer

Theorem chebbnd2

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

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

Proof

Step Hyp Ref Expression
1 ovexd 
 |-  ( T. -> ( 2 [,) +oo ) e. _V )
2 ovexd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / x ) e. _V )
3 ovexd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) e. _V )
4 eqidd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) )
5 2re 
 |-  2 e. RR
6 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
7 5 6 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
8 7 bilani 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( x e. RR /\ 2 <_ x ) )
9 chtrpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( theta ` x ) e. RR+ )
10 8 9 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( theta ` x ) e. RR+ )
11 10 rpcnne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) )
12 ppinncl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. NN )
13 8 12 syl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ppi ` x ) e. NN )
14 13 nnrpd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ppi ` x ) e. RR+ )
15 8 simpld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> x e. RR )
16 1red 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 e. RR )
17 5 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 2 e. RR )
18 1lt2 
 |-  1 < 2
19 18 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 < 2 )
20 8 simprd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 2 <_ x )
21 16 17 15 19 20 ltletrd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 < x )
22 15 21 rplogcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( log ` x ) e. RR+ )
23 14 22 rpmulcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. RR+ )
24 23 rpcnne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) e. CC /\ ( ( ppi ` x ) x. ( log ` x ) ) =/= 0 ) )
25 recdiv 
 |-  ( ( ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) /\ ( ( ( ppi ` x ) x. ( log ` x ) ) e. CC /\ ( ( ppi ` x ) x. ( log ` x ) ) =/= 0 ) ) -> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) )
26 11 24 25 syl2anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) )
27 26 mpteq2dva 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
28 1 2 3 4 27 offval2 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( theta ` x ) / x ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ) )
29 0red 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 0 e. RR )
30 2pos 
 |-  0 < 2
31 30 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 0 < 2 )
32 29 17 15 31 20 ltletrd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 0 < x )
33 15 32 elrpd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> x e. RR+ )
34 33 rpcnne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( x e. CC /\ x =/= 0 ) )
35 23 rpcnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. CC )
36 dmdcan 
 |-  ( ( ( ( theta ` x ) e. CC /\ ( theta ` x ) =/= 0 ) /\ ( x e. CC /\ x =/= 0 ) /\ ( ( ppi ` x ) x. ( log ` x ) ) e. CC ) -> ( ( ( theta ` x ) / x ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
37 11 34 35 36 syl3anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( theta ` x ) / x ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
38 14 rpcnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ppi ` x ) e. CC )
39 22 rpcnne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( log ` x ) e. CC /\ ( log ` x ) =/= 0 ) )
40 divdiv2 
 |-  ( ( ( ppi ` x ) e. CC /\ ( x e. CC /\ x =/= 0 ) /\ ( ( log ` x ) e. CC /\ ( log ` x ) =/= 0 ) ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
41 38 34 39 40 syl3anc 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / x ) )
42 37 41 eqtr4d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( theta ` x ) / x ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) = ( ( ppi ` x ) / ( x / ( log ` x ) ) ) )
43 42 mpteq2dva 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ( theta ` x ) / x ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) )
44 28 43 eqtrd 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) )
45 33 ex 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) -> x e. RR+ ) )
46 45 ssrdv 
 |-  ( T. -> ( 2 [,) +oo ) C_ RR+ )
47 chto1ub 
 |-  ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1)
48 47 a1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1) )
49 46 48 o1res2 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) e. O(1) )
50 ax-1cn 
 |-  1 e. CC
51 50 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 e. CC )
52 10 23 rpdivcld 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR+ )
53 52 rpcnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
54 pnfxr 
 |-  +oo e. RR*
55 icossre 
 |-  ( ( 2 e. RR /\ +oo e. RR* ) -> ( 2 [,) +oo ) C_ RR )
56 5 54 55 mp2an 
 |-  ( 2 [,) +oo ) C_ RR
57 rlimconst 
 |-  ( ( ( 2 [,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1 )
58 56 50 57 mp2an 
 |-  ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1
59 58 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1 )
60 chtppilim 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1
61 60 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1 )
62 ax-1ne0 
 |-  1 =/= 0
63 62 a1i 
 |-  ( T. -> 1 =/= 0 )
64 52 rpne0d 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) =/= 0 )
65 51 53 59 61 63 64 rlimdiv 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ~~>r ( 1 / 1 ) )
66 rlimo1 
 |-  ( ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ~~>r ( 1 / 1 ) -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) e. O(1) )
67 65 66 syl 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) e. O(1) )
68 o1mul 
 |-  ( ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) e. O(1) /\ ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) e. O(1) ) -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) e. O(1) )
69 49 67 68 syl2anc 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / x ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) e. O(1) )
70 44 69 eqeltrrd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) e. O(1) )
71 70 mptru 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( ppi ` x ) / ( x / ( log ` x ) ) ) ) e. O(1)