Proof of Theorem chtppilimlem2
Step | Hyp | Ref
| Expression |
1 | | simpr 476 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈
(2[,)+∞)) |
2 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
3 | | elicopnf 12140 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ → (𝑥 ∈
(2[,)+∞) ↔ (𝑥
∈ ℝ ∧ 2 ≤ 𝑥))) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑥 ∈ (2[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 2
≤ 𝑥)) |
5 | 1, 4 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 ∈ ℝ ∧ 2 ≤
𝑥)) |
6 | 5 | simpld 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈
ℝ) |
7 | | 0red 9920 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 ∈
ℝ) |
8 | 2 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 2 ∈
ℝ) |
9 | | 2pos 10989 |
. . . . . . . . 9
⊢ 0 <
2 |
10 | 9 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 <
2) |
11 | 5 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 2 ≤ 𝑥) |
12 | 7, 8, 6, 10, 11 | ltletrd 10076 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 < 𝑥) |
13 | 6, 12 | elrpd 11745 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈
ℝ+) |
14 | | chtppilim.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
15 | 14 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
16 | 15 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝐴 ∈
ℝ) |
17 | 13, 16 | rpcxpcld 24276 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐𝐴) ∈
ℝ+) |
18 | | ppinncl 24700 |
. . . . . . 7
⊢ ((𝑥 ∈ ℝ ∧ 2 ≤
𝑥) →
(π‘𝑥)
∈ ℕ) |
19 | 5, 18 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(π‘𝑥)
∈ ℕ) |
20 | 19 | nnrpd 11746 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(π‘𝑥)
∈ ℝ+) |
21 | 17, 20 | rpdivcld 11765 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈
ℝ+) |
22 | 21 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ (2[,)+∞)((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈
ℝ+) |
23 | | chtppilim.2 |
. . . 4
⊢ (𝜑 → 𝐴 < 1) |
24 | | 1re 9918 |
. . . . 5
⊢ 1 ∈
ℝ |
25 | | difrp 11744 |
. . . . 5
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 < 1
↔ (1 − 𝐴) ∈
ℝ+)) |
26 | 15, 24, 25 | sylancl 693 |
. . . 4
⊢ (𝜑 → (𝐴 < 1 ↔ (1 − 𝐴) ∈
ℝ+)) |
27 | 23, 26 | mpbid 221 |
. . 3
⊢ (𝜑 → (1 − 𝐴) ∈
ℝ+) |
28 | | ovex 6577 |
. . . . . . 7
⊢
(2[,)+∞) ∈ V |
29 | 28 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (2[,)+∞) ∈
V) |
30 | 24 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 ∈
ℝ) |
31 | | 1lt2 11071 |
. . . . . . . . . . 11
⊢ 1 <
2 |
32 | 31 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 <
2) |
33 | 30, 8, 6, 32, 11 | ltletrd 10076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 < 𝑥) |
34 | 6, 33 | rplogcld 24179 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
35 | 13, 34 | rpdivcld 11765 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 / (log‘𝑥)) ∈
ℝ+) |
36 | 35, 20 | rpdivcld 11765 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) / (π‘𝑥)) ∈
ℝ+) |
37 | 27 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 −
𝐴) ∈
ℝ+) |
38 | 37 | rpred 11748 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 −
𝐴) ∈
ℝ) |
39 | 13, 38 | rpcxpcld 24276 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐(1
− 𝐴)) ∈
ℝ+) |
40 | 34, 39 | rpdivcld 11765 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))) ∈
ℝ+) |
41 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) = (𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥)))) |
42 | | eqidd 2611 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴)))) = (𝑥 ∈ (2[,)+∞) ↦
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))))) |
43 | 29, 36, 40, 41, 42 | offval2 6812 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (2[,)+∞)
↦ ((log‘𝑥) /
(𝑥↑𝑐(1 − 𝐴))))) = (𝑥 ∈ (2[,)+∞) ↦ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))))) |
44 | 35 | rpcnd 11750 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 / (log‘𝑥)) ∈ ℂ) |
45 | 40 | rpcnd 11750 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))) ∈
ℂ) |
46 | 20 | rpcnne0d 11757 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
((π‘𝑥)
∈ ℂ ∧ (π‘𝑥) ≠ 0)) |
47 | | div23 10583 |
. . . . . . . 8
⊢ (((𝑥 / (log‘𝑥)) ∈ ℂ ∧ ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) ∈ ℂ ∧
((π‘𝑥)
∈ ℂ ∧ (π‘𝑥) ≠ 0)) → (((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) / (π‘𝑥)) = (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) |
48 | 44, 45, 46, 47 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) / (π‘𝑥)) = (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) |
49 | 34 | rpcnne0d 11757 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
((log‘𝑥) ∈
ℂ ∧ (log‘𝑥)
≠ 0)) |
50 | 39 | rpcnne0d 11757 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐(1
− 𝐴)) ∈ ℂ
∧ (𝑥↑𝑐(1 − 𝐴)) ≠ 0)) |
51 | 6 | recnd 9947 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝑥 ∈
ℂ) |
52 | | dmdcan 10614 |
. . . . . . . . . 10
⊢
((((log‘𝑥)
∈ ℂ ∧ (log‘𝑥) ≠ 0) ∧ ((𝑥↑𝑐(1 − 𝐴)) ∈ ℂ ∧ (𝑥↑𝑐(1
− 𝐴)) ≠ 0) ∧
𝑥 ∈ ℂ) →
(((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))) ·
(𝑥 / (log‘𝑥))) = (𝑥 / (𝑥↑𝑐(1 − 𝐴)))) |
53 | 49, 50, 51, 52 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))) ·
(𝑥 / (log‘𝑥))) = (𝑥 / (𝑥↑𝑐(1 − 𝐴)))) |
54 | 44, 45 | mulcomd 9940 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = (((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))) · (𝑥 / (log‘𝑥)))) |
55 | 13 | rpcnne0d 11757 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
56 | | ax-1cn 9873 |
. . . . . . . . . . . . 13
⊢ 1 ∈
ℂ |
57 | 56 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 1 ∈
ℂ) |
58 | 37 | rpcnd 11750 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 −
𝐴) ∈
ℂ) |
59 | | cxpsub 24228 |
. . . . . . . . . . . 12
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ 1 ∈ ℂ
∧ (1 − 𝐴) ∈
ℂ) → (𝑥↑𝑐(1 − (1
− 𝐴))) = ((𝑥↑𝑐1) /
(𝑥↑𝑐(1 − 𝐴)))) |
60 | 55, 57, 58, 59 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐(1
− (1 − 𝐴))) =
((𝑥↑𝑐1) / (𝑥↑𝑐(1
− 𝐴)))) |
61 | 16 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 𝐴 ∈
ℂ) |
62 | | nncan 10189 |
. . . . . . . . . . . . 13
⊢ ((1
∈ ℂ ∧ 𝐴
∈ ℂ) → (1 − (1 − 𝐴)) = 𝐴) |
63 | 56, 61, 62 | sylancr 694 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (1 − (1
− 𝐴)) = 𝐴) |
64 | 63 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐(1
− (1 − 𝐴))) =
(𝑥↑𝑐𝐴)) |
65 | 60, 64 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐1) /
(𝑥↑𝑐(1 − 𝐴))) = (𝑥↑𝑐𝐴)) |
66 | 51 | cxp1d 24252 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐1) =
𝑥) |
67 | 66 | oveq1d 6564 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐1) /
(𝑥↑𝑐(1 − 𝐴))) = (𝑥 / (𝑥↑𝑐(1 − 𝐴)))) |
68 | 65, 67 | eqtr3d 2646 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (𝑥↑𝑐𝐴) = (𝑥 / (𝑥↑𝑐(1 − 𝐴)))) |
69 | 53, 54, 68 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = (𝑥↑𝑐𝐴)) |
70 | 69 | oveq1d 6564 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥 / (log‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) / (π‘𝑥)) = ((𝑥↑𝑐𝐴) / (π‘𝑥))) |
71 | 48, 70 | eqtr3d 2646 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴)))) = ((𝑥↑𝑐𝐴) / (π‘𝑥))) |
72 | 71 | mpteq2dva 4672 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ (((𝑥 / (log‘𝑥)) / (π‘𝑥)) · ((log‘𝑥) / (𝑥↑𝑐(1 − 𝐴))))) = (𝑥 ∈ (2[,)+∞) ↦ ((𝑥↑𝑐𝐴) / (π‘𝑥)))) |
73 | 43, 72 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (2[,)+∞)
↦ ((log‘𝑥) /
(𝑥↑𝑐(1 − 𝐴))))) = (𝑥 ∈ (2[,)+∞) ↦ ((𝑥↑𝑐𝐴) / (π‘𝑥)))) |
74 | | chebbnd1 24961 |
. . . . 5
⊢ (𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈
𝑂(1) |
75 | 13 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) → 𝑥 ∈
ℝ+)) |
76 | 75 | ssrdv 3574 |
. . . . . 6
⊢ (𝜑 → (2[,)+∞) ⊆
ℝ+) |
77 | | cxploglim 24504 |
. . . . . . 7
⊢ ((1
− 𝐴) ∈
ℝ+ → (𝑥 ∈ ℝ+ ↦
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))))
⇝𝑟 0) |
78 | 27, 77 | syl 17 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))))
⇝𝑟 0) |
79 | 76, 78 | rlimres2 14140 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴))))
⇝𝑟 0) |
80 | | o1rlimmul 14197 |
. . . . 5
⊢ (((𝑥 ∈ (2[,)+∞) ↦
((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∈ 𝑂(1) ∧
(𝑥 ∈ (2[,)+∞)
↦ ((log‘𝑥) /
(𝑥↑𝑐(1 − 𝐴)))) ⇝𝑟
0) → ((𝑥 ∈
(2[,)+∞) ↦ ((𝑥
/ (log‘𝑥)) /
(π‘𝑥)))
∘𝑓 · (𝑥 ∈ (2[,)+∞) ↦
((log‘𝑥) / (𝑥↑𝑐(1
− 𝐴)))))
⇝𝑟 0) |
81 | 74, 79, 80 | sylancr 694 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (2[,)+∞) ↦ ((𝑥 / (log‘𝑥)) / (π‘𝑥))) ∘𝑓 ·
(𝑥 ∈ (2[,)+∞)
↦ ((log‘𝑥) /
(𝑥↑𝑐(1 − 𝐴)))))
⇝𝑟 0) |
82 | 73, 81 | eqbrtrrd 4607 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (2[,)+∞) ↦ ((𝑥↑𝑐𝐴) / (π‘𝑥))) ⇝𝑟
0) |
83 | 22, 27, 82 | rlimi 14092 |
. 2
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴))) |
84 | 21 | rpcnd 11750 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈
ℂ) |
85 | 84 | subid1d 10260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0) = ((𝑥↑𝑐𝐴) / (π‘𝑥))) |
86 | 85 | fveq2d 6107 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) = (abs‘((𝑥↑𝑐𝐴) / (π‘𝑥)))) |
87 | 21 | rpred 11748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) ∈
ℝ) |
88 | 21 | rpge0d 11752 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → 0 ≤ ((𝑥↑𝑐𝐴) / (π‘𝑥))) |
89 | 87, 88 | absidd 14009 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(abs‘((𝑥↑𝑐𝐴) / (π‘𝑥))) = ((𝑥↑𝑐𝐴) / (π‘𝑥))) |
90 | 86, 89 | eqtrd 2644 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
(abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) = ((𝑥↑𝑐𝐴) / (π‘𝑥))) |
91 | 90 | breq1d 4593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
((abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴) ↔ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) |
92 | 14 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → 𝐴 ∈
ℝ+) |
93 | 23 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → 𝐴 < 1) |
94 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → 𝑥 ∈ (2[,)+∞)) |
95 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴)) |
96 | 92, 93, 94, 95 | chtppilimlem1 24962 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (2[,)+∞) ∧ ((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴))) → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)) |
97 | 96 | expr 641 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → (((𝑥↑𝑐𝐴) / (π‘𝑥)) < (1 − 𝐴) → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) |
98 | 91, 97 | sylbid 229 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) →
((abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴) → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) |
99 | 98 | imim2d 55 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (2[,)+∞)) → ((𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)) → (𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))) |
100 | 99 | ralimdva 2945 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)) → ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))) |
101 | 100 | reximdv 2999 |
. 2
⊢ (𝜑 → (∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → (abs‘(((𝑥↑𝑐𝐴) / (π‘𝑥)) − 0)) < (1 − 𝐴)) → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥)))) |
102 | 83, 101 | mpd 15 |
1
⊢ (𝜑 → ∃𝑧 ∈ ℝ ∀𝑥 ∈ (2[,)+∞)(𝑧 ≤ 𝑥 → ((𝐴↑2) · ((π‘𝑥) · (log‘𝑥))) < (θ‘𝑥))) |