Step | Hyp | Ref
| Expression |
1 | | rpssre 11719 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
2 | | eqid 2610 |
. . . . . . . . . . 11
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
3 | 2 | subcn 22477 |
. . . . . . . . . . . 12
⊢ −
∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld)) |
4 | 3 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
− ∈ (((TopOpen‘ℂfld) ×t
(TopOpen‘ℂfld)) Cn
(TopOpen‘ℂfld))) |
5 | | ssid 3587 |
. . . . . . . . . . . . 13
⊢ ℂ
⊆ ℂ |
6 | | cncfmptid 22523 |
. . . . . . . . . . . . 13
⊢ ((ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ)) |
7 | 5, 5, 6 | mp2an 704 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ) |
8 | 7 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝑝) ∈ (ℂ–cn→ℂ)) |
9 | | pntlem3.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐶 ∈
ℝ+) |
10 | 9 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈
ℝ+) |
11 | 10 | rpcnd 11750 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → 𝐶 ∈
ℂ) |
12 | 5 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
ℂ ⊆ ℂ) |
13 | | cncfmptc 22522 |
. . . . . . . . . . . . 13
⊢ ((𝐶 ∈ ℂ ∧ ℂ
⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ)) |
14 | 11, 12, 12, 13 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ 𝐶) ∈ (ℂ–cn→ℂ)) |
15 | | 3nn0 11187 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℕ0 |
16 | 2 | expcn 22483 |
. . . . . . . . . . . . . 14
⊢ (3 ∈
ℕ0 → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
17 | 15, 16 | mp1i 13 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld))) |
18 | 2 | cncfcn1 22521 |
. . . . . . . . . . . . 13
⊢
(ℂ–cn→ℂ) =
((TopOpen‘ℂfld) Cn
(TopOpen‘ℂfld)) |
19 | 17, 18 | syl6eleqr 2699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝↑3)) ∈
(ℂ–cn→ℂ)) |
20 | 14, 19 | mulcncf 23023 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝐶 · (𝑝↑3))) ∈ (ℂ–cn→ℂ)) |
21 | 2, 4, 8, 20 | cncfmpt2f 22525 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ)) |
22 | | pntlem3.1 |
. . . . . . . . . . . . . . 15
⊢ 𝑇 = {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡} |
23 | | ssrab2 3650 |
. . . . . . . . . . . . . . 15
⊢ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡} ⊆ (0[,]𝐴) |
24 | 22, 23 | eqsstri 3598 |
. . . . . . . . . . . . . 14
⊢ 𝑇 ⊆ (0[,]𝐴) |
25 | | 0re 9919 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
26 | | pntlem3.a |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
27 | 26 | rpred 11748 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ ℝ) |
28 | | iccssre 12126 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0[,]𝐴) ⊆ ℝ) |
29 | 25, 27, 28 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (0[,]𝐴) ⊆ ℝ) |
30 | 24, 29 | syl5ss 3579 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ⊆ ℝ) |
31 | | 0xr 9965 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
ℝ* |
32 | 31 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ∈
ℝ*) |
33 | 26 | rpxrd 11749 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐴 ∈
ℝ*) |
34 | 26 | rpge0d 11752 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 0 ≤ 𝐴) |
35 | | ubicc2 12160 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ 𝐴 ∈ ℝ* ∧ 0 ≤
𝐴) → 𝐴 ∈ (0[,]𝐴)) |
36 | 32, 33, 34, 35 | syl3anc 1318 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ (0[,]𝐴)) |
37 | | 1rp 11712 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ+ |
38 | | 1re 9918 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 1 ∈
ℝ |
39 | | elicopnf 12140 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (1 ∈
ℝ → (𝑧 ∈
(1[,)+∞) ↔ (𝑧
∈ ℝ ∧ 1 ≤ 𝑧))) |
40 | 38, 39 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑧 ∈ (1[,)+∞) ↔ (𝑧 ∈ ℝ ∧ 1 ≤
𝑧))) |
41 | 40 | simprbda 651 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 𝑧 ∈
ℝ) |
42 | | 0red 9920 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 0 ∈
ℝ) |
43 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 1 ∈
ℝ) |
44 | | 0lt1 10429 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 <
1 |
45 | 44 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 0 <
1) |
46 | 40 | simplbda 652 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 1 ≤ 𝑧) |
47 | 42, 43, 41, 45, 46 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 0 < 𝑧) |
48 | 41, 47 | elrpd 11745 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → 𝑧 ∈
ℝ+) |
49 | | pntlem3.A |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
50 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) → ∀𝑥 ∈ ℝ+
(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴) |
51 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → (𝑅‘𝑥) = (𝑅‘𝑧)) |
52 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 = 𝑧 → 𝑥 = 𝑧) |
53 | 51, 52 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 = 𝑧 → ((𝑅‘𝑥) / 𝑥) = ((𝑅‘𝑧) / 𝑧)) |
54 | 53 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑧 → (abs‘((𝑅‘𝑥) / 𝑥)) = (abs‘((𝑅‘𝑧) / 𝑧))) |
55 | 54 | breq1d 4593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑧 → ((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 ↔ (abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
56 | 55 | rspcv 3278 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∈ ℝ+
→ (∀𝑥 ∈
ℝ+ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝐴 → (abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
57 | 48, 50, 56 | sylc 63 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑧 ∈ (1[,)+∞)) →
(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
58 | 57 | ralrimiva 2949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
59 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = 1 → (𝑦[,)+∞) =
(1[,)+∞)) |
60 | 59 | raleqdv 3121 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 1 → (∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴 ↔ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
61 | 60 | rspcev 3282 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ ∀𝑧 ∈ (1[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
62 | 37, 58, 61 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴) |
63 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑡 = 𝐴 → ((abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
64 | 63 | rexralbidv 3040 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 = 𝐴 → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
65 | 64, 22 | elrab2 3333 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ 𝑇 ↔ (𝐴 ∈ (0[,]𝐴) ∧ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝐴)) |
66 | 36, 62, 65 | sylanbrc 695 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑇) |
67 | | ne0i 3880 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ 𝑇 → 𝑇 ≠ ∅) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ≠ ∅) |
69 | | elicc2 12109 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (𝑡
∈ (0[,]𝐴) ↔
(𝑡 ∈ ℝ ∧ 0
≤ 𝑡 ∧ 𝑡 ≤ 𝐴))) |
70 | 25, 27, 69 | sylancr 694 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (𝑡 ∈ (0[,]𝐴) ↔ (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴))) |
71 | 70 | biimpa 500 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]𝐴)) → (𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 𝐴)) |
72 | 71 | simp2d 1067 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]𝐴)) → 0 ≤ 𝑡) |
73 | 72 | a1d 25 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ (0[,]𝐴)) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
74 | 73 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
75 | 22 | raleqi 3119 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
𝑇 0 ≤ 𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤) |
76 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 = 𝑡 → (0 ≤ 𝑤 ↔ 0 ≤ 𝑡)) |
77 | 76 | ralrab2 3339 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑤 ∈
{𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
78 | 75, 77 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑤 ∈
𝑇 0 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 0 ≤ 𝑡)) |
79 | 74, 78 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∀𝑤 ∈ 𝑇 0 ≤ 𝑤) |
80 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑤 ↔ 0 ≤ 𝑤)) |
81 | 80 | ralbidv 2969 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 0 → (∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ↔ ∀𝑤 ∈ 𝑇 0 ≤ 𝑤)) |
82 | 81 | rspcev 3282 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ ∧ ∀𝑤 ∈ 𝑇 0 ≤ 𝑤) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
83 | 25, 79, 82 | sylancr 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
84 | | infrecl 10882 |
. . . . . . . . . . . . 13
⊢ ((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) → inf(𝑇, ℝ, < ) ∈
ℝ) |
85 | 30, 68, 83, 84 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈
ℝ) |
86 | 85 | recnd 9947 |
. . . . . . . . . . 11
⊢ (𝜑 → inf(𝑇, ℝ, < ) ∈
ℂ) |
87 | 86 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
inf(𝑇, ℝ, < )
∈ ℂ) |
88 | | elrp 11710 |
. . . . . . . . . . . . . 14
⊢
(inf(𝑇, ℝ,
< ) ∈ ℝ+ ↔ (inf(𝑇, ℝ, < ) ∈ ℝ ∧ 0
< inf(𝑇, ℝ, <
))) |
89 | 88 | biimpri 217 |
. . . . . . . . . . . . 13
⊢
((inf(𝑇, ℝ,
< ) ∈ ℝ ∧ 0 < inf(𝑇, ℝ, < )) → inf(𝑇, ℝ, < ) ∈
ℝ+) |
90 | 85, 89 | sylan 487 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
inf(𝑇, ℝ, < )
∈ ℝ+) |
91 | | 3z 11287 |
. . . . . . . . . . . 12
⊢ 3 ∈
ℤ |
92 | | rpexpcl 12741 |
. . . . . . . . . . . 12
⊢
((inf(𝑇, ℝ,
< ) ∈ ℝ+ ∧ 3 ∈ ℤ) → (inf(𝑇, ℝ, < )↑3) ∈
ℝ+) |
93 | 90, 91, 92 | sylancl 693 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
(inf(𝑇, ℝ, <
)↑3) ∈ ℝ+) |
94 | 10, 93 | rpmulcld 11764 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈
ℝ+) |
95 | | cncfi 22505 |
. . . . . . . . . 10
⊢ (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) ∈ (ℂ–cn→ℂ) ∧ inf(𝑇, ℝ, < ) ∈ ℂ ∧
(𝐶 · (inf(𝑇, ℝ, < )↑3))
∈ ℝ+) → ∃𝑠 ∈ ℝ+ ∀𝑢 ∈ ℂ
((abs‘(𝑢 −
inf(𝑇, ℝ, < )))
< 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
96 | 21, 87, 94, 95 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) →
∃𝑠 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
97 | 85 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ inf(𝑇, ℝ, <
) ∈ ℝ) |
98 | | rphalfcl 11734 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ℝ+
→ (𝑠 / 2) ∈
ℝ+) |
99 | 98 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (𝑠 / 2) ∈
ℝ+) |
100 | 97, 99 | ltaddrpd 11781 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ inf(𝑇, ℝ, <
) < (inf(𝑇, ℝ,
< ) + (𝑠 /
2))) |
101 | 99 | rpred 11748 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (𝑠 / 2) ∈
ℝ) |
102 | 97, 101 | readdcld 9948 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (inf(𝑇, ℝ,
< ) + (𝑠 / 2)) ∈
ℝ) |
103 | 97, 102 | ltnled 10063 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (inf(𝑇, ℝ,
< ) < (inf(𝑇,
ℝ, < ) + (𝑠 / 2))
↔ ¬ (inf(𝑇,
ℝ, < ) + (𝑠 / 2))
≤ inf(𝑇, ℝ, <
))) |
104 | 100, 103 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ¬ (inf(𝑇,
ℝ, < ) + (𝑠 / 2))
≤ inf(𝑇, ℝ, <
)) |
105 | | ax-resscn 9872 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
106 | 30, 105 | syl6ss 3580 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ⊆ ℂ) |
107 | 106 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ 𝑇 ⊆
ℂ) |
108 | | ssralv 3629 |
. . . . . . . . . . . . 13
⊢ (𝑇 ⊆ ℂ →
(∀𝑢 ∈ ℂ
((abs‘(𝑢 −
inf(𝑇, ℝ, < )))
< 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
∀𝑢 ∈ 𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3))))) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
ℂ ((abs‘(𝑢
− inf(𝑇, ℝ,
< ))) < 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
∀𝑢 ∈ 𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3))))) |
110 | 30 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ 𝑇 ⊆
ℝ) |
111 | 110 | sselda 3568 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑢 ∈ ℝ) |
112 | 102 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ) |
113 | 111, 112 | ltnled 10063 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ↔ ¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
114 | 85 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈
ℝ) |
115 | 101 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑠 / 2) ∈ ℝ) |
116 | 114, 115 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) ∈
ℝ) |
117 | 97, 99 | ltsubrpd 11780 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (inf(𝑇, ℝ,
< ) − (𝑠 / 2))
< inf(𝑇, ℝ, <
)) |
118 | 117 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < inf(𝑇, ℝ, <
)) |
119 | 30 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑇 ⊆ ℝ) |
120 | 83 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
121 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑢 ∈ 𝑇) |
122 | | infrelb 10885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑇 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢) |
123 | 119, 120,
121, 122 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ 𝑢) |
124 | 116, 114,
111, 118, 123 | ltletrd 10076 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢) |
125 | 111, 114,
115 | absdifltd 14020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ↔ ((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢 ∧ 𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2))))) |
126 | 125 | biimprd 237 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((inf(𝑇, ℝ, < ) − (𝑠 / 2)) < 𝑢 ∧ 𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2))) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2))) |
127 | 124, 126 | mpand 707 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2))) |
128 | | rphalflt 11736 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑠 ∈ ℝ+
→ (𝑠 / 2) < 𝑠) |
129 | 128 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑠 / 2) < 𝑠) |
130 | 111, 114 | resubcld 10337 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈
ℝ) |
131 | 130 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − inf(𝑇, ℝ, < )) ∈
ℂ) |
132 | 131 | abscld 14023 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) ∈
ℝ) |
133 | | rpre 11715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑠 ∈ ℝ+
→ 𝑠 ∈
ℝ) |
134 | 133 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑠 ∈ ℝ) |
135 | | lttr 9993 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((abs‘(𝑢
− inf(𝑇, ℝ,
< ))) ∈ ℝ ∧ (𝑠 / 2) ∈ ℝ ∧ 𝑠 ∈ ℝ) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
136 | 132, 115,
134, 135 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) ∧ (𝑠 / 2) < 𝑠) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
137 | 129, 136 | mpan2d 706 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < (𝑠 / 2) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
138 | 127, 137 | syld 46 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 < (inf(𝑇, ℝ, < ) + (𝑠 / 2)) → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
139 | 113, 138 | sylbird 249 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (¬ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢 → (abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠)) |
140 | 139 | con1d 138 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (¬
(abs‘(𝑢 −
inf(𝑇, ℝ, < )))
< 𝑠 → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
141 | 111 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝑢 ∈ ℂ) |
142 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = 𝑢 → 𝑝 = 𝑢) |
143 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = 𝑢 → (𝑝↑3) = (𝑢↑3)) |
144 | 143 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = 𝑢 → (𝐶 · (𝑝↑3)) = (𝐶 · (𝑢↑3))) |
145 | 142, 144 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = 𝑢 → (𝑝 − (𝐶 · (𝑝↑3))) = (𝑢 − (𝐶 · (𝑢↑3)))) |
146 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) = (𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3)))) |
147 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑢 − (𝐶 · (𝑢↑3))) ∈ V |
148 | 145, 146,
147 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑢 ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3)))) |
149 | 141, 148 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) = (𝑢 − (𝐶 · (𝑢↑3)))) |
150 | 87 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ∈
ℂ) |
151 | | id 22 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = inf(𝑇, ℝ, < ) → 𝑝 = inf(𝑇, ℝ, < )) |
152 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑝 = inf(𝑇, ℝ, < ) → (𝑝↑3) = (inf(𝑇, ℝ, < )↑3)) |
153 | 152 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑝 = inf(𝑇, ℝ, < ) → (𝐶 · (𝑝↑3)) = (𝐶 · (inf(𝑇, ℝ, < )↑3))) |
154 | 151, 153 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑝 = inf(𝑇, ℝ, < ) → (𝑝 − (𝐶 · (𝑝↑3))) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
155 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(inf(𝑇, ℝ,
< ) − (𝐶 ·
(inf(𝑇, ℝ, <
)↑3))) ∈ V |
156 | 154, 146,
155 | fvmpt 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(inf(𝑇, ℝ,
< ) ∈ ℂ → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
157 | 150, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )) = (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
158 | 149, 157 | oveq12d 6567 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < ))) = ((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3))))) |
159 | 158 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) = (abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, <
)↑3)))))) |
160 | 159 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔
(abs‘((𝑢 −
(𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
161 | 9 | rpred 11748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐶 ∈ ℝ) |
162 | 161 | ad3antrrr 762 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 𝐶 ∈ ℝ) |
163 | | reexpcl 12739 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑢 ∈ ℝ ∧ 3 ∈
ℕ0) → (𝑢↑3) ∈ ℝ) |
164 | 111, 15, 163 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢↑3) ∈ ℝ) |
165 | 162, 164 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝐶 · (𝑢↑3)) ∈ ℝ) |
166 | 111, 165 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ ℝ) |
167 | 15 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → 3 ∈
ℕ0) |
168 | 114, 167 | reexpcld 12887 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < )↑3) ∈
ℝ) |
169 | 162, 168 | remulcld 9949 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈
ℝ) |
170 | 114, 169 | resubcld 10337 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) ∈
ℝ) |
171 | 166, 170,
169 | absdifltd 14020 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) ↔
(((inf(𝑇, ℝ, < )
− (𝐶 ·
(inf(𝑇, ℝ, <
)↑3))) − (𝐶
· (inf(𝑇, ℝ,
< )↑3))) < (𝑢
− (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, <
)↑3)))))) |
172 | 169 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝐶 · (inf(𝑇, ℝ, < )↑3)) ∈
ℂ) |
173 | 150, 172 | npcand 10275 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) = inf(𝑇, ℝ, <
)) |
174 | 173 | breq2d 4595 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) ↔ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ))) |
175 | | pntlem3.3 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑢 ∈ 𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) |
176 | 175 | ad4ant14 1285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) |
177 | | infrelb 10885 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑇 ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤 ∧ (𝑢 − (𝐶 · (𝑢↑3))) ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3)))) |
178 | 119, 120,
176, 177 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → inf(𝑇, ℝ, < ) ≤ (𝑢 − (𝐶 · (𝑢↑3)))) |
179 | 114, 166,
178 | lensymd 10067 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ¬ (𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < )) |
180 | 179 | pm2.21d 117 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < inf(𝑇, ℝ, < ) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
181 | 174, 180 | sylbid 229 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ 𝑢)) |
182 | 181 | adantld 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) < (𝑢 − (𝐶 · (𝑢↑3))) ∧ (𝑢 − (𝐶 · (𝑢↑3))) < ((inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))) + (𝐶 · (inf(𝑇, ℝ, < )↑3)))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ 𝑢)) |
183 | 171, 182 | sylbid 229 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘((𝑢 − (𝐶 · (𝑢↑3))) − (inf(𝑇, ℝ, < ) − (𝐶 · (inf(𝑇, ℝ, < )↑3))))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
184 | 160, 183 | sylbid 229 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → ((abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3)) → (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
185 | 140, 184 | jad 173 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
∧ 𝑢 ∈ 𝑇) → (((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ 𝑢)) |
186 | 185 | ralimdva 2945 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
∀𝑢 ∈ 𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
187 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ 𝑇 ≠
∅) |
188 | 83 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ∃𝑥 ∈
ℝ ∀𝑤 ∈
𝑇 𝑥 ≤ 𝑤) |
189 | | infregelb 10884 |
. . . . . . . . . . . . . 14
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) ∧ (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ∈ ℝ) → ((inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ inf(𝑇, ℝ, < ) ↔
∀𝑢 ∈ 𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
190 | 110, 187,
188, 102, 189 | syl31anc 1321 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ((inf(𝑇, ℝ,
< ) + (𝑠 / 2)) ≤
inf(𝑇, ℝ, < )
↔ ∀𝑢 ∈
𝑇 (inf(𝑇, ℝ, < ) + (𝑠 / 2)) ≤ 𝑢)) |
191 | 186, 190 | sylibrd 248 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
𝑇 ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ inf(𝑇, ℝ, <
))) |
192 | 109, 191 | syld 46 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ (∀𝑢 ∈
ℂ ((abs‘(𝑢
− inf(𝑇, ℝ,
< ))) < 𝑠 →
(abs‘(((𝑝 ∈
ℂ ↦ (𝑝 −
(𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, < )↑3))) →
(inf(𝑇, ℝ, < ) +
(𝑠 / 2)) ≤ inf(𝑇, ℝ, <
))) |
193 | 104, 192 | mtod 188 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) ∧ 𝑠 ∈ ℝ+)
→ ¬ ∀𝑢
∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
194 | 193 | nrexdv 2984 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 0 < inf(𝑇, ℝ, < )) → ¬
∃𝑠 ∈
ℝ+ ∀𝑢 ∈ ℂ ((abs‘(𝑢 − inf(𝑇, ℝ, < ))) < 𝑠 → (abs‘(((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘𝑢) − ((𝑝 ∈ ℂ ↦ (𝑝 − (𝐶 · (𝑝↑3))))‘inf(𝑇, ℝ, < )))) < (𝐶 · (inf(𝑇, ℝ, <
)↑3)))) |
195 | 96, 194 | pm2.65da 598 |
. . . . . . . 8
⊢ (𝜑 → ¬ 0 < inf(𝑇, ℝ, <
)) |
196 | 195 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → ¬ 0
< inf(𝑇, ℝ, <
)) |
197 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 𝑇 ⊆
ℝ) |
198 | 68 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 𝑇 ≠ ∅) |
199 | 83 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑥 ∈ ℝ
∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) |
200 | 133 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 𝑠 ∈
ℝ) |
201 | | infregelb 10884 |
. . . . . . . . . 10
⊢ (((𝑇 ⊆ ℝ ∧ 𝑇 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝑇 𝑥 ≤ 𝑤) ∧ 𝑠 ∈ ℝ) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤 ∈ 𝑇 𝑠 ≤ 𝑤)) |
202 | 197, 198,
199, 200, 201 | syl31anc 1321 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑤 ∈ 𝑇 𝑠 ≤ 𝑤)) |
203 | 22 | raleqi 3119 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
𝑇 𝑠 ≤ 𝑤 ↔ ∀𝑤 ∈ {𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}𝑠 ≤ 𝑤) |
204 | | breq2 4587 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑡 → (𝑠 ≤ 𝑤 ↔ 𝑠 ≤ 𝑡)) |
205 | 204 | ralrab2 3339 |
. . . . . . . . . 10
⊢
(∀𝑤 ∈
{𝑡 ∈ (0[,]𝐴) ∣ ∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡}𝑠 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
206 | 203, 205 | bitri 263 |
. . . . . . . . 9
⊢
(∀𝑤 ∈
𝑇 𝑠 ≤ 𝑤 ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
207 | 202, 206 | syl6bb 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) ↔ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡))) |
208 | | rpgt0 11720 |
. . . . . . . . . 10
⊢ (𝑠 ∈ ℝ+
→ 0 < 𝑠) |
209 | 208 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 0 <
𝑠) |
210 | | 0red 9920 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → 0 ∈
ℝ) |
211 | 85 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → inf(𝑇, ℝ, < ) ∈
ℝ) |
212 | | ltletr 10008 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ ∧ 𝑠
∈ ℝ ∧ inf(𝑇,
ℝ, < ) ∈ ℝ) → ((0 < 𝑠 ∧ 𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, <
))) |
213 | 210, 200,
211, 212 | syl3anc 1318 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → ((0 <
𝑠 ∧ 𝑠 ≤ inf(𝑇, ℝ, < )) → 0 < inf(𝑇, ℝ, <
))) |
214 | 209, 213 | mpand 707 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → (𝑠 ≤ inf(𝑇, ℝ, < ) → 0 < inf(𝑇, ℝ, <
))) |
215 | 207, 214 | sylbird 249 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
(∀𝑡 ∈
(0[,]𝐴)(∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡) → 0 < inf(𝑇, ℝ, < ))) |
216 | 196, 215 | mtod 188 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) → ¬
∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
217 | | rexanali 2981 |
. . . . . 6
⊢
(∃𝑡 ∈
(0[,]𝐴)(∃𝑦 ∈ ℝ+
∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡) ↔ ¬ ∀𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → 𝑠 ≤ 𝑡)) |
218 | 216, 217 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡)) |
219 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → (𝑅‘𝑧) = (𝑅‘𝑥)) |
220 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = 𝑥 → 𝑧 = 𝑥) |
221 | 219, 220 | oveq12d 6567 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑥 → ((𝑅‘𝑧) / 𝑧) = ((𝑅‘𝑥) / 𝑥)) |
222 | 221 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑥 → (abs‘((𝑅‘𝑧) / 𝑧)) = (abs‘((𝑅‘𝑥) / 𝑥))) |
223 | 222 | breq1d 4593 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑥 → ((abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡)) |
224 | 223 | cbvralv 3147 |
. . . . . . . . . . 11
⊢
(∀𝑧 ∈
(𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ↔ ∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) |
225 | | rpre 11715 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
226 | 225 | ad2antll 761 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ∈
ℝ) |
227 | | simprl 790 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑦 ≤ 𝑥) |
228 | | simplr 788 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑦 ∈
ℝ+) |
229 | 228 | rpred 11748 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑦 ∈
ℝ) |
230 | | elicopnf 12140 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ℝ → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥))) |
231 | 229, 230 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑥 ∈ (𝑦[,)+∞) ↔ (𝑥 ∈ ℝ ∧ 𝑦 ≤ 𝑥))) |
232 | 226, 227,
231 | mpbir2and 959 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ∈ (𝑦[,)+∞)) |
233 | | pntlem3.r |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
234 | 233 | pntrval 25051 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
235 | 234 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑅‘𝑥) = ((ψ‘𝑥) − 𝑥)) |
236 | 235 | oveq1d 6564 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → ((𝑅‘𝑥) / 𝑥) = (((ψ‘𝑥) − 𝑥) / 𝑥)) |
237 | | chpcl 24650 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
238 | 226, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(ψ‘𝑥) ∈
ℝ) |
239 | 238 | recnd 9947 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(ψ‘𝑥) ∈
ℂ) |
240 | | rpcn 11717 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
241 | 240 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ∈
ℂ) |
242 | | rpne0 11724 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
243 | 242 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑥 ≠ 0) |
244 | 239, 241,
241, 243 | divsubdird 10719 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) −
𝑥) / 𝑥) = (((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥))) |
245 | 241, 243 | dividd 10678 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑥 / 𝑥) = 1) |
246 | 245 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − (𝑥 / 𝑥)) = (((ψ‘𝑥) / 𝑥) − 1)) |
247 | 236, 244,
246 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − 1) = ((𝑅‘𝑥) / 𝑥)) |
248 | 247 | fveq2d 6107 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(abs‘(((ψ‘𝑥) / 𝑥) − 1)) = (abs‘((𝑅‘𝑥) / 𝑥))) |
249 | 248 | breq1d 4593 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ↔ (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡)) |
250 | | simprr 792 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) → ¬ 𝑠 ≤ 𝑡) |
251 | 250 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → ¬
𝑠 ≤ 𝑡) |
252 | 29 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) → (0[,]𝐴) ⊆ ℝ) |
253 | 252 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(0[,]𝐴) ⊆
ℝ) |
254 | | simplrl 796 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) → 𝑡 ∈ (0[,]𝐴)) |
255 | 254 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑡 ∈ (0[,]𝐴)) |
256 | 253, 255 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑡 ∈
ℝ) |
257 | | simp-4r 803 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑠 ∈
ℝ+) |
258 | 257 | rpred 11748 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑠 ∈
ℝ) |
259 | 256, 258 | ltnled 10063 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → (𝑡 < 𝑠 ↔ ¬ 𝑠 ≤ 𝑡)) |
260 | 251, 259 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → 𝑡 < 𝑠) |
261 | 225, 237 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑥 ∈ ℝ+
→ (ψ‘𝑥)
∈ ℝ) |
262 | | rerpdivcl 11737 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((ψ‘𝑥)
∈ ℝ ∧ 𝑥
∈ ℝ+) → ((ψ‘𝑥) / 𝑥) ∈ ℝ) |
263 | 261, 262 | mpancom 700 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥) /
𝑥) ∈
ℝ) |
264 | 263 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((ψ‘𝑥) / 𝑥) ∈
ℝ) |
265 | | resubcl 10224 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((ψ‘𝑥) /
𝑥) ∈ ℝ ∧ 1
∈ ℝ) → (((ψ‘𝑥) / 𝑥) − 1) ∈ ℝ) |
266 | 264, 38, 265 | sylancl 693 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − 1) ∈
ℝ) |
267 | 266 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((ψ‘𝑥) / 𝑥) − 1) ∈
ℂ) |
268 | 267 | abscld 14023 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈
ℝ) |
269 | | lelttr 10007 |
. . . . . . . . . . . . . . . . . 18
⊢
(((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ∈ ℝ ∧ 𝑡 ∈ ℝ ∧ 𝑠 ∈ ℝ) →
(((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ∧ 𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
270 | 268, 256,
258, 269 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
(((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 ∧ 𝑡 < 𝑠) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
271 | 260, 270 | mpan2d 706 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((abs‘(((ψ‘𝑥) / 𝑥) − 1)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
272 | 249, 271 | sylbird 249 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) →
((abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
273 | 232, 272 | embantd 57 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑠 ∈ ℝ+)
∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) ∧ (𝑦 ≤ 𝑥 ∧ 𝑥 ∈ ℝ+)) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
274 | 273 | exp32 629 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) → (𝑦 ≤ 𝑥 → (𝑥 ∈ ℝ+ → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))) |
275 | 274 | com24 93 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) → ((𝑥 ∈ (𝑦[,)+∞) → (abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡) → (𝑥 ∈ ℝ+ → (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)))) |
276 | 275 | ralimdv2 2944 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) →
(∀𝑥 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑥) / 𝑥)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
277 | 224, 276 | syl5bi 231 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) ∧ 𝑦 ∈ ℝ+) →
(∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
278 | 277 | reximdva 3000 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ (𝑡 ∈ (0[,]𝐴) ∧ ¬ 𝑠 ≤ 𝑡)) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
279 | 278 | anassrs 678 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ¬ 𝑠 ≤ 𝑡) → (∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
280 | 279 | impancom 455 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) ∧ ∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡) → (¬ 𝑠 ≤ 𝑡 → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
281 | 280 | expimpd 627 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑠 ∈ ℝ+) ∧ 𝑡 ∈ (0[,]𝐴)) → ((∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
282 | 281 | rexlimdva 3013 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
(∃𝑡 ∈ (0[,]𝐴)(∃𝑦 ∈ ℝ+ ∀𝑧 ∈ (𝑦[,)+∞)(abs‘((𝑅‘𝑧) / 𝑧)) ≤ 𝑡 ∧ ¬ 𝑠 ≤ 𝑡) → ∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
283 | 218, 282 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑦 ∈
ℝ+ ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
284 | | ssrexv 3630 |
. . . 4
⊢
(ℝ+ ⊆ ℝ → (∃𝑦 ∈ ℝ+ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
285 | 1, 283, 284 | mpsyl 66 |
. . 3
⊢ ((𝜑 ∧ 𝑠 ∈ ℝ+) →
∃𝑦 ∈ ℝ
∀𝑥 ∈
ℝ+ (𝑦 ≤
𝑥 →
(abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
286 | 285 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑠 ∈ ℝ+ ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+
(𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠)) |
287 | 263 | recnd 9947 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ ((ψ‘𝑥) /
𝑥) ∈
ℂ) |
288 | 287 | rgen 2906 |
. . . 4
⊢
∀𝑥 ∈
ℝ+ ((ψ‘𝑥) / 𝑥) ∈ ℂ |
289 | 288 | a1i 11 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ℝ+
((ψ‘𝑥) / 𝑥) ∈
ℂ) |
290 | 1 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ+
⊆ ℝ) |
291 | | 1cnd 9935 |
. . 3
⊢ (𝜑 → 1 ∈
ℂ) |
292 | 289, 290,
291 | rlim2 14075 |
. 2
⊢ (𝜑 → ((𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥)) ⇝𝑟 1
↔ ∀𝑠 ∈
ℝ+ ∃𝑦 ∈ ℝ ∀𝑥 ∈ ℝ+ (𝑦 ≤ 𝑥 → (abs‘(((ψ‘𝑥) / 𝑥) − 1)) < 𝑠))) |
293 | 286, 292 | mpbird 246 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
((ψ‘𝑥) / 𝑥)) ⇝𝑟
1) |