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