Proof of Theorem chto1lb
Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . . 6
⊢
(2[,)+∞) ∈ V |
2 | 1 | a1i 11 |
. . . . 5
⊢ (⊤
→ (2[,)+∞) ∈ V) |
3 | | 2re 10967 |
. . . . . . . . . . . 12
⊢ 2 ∈
ℝ |
4 | | elicopnf 12140 |
. . . . . . . . . . . 12
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
6 | 5 | biimpi 205 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
7 | 6 | simpld 474 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ) |
8 | | 0red 9920 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 0
∈ ℝ) |
9 | 3 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 2
∈ ℝ) |
10 | | 2pos 10989 |
. . . . . . . . . . 11
⊢ 0 <
2 |
11 | 10 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 2) |
12 | 6 | simprd 478 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 2
≤ 𝑥) |
13 | 8, 9, 7, 11, 12 | ltletrd 10076 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 𝑥) |
14 | 7, 13 | elrpd 11745 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ+) |
15 | | ppinncl 24700 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) |
16 | 15 | nnrpd 11746 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℝ+) |
17 | 6, 16 | syl 17 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℝ+) |
18 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) → 1
∈ ℝ) |
19 | | 1lt2 11071 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 2) |
21 | 18, 9, 7, 20, 12 | ltletrd 10076 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) → 1
< 𝑥) |
22 | 7, 21 | rplogcld 24179 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ∈
ℝ+) |
23 | 17, 22 | rpmulcld 11764 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
∈ ℝ+) |
24 | 14, 23 | rpdivcld 11765 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 /
((π‘𝑥)
· (log‘𝑥)))
∈ ℝ+) |
25 | 24 | rpcnd 11750 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 /
((π‘𝑥)
· (log‘𝑥)))
∈ ℂ) |
26 | 25 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (𝑥 / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) |
27 | | chtrpcl 24701 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(θ‘𝑥) ∈
ℝ+) |
28 | 6, 27 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℝ+) |
29 | 23, 28 | rpdivcld 11765 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)) ∈
ℝ+) |
30 | 29 | rpcnd 11750 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)) ∈
ℂ) |
31 | 30 | adantl 481 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)) ∈ ℂ) |
32 | 7 | recnd 9947 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℂ) |
33 | 22 | rpcnd 11750 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ∈
ℂ) |
34 | 17 | rpcnd 11750 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥)
∈ ℂ) |
35 | 22 | rpne0d 11753 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(log‘𝑥) ≠
0) |
36 | 17 | rpne0d 11753 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
(π‘𝑥) ≠
0) |
37 | 32, 33, 34, 35, 36 | divdiv1d 10711 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 / (log‘𝑥)) / (π‘𝑥)) = (𝑥 / ((log‘𝑥) · (π‘𝑥)))) |
38 | 33, 34 | mulcomd 9940 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
((log‘𝑥) ·
(π‘𝑥)) =
((π‘𝑥)
· (log‘𝑥))) |
39 | 38 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 / ((log‘𝑥) ·
(π‘𝑥))) =
(𝑥 /
((π‘𝑥)
· (log‘𝑥)))) |
40 | 37, 39 | eqtrd 2644 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 / (log‘𝑥)) / (π‘𝑥)) = (𝑥 / ((π‘𝑥) · (log‘𝑥)))) |
41 | 40 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) = (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / ((π‘𝑥) · (log‘𝑥)))) |
42 | 41 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥))) =
(𝑥 ∈ (2[,)+∞)
↦ (𝑥 /
((π‘𝑥)
· (log‘𝑥))))) |
43 | 28 | rpcnd 11750 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℂ) |
44 | 23 | rpcnd 11750 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
∈ ℂ) |
45 | 28 | rpne0d 11753 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ≠
0) |
46 | 23 | rpne0d 11753 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((π‘𝑥)
· (log‘𝑥))
≠ 0) |
47 | 43, 44, 45, 46 | recdivd 10697 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) → (1
/ ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))) =
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥))) |
48 | 47 | mpteq2ia 4668 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
= (𝑥 ∈ (2[,)+∞)
↦ (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) |
49 | 48 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) = (𝑥 ∈ (2[,)+∞) ↦
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)))) |
50 | 2, 26, 31, 42, 49 | offval2 6812 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘𝑓 · (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
= (𝑥 ∈ (2[,)+∞)
↦ ((𝑥 /
((π‘𝑥)
· (log‘𝑥)))
· (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))))) |
51 | 32, 44, 43, 46, 45 | dmdcan2d 10710 |
. . . . 5
⊢ (𝑥 ∈ (2[,)+∞) →
((𝑥 /
((π‘𝑥)
· (log‘𝑥)))
· (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) = (𝑥 / (θ‘𝑥))) |
52 | 51 | mpteq2ia 4668 |
. . . 4
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 /
((π‘𝑥)
· (log‘𝑥)))
· (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)))) = (𝑥 ∈ (2[,)+∞) ↦ (𝑥 / (θ‘𝑥))) |
53 | 50, 52 | syl6eq 2660 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘𝑓 · (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
= (𝑥 ∈ (2[,)+∞)
↦ (𝑥 /
(θ‘𝑥)))) |
54 | | chebbnd1 24961 |
. . . 4
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈
𝑂(1) |
55 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
56 | 55 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 ∈ ℂ) |
57 | 28, 23 | rpdivcld 11765 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
∈ ℝ+) |
58 | 57 | adantl 481 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈
ℝ+) |
59 | 58 | rpcnd 11750 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) |
60 | 7 | ssriv 3572 |
. . . . . . . 8
⊢
(2[,)+∞) ⊆ ℝ |
61 | | rlimconst 14123 |
. . . . . . . 8
⊢
(((2[,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1) |
62 | 60, 55, 61 | mp2an 704 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1 |
63 | 62 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ 1) ⇝𝑟 1) |
64 | | chtppilim 24964 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
⇝𝑟 1 |
65 | 64 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟
1) |
66 | | ax-1ne0 9884 |
. . . . . . 7
⊢ 1 ≠
0 |
67 | 66 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 1 ≠ 0) |
68 | 57 | rpne0d 11753 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))
≠ 0) |
69 | 68 | adantl 481 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ≠ 0) |
70 | 56, 59, 63, 65, 67, 69 | rlimdiv 14224 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ⇝𝑟 (1 /
1)) |
71 | | rlimo1 14195 |
. . . . 5
⊢ ((𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
⇝𝑟 (1 / 1) → (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
∈ 𝑂(1)) |
72 | 70, 71 | syl 17 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) |
73 | | o1mul 14193 |
. . . 4
⊢ (((𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) ∧
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) → ((𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘𝑓
· (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) ∈ 𝑂(1)) |
74 | 54, 72, 73 | sylancr 694 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘𝑓 · (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
∈ 𝑂(1)) |
75 | 53, 74 | eqeltrrd 2689 |
. 2
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (𝑥 /
(θ‘𝑥))) ∈
𝑂(1)) |
76 | 75 | trud 1484 |
1
⊢ (𝑥 ∈ (2[,)+∞) ↦
(𝑥 / (θ‘𝑥))) ∈
𝑂(1) |