Proof of Theorem chebbnd2
Step | Hyp | Ref
| Expression |
1 | | ovexd 7248 |
. . . . 5
⊢ (⊤
→ (2[,)+∞) ∈ V) |
2 | | ovexd 7248 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / 𝑥) ∈ V) |
3 | | ovexd 7248 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)) ∈ V) |
4 | | eqidd 2738 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) = (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥))) |
5 | | simpr 488 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 𝑥 ∈ (2[,)+∞)) |
6 | | 2re 11904 |
. . . . . . . . . . 11
⊢ 2 ∈
ℝ |
7 | | elicopnf 13033 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
9 | 5, 8 | sylib 221 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (𝑥 ∈ ℝ ∧ 2 ≤ 𝑥)) |
10 | | chtrpcl 26057 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(θ‘𝑥) ∈
ℝ+) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (θ‘𝑥) ∈
ℝ+) |
12 | 11 | rpcnne0d 12637 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) ∈ ℂ ∧ (θ‘𝑥) ≠ 0)) |
13 | | ppinncl 26056 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) |
14 | 9, 13 | syl 17 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (π‘𝑥) ∈ ℕ) |
15 | 14 | nnrpd 12626 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (π‘𝑥) ∈
ℝ+) |
16 | 9 | simpld 498 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 𝑥 ∈ ℝ) |
17 | | 1red 10834 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 ∈ ℝ) |
18 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 2 ∈ ℝ) |
19 | | 1lt2 12001 |
. . . . . . . . . . . 12
⊢ 1 <
2 |
20 | 19 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 < 2) |
21 | 9 | simprd 499 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 2 ≤ 𝑥) |
22 | 17, 18, 16, 20, 21 | ltletrd 10992 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 < 𝑥) |
23 | 16, 22 | rplogcld 25517 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (log‘𝑥) ∈
ℝ+) |
24 | 15, 23 | rpmulcld 12644 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((π‘𝑥) · (log‘𝑥)) ∈
ℝ+) |
25 | 24 | rpcnne0d 12637 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((π‘𝑥) · (log‘𝑥)) ∈ ℂ ∧
((π‘𝑥)
· (log‘𝑥))
≠ 0)) |
26 | | recdiv 11538 |
. . . . . . 7
⊢
((((θ‘𝑥)
∈ ℂ ∧ (θ‘𝑥) ≠ 0) ∧ (((π‘𝑥) · (log‘𝑥)) ∈ ℂ ∧
((π‘𝑥)
· (log‘𝑥))
≠ 0)) → (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) = (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) |
27 | 12, 25, 26 | syl2anc 587 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) = (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) |
28 | 27 | mpteq2dva 5150 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) = (𝑥 ∈ (2[,)+∞) ↦
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥)))) |
29 | 1, 2, 3, 4, 28 | offval2 7488 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
= (𝑥 ∈ (2[,)+∞)
↦ (((θ‘𝑥)
/ 𝑥) ·
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥))))) |
30 | | 0red 10836 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 0 ∈ ℝ) |
31 | | 2pos 11933 |
. . . . . . . . . . 11
⊢ 0 <
2 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 0 < 2) |
33 | 30, 18, 16, 32, 21 | ltletrd 10992 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 0 < 𝑥) |
34 | 16, 33 | elrpd 12625 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 𝑥 ∈ ℝ+) |
35 | 34 | rpcnne0d 12637 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
36 | 24 | rpcnd 12630 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((π‘𝑥) · (log‘𝑥)) ∈ ℂ) |
37 | | dmdcan 11542 |
. . . . . . 7
⊢
((((θ‘𝑥)
∈ ℂ ∧ (θ‘𝑥) ≠ 0) ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((π‘𝑥) · (log‘𝑥)) ∈ ℂ) →
(((θ‘𝑥) / 𝑥) ·
(((π‘𝑥)
· (log‘𝑥)) /
(θ‘𝑥))) =
(((π‘𝑥)
· (log‘𝑥)) /
𝑥)) |
38 | 12, 35, 36, 37 | syl3anc 1373 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((θ‘𝑥) / 𝑥) · (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) = (((π‘𝑥) · (log‘𝑥)) / 𝑥)) |
39 | 15 | rpcnd 12630 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (π‘𝑥) ∈ ℂ) |
40 | 23 | rpcnne0d 12637 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0)) |
41 | | divdiv2 11544 |
. . . . . . 7
⊢
(((π‘𝑥) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ ((log‘𝑥) ∈ ℂ ∧ (log‘𝑥) ≠ 0)) →
((π‘𝑥) /
(𝑥 / (log‘𝑥))) = (((π‘𝑥) · (log‘𝑥)) / 𝑥)) |
42 | 39, 35, 40, 41 | syl3anc 1373 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((π‘𝑥) / (𝑥 / (log‘𝑥))) = (((π‘𝑥) · (log‘𝑥)) / 𝑥)) |
43 | 38, 42 | eqtr4d 2780 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → (((θ‘𝑥) / 𝑥) · (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥))) = ((π‘𝑥) / (𝑥 / (log‘𝑥)))) |
44 | 43 | mpteq2dva 5150 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (((θ‘𝑥) / 𝑥) · (((π‘𝑥) · (log‘𝑥)) / (θ‘𝑥)))) = (𝑥 ∈ (2[,)+∞) ↦
((π‘𝑥) /
(𝑥 / (log‘𝑥))))) |
45 | 29, 44 | eqtrd 2777 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
= (𝑥 ∈ (2[,)+∞)
↦ ((π‘𝑥) / (𝑥 / (log‘𝑥))))) |
46 | 34 | ex 416 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) → 𝑥
∈ ℝ+)) |
47 | 46 | ssrdv 3907 |
. . . . 5
⊢ (⊤
→ (2[,)+∞) ⊆ ℝ+) |
48 | | chto1ub 26357 |
. . . . . 6
⊢ (𝑥 ∈ ℝ+
↦ ((θ‘𝑥)
/ 𝑥)) ∈
𝑂(1) |
49 | 48 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
50 | 47, 49 | o1res2 15124 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∈ 𝑂(1)) |
51 | | ax-1cn 10787 |
. . . . . . 7
⊢ 1 ∈
ℂ |
52 | 51 | a1i 11 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → 1 ∈ ℂ) |
53 | 11, 24 | rpdivcld 12645 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈
ℝ+) |
54 | 53 | rpcnd 12630 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ∈ ℂ) |
55 | | pnfxr 10887 |
. . . . . . . . 9
⊢ +∞
∈ ℝ* |
56 | | icossre 13016 |
. . . . . . . . 9
⊢ ((2
∈ ℝ ∧ +∞ ∈ ℝ*) → (2[,)+∞)
⊆ ℝ) |
57 | 6, 55, 56 | mp2an 692 |
. . . . . . . 8
⊢
(2[,)+∞) ⊆ ℝ |
58 | | rlimconst 15105 |
. . . . . . . 8
⊢
(((2[,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1) |
59 | 57, 51, 58 | mp2an 692 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) ↦
1) ⇝𝑟 1 |
60 | 59 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ 1) ⇝𝑟 1) |
61 | | chtppilim 26356 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))
⇝𝑟 1 |
62 | 61 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))) ⇝𝑟
1) |
63 | | ax-1ne0 10798 |
. . . . . . 7
⊢ 1 ≠
0 |
64 | 63 | a1i 11 |
. . . . . 6
⊢ (⊤
→ 1 ≠ 0) |
65 | 53 | rpne0d 12633 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))) ≠ 0) |
66 | 52, 54, 60, 62, 64, 65 | rlimdiv 15209 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ⇝𝑟 (1 /
1)) |
67 | | rlimo1 15178 |
. . . . 5
⊢ ((𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
⇝𝑟 (1 / 1) → (𝑥 ∈ (2[,)+∞) ↦ (1 /
((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥)))))
∈ 𝑂(1)) |
68 | 66, 67 | syl 17 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) |
69 | | o1mul 15176 |
. . . 4
⊢ (((𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥)) ∈ 𝑂(1) ∧
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥))))) ∈ 𝑂(1)) → ((𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥)) ∘f ·
(𝑥 ∈ (2[,)+∞)
↦ (1 / ((θ‘𝑥) / ((π‘𝑥) · (log‘𝑥)))))) ∈ 𝑂(1)) |
70 | 50, 68, 69 | syl2anc 587 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) ∘f · (𝑥 ∈ (2[,)+∞) ↦
(1 / ((θ‘𝑥) /
((π‘𝑥)
· (log‘𝑥))))))
∈ 𝑂(1)) |
71 | 45, 70 | eqeltrrd 2839 |
. 2
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((π‘𝑥) / (𝑥 / (log‘𝑥)))) ∈ 𝑂(1)) |
72 | 71 | mptru 1550 |
1
⊢ (𝑥 ∈ (2[,)+∞) ↦
((π‘𝑥) /
(𝑥 / (log‘𝑥)))) ∈
𝑂(1) |