Proof of Theorem chebbnd2
Step | Hyp | Ref
| Expression |
1 | | ovex 6577 |
. . . . . 6
⊢
(2[,)+∞) ∈ V |
2 | 1 | a1i 11 |
. . . . 5
⊢ (⊤
→ (2[,)+∞) ∈ V) |
3 | | ovex 6577 |
. . . . . 6
⊢
((θ‘𝑥) /
𝑥) ∈
V |
4 | 3 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / 𝑥) ∈ V) |
5 | | ovex 6577 |
. . . . . 6
⊢
(((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)) ∈ V |
6 | 5 | a1i 11 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)) ∈ V) |
7 | | eqidd 2611 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) = (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥))) |
8 | | simpr 476 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 𝑥 ∈ (2[,)+∞)) |
9 | | 2re 10967 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
10 | | elicopnf 12140 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) |
11 | 9, 10 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
12 | 8, 11 | sylib 207 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥)) |
13 | | chtrpcl 24701 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(θ‘𝑥) ∈
ℝ+) |
14 | 12, 13 | syl 17 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (θ‘𝑥) ∈
ℝ+) |
15 | 14 | rpcnne0d 11757 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) ∈ ℂ ∧ (θ‘𝑥) ≠ 0)) |
16 | | ppinncl 24700 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) |
17 | 12, 16 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (π‘𝑥) ∈ ℕ) |
18 | 17 | nnrpd 11746 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (π‘𝑥) ∈
ℝ+) |
19 | 12 | simpld 474 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 𝑥 ∈ ℝ) |
20 | | 1red 9934 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 ∈ ℝ) |
21 | 9 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 2 ∈ ℝ) |
22 | | 1lt2 11071 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
23 | 22 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 < 2) |
24 | 12 | simprd 478 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 2 ≤ 𝑥) |
25 | 20, 21, 19, 23, 24 | ltletrd 10076 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 < 𝑥) |
26 | 19, 25 | rplogcld 24179 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (log‘𝑥) ∈
ℝ+) |
27 | 18, 26 | rpmulcld 11764 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((π‘𝑥) · (log‘𝑥)) ∈
ℝ+) |
28 | 27 | rpcnne0d 11757 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) ∈ ℂ ∧
((π‘𝑥)
· (log‘𝑥))
≠ 0)) |
29 | | recdiv 10610 |
. . . . . . 7
⊢
((((θ‘𝑥)
∈ ℂ ∧ (θ‘𝑥) ≠ 0) ∧ (((π‘𝑥) · (log‘𝑥)) ∈ ℂ ∧
((π‘𝑥)
· (log‘𝑥))
≠ 0)) → (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) = (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) |
30 | 15, 28, 29 | syl2anc 691 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) = (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) |
31 | 30 | mpteq2dva 4672 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) = (𝑥 ∈ (2[,)+∞) ↦
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)))) |
32 | 2, 4, 6, 7, 31 | offval2 6812 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) = (𝑥 ∈ (2[,)+∞) ↦
(((θ‘𝑥) / 𝑥) ·
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥))))) |
33 | | 0red 9920 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 0 ∈ ℝ) |
34 | | 2pos 10989 |
. . . . . . . . . . 11
⊢ 0 <
2 |
35 | 34 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 0 < 2) |
36 | 33, 21, 19, 35, 24 | ltletrd 10076 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 0 < 𝑥) |
37 | 19, 36 | elrpd 11745 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 𝑥 ∈ ℝ+) |
38 | 37 | rpcnne0d 11757 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
39 | 27 | rpcnd 11750 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((π‘𝑥) · (log‘𝑥)) ∈ ℂ) |
40 | | dmdcan 10614 |
. . . . . . 7
⊢
((((θ‘𝑥)
∈ ℂ ∧ (θ‘𝑥) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((π‘𝑥) · (log‘𝑥)) ∈ ℂ) →
(((θ‘𝑥) / 𝑥) ·
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥))) =
(((π‘𝑥)
· (log‘𝑥)) /
𝑥)) |
41 | 15, 38, 39, 40 | syl3anc 1318 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((θ‘𝑥) / 𝑥) · (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) = (((π‘𝑥) · (log‘𝑥)) / 𝑥)) |
42 | 18 | rpcnd 11750 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (π‘𝑥) ∈ ℂ) |
43 | 26 | rpcnne0d 11757 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0)) |
44 | | divdiv2 10616 |
. . . . . . 7
⊢
(((π‘𝑥) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0)) →
((π‘𝑥) /
(𝑥 / (log‘𝑥))) = (((π‘𝑥) · (log‘𝑥)) / 𝑥)) |
45 | 42, 38, 43, 44 | syl3anc 1318 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((π‘𝑥) / (𝑥 / (log‘𝑥))) = (((π‘𝑥) · (log‘𝑥)) / 𝑥)) |
46 | 41, 45 | eqtr4d 2647 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((θ‘𝑥) / 𝑥) · (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) = ((π‘𝑥) / (𝑥 / (log‘𝑥)))) |
47 | 46 | mpteq2dva 4672 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (((θ‘𝑥) / 𝑥) · (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)))) = (𝑥 ∈ (2[,)+∞) ↦
((π‘𝑥) /
(𝑥 / (log‘𝑥))))) |
48 | 32, 47 | eqtrd 2644 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) = (𝑥 ∈ (2[,)+∞) ↦
((π‘𝑥) /
(𝑥 / (log‘𝑥))))) |
49 | 37 | ex 449 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) → 𝑥
∈ ℝ+)) |
50 | 49 | ssrdv 3574 |
. . . . 5
⊢ (⊤
→ (2[,)+∞) ⊆ ℝ+) |
51 | | chto1ub 24965 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((θ‘𝑥)
/ 𝑥)) ∈
𝑂(1) |
52 | 51 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
53 | 50, 52 | o1res2 14142 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
54 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
55 | 54 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 ∈ ℂ) |
56 | 14, 27 | rpdivcld 11765 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈
ℝ+) |
57 | 56 | rpcnd 11750 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) |
58 | | pnfxr 9971 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
59 | | icossre 12125 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ +∞ ∈ ℝ*) → (2[,)+∞)
⊆ ℝ) |
60 | 9, 58, 59 | mp2an 704 |
. . . . . . . 8
⊢
(2[,)+∞) ⊆ ℝ |
61 | | rlimconst 14123 |
. . . . . . . 8
⊢
(((2[,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1) |
62 | 60, 54, 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 | 56 | rpne0d 11753 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ≠ 0) |
69 | 55, 57, 63, 65, 67, 68 | rlimdiv 14224 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ⇝𝑟 (1 /
1)) |
70 | | rlimo1 14195 |
. . . . 5
⊢ ((𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
⇝𝑟 (1 / 1) → (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
∈ 𝑂(1)) |
71 | 69, 70 | syl 17 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) |
72 | | o1mul 14193 |
. . . 4
⊢ (((𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) → ((𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥)) ∘𝑓
· (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) ∈ 𝑂(1)) |
73 | 53, 71, 72 | syl2anc 691 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∘𝑓 ·
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) ∈ 𝑂(1)) |
74 | 48, 73 | eqeltrrd 2689 |
. 2
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((π‘𝑥) / (𝑥 / (log‘𝑥)))) ∈ 𝑂(1)) |
75 | 74 | trud 1484 |
1
⊢ (𝑥 ∈ (2[,)+∞) ↦
((π‘𝑥) /
(𝑥 / (log‘𝑥)))) ∈
𝑂(1) |