Proof of Theorem pnt2
Step | Hyp | Ref
| Expression |
1 | | 2re 11090 |
. . . . . . . . 9
⊢ 2 ∈
ℝ |
2 | | elicopnf 12269 |
. . . . . . . . 9
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) |
3 | 1, 2 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
4 | | chprpcl 24932 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(ψ‘𝑥) ∈
ℝ+) |
5 | 3, 4 | sylbi 207 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(ψ‘𝑥) ∈
ℝ+) |
6 | 3 | simplbi 476 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ) |
7 | | 0red 10041 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 0
∈ ℝ) |
8 | 1 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 2
∈ ℝ) |
9 | | 2pos 11112 |
. . . . . . . . . 10
⊢ 0 <
2 |
10 | 9 | a1i 11 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 2) |
11 | 3 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) → 2
≤ 𝑥) |
12 | 7, 8, 6, 10, 11 | ltletrd 10197 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) → 0
< 𝑥) |
13 | 6, 12 | elrpd 11869 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℝ+) |
14 | 5, 13 | rpdivcld 11889 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
((ψ‘𝑥) / 𝑥) ∈
ℝ+) |
15 | 14 | adantl 482 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((ψ‘𝑥) / 𝑥) ∈
ℝ+) |
16 | | chtrpcl 24901 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(θ‘𝑥) ∈
ℝ+) |
17 | 3, 16 | sylbi 207 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℝ+) |
18 | 5, 17 | rpdivcld 11889 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
((ψ‘𝑥) /
(θ‘𝑥)) ∈
ℝ+) |
19 | 18 | adantl 482 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((ψ‘𝑥) / (θ‘𝑥)) ∈
ℝ+) |
20 | 13 | ssriv 3607 |
. . . . . . 7
⊢
(2[,)+∞) ⊆ ℝ+ |
21 | 20 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (2[,)+∞) ⊆ ℝ+) |
22 | | pnt3 25301 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ ((ψ‘𝑥) /
𝑥))
⇝𝑟 1 |
23 | 22 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟
1) |
24 | 21, 23 | rlimres2 14292 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((ψ‘𝑥) / 𝑥)) ⇝𝑟
1) |
25 | | chpchtlim 25168 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) ↦
((ψ‘𝑥) /
(θ‘𝑥)))
⇝𝑟 1 |
26 | 25 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ ((ψ‘𝑥) / (θ‘𝑥))) ⇝𝑟
1) |
27 | | ax-1ne0 10005 |
. . . . . 6
⊢ 1 ≠
0 |
28 | 27 | a1i 11 |
. . . . 5
⊢ (⊤
→ 1 ≠ 0) |
29 | 19 | rpne0d 11877 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (2[,)+∞)) → ((ψ‘𝑥) / (θ‘𝑥)) ≠ 0) |
30 | 15, 19, 24, 26, 28, 29 | rlimdiv 14376 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(2[,)+∞) ↦ (((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥)))) ⇝𝑟 (1 /
1)) |
31 | | rpre 11839 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
32 | | chpcl 24850 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
33 | 31, 32 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
34 | 33 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℂ) |
35 | 13, 34 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(ψ‘𝑥) ∈
ℂ) |
36 | 13 | rpcnne0d 11881 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) |
37 | 5 | rpcnne0d 11881 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((ψ‘𝑥) ∈
ℂ ∧ (ψ‘𝑥) ≠ 0)) |
38 | 17 | rpcnne0d 11881 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
((θ‘𝑥) ∈
ℂ ∧ (θ‘𝑥) ≠ 0)) |
39 | | divdivdiv 10726 |
. . . . . . . 8
⊢
((((ψ‘𝑥)
∈ ℂ ∧ (𝑥
∈ ℂ ∧ 𝑥 ≠
0)) ∧ (((ψ‘𝑥)
∈ ℂ ∧ (ψ‘𝑥) ≠ 0) ∧ ((θ‘𝑥) ∈ ℂ ∧
(θ‘𝑥) ≠ 0)))
→ (((ψ‘𝑥) /
𝑥) / ((ψ‘𝑥) / (θ‘𝑥))) = (((ψ‘𝑥) · (θ‘𝑥)) / (𝑥 · (ψ‘𝑥)))) |
40 | 35, 36, 37, 38, 39 | syl22anc 1327 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥))) = (((ψ‘𝑥) · (θ‘𝑥)) / (𝑥 · (ψ‘𝑥)))) |
41 | 6 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) →
𝑥 ∈
ℂ) |
42 | 41, 35 | mulcomd 10061 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(𝑥 ·
(ψ‘𝑥)) =
((ψ‘𝑥) ·
𝑥)) |
43 | 42 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(((ψ‘𝑥) ·
(θ‘𝑥)) / (𝑥 · (ψ‘𝑥))) = (((ψ‘𝑥) · (θ‘𝑥)) / ((ψ‘𝑥) · 𝑥))) |
44 | | chtcl 24835 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ →
(θ‘𝑥) ∈
ℝ) |
45 | 31, 44 | syl 17 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (θ‘𝑥)
∈ ℝ) |
46 | 45 | recnd 10068 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (θ‘𝑥)
∈ ℂ) |
47 | 13, 46 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (2[,)+∞) →
(θ‘𝑥) ∈
ℂ) |
48 | | divcan5 10727 |
. . . . . . . 8
⊢
(((θ‘𝑥)
∈ ℂ ∧ (𝑥
∈ ℂ ∧ 𝑥 ≠
0) ∧ ((ψ‘𝑥)
∈ ℂ ∧ (ψ‘𝑥) ≠ 0)) → (((ψ‘𝑥) · (θ‘𝑥)) / ((ψ‘𝑥) · 𝑥)) = ((θ‘𝑥) / 𝑥)) |
49 | 47, 36, 37, 48 | syl3anc 1326 |
. . . . . . 7
⊢ (𝑥 ∈ (2[,)+∞) →
(((ψ‘𝑥) ·
(θ‘𝑥)) /
((ψ‘𝑥) ·
𝑥)) = ((θ‘𝑥) / 𝑥)) |
50 | 40, 43, 49 | 3eqtrd 2660 |
. . . . . 6
⊢ (𝑥 ∈ (2[,)+∞) →
(((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥))) = ((θ‘𝑥) / 𝑥)) |
51 | 50 | mpteq2ia 4740 |
. . . . 5
⊢ (𝑥 ∈ (2[,)+∞) ↦
(((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥)))) = (𝑥 ∈ (2[,)+∞) ↦
((θ‘𝑥) / 𝑥)) |
52 | | resmpt 5449 |
. . . . . 6
⊢
((2[,)+∞) ⊆ ℝ+ → ((𝑥 ∈ ℝ+ ↦
((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞)) =
(𝑥 ∈ (2[,)+∞)
↦ ((θ‘𝑥)
/ 𝑥))) |
53 | 20, 52 | ax-mp 5 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
↦ ((θ‘𝑥)
/ 𝑥)) ↾
(2[,)+∞)) = (𝑥 ∈
(2[,)+∞) ↦ ((θ‘𝑥) / 𝑥)) |
54 | 51, 53 | eqtr4i 2647 |
. . . 4
⊢ (𝑥 ∈ (2[,)+∞) ↦
(((ψ‘𝑥) / 𝑥) / ((ψ‘𝑥) / (θ‘𝑥)))) = ((𝑥 ∈ ℝ+ ↦
((θ‘𝑥) / 𝑥)) ↾
(2[,)+∞)) |
55 | | 1div1e1 10717 |
. . . 4
⊢ (1 / 1) =
1 |
56 | 30, 54, 55 | 3brtr3g 4686 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞))
⇝𝑟 1) |
57 | | rerpdivcl 11861 |
. . . . . . . 8
⊢
(((θ‘𝑥)
∈ ℝ ∧ 𝑥
∈ ℝ+) → ((θ‘𝑥) / 𝑥) ∈ ℝ) |
58 | 45, 57 | mpancom 703 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
→ ((θ‘𝑥) /
𝑥) ∈
ℝ) |
59 | 58 | adantl 482 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((θ‘𝑥) / 𝑥) ∈ ℝ) |
60 | 59 | recnd 10068 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((θ‘𝑥) / 𝑥) ∈ ℂ) |
61 | | eqid 2622 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
↦ ((θ‘𝑥)
/ 𝑥)) = (𝑥 ∈ ℝ+ ↦
((θ‘𝑥) / 𝑥)) |
62 | 60, 61 | fmptd 6385 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)):ℝ+⟶ℂ) |
63 | | rpssre 11843 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
64 | 63 | a1i 11 |
. . . 4
⊢ (⊤
→ ℝ+ ⊆ ℝ) |
65 | 1 | a1i 11 |
. . . 4
⊢ (⊤
→ 2 ∈ ℝ) |
66 | 62, 64, 65 | rlimresb 14296 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟 1 ↔
((𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ↾ (2[,)+∞))
⇝𝑟 1)) |
67 | 56, 66 | mpbird 247 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((θ‘𝑥) / 𝑥)) ⇝𝑟
1) |
68 | 67 | trud 1493 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((θ‘𝑥)
/ 𝑥))
⇝𝑟 1 |