Proof of Theorem chto1lb
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ovexd 7466 | . . . . 5
⊢ (⊤
→ (2[,)+∞) ∈ V) | 
| 2 |  | 2re 12340 | . . . . . . . . . . . 12
⊢ 2 ∈
ℝ | 
| 3 |  | elicopnf 13485 | . . . . . . . . . . . 12
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) | 
| 4 | 2, 3 | ax-mp 5 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) | 
| 5 | 4 | biimpi 216 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) | 
| 6 | 5 | simpld 494 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ) | 
| 7 |  | 0red 11264 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 0
∈ ℝ) | 
| 8 | 2 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 2
∈ ℝ) | 
| 9 |  | 2pos 12369 | . . . . . . . . . . 11
⊢ 0 <
2 | 
| 10 | 9 | a1i 11 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 2) | 
| 11 | 5 | simprd 495 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 2
≤ 𝑥) | 
| 12 | 7, 8, 6, 10, 11 | ltletrd 11421 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 𝑥) | 
| 13 | 6, 12 | elrpd 13074 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ+) | 
| 14 |  | ppinncl 27217 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) | 
| 15 | 14 | nnrpd 13075 | . . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℝ+) | 
| 16 | 5, 15 | syl 17 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℝ+) | 
| 17 |  | 1red 11262 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) → 1
∈ ℝ) | 
| 18 |  | 1lt2 12437 | . . . . . . . . . . . 12
⊢ 1 <
2 | 
| 19 | 18 | a1i 11 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 2) | 
| 20 | 17, 8, 6, 19, 11 | ltletrd 11421 | . . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 𝑥) | 
| 21 | 6, 20 | rplogcld 26671 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ∈
ℝ+) | 
| 22 | 16, 21 | rpmulcld 13093 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
∈ ℝ+) | 
| 23 | 13, 22 | rpdivcld 13094 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 /
((π‘𝑥)
· (log‘𝑥)))
∈ ℝ+) | 
| 24 | 23 | rpcnd 13079 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 /
((π‘𝑥)
· (log‘𝑥)))
∈ ℂ) | 
| 25 | 24 | adantl 481 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (𝑥 / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) | 
| 26 |  | chtrpcl 27218 | . . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(θ‘𝑥) ∈
ℝ+) | 
| 27 | 5, 26 | syl 17 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℝ+) | 
| 28 | 22, 27 | rpdivcld 13094 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)) ∈
ℝ+) | 
| 29 | 28 | rpcnd 13079 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)) ∈
ℂ) | 
| 30 | 29 | adantl 481 | . . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)) ∈ ℂ) | 
| 31 | 6 | recnd 11289 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℂ) | 
| 32 | 21 | rpcnd 13079 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ∈
ℂ) | 
| 33 | 16 | rpcnd 13079 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℂ) | 
| 34 | 21 | rpne0d 13082 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ≠
0) | 
| 35 | 16 | rpne0d 13082 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥) ≠
0) | 
| 36 | 31, 32, 33, 34, 35 | divdiv1d 12074 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 / (log‘𝑥)) / (π‘𝑥)) = (𝑥 / ((log‘𝑥) · (π‘𝑥)))) | 
| 37 | 32, 33 | mulcomd 11282 | . . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
((log‘𝑥) ·
(π‘𝑥)) =
((π‘𝑥)
· (log‘𝑥))) | 
| 38 | 37 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 / ((log‘𝑥) ·
(π‘𝑥))) =
(𝑥 /
((π‘𝑥)
· (log‘𝑥)))) | 
| 39 | 36, 38 | eqtrd 2777 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 / (log‘𝑥)) / (π‘𝑥)) = (𝑥 / ((π‘𝑥) · (log‘𝑥)))) | 
| 40 | 39 | mpteq2ia 5245 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) = (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / ((π‘𝑥) · (log‘𝑥)))) | 
| 41 | 40 | a1i 11 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥))) =
(𝑥 ∈ (2[,)+∞)
↦ (𝑥 /
((π‘𝑥)
· (log‘𝑥))))) | 
| 42 | 27 | rpcnd 13079 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℂ) | 
| 43 | 22 | rpcnd 13079 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
∈ ℂ) | 
| 44 | 27 | rpne0d 13082 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ≠
0) | 
| 45 | 22 | rpne0d 13082 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
≠ 0) | 
| 46 | 42, 43, 44, 45 | recdivd 12060 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) → (1
/ ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))) =
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥))) | 
| 47 | 46 | mpteq2ia 5245 | . . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
= (𝑥 ∈ (2[,)+∞)
↦ (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) | 
| 48 | 47 | a1i 11 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) = (𝑥 ∈ (2[,)+∞) ↦
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)))) | 
| 49 | 1, 25, 30, 41, 48 | offval2 7717 | . . . 4
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘f · (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
= (𝑥 ∈ (2[,)+∞)
↦ ((𝑥 /
((π‘𝑥)
· (log‘𝑥)))
· (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))))) | 
| 50 | 31, 43, 42, 45, 44 | dmdcan2d 12073 | . . . . 5
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 /
((π‘𝑥)
· (log‘𝑥)))
· (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) = (𝑥 / (θ‘𝑥))) | 
| 51 | 50 | mpteq2ia 5245 | . . . 4
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 /
((π‘𝑥)
· (log‘𝑥)))
· (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)))) = (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) | 
| 52 | 49, 51 | eqtrdi 2793 | . . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘f · (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
= (𝑥 ∈ (2[,)+∞)
↦ (𝑥 /
(θ‘𝑥)))) | 
| 53 |  | chebbnd1 27516 | . . . 4
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈
𝑂(1) | 
| 54 |  | ax-1cn 11213 | . . . . . . 7
⊢ 1 ∈
ℂ | 
| 55 | 54 | a1i 11 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 ∈ ℂ) | 
| 56 | 27, 22 | rpdivcld 13094 | . . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
∈ ℝ+) | 
| 57 | 56 | adantl 481 | . . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈
ℝ+) | 
| 58 | 57 | rpcnd 13079 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) | 
| 59 | 6 | ssriv 3987 | . . . . . . . 8
⊢
(2[,)+∞) ⊆ ℝ | 
| 60 |  | rlimconst 15580 | . . . . . . . 8
⊢
(((2[,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1) | 
| 61 | 59, 54, 60 | mp2an 692 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1 | 
| 62 | 61 | a1i 11 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ 1) ⇝𝑟 1) | 
| 63 |  | chtppilim 27519 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
⇝𝑟 1 | 
| 64 | 63 | a1i 11 | . . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟
1) | 
| 65 |  | ax-1ne0 11224 | . . . . . . 7
⊢ 1 ≠
0 | 
| 66 | 65 | a1i 11 | . . . . . 6
⊢ (⊤
→ 1 ≠ 0) | 
| 67 | 56 | rpne0d 13082 | . . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
≠ 0) | 
| 68 | 67 | adantl 481 | . . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ≠ 0) | 
| 69 | 55, 58, 62, 64, 66, 68 | rlimdiv 15682 | . . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ⇝𝑟 (1 /
1)) | 
| 70 |  | rlimo1 15653 | . . . . 5
⊢ ((𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
⇝𝑟 (1 / 1) → (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
∈ 𝑂(1)) | 
| 71 | 69, 70 | syl 17 | . . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) | 
| 72 |  | o1mul 15651 | . . . 4
⊢ (((𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) ∧
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) → ((𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘f ·
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) ∈ 𝑂(1)) | 
| 73 | 53, 71, 72 | sylancr 587 | . . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘f · (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
∈ 𝑂(1)) | 
| 74 | 52, 73 | eqeltrrd 2842 | . 2
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (𝑥 /
(θ‘𝑥))) ∈
𝑂(1)) | 
| 75 | 74 | mptru 1547 | 1
⊢ (𝑥 ∈ (2[,)+∞) ↦
(𝑥 / (θ‘𝑥))) ∈
𝑂(1) |