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 ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 ovexd ( ⊤ → ( 2 [,) +∞ ) ∈ V )
2 2re 2 ∈ ℝ
3 elicopnf ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
4 2 3 ax-mp ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
5 4 biimpi ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
6 5 simpld ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
7 0red ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
8 2 a1i ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
9 2pos 0 < 2
10 9 a1i ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 2 )
11 5 simprd ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
12 7 8 6 10 11 ltletrd ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
13 6 12 elrpd ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
14 ppinncl ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π𝑥 ) ∈ ℕ )
15 14 nnrpd ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π𝑥 ) ∈ ℝ+ )
16 5 15 syl ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π𝑥 ) ∈ ℝ+ )
17 1red ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 ∈ ℝ )
18 1lt2 1 < 2
19 18 a1i ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 2 )
20 17 8 6 19 11 ltletrd ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 𝑥 )
21 6 20 rplogcld ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
22 16 21 rpmulcld ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
23 13 22 rpdivcld ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ+ )
24 23 rpcnd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
25 24 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
26 chtrpcl ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
27 5 26 syl ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℝ+ )
28 22 27 rpdivcld ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ∈ ℝ+ )
29 28 rpcnd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ∈ ℂ )
30 29 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ∈ ℂ )
31 6 recnd ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℂ )
32 21 rpcnd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℂ )
33 16 rpcnd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π𝑥 ) ∈ ℂ )
34 21 rpne0d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ≠ 0 )
35 16 rpne0d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π𝑥 ) ≠ 0 )
36 31 32 33 34 35 divdiv1d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) = ( 𝑥 / ( ( log ‘ 𝑥 ) · ( π𝑥 ) ) ) )
37 32 33 mulcomd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( log ‘ 𝑥 ) · ( π𝑥 ) ) = ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) )
38 37 oveq2d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 / ( ( log ‘ 𝑥 ) · ( π𝑥 ) ) ) = ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) )
39 36 38 eqtrd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) = ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) )
40 39 mpteq2ia ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) )
41 40 a1i ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) )
42 27 rpcnd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ∈ ℂ )
43 22 rpcnd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
44 27 rpne0d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( θ ‘ 𝑥 ) ≠ 0 )
45 22 rpne0d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ≠ 0 )
46 42 43 44 45 recdivd ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) = ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) )
47 46 mpteq2ia ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) )
48 47 a1i ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) )
49 1 25 30 41 48 offval2 ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ) )
50 31 43 42 45 44 dmdcan2d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) = ( 𝑥 / ( θ ‘ 𝑥 ) ) )
51 50 mpteq2ia ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) · ( ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) / ( θ ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) )
52 49 51 eqtrdi ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) = ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) )
53 chebbnd1 ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) ∈ 𝑂(1)
54 ax-1cn 1 ∈ ℂ
55 54 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → 1 ∈ ℂ )
56 27 22 rpdivcld ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ+ )
57 56 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ+ )
58 57 rpcnd ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
59 6 ssriv ( 2 [,) +∞ ) ⊆ ℝ
60 rlimconst ( ( ( 2 [,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1 )
61 59 54 60 mp2an ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1
62 61 a1i ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ 1 ) ⇝𝑟 1 )
63 chtppilim ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1
64 63 a1i ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ⇝𝑟 1 )
65 ax-1ne0 1 ≠ 0
66 65 a1i ( ⊤ → 1 ≠ 0 )
67 56 rpne0d ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ≠ 0 )
68 67 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ≠ 0 )
69 55 58 62 64 66 68 rlimdiv ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ⇝𝑟 ( 1 / 1 ) )
70 rlimo1 ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ⇝𝑟 ( 1 / 1 ) → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
71 69 70 syl ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
72 o1mul ( ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) ∈ 𝑂(1) )
73 53 71 72 sylancr ( ⊤ → ( ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π𝑥 ) ) ) ∘f · ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 1 / ( ( θ ‘ 𝑥 ) / ( ( π𝑥 ) · ( log ‘ 𝑥 ) ) ) ) ) ) ∈ 𝑂(1) )
74 52 73 eqeltrrd ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
75 74 mptru ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( 𝑥 / ( θ ‘ 𝑥 ) ) ) ∈ 𝑂(1)