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)