Proof of Theorem chebbnd1
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2re 12340 | . . . . 5
⊢ 2 ∈
ℝ | 
| 2 |  | pnfxr 11315 | . . . . 5
⊢ +∞
∈ ℝ* | 
| 3 |  | icossre 13468 | . . . . 5
⊢ ((2
∈ ℝ ∧ +∞ ∈ ℝ*) → (2[,)+∞)
⊆ ℝ) | 
| 4 | 1, 2, 3 | mp2an 692 | . . . 4
⊢
(2[,)+∞) ⊆ ℝ | 
| 5 | 4 | a1i 11 | . . 3
⊢ (⊤
→ (2[,)+∞) ⊆ ℝ) | 
| 6 |  | elicopnf 13485 | . . . . . . . . . 10
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) | 
| 7 | 1, 6 | ax-mp 5 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) | 
| 8 | 7 | simplbi 497 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ) | 
| 9 |  | 0red 11264 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 0
∈ ℝ) | 
| 10 |  | 1re 11261 | . . . . . . . . . 10
⊢ 1 ∈
ℝ | 
| 11 | 10 | a1i 11 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 1
∈ ℝ) | 
| 12 |  | 0lt1 11785 | . . . . . . . . . 10
⊢ 0 <
1 | 
| 13 | 12 | a1i 11 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 1) | 
| 14 | 1 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 2
∈ ℝ) | 
| 15 |  | 1lt2 12437 | . . . . . . . . . . 11
⊢ 1 <
2 | 
| 16 | 15 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 2) | 
| 17 | 7 | simprbi 496 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 2
≤ 𝑥) | 
| 18 | 11, 14, 8, 16, 17 | ltletrd 11421 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 𝑥) | 
| 19 | 9, 11, 8, 13, 18 | lttrd 11422 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 𝑥) | 
| 20 | 8, 19 | elrpd 13074 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ+) | 
| 21 | 8, 18 | rplogcld 26671 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ∈
ℝ+) | 
| 22 | 20, 21 | rpdivcld 13094 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 / (log‘𝑥)) ∈
ℝ+) | 
| 23 |  | ppinncl 27217 | . . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) | 
| 24 | 7, 23 | sylbi 217 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℕ) | 
| 25 | 24 | nnrpd 13075 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℝ+) | 
| 26 | 22, 25 | rpdivcld 13094 | . . . . 5
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈
ℝ+) | 
| 27 | 26 | rpcnd 13079 | . . . 4
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈
ℂ) | 
| 28 | 27 | adantl 481 | . . 3
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℂ) | 
| 29 |  | 8re 12362 | . . . 4
⊢ 8 ∈
ℝ | 
| 30 | 29 | a1i 11 | . . 3
⊢ (⊤
→ 8 ∈ ℝ) | 
| 31 |  | 2rp 13039 | . . . . . . . 8
⊢ 2 ∈
ℝ+ | 
| 32 |  | relogcl 26617 | . . . . . . . 8
⊢ (2 ∈
ℝ+ → (log‘2) ∈ ℝ) | 
| 33 | 31, 32 | ax-mp 5 | . . . . . . 7
⊢
(log‘2) ∈ ℝ | 
| 34 |  | ere 16125 | . . . . . . . . 9
⊢ e ∈
ℝ | 
| 35 | 1, 34 | remulcli 11277 | . . . . . . . 8
⊢ (2
· e) ∈ ℝ | 
| 36 |  | 2pos 12369 | . . . . . . . . . 10
⊢ 0 <
2 | 
| 37 |  | epos 16243 | . . . . . . . . . 10
⊢ 0 <
e | 
| 38 | 1, 34, 36, 37 | mulgt0ii 11394 | . . . . . . . . 9
⊢ 0 < (2
· e) | 
| 39 | 35, 38 | gt0ne0ii 11799 | . . . . . . . 8
⊢ (2
· e) ≠ 0 | 
| 40 | 35, 39 | rereccli 12032 | . . . . . . 7
⊢ (1 / (2
· e)) ∈ ℝ | 
| 41 | 33, 40 | resubcli 11571 | . . . . . 6
⊢
((log‘2) − (1 / (2 · e))) ∈
ℝ | 
| 42 |  | 2t1e2 12429 | . . . . . . . . . 10
⊢ (2
· 1) = 2 | 
| 43 |  | egt2lt3 16242 | . . . . . . . . . . . . 13
⊢ (2 < e
∧ e < 3) | 
| 44 | 43 | simpli 483 | . . . . . . . . . . . 12
⊢ 2 <
e | 
| 45 | 10, 1, 34 | lttri 11387 | . . . . . . . . . . . 12
⊢ ((1 <
2 ∧ 2 < e) → 1 < e) | 
| 46 | 15, 44, 45 | mp2an 692 | . . . . . . . . . . 11
⊢ 1 <
e | 
| 47 | 10, 34, 1 | ltmul2i 12189 | . . . . . . . . . . . 12
⊢ (0 < 2
→ (1 < e ↔ (2 · 1) < (2 · e))) | 
| 48 | 36, 47 | ax-mp 5 | . . . . . . . . . . 11
⊢ (1 < e
↔ (2 · 1) < (2 · e)) | 
| 49 | 46, 48 | mpbi 230 | . . . . . . . . . 10
⊢ (2
· 1) < (2 · e) | 
| 50 | 42, 49 | eqbrtrri 5166 | . . . . . . . . 9
⊢ 2 < (2
· e) | 
| 51 | 1, 35, 36, 38 | ltrecii 12184 | . . . . . . . . 9
⊢ (2 <
(2 · e) ↔ (1 / (2 · e)) < (1 / 2)) | 
| 52 | 50, 51 | mpbi 230 | . . . . . . . 8
⊢ (1 / (2
· e)) < (1 / 2) | 
| 53 | 43 | simpri 485 | . . . . . . . . . . . 12
⊢ e <
3 | 
| 54 |  | 3lt4 12440 | . . . . . . . . . . . 12
⊢ 3 <
4 | 
| 55 |  | 3re 12346 | . . . . . . . . . . . . 13
⊢ 3 ∈
ℝ | 
| 56 |  | 4re 12350 | . . . . . . . . . . . . 13
⊢ 4 ∈
ℝ | 
| 57 | 34, 55, 56 | lttri 11387 | . . . . . . . . . . . 12
⊢ ((e <
3 ∧ 3 < 4) → e < 4) | 
| 58 | 53, 54, 57 | mp2an 692 | . . . . . . . . . . 11
⊢ e <
4 | 
| 59 |  | epr 16244 | . . . . . . . . . . . 12
⊢ e ∈
ℝ+ | 
| 60 |  | 4pos 12373 | . . . . . . . . . . . . 13
⊢ 0 <
4 | 
| 61 | 56, 60 | elrpii 13037 | . . . . . . . . . . . 12
⊢ 4 ∈
ℝ+ | 
| 62 |  | logltb 26642 | . . . . . . . . . . . 12
⊢ ((e
∈ ℝ+ ∧ 4 ∈ ℝ+) → (e < 4
↔ (log‘e) < (log‘4))) | 
| 63 | 59, 61, 62 | mp2an 692 | . . . . . . . . . . 11
⊢ (e < 4
↔ (log‘e) < (log‘4)) | 
| 64 | 58, 63 | mpbi 230 | . . . . . . . . . 10
⊢
(log‘e) < (log‘4) | 
| 65 |  | loge 26628 | . . . . . . . . . 10
⊢
(log‘e) = 1 | 
| 66 |  | sq2 14236 | . . . . . . . . . . . 12
⊢
(2↑2) = 4 | 
| 67 | 66 | fveq2i 6909 | . . . . . . . . . . 11
⊢
(log‘(2↑2)) = (log‘4) | 
| 68 |  | 2z 12649 | . . . . . . . . . . . 12
⊢ 2 ∈
ℤ | 
| 69 |  | relogexp 26638 | . . . . . . . . . . . 12
⊢ ((2
∈ ℝ+ ∧ 2 ∈ ℤ) →
(log‘(2↑2)) = (2 · (log‘2))) | 
| 70 | 31, 68, 69 | mp2an 692 | . . . . . . . . . . 11
⊢
(log‘(2↑2)) = (2 · (log‘2)) | 
| 71 | 67, 70 | eqtr3i 2767 | . . . . . . . . . 10
⊢
(log‘4) = (2 · (log‘2)) | 
| 72 | 64, 65, 71 | 3brtr3i 5172 | . . . . . . . . 9
⊢ 1 < (2
· (log‘2)) | 
| 73 | 1, 36 | pm3.2i 470 | . . . . . . . . . 10
⊢ (2 ∈
ℝ ∧ 0 < 2) | 
| 74 |  | ltdivmul 12143 | . . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ (log‘2) ∈ ℝ ∧ (2 ∈ ℝ ∧
0 < 2)) → ((1 / 2) < (log‘2) ↔ 1 < (2 ·
(log‘2)))) | 
| 75 | 10, 33, 73, 74 | mp3an 1463 | . . . . . . . . 9
⊢ ((1 / 2)
< (log‘2) ↔ 1 < (2 · (log‘2))) | 
| 76 | 72, 75 | mpbir 231 | . . . . . . . 8
⊢ (1 / 2)
< (log‘2) | 
| 77 |  | halfre 12480 | . . . . . . . . 9
⊢ (1 / 2)
∈ ℝ | 
| 78 | 40, 77, 33 | lttri 11387 | . . . . . . . 8
⊢ (((1 / (2
· e)) < (1 / 2) ∧ (1 / 2) < (log‘2)) → (1 / (2
· e)) < (log‘2)) | 
| 79 | 52, 76, 78 | mp2an 692 | . . . . . . 7
⊢ (1 / (2
· e)) < (log‘2) | 
| 80 | 40, 33 | posdifi 11813 | . . . . . . 7
⊢ ((1 / (2
· e)) < (log‘2) ↔ 0 < ((log‘2) − (1 / (2
· e)))) | 
| 81 | 79, 80 | mpbi 230 | . . . . . 6
⊢ 0 <
((log‘2) − (1 / (2 · e))) | 
| 82 | 41, 81 | elrpii 13037 | . . . . 5
⊢
((log‘2) − (1 / (2 · e))) ∈
ℝ+ | 
| 83 |  | rerpdivcl 13065 | . . . . 5
⊢ ((2
∈ ℝ ∧ ((log‘2) − (1 / (2 · e))) ∈
ℝ+) → (2 / ((log‘2) − (1 / (2 · e))))
∈ ℝ) | 
| 84 | 1, 82, 83 | mp2an 692 | . . . 4
⊢ (2 /
((log‘2) − (1 / (2 · e)))) ∈ ℝ | 
| 85 | 84 | a1i 11 | . . 3
⊢ (⊤
→ (2 / ((log‘2) − (1 / (2 · e)))) ∈
ℝ) | 
| 86 |  | rpre 13043 | . . . . . . . 8
⊢ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ+ → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ) | 
| 87 |  | rpge0 13048 | . . . . . . . 8
⊢ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ+ → 0 ≤
((𝑥 / (log‘𝑥)) / (π‘𝑥))) | 
| 88 | 86, 87 | absidd 15461 | . . . . . . 7
⊢ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ+ →
(abs‘((𝑥 /
(log‘𝑥)) /
(π‘𝑥))) =
((𝑥 / (log‘𝑥)) / (π‘𝑥))) | 
| 89 | 26, 88 | syl 17 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(abs‘((𝑥 /
(log‘𝑥)) /
(π‘𝑥))) =
((𝑥 / (log‘𝑥)) / (π‘𝑥))) | 
| 90 | 89 | adantr 480 | . . . . 5
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) →
(abs‘((𝑥 /
(log‘𝑥)) /
(π‘𝑥))) =
((𝑥 / (log‘𝑥)) / (π‘𝑥))) | 
| 91 |  | eqid 2737 | . . . . . . . . . 10
⊢
(⌊‘(𝑥 /
2)) = (⌊‘(𝑥 /
2)) | 
| 92 | 91 | chebbnd1lem3 27515 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 8 ≤
𝑥) → (((log‘2)
− (1 / (2 · e))) / 2) < ((π‘𝑥) · ((log‘𝑥) / 𝑥))) | 
| 93 | 8, 92 | sylan 580 | . . . . . . . 8
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) →
(((log‘2) − (1 / (2 · e))) / 2) <
((π‘𝑥)
· ((log‘𝑥) /
𝑥))) | 
| 94 | 1 | recni 11275 | . . . . . . . . . 10
⊢ 2 ∈
ℂ | 
| 95 |  | 2ne0 12370 | . . . . . . . . . 10
⊢ 2 ≠
0 | 
| 96 | 41 | recni 11275 | . . . . . . . . . 10
⊢
((log‘2) − (1 / (2 · e))) ∈
ℂ | 
| 97 | 41, 81 | gt0ne0ii 11799 | . . . . . . . . . 10
⊢
((log‘2) − (1 / (2 · e))) ≠ 0 | 
| 98 |  | recdiv 11973 | . . . . . . . . . 10
⊢ (((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 693 | . . . . . . . . 9
⊢ (1 / (2 /
((log‘2) − (1 / (2 · e))))) = (((log‘2) − (1 /
(2 · e))) / 2) | 
| 100 | 99 | a1i 11 | . . . . . . . 8
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → (1 / (2 /
((log‘2) − (1 / (2 · e))))) = (((log‘2) − (1 /
(2 · e))) / 2)) | 
| 101 | 22 | rpcnd 13079 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 / (log‘𝑥)) ∈
ℂ) | 
| 102 | 24 | nncnd 12282 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℂ) | 
| 103 | 22 | rpne0d 13082 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 / (log‘𝑥)) ≠ 0) | 
| 104 | 24 | nnne0d 12316 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥) ≠
0) | 
| 105 | 101, 102,
103, 104 | recdivd 12060 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → (1
/ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) = ((π‘𝑥) / (𝑥 / (log‘𝑥)))) | 
| 106 | 102, 101,
103 | divrecd 12046 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥) /
(𝑥 / (log‘𝑥))) = ((π‘𝑥) · (1 / (𝑥 / (log‘𝑥))))) | 
| 107 | 20 | rpcnne0d 13086 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) | 
| 108 | 21 | rpcnne0d 13086 | . . . . . . . . . . . 12
⊢ (𝑥 ∈ (2[,)+∞) →
((log‘𝑥) ∈
ℂ ∧ (log‘𝑥)
≠ 0)) | 
| 109 |  | recdiv 11973 | . . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((log‘𝑥) ∈ ℂ ∧
(log‘𝑥) ≠ 0))
→ (1 / (𝑥 /
(log‘𝑥))) =
((log‘𝑥) / 𝑥)) | 
| 110 | 107, 108,
109 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) → (1
/ (𝑥 / (log‘𝑥))) = ((log‘𝑥) / 𝑥)) | 
| 111 | 110 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (1 / (𝑥 /
(log‘𝑥)))) =
((π‘𝑥)
· ((log‘𝑥) /
𝑥))) | 
| 112 | 105, 106,
111 | 3eqtrd 2781 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → (1
/ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) = ((π‘𝑥) · ((log‘𝑥) / 𝑥))) | 
| 113 | 112 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → (1 / ((𝑥 / (log‘𝑥)) / (π‘𝑥))) = ((π‘𝑥) · ((log‘𝑥) / 𝑥))) | 
| 114 | 93, 100, 113 | 3brtr4d 5175 | . . . . . . 7
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → (1 / (2 /
((log‘2) − (1 / (2 · e))))) < (1 / ((𝑥 / (log‘𝑥)) / (π‘𝑥)))) | 
| 115 | 26 | adantr 480 | . . . . . . . 8
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈
ℝ+) | 
| 116 |  | elrp 13036 | . . . . . . . . 9
⊢ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ+ ↔ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ ∧ 0 < ((𝑥 / (log‘𝑥)) / (π‘𝑥)))) | 
| 117 | 1, 41, 36, 81 | divgt0ii 12185 | . . . . . . . . . 10
⊢ 0 < (2
/ ((log‘2) − (1 / (2 · e)))) | 
| 118 |  | ltrec 12150 | . . . . . . . . . 10
⊢
(((((𝑥 /
(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 705 | . . . . . . . . 9
⊢ ((((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ ∧ 0 < ((𝑥 / (log‘𝑥)) / (π‘𝑥))) → (((𝑥 / (log‘𝑥)) / (π‘𝑥)) < (2 / ((log‘2) − (1 / (2
· e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e)))))
< (1 / ((𝑥 /
(log‘𝑥)) /
(π‘𝑥))))) | 
| 120 | 116, 119 | sylbi 217 | . . . . . . . 8
⊢ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ+ → (((𝑥 / (log‘𝑥)) / (π‘𝑥)) < (2 / ((log‘2) − (1 / (2
· e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e)))))
< (1 / ((𝑥 /
(log‘𝑥)) /
(π‘𝑥))))) | 
| 121 | 115, 120 | syl 17 | . . . . . . 7
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → (((𝑥 / (log‘𝑥)) / (π‘𝑥)) < (2 / ((log‘2) − (1 / (2
· e)))) ↔ (1 / (2 / ((log‘2) − (1 / (2 · e)))))
< (1 / ((𝑥 /
(log‘𝑥)) /
(π‘𝑥))))) | 
| 122 | 114, 121 | mpbird 257 | . . . . . 6
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) < (2 / ((log‘2) − (1 / (2
· e))))) | 
| 123 | 115 | rpred 13077 | . . . . . . 7
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈ ℝ) | 
| 124 |  | ltle 11349 | . . . . . . 7
⊢ ((((𝑥 / (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 586 | . . . . . 6
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → (((𝑥 / (log‘𝑥)) / (π‘𝑥)) < (2 / ((log‘2) − (1 / (2
· e)))) → ((𝑥 /
(log‘𝑥)) /
(π‘𝑥)) ≤
(2 / ((log‘2) − (1 / (2 · e)))))) | 
| 126 | 122, 125 | mpd 15 | . . . . 5
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ≤ (2 / ((log‘2) − (1 / (2
· e))))) | 
| 127 | 90, 126 | eqbrtrd 5165 | . . . 4
⊢ ((𝑥 ∈ (2[,)+∞) ∧ 8
≤ 𝑥) →
(abs‘((𝑥 /
(log‘𝑥)) /
(π‘𝑥)))
≤ (2 / ((log‘2) − (1 / (2 · e))))) | 
| 128 | 127 | adantl 481 | . . 3
⊢
((⊤ ∧ (𝑥
∈ (2[,)+∞) ∧ 8 ≤ 𝑥)) → (abs‘((𝑥 / (log‘𝑥)) / (π‘𝑥))) ≤ (2 / ((log‘2) − (1 / (2
· e))))) | 
| 129 | 5, 28, 30, 85, 128 | elo1d 15572 | . 2
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∈ 𝑂(1)) | 
| 130 | 129 | mptru 1547 | 1
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈
𝑂(1) |