This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem chebbnd1

Description: The Chebyshev bound: The function ppi ( x ) is eventually lower bounded by a positive constant times x / log ( x ) . Alternatively stated, the function ( x / log ( x ) ) / ppi ( x ) is eventually bounded. (Contributed by Mario Carneiro, 22-Sep-2014)

Ref Expression
Assertion chebbnd1 ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 pnfxr ⊢ +∞ ∈ ℝ*
3 icossre ⊢ ( ( 2 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 2 [,) +∞ ) ⊆ ℝ )
4 1 2 3 mp2an ⊢ ( 2 [,) +∞ ) ⊆ ℝ
5 4 a1i ⊢ ( ⊤ → ( 2 [,) +∞ ) ⊆ ℝ )
6 elicopnf ⊢ ( 2 ∈ ℝ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) ) )
7 1 6 ax-mp ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) )
8 7 simplbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ )
9 0red ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 ∈ ℝ )
10 1re ⊢ 1 ∈ ℝ
11 10 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 ∈ ℝ )
12 0lt1 ⊢ 0 < 1
13 12 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 1 )
14 1 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ∈ ℝ )
15 1lt2 ⊢ 1 < 2
16 15 a1i ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 2 )
17 7 simprbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 2 ≤ 𝑥 )
18 11 14 8 16 17 ltletrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 1 < 𝑥 )
19 9 11 8 13 18 lttrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 0 < 𝑥 )
20 8 19 elrpd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → 𝑥 ∈ ℝ+ )
21 8 18 rplogcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
22 20 21 rpdivcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
23 ppinncl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ≤ 𝑥 ) → ( π ‘ 𝑥 ) ∈ ℕ )
24 7 23 sylbi ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℕ )
25 24 nnrpd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℝ+ )
26 22 25 rpdivcld ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ )
27 26 rpcnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℂ )
28 27 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 2 [,) +∞ ) ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℂ )
29 8re ⊢ 8 ∈ ℝ
30 29 a1i ⊢ ( ⊤ → 8 ∈ ℝ )
31 2rp ⊢ 2 ∈ ℝ+
32 relogcl ⊢ ( 2 ∈ ℝ+ → ( log ‘ 2 ) ∈ ℝ )
33 31 32 ax-mp ⊢ ( log ‘ 2 ) ∈ ℝ
34 ere ⊢ e ∈ ℝ
35 1 34 remulcli ⊢ ( 2 · e ) ∈ ℝ
36 2pos ⊢ 0 < 2
37 epos ⊢ 0 < e
38 1 34 36 37 mulgt0ii ⊢ 0 < ( 2 · e )
39 35 38 gt0ne0ii ⊢ ( 2 · e ) ≠ 0
40 35 39 rereccli ⊢ ( 1 / ( 2 · e ) ) ∈ ℝ
41 33 40 resubcli ⊢ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ
42 2t1e2 ⊢ ( 2 · 1 ) = 2
43 egt2lt3 ⊢ ( 2 < e ∧ e < 3 )
44 43 simpli ⊢ 2 < e
45 10 1 34 lttri ⊢ ( ( 1 < 2 ∧ 2 < e ) → 1 < e )
46 15 44 45 mp2an ⊢ 1 < e
47 10 34 1 ltmul2i ⊢ ( 0 < 2 → ( 1 < e ↔ ( 2 · 1 ) < ( 2 · e ) ) )
48 36 47 ax-mp ⊢ ( 1 < e ↔ ( 2 · 1 ) < ( 2 · e ) )
49 46 48 mpbi ⊢ ( 2 · 1 ) < ( 2 · e )
50 42 49 eqbrtrri ⊢ 2 < ( 2 · e )
51 1 35 36 38 ltrecii ⊢ ( 2 < ( 2 · e ) ↔ ( 1 / ( 2 · e ) ) < ( 1 / 2 ) )
52 50 51 mpbi ⊢ ( 1 / ( 2 · e ) ) < ( 1 / 2 )
53 43 simpri ⊢ e < 3
54 3lt4 ⊢ 3 < 4
55 3re ⊢ 3 ∈ ℝ
56 4re ⊢ 4 ∈ ℝ
57 34 55 56 lttri ⊢ ( ( e < 3 ∧ 3 < 4 ) → e < 4 )
58 53 54 57 mp2an ⊢ e < 4
59 epr ⊢ e ∈ ℝ+
60 4pos ⊢ 0 < 4
61 56 60 elrpii ⊢ 4 ∈ ℝ+
62 logltb ⊢ ( ( e ∈ ℝ+ ∧ 4 ∈ ℝ+ ) → ( e < 4 ↔ ( log ‘ e ) < ( log ‘ 4 ) ) )
63 59 61 62 mp2an ⊢ ( e < 4 ↔ ( log ‘ e ) < ( log ‘ 4 ) )
64 58 63 mpbi ⊢ ( log ‘ e ) < ( log ‘ 4 )
65 loge ⊢ ( log ‘ e ) = 1
66 sq2 ⊢ ( 2 ↑ 2 ) = 4
67 66 fveq2i ⊢ ( log ‘ ( 2 ↑ 2 ) ) = ( log ‘ 4 )
68 2z ⊢ 2 ∈ ℤ
69 relogexp ⊢ ( ( 2 ∈ ℝ+ ∧ 2 ∈ ℤ ) → ( log ‘ ( 2 ↑ 2 ) ) = ( 2 · ( log ‘ 2 ) ) )
70 31 68 69 mp2an ⊢ ( log ‘ ( 2 ↑ 2 ) ) = ( 2 · ( log ‘ 2 ) )
71 67 70 eqtr3i ⊢ ( log ‘ 4 ) = ( 2 · ( log ‘ 2 ) )
72 64 65 71 3brtr3i ⊢ 1 < ( 2 · ( log ‘ 2 ) )
73 1 36 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
74 ltdivmul ⊢ ( ( 1 ∈ ℝ ∧ ( log ‘ 2 ) ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( 1 / 2 ) < ( log ‘ 2 ) ↔ 1 < ( 2 · ( log ‘ 2 ) ) ) )
75 10 33 73 74 mp3an ⊢ ( ( 1 / 2 ) < ( log ‘ 2 ) ↔ 1 < ( 2 · ( log ‘ 2 ) ) )
76 72 75 mpbir ⊢ ( 1 / 2 ) < ( log ‘ 2 )
77 halfre ⊢ ( 1 / 2 ) ∈ ℝ
78 40 77 33 lttri ⊢ ( ( ( 1 / ( 2 · e ) ) < ( 1 / 2 ) ∧ ( 1 / 2 ) < ( log ‘ 2 ) ) → ( 1 / ( 2 · e ) ) < ( log ‘ 2 ) )
79 52 76 78 mp2an ⊢ ( 1 / ( 2 · e ) ) < ( log ‘ 2 )
80 40 33 posdifi ⊢ ( ( 1 / ( 2 · e ) ) < ( log ‘ 2 ) ↔ 0 < ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) )
81 79 80 mpbi ⊢ 0 < ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) )
82 41 81 elrpii ⊢ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ+
83 rerpdivcl ⊢ ( ( 2 ∈ ℝ ∧ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℝ+ ) → ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ∈ ℝ )
84 1 82 83 mp2an ⊢ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ∈ ℝ
85 84 a1i ⊢ ( ⊤ → ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ∈ ℝ )
86 rpre ⊢ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ )
87 rpge0 ⊢ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ → 0 ≤ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) )
88 86 87 absidd ⊢ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ → ( abs ‘ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) )
89 26 88 syl ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( abs ‘ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) )
90 89 adantr ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( abs ‘ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) )
91 eqid ⊢ ( ⌊ ‘ ( 𝑥 / 2 ) ) = ( ⌊ ‘ ( 𝑥 / 2 ) )
92 91 chebbnd1lem3 ⊢ ( ( 𝑥 ∈ ℝ ∧ 8 ≤ 𝑥 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( π ‘ 𝑥 ) · ( ( log ‘ 𝑥 ) / 𝑥 ) ) )
93 8 92 sylan ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) < ( ( π ‘ 𝑥 ) · ( ( log ‘ 𝑥 ) / 𝑥 ) ) )
94 1 recni ⊢ 2 ∈ ℂ
95 2ne0 ⊢ 2 ≠ 0
96 41 recni ⊢ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℂ
97 41 81 gt0ne0ii ⊢ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ≠ 0
98 recdiv ⊢ ( ( ( 2 ∈ ℂ ∧ 2 ≠ 0 ) ∧ ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ∈ ℂ ∧ ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ≠ 0 ) ) → ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) = ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) )
99 94 95 96 97 98 mp4an ⊢ ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) = ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 )
100 99 a1i ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) = ( ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) / 2 ) )
101 22 rpcnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 / ( log ‘ 𝑥 ) ) ∈ ℂ )
102 24 nncnd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ∈ ℂ )
103 22 rpne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 / ( log ‘ 𝑥 ) ) ≠ 0 )
104 24 nnne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( π ‘ 𝑥 ) ≠ 0 )
105 101 102 103 104 recdivd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) )
106 102 101 103 divrecd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) / ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( ( π ‘ 𝑥 ) · ( 1 / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) )
107 20 rpcnne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
108 21 rpcnne0d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( log ‘ 𝑥 ) ≠ 0 ) )
109 recdiv ⊢ ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( ( log ‘ 𝑥 ) ∈ ℂ ∧ ( log ‘ 𝑥 ) ≠ 0 ) ) → ( 1 / ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( ( log ‘ 𝑥 ) / 𝑥 ) )
110 107 108 109 syl2anc ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 1 / ( 𝑥 / ( log ‘ 𝑥 ) ) ) = ( ( log ‘ 𝑥 ) / 𝑥 ) )
111 110 oveq2d ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( ( π ‘ 𝑥 ) · ( 1 / ( 𝑥 / ( log ‘ 𝑥 ) ) ) ) = ( ( π ‘ 𝑥 ) · ( ( log ‘ 𝑥 ) / 𝑥 ) ) )
112 105 106 111 3eqtrd ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) → ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( ( π ‘ 𝑥 ) · ( ( log ‘ 𝑥 ) / 𝑥 ) ) )
113 112 adantr ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) = ( ( π ‘ 𝑥 ) · ( ( log ‘ 𝑥 ) / 𝑥 ) ) )
114 93 100 113 3brtr4d ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) < ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) )
115 26 adantr ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ )
116 elrp ⊢ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ ↔ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) )
117 1 41 36 81 divgt0ii ⊢ 0 < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) )
118 ltrec ⊢ ( ( ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∧ ( ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ∈ ℝ ∧ 0 < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ↔ ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) < ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ) )
119 84 117 118 mpanr12 ⊢ ( ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ ∧ 0 < ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ↔ ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) < ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ) )
120 116 119 sylbi ⊢ ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ+ → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ↔ ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) < ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ) )
121 115 120 syl ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ↔ ( 1 / ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) < ( 1 / ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ) )
122 114 121 mpbird ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) )
123 115 rpred ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ )
124 ltle ⊢ ( ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ∈ ℝ ∧ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ∈ ℝ ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ≤ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) )
125 123 84 124 sylancl ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) < ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ≤ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) ) )
126 122 125 mpd ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ≤ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) )
127 90 126 eqbrtrd ⊢ ( ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) → ( abs ‘ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ≤ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) )
128 127 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 2 [,) +∞ ) ∧ 8 ≤ 𝑥 ) ) → ( abs ‘ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ≤ ( 2 / ( ( log ‘ 2 ) − ( 1 / ( 2 · e ) ) ) ) )
129 5 28 30 85 128 elo1d ⊢ ( ⊤ → ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
130 129 mptru ⊢ ( 𝑥 ∈ ( 2 [,) +∞ ) ↦ ( ( 𝑥 / ( log ‘ 𝑥 ) ) / ( π ‘ 𝑥 ) ) ) ∈ 𝑂(1)