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)