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 ( 𝑥 ∈ ℝ+ ↦ ( ( θ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)

Proof

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