Metamath Proof Explorer

Theorem chto1lb

Description: The theta function is lower bounded by a linear term. Corollary of chebbnd1 . (Contributed by Mario Carneiro, 8-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 ovexd 
 |-  ( T. -> ( 2 [,) +oo ) e. _V )
2 2re 
 |-  2 e. RR
3 elicopnf 
 |-  ( 2 e. RR -> ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) ) )
4 2 3 ax-mp 
 |-  ( x e. ( 2 [,) +oo ) <-> ( x e. RR /\ 2 <_ x ) )
5 4 biimpi 
 |-  ( x e. ( 2 [,) +oo ) -> ( x e. RR /\ 2 <_ x ) )
6 5 simpld 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR )
7 0red 
 |-  ( x e. ( 2 [,) +oo ) -> 0 e. RR )
8 2 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 2 e. RR )
9 2pos 
 |-  0 < 2
10 9 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < 2 )
11 5 simprd 
 |-  ( x e. ( 2 [,) +oo ) -> 2 <_ x )
12 7 8 6 10 11 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 0 < x )
13 6 12 elrpd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. RR+ )
14 ppinncl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. NN )
15 14 nnrpd 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( ppi ` x ) e. RR+ )
16 5 15 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. RR+ )
17 1red 
 |-  ( x e. ( 2 [,) +oo ) -> 1 e. RR )
18 1lt2 
 |-  1 < 2
19 18 a1i 
 |-  ( x e. ( 2 [,) +oo ) -> 1 < 2 )
20 17 8 6 19 11 ltletrd 
 |-  ( x e. ( 2 [,) +oo ) -> 1 < x )
21 6 20 rplogcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. RR+ )
22 16 21 rpmulcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. RR+ )
23 13 22 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR+ )
24 23 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
25 24 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
26 chtrpcl 
 |-  ( ( x e. RR /\ 2 <_ x ) -> ( theta ` x ) e. RR+ )
27 5 26 syl 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. RR+ )
28 22 27 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) e. RR+ )
29 28 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) e. CC )
30 29 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) e. CC )
31 6 recnd 
 |-  ( x e. ( 2 [,) +oo ) -> x e. CC )
32 21 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) e. CC )
33 16 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) e. CC )
34 21 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( log ` x ) =/= 0 )
35 16 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ppi ` x ) =/= 0 )
36 31 32 33 34 35 divdiv1d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) = ( x / ( ( log ` x ) x. ( ppi ` x ) ) ) )
37 32 33 mulcomd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( log ` x ) x. ( ppi ` x ) ) = ( ( ppi ` x ) x. ( log ` x ) ) )
38 37 oveq2d 
 |-  ( x e. ( 2 [,) +oo ) -> ( x / ( ( log ` x ) x. ( ppi ` x ) ) ) = ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) )
39 36 38 eqtrd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) = ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) )
40 39 mpteq2ia 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) )
41 40 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) ) )
42 27 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) e. CC )
43 22 rpcnd 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) e. CC )
44 27 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( theta ` x ) =/= 0 )
45 22 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( ppi ` x ) x. ( log ` x ) ) =/= 0 )
46 42 43 44 45 recdivd 
 |-  ( x e. ( 2 [,) +oo ) -> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) = ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) )
47 46 mpteq2ia 
 |-  ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) )
48 47 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) )
49 1 25 30 41 48 offval2 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ) )
50 31 43 42 45 44 dmdcan2d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) = ( x / ( theta ` x ) ) )
51 50 mpteq2ia 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( x / ( ( ppi ` x ) x. ( log ` x ) ) ) x. ( ( ( ppi ` x ) x. ( log ` x ) ) / ( theta ` x ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) )
52 49 51 eqtrdi 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) = ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) )
53 chebbnd1 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1)
54 ax-1cn 
 |-  1 e. CC
55 54 a1i 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> 1 e. CC )
56 27 22 rpdivcld 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR+ )
57 56 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. RR+ )
58 57 rpcnd 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) e. CC )
59 6 ssriv 
 |-  ( 2 [,) +oo ) C_ RR
60 rlimconst 
 |-  ( ( ( 2 [,) +oo ) C_ RR /\ 1 e. CC ) -> ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1 )
61 59 54 60 mp2an 
 |-  ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1
62 61 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> 1 ) ~~>r 1 )
63 chtppilim 
 |-  ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1
64 63 a1i 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ~~>r 1 )
65 ax-1ne0 
 |-  1 =/= 0
66 65 a1i 
 |-  ( T. -> 1 =/= 0 )
67 56 rpne0d 
 |-  ( x e. ( 2 [,) +oo ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) =/= 0 )
68 67 adantl 
 |-  ( ( T. /\ x e. ( 2 [,) +oo ) ) -> ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) =/= 0 )
69 55 58 62 64 66 68 rlimdiv 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ~~>r ( 1 / 1 ) )
70 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) )
71 69 70 syl 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) e. O(1) )
72 o1mul 
 |-  ( ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) e. O(1) /\ ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) e. O(1) ) -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) e. O(1) )
73 53 71 72 sylancr 
 |-  ( T. -> ( ( x e. ( 2 [,) +oo ) |-> ( ( x / ( log ` x ) ) / ( ppi ` x ) ) ) oF x. ( x e. ( 2 [,) +oo ) |-> ( 1 / ( ( theta ` x ) / ( ( ppi ` x ) x. ( log ` x ) ) ) ) ) ) e. O(1) )
74 52 73 eqeltrrd 
 |-  ( T. -> ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) e. O(1) )
75 74 mptru 
 |-  ( x e. ( 2 [,) +oo ) |-> ( x / ( theta ` x ) ) ) e. O(1)