Step | Hyp | Ref
| Expression |
1 | | rpreccl 12642 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ (1 / 𝑟) ∈
ℝ+) |
2 | 1 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (1 /
𝑟) ∈
ℝ+) |
3 | | rpreccl 12642 |
. . . . . . . . 9
⊢ (𝑡 ∈ ℝ+
→ (1 / 𝑡) ∈
ℝ+) |
4 | | rpcnne0 12634 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ+
→ (𝑡 ∈ ℂ
∧ 𝑡 ≠
0)) |
5 | 4 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) |
6 | | recrec 11559 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / (1 / 𝑡)) = 𝑡) |
7 | 5, 6 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / (1 /
𝑡)) = 𝑡) |
8 | 7 | eqcomd 2745 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 = (1 / (1 / 𝑡))) |
9 | | oveq2 7243 |
. . . . . . . . . 10
⊢ (𝑟 = (1 / 𝑡) → (1 / 𝑟) = (1 / (1 / 𝑡))) |
10 | 9 | rspceeqv 3567 |
. . . . . . . . 9
⊢ (((1 /
𝑡) ∈
ℝ+ ∧ 𝑡
= (1 / (1 / 𝑡))) →
∃𝑟 ∈
ℝ+ 𝑡 = (1
/ 𝑟)) |
11 | 3, 8, 10 | syl2an2 686 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
∃𝑟 ∈
ℝ+ 𝑡 = (1
/ 𝑟)) |
12 | | simpr 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → 𝑡 = (1 / 𝑟)) |
13 | 12 | breq1d 5080 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (𝑡 < 𝑦 ↔ (1 / 𝑟) < 𝑦)) |
14 | 13 | imbi1d 345 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → ((𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
15 | 14 | ralbidv 3121 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
16 | 2, 11, 15 | rexxfrd 5319 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
17 | 16 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
18 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑟 ∈ ℝ+) |
19 | | rlimcnp.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆
ℝ+) |
20 | 19 | sselda 3918 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+) |
21 | 20 | adantlr 715 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+) |
22 | | elrp 12618 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ℝ+
↔ (𝑟 ∈ ℝ
∧ 0 < 𝑟)) |
23 | | elrp 12618 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
↔ (𝑦 ∈ ℝ
∧ 0 < 𝑦)) |
24 | | ltrec1 11749 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ ℝ ∧ 0 <
𝑟) ∧ (𝑦 ∈ ℝ ∧ 0 <
𝑦)) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
25 | 22, 23, 24 | syl2anb 601 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
26 | 18, 21, 25 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
27 | 26 | imbi1d 345 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
28 | 27 | ralbidva 3120 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
29 | 28 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
30 | | rpcn 12626 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
31 | | rpne0 12632 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
32 | 30, 31 | recrecd 11635 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / (1 / 𝑦)) =
𝑦) |
33 | 20, 32 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) = 𝑦) |
34 | | simpr 488 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
35 | 33, 34 | eqeltrd 2840 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) ∈ 𝐵) |
36 | | eleq1 2827 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑦) ∈ 𝐴)) |
37 | | oveq2 7243 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦))) |
38 | 37 | eleq1d 2824 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → ((1 / 𝑥) ∈ 𝐵 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)) |
39 | 36, 38 | bibi12d 349 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1 / 𝑦) → ((𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵) ↔ ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵))) |
40 | | rlimcnp.d |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
41 | 40 | ralrimiva 3108 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
42 | 41 | adantr 484 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
43 | 20 | rpreccld 12668 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈
ℝ+) |
44 | 39, 42, 43 | rspcdva 3554 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)) |
45 | 35, 44 | mpbird 260 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ 𝐴) |
46 | 43 | rpne0d 12663 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ≠ 0) |
47 | | eldifsn 4717 |
. . . . . . . . . . . 12
⊢ ((1 /
𝑦) ∈ (𝐴 ∖ {0}) ↔ ((1 / 𝑦) ∈ 𝐴 ∧ (1 / 𝑦) ≠ 0)) |
48 | 45, 46, 47 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ (𝐴 ∖ {0})) |
49 | | eldifi 4058 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ∈ 𝐴) |
50 | 49 | adantl 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ 𝐴) |
51 | | rge0ssre 13074 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
52 | | rlimcnp.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) |
53 | 52 | ssdifssd 4074 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∖ {0}) ⊆
(0[,)+∞)) |
54 | 53 | sselda 3918 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ (0[,)+∞)) |
55 | 51, 54 | sselid 3915 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ) |
56 | | 0re 10865 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
57 | | pnfxr 10917 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
58 | | elico2 13029 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 <
+∞))) |
59 | 56, 57, 58 | mp2an 692 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 <
+∞)) |
60 | 59 | simp2bi 1148 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0[,)+∞) → 0
≤ 𝑥) |
61 | 54, 60 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 ≤ 𝑥) |
62 | | eldifsni 4720 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ≠ 0) |
63 | 62 | adantl 485 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ≠ 0) |
64 | 55, 61, 63 | ne0gt0d 10999 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 < 𝑥) |
65 | 55, 64 | elrpd 12655 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ+) |
66 | 65, 40 | syldan 594 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
67 | 50, 66 | mpbid 235 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / 𝑥) ∈ 𝐵) |
68 | | rpcn 12626 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
69 | | rpne0 12632 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
70 | 68, 69 | recrecd 11635 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (1 / (1 / 𝑥)) =
𝑥) |
71 | 65, 70 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / (1 / 𝑥)) = 𝑥) |
72 | 71 | eqcomd 2745 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 = (1 / (1 / 𝑥))) |
73 | | oveq2 7243 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑥) → (1 / 𝑦) = (1 / (1 / 𝑥))) |
74 | 73 | rspceeqv 3567 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑥) ∈ 𝐵 ∧ 𝑥 = (1 / (1 / 𝑥))) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦)) |
75 | 67, 72, 74 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦)) |
76 | | breq1 5073 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 / 𝑦) → (𝑥 < 𝑟 ↔ (1 / 𝑦) < 𝑟)) |
77 | | rlimcnp.s |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆) |
78 | 77 | fvoveq1d 7257 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1 / 𝑦) → (abs‘(𝑅 − 𝐶)) = (abs‘(𝑆 − 𝐶))) |
79 | 78 | breq1d 5080 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 / 𝑦) → ((abs‘(𝑅 − 𝐶)) < 𝑧 ↔ (abs‘(𝑆 − 𝐶)) < 𝑧)) |
80 | 76, 79 | imbi12d 348 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1 / 𝑦) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
81 | 80 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = (1 / 𝑦)) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
82 | 48, 75, 81 | ralxfrd 5318 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
83 | 82 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
84 | 29, 83 | bitr4d 285 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
85 | | elsni 4575 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
86 | 85 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑥 = 0) |
87 | | rlimcnp.c |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → 𝑅 = 𝐶) |
88 | 86, 87 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑅 = 𝐶) |
89 | 88 | oveq1d 7250 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = (𝐶 − 𝐶)) |
90 | 87 | eleq1d 2824 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
91 | | rlimcnp.r |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
92 | 91 | ralrimiva 3108 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
93 | | rlimcnp.0 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ 𝐴) |
94 | 90, 92, 93 | rspcdva 3554 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ℂ) |
95 | 94 | subidd 11207 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 − 𝐶) = 0) |
96 | 95 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝐶 − 𝐶) = 0) |
97 | 89, 96 | eqtrd 2779 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = 0) |
98 | 97 | abs00bd 14888 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) →
(abs‘(𝑅 − 𝐶)) = 0) |
99 | | rpgt0 12628 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ 0 < 𝑧) |
100 | 99 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 0 < 𝑧) |
101 | 98, 100 | eqbrtrd 5092 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) →
(abs‘(𝑅 − 𝐶)) < 𝑧) |
102 | 101 | a1d 25 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
103 | 102 | ralrimiva 3108 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
104 | 103 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ ∀𝑥 ∈ {0}
(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
105 | 104 | biantrud 535 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))) |
106 | | ralunb 4122 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
((𝐴 ∖ {0}) ∪
{0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
107 | 105, 106 | bitr4di 292 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ ((𝐴 ∖ {0}) ∪ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
108 | | undif1 4407 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ {0}) ∪ {0}) =
(𝐴 ∪
{0}) |
109 | 93 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ 0 ∈ 𝐴) |
110 | 109 | snssd 4739 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ {0} ⊆ 𝐴) |
111 | | ssequn2 4114 |
. . . . . . . . . . 11
⊢ ({0}
⊆ 𝐴 ↔ (𝐴 ∪ {0}) = 𝐴) |
112 | 110, 111 | sylib 221 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (𝐴 ∪ {0}) =
𝐴) |
113 | 108, 112 | syl5eq 2792 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ ((𝐴 ∖ {0})
∪ {0}) = 𝐴) |
114 | 113 | raleqdv 3340 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
((𝐴 ∖ {0}) ∪
{0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
115 | 84, 107, 114 | 3bitrd 308 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
116 | 115 | rexbidva 3225 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑟 ∈
ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
117 | 17, 116 | bitrd 282 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
118 | 117 | ralbidva 3120 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
119 | | nfv 1922 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑤((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 |
120 | | nffvmpt1 6750 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) |
121 | | nfcv 2907 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs
∘ − ) |
122 | | nffvmpt1 6750 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) |
123 | 120, 121,
122 | nfov 7265 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) |
124 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
< |
125 | | nfcv 2907 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 |
126 | 123, 124,
125 | nfbr 5117 |
. . . . . . . . 9
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 |
127 | 119, 126 | nfim 1904 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑤((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) |
128 | | nfv 1922 |
. . . . . . . 8
⊢
Ⅎ𝑤((𝑥((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) |
129 | | oveq1 7242 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0)) |
130 | 129 | breq1d 5080 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟)) |
131 | | fveq2 6739 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)) |
132 | 131 | oveq1d 7250 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0))) |
133 | 132 | breq1d 5080 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)) |
134 | 130, 133 | imbi12d 348 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))) |
135 | 127, 128,
134 | cbvralw 3364 |
. . . . . . 7
⊢
(∀𝑤 ∈
𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)) |
136 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
137 | 93 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐴) |
138 | 136, 137 | ovresd 7397 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥(abs ∘ − )0)) |
139 | 52, 51 | sstrdi 3930 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
140 | | ax-resscn 10816 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
141 | 139, 140 | sstrdi 3930 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
142 | 141 | sselda 3918 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
143 | | 0cnd 10856 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ) |
144 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
145 | 144 | cnmetdval 23700 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑥(abs
∘ − )0) = (abs‘(𝑥 − 0))) |
146 | 142, 143,
145 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0))) |
147 | 142 | subid1d 11208 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 − 0) = 𝑥) |
148 | 147 | fveq2d 6743 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝑥 − 0)) = (abs‘𝑥)) |
149 | 138, 146,
148 | 3eqtrd 2783 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (abs‘𝑥)) |
150 | 139 | sselda 3918 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
151 | 52 | sselda 3918 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (0[,)+∞)) |
152 | 151, 60 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝑥) |
153 | 150, 152 | absidd 15019 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝑥) = 𝑥) |
154 | 149, 153 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = 𝑥) |
155 | 154 | breq1d 5080 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ 𝑥 < 𝑟)) |
156 | | eqid 2739 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
157 | 156 | fvmpt2 6851 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
158 | 136, 91, 157 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
159 | 94 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
160 | 156, 87, 137, 159 | fvmptd3 6863 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) = 𝐶) |
161 | 158, 160 | oveq12d 7253 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (𝑅(abs ∘ − )𝐶)) |
162 | 144 | cnmetdval 23700 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
163 | 91, 159, 162 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
164 | 161, 163 | eqtrd 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (abs‘(𝑅 − 𝐶))) |
165 | 164 | breq1d 5080 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (abs‘(𝑅 − 𝐶)) < 𝑧)) |
166 | 155, 165 | imbi12d 348 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
167 | 166 | ralbidva 3120 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
168 | 135, 167 | syl5bb 286 |
. . . . . 6
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
169 | 168 | rexbidv 3226 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
170 | 169 | ralbidv 3121 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
171 | 91 | fmpttd 6954 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
172 | 171 | biantrurd 536 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
173 | 118, 170,
172 | 3bitr2d 310 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
174 | 77 | eleq1d 2824 |
. . . . . . . 8
⊢ (𝑥 = (1 / 𝑦) → (𝑅 ∈ ℂ ↔ 𝑆 ∈ ℂ)) |
175 | 92 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
176 | 174, 175,
45 | rspcdva 3554 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
177 | 176 | ralrimiva 3108 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 𝑆 ∈ ℂ) |
178 | | rpssre 12623 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
179 | 19, 178 | sstrdi 3930 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
180 | | 1red 10864 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
181 | 177, 179,
94, 180 | rlim3 15092 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
182 | | 0xr 10910 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
183 | | 0lt1 11384 |
. . . . . . . . . 10
⊢ 0 <
1 |
184 | | df-ioo 12969 |
. . . . . . . . . . 11
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
185 | | df-ico 12971 |
. . . . . . . . . . 11
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
186 | | xrltletr 12777 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
187 | 184, 185,
186 | ixxss1 12983 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
188 | 182, 183,
187 | mp2an 692 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
189 | | ioorp 13043 |
. . . . . . . . 9
⊢
(0(,)+∞) = ℝ+ |
190 | 188, 189 | sseqtri 3954 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ ℝ+ |
191 | | ssrexv 3985 |
. . . . . . . 8
⊢
((1[,)+∞) ⊆ ℝ+ → (∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
192 | 190, 191 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
193 | | simplr 769 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ+) |
194 | 178, 193 | sselid 3915 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ) |
195 | 179 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ⊆
ℝ) |
196 | 195 | sselda 3918 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ) |
197 | | ltle 10951 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦)) |
198 | 194, 196,
197 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦)) |
199 | 198 | imim1d 82 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
200 | 199 | ralimdva 3103 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
201 | 200 | reximdva 3203 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
202 | 192, 201 | syl5 34 |
. . . . . 6
⊢ (𝜑 → (∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
203 | 202 | ralimdv 3104 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+
∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
204 | 181, 203 | sylbid 243 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 → ∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
205 | | ssrexv 3985 |
. . . . . . 7
⊢
(ℝ+ ⊆ ℝ → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
206 | 178, 205 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
207 | 206 | ralimi 3087 |
. . . . 5
⊢
(∀𝑧 ∈
ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
208 | 177, 179,
94 | rlim2lt 15091 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈ ℝ
∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
209 | 207, 208 | syl5ibr 249 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶)) |
210 | 204, 209 | impbid 215 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
211 | | cnxmet 23702 |
. . . . 5
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
212 | | xmetres2 23291 |
. . . . 5
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐴
× 𝐴)) ∈
(∞Met‘𝐴)) |
213 | 211, 141,
212 | sylancr 590 |
. . . 4
⊢ (𝜑 → ((abs ∘ − )
↾ (𝐴 × 𝐴)) ∈
(∞Met‘𝐴)) |
214 | 211 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
215 | | eqid 2739 |
. . . . 5
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴))) |
216 | | rlimcnp.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
217 | 216 | cnfldtopn 23711 |
. . . . 5
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
218 | 215, 217 | metcnp2 23472 |
. . . 4
⊢ ((((abs
∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴) ∧ (abs ∘ − )
∈ (∞Met‘ℂ) ∧ 0 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
219 | 213, 214,
93, 218 | syl3anc 1373 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
220 | 173, 210,
219 | 3bitr4d 314 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0))) |
221 | | rlimcnp.k |
. . . . . 6
⊢ 𝐾 = (𝐽 ↾t 𝐴) |
222 | | eqid 2739 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (𝐴 × 𝐴)) = ((abs ∘ − ) ↾ (𝐴 × 𝐴)) |
223 | 222, 217,
215 | metrest 23454 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
224 | 211, 141,
223 | sylancr 590 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
225 | 221, 224 | syl5eq 2792 |
. . . . 5
⊢ (𝜑 → 𝐾 = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
226 | 225 | oveq1d 7250 |
. . . 4
⊢ (𝜑 → (𝐾 CnP 𝐽) = ((MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴))) CnP 𝐽)) |
227 | 226 | fveq1d 6741 |
. . 3
⊢ (𝜑 → ((𝐾 CnP 𝐽)‘0) = (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0)) |
228 | 227 | eleq2d 2825 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0))) |
229 | 220, 228 | bitr4d 285 |
1
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0))) |