Metamath Proof Explorer

Theorem chto1ub

Description: The theta function is upper bounded by a linear term. Corollary of chtub . (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chto1ub 
|- ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 rpssre 
 |-  RR+ C_ RR
2 1 a1i 
 |-  ( T. -> RR+ C_ RR )
3 rpre 
 |-  ( x e. RR+ -> x e. RR )
4 chtcl 
 |-  ( x e. RR -> ( theta ` x ) e. RR )
5 3 4 syl 
 |-  ( x e. RR+ -> ( theta ` x ) e. RR )
6 rerpdivcl 
 |-  ( ( ( theta ` x ) e. RR /\ x e. RR+ ) -> ( ( theta ` x ) / x ) e. RR )
7 5 6 mpancom 
 |-  ( x e. RR+ -> ( ( theta ` x ) / x ) e. RR )
8 7 recnd 
 |-  ( x e. RR+ -> ( ( theta ` x ) / x ) e. CC )
9 8 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( theta ` x ) / x ) e. CC )
10 3re 
 |-  3 e. RR
11 10 a1i 
 |-  ( T. -> 3 e. RR )
12 2rp 
 |-  2 e. RR+
13 relogcl 
 |-  ( 2 e. RR+ -> ( log ` 2 ) e. RR )
14 12 13 ax-mp 
 |-  ( log ` 2 ) e. RR
15 2re 
 |-  2 e. RR
16 14 15 remulcli 
 |-  ( ( log ` 2 ) x. 2 ) e. RR
17 16 a1i 
 |-  ( T. -> ( ( log ` 2 ) x. 2 ) e. RR )
18 chtge0 
 |-  ( x e. RR -> 0 <_ ( theta ` x ) )
19 3 18 syl 
 |-  ( x e. RR+ -> 0 <_ ( theta ` x ) )
20 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
21 divge0 
 |-  ( ( ( ( theta ` x ) e. RR /\ 0 <_ ( theta ` x ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( theta ` x ) / x ) )
22 5 19 20 21 syl21anc 
 |-  ( x e. RR+ -> 0 <_ ( ( theta ` x ) / x ) )
23 7 22 absidd 
 |-  ( x e. RR+ -> ( abs ` ( ( theta ` x ) / x ) ) = ( ( theta ` x ) / x ) )
24 23 adantr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( abs ` ( ( theta ` x ) / x ) ) = ( ( theta ` x ) / x ) )
25 7 adantr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( theta ` x ) / x ) e. RR )
26 16 a1i 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( log ` 2 ) x. 2 ) e. RR )
27 5 adantr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( theta ` x ) e. RR )
28 3 adantr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> x e. RR )
29 remulcl 
 |-  ( ( 2 e. RR /\ x e. RR ) -> ( 2 x. x ) e. RR )
30 15 28 29 sylancr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( 2 x. x ) e. RR )
31 resubcl 
 |-  ( ( ( 2 x. x ) e. RR /\ 3 e. RR ) -> ( ( 2 x. x ) - 3 ) e. RR )
32 30 10 31 sylancl 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( 2 x. x ) - 3 ) e. RR )
33 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( ( 2 x. x ) - 3 ) e. RR ) -> ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) e. RR )
34 14 32 33 sylancr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) e. RR )
35 remulcl 
 |-  ( ( ( log ` 2 ) e. RR /\ ( 2 x. x ) e. RR ) -> ( ( log ` 2 ) x. ( 2 x. x ) ) e. RR )
36 14 30 35 sylancr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( log ` 2 ) x. ( 2 x. x ) ) e. RR )
37 15 a1i 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> 2 e. RR )
38 10 a1i 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> 3 e. RR )
39 2lt3 
 |-  2 < 3
40 39 a1i 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> 2 < 3 )
41 simpr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> 3 <_ x )
42 37 38 28 40 41 ltletrd 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> 2 < x )
43 chtub 
 |-  ( ( x e. RR /\ 2 < x ) -> ( theta ` x ) < ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) )
44 28 42 43 syl2anc 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( theta ` x ) < ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) )
45 3rp 
 |-  3 e. RR+
46 ltsubrp 
 |-  ( ( ( 2 x. x ) e. RR /\ 3 e. RR+ ) -> ( ( 2 x. x ) - 3 ) < ( 2 x. x ) )
47 30 45 46 sylancl 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( 2 x. x ) - 3 ) < ( 2 x. x ) )
48 1lt2 
 |-  1 < 2
49 rplogcl 
 |-  ( ( 2 e. RR /\ 1 < 2 ) -> ( log ` 2 ) e. RR+ )
50 15 48 49 mp2an 
 |-  ( log ` 2 ) e. RR+
51 elrp 
 |-  ( ( log ` 2 ) e. RR+ <-> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
52 50 51 mpbi 
 |-  ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) )
53 52 a1i 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) )
54 ltmul2 
 |-  ( ( ( ( 2 x. x ) - 3 ) e. RR /\ ( 2 x. x ) e. RR /\ ( ( log ` 2 ) e. RR /\ 0 < ( log ` 2 ) ) ) -> ( ( ( 2 x. x ) - 3 ) < ( 2 x. x ) <-> ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) < ( ( log ` 2 ) x. ( 2 x. x ) ) ) )
55 32 30 53 54 syl3anc 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( ( 2 x. x ) - 3 ) < ( 2 x. x ) <-> ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) < ( ( log ` 2 ) x. ( 2 x. x ) ) ) )
56 47 55 mpbid 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( log ` 2 ) x. ( ( 2 x. x ) - 3 ) ) < ( ( log ` 2 ) x. ( 2 x. x ) ) )
57 27 34 36 44 56 lttrd 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( theta ` x ) < ( ( log ` 2 ) x. ( 2 x. x ) ) )
58 14 recni 
 |-  ( log ` 2 ) e. CC
59 58 a1i 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( log ` 2 ) e. CC )
60 2cnd 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> 2 e. CC )
61 3 recnd 
 |-  ( x e. RR+ -> x e. CC )
62 61 adantr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> x e. CC )
63 59 60 62 mulassd 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( ( log ` 2 ) x. 2 ) x. x ) = ( ( log ` 2 ) x. ( 2 x. x ) ) )
64 57 63 breqtrrd 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( theta ` x ) < ( ( ( log ` 2 ) x. 2 ) x. x ) )
65 20 adantr 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( x e. RR /\ 0 < x ) )
66 ltdivmul2 
 |-  ( ( ( theta ` x ) e. RR /\ ( ( log ` 2 ) x. 2 ) e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( ( theta ` x ) / x ) < ( ( log ` 2 ) x. 2 ) <-> ( theta ` x ) < ( ( ( log ` 2 ) x. 2 ) x. x ) ) )
67 27 26 65 66 syl3anc 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( ( theta ` x ) / x ) < ( ( log ` 2 ) x. 2 ) <-> ( theta ` x ) < ( ( ( log ` 2 ) x. 2 ) x. x ) ) )
68 64 67 mpbird 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( theta ` x ) / x ) < ( ( log ` 2 ) x. 2 ) )
69 25 26 68 ltled 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( ( theta ` x ) / x ) <_ ( ( log ` 2 ) x. 2 ) )
70 24 69 eqbrtrd 
 |-  ( ( x e. RR+ /\ 3 <_ x ) -> ( abs ` ( ( theta ` x ) / x ) ) <_ ( ( log ` 2 ) x. 2 ) )
71 70 adantl 
 |-  ( ( T. /\ ( x e. RR+ /\ 3 <_ x ) ) -> ( abs ` ( ( theta ` x ) / x ) ) <_ ( ( log ` 2 ) x. 2 ) )
72 2 9 11 17 71 elo1d 
 |-  ( T. -> ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1) )
73 72 mptru 
 |-  ( x e. RR+ |-> ( ( theta ` x ) / x ) ) e. O(1)