Step | Hyp | Ref
| Expression |
1 | | rpreccl 12165 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ (1 / 𝑟) ∈
ℝ+) |
2 | 1 | adantl 475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (1 /
𝑟) ∈
ℝ+) |
3 | | rpreccl 12165 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ+
→ (1 / 𝑡) ∈
ℝ+) |
4 | 3 | adantl 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 /
𝑡) ∈
ℝ+) |
5 | | rpcnne0 12157 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ+
→ (𝑡 ∈ ℂ
∧ 𝑡 ≠
0)) |
6 | 5 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) |
7 | | recrec 11072 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / (1 / 𝑡)) = 𝑡) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / (1 /
𝑡)) = 𝑡) |
9 | 8 | eqcomd 2784 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 = (1 / (1 / 𝑡))) |
10 | | oveq2 6930 |
. . . . . . . . . 10
⊢ (𝑟 = (1 / 𝑡) → (1 / 𝑟) = (1 / (1 / 𝑡))) |
11 | 10 | rspceeqv 3529 |
. . . . . . . . 9
⊢ (((1 /
𝑡) ∈
ℝ+ ∧ 𝑡
= (1 / (1 / 𝑡))) →
∃𝑟 ∈
ℝ+ 𝑡 = (1
/ 𝑟)) |
12 | 4, 9, 11 | syl2anc 579 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
∃𝑟 ∈
ℝ+ 𝑡 = (1
/ 𝑟)) |
13 | | simpr 479 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → 𝑡 = (1 / 𝑟)) |
14 | 13 | breq1d 4896 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (𝑡 < 𝑦 ↔ (1 / 𝑟) < 𝑦)) |
15 | 14 | imbi1d 333 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → ((𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
16 | 15 | ralbidv 3168 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
17 | 2, 12, 16 | rexxfrd 5121 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
18 | 17 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
19 | | simplr 759 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑟 ∈ ℝ+) |
20 | | rlimcnp.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆
ℝ+) |
21 | 20 | sselda 3821 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+) |
22 | 21 | adantlr 705 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+) |
23 | | elrp 12139 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ℝ+
↔ (𝑟 ∈ ℝ
∧ 0 < 𝑟)) |
24 | | elrp 12139 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
↔ (𝑦 ∈ ℝ
∧ 0 < 𝑦)) |
25 | | ltrec1 11264 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ ℝ ∧ 0 <
𝑟) ∧ (𝑦 ∈ ℝ ∧ 0 <
𝑦)) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
26 | 23, 24, 25 | syl2anb 591 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
27 | 19, 22, 26 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
28 | 27 | imbi1d 333 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
29 | 28 | ralbidva 3167 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
30 | 29 | adantlr 705 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
31 | | rpcn 12149 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
32 | | rpne0 12155 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
33 | 31, 32 | recrecd 11148 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / (1 / 𝑦)) =
𝑦) |
34 | 21, 33 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) = 𝑦) |
35 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
36 | 34, 35 | eqeltrd 2859 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) ∈ 𝐵) |
37 | | eleq1 2847 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑦) ∈ 𝐴)) |
38 | | oveq2 6930 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦))) |
39 | 38 | eleq1d 2844 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → ((1 / 𝑥) ∈ 𝐵 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)) |
40 | 37, 39 | bibi12d 337 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1 / 𝑦) → ((𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵) ↔ ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵))) |
41 | | rlimcnp.d |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
42 | 41 | ralrimiva 3148 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
43 | 42 | adantr 474 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
44 | | rpreccl 12165 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
45 | 21, 44 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈
ℝ+) |
46 | 40, 43, 45 | rspcdva 3517 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)) |
47 | 36, 46 | mpbird 249 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ 𝐴) |
48 | 45 | rpne0d 12186 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ≠ 0) |
49 | | eldifsn 4550 |
. . . . . . . . . . . 12
⊢ ((1 /
𝑦) ∈ (𝐴 ∖ {0}) ↔ ((1 / 𝑦) ∈ 𝐴 ∧ (1 / 𝑦) ≠ 0)) |
50 | 47, 48, 49 | sylanbrc 578 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ (𝐴 ∖ {0})) |
51 | | eldifi 3955 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ∈ 𝐴) |
52 | 51 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ 𝐴) |
53 | | rge0ssre 12594 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
54 | | rlimcnp.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) |
55 | 54 | ssdifssd 3971 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∖ {0}) ⊆
(0[,)+∞)) |
56 | 55 | sselda 3821 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ (0[,)+∞)) |
57 | 53, 56 | sseldi 3819 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ) |
58 | | 0re 10378 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
59 | | pnfxr 10430 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
60 | | elico2 12549 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 <
+∞))) |
61 | 58, 59, 60 | mp2an 682 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 <
+∞)) |
62 | 61 | simp2bi 1137 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0[,)+∞) → 0
≤ 𝑥) |
63 | 56, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 ≤ 𝑥) |
64 | | eldifsni 4553 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ≠ 0) |
65 | 64 | adantl 475 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ≠ 0) |
66 | 57, 63, 65 | ne0gt0d 10513 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 < 𝑥) |
67 | 57, 66 | elrpd 12178 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ+) |
68 | 67, 41 | syldan 585 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
69 | 52, 68 | mpbid 224 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / 𝑥) ∈ 𝐵) |
70 | | rpcn 12149 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
71 | | rpne0 12155 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
72 | 70, 71 | recrecd 11148 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (1 / (1 / 𝑥)) =
𝑥) |
73 | 67, 72 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / (1 / 𝑥)) = 𝑥) |
74 | 73 | eqcomd 2784 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 = (1 / (1 / 𝑥))) |
75 | | oveq2 6930 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑥) → (1 / 𝑦) = (1 / (1 / 𝑥))) |
76 | 75 | rspceeqv 3529 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑥) ∈ 𝐵 ∧ 𝑥 = (1 / (1 / 𝑥))) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦)) |
77 | 69, 74, 76 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦)) |
78 | | breq1 4889 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 / 𝑦) → (𝑥 < 𝑟 ↔ (1 / 𝑦) < 𝑟)) |
79 | | rlimcnp.s |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆) |
80 | 79 | fvoveq1d 6944 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1 / 𝑦) → (abs‘(𝑅 − 𝐶)) = (abs‘(𝑆 − 𝐶))) |
81 | 80 | breq1d 4896 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 / 𝑦) → ((abs‘(𝑅 − 𝐶)) < 𝑧 ↔ (abs‘(𝑆 − 𝐶)) < 𝑧)) |
82 | 78, 81 | imbi12d 336 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1 / 𝑦) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
83 | 82 | adantl 475 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = (1 / 𝑦)) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
84 | 50, 77, 83 | ralxfrd 5120 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
85 | 84 | ad2antrr 716 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
86 | 30, 85 | bitr4d 274 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
87 | | elsni 4415 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
88 | 87 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑥 = 0) |
89 | | rlimcnp.c |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → 𝑅 = 𝐶) |
90 | 88, 89 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑅 = 𝐶) |
91 | 90 | oveq1d 6937 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = (𝐶 − 𝐶)) |
92 | 89 | eleq1d 2844 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 0 → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
93 | | rlimcnp.r |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
94 | 93 | ralrimiva 3148 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
95 | | rlimcnp.0 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ 𝐴) |
96 | 92, 94, 95 | rspcdva 3517 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ℂ) |
97 | 96 | subidd 10722 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 − 𝐶) = 0) |
98 | 97 | ad2antrr 716 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝐶 − 𝐶) = 0) |
99 | 91, 98 | eqtrd 2814 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = 0) |
100 | 99 | abs00bd 14438 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) →
(abs‘(𝑅 − 𝐶)) = 0) |
101 | | rpgt0 12151 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ 0 < 𝑧) |
102 | 101 | ad2antlr 717 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 0 < 𝑧) |
103 | 100, 102 | eqbrtrd 4908 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) →
(abs‘(𝑅 − 𝐶)) < 𝑧) |
104 | 103 | a1d 25 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
105 | 104 | ralrimiva 3148 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
106 | 105 | adantr 474 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ ∀𝑥 ∈ {0}
(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
107 | 106 | biantrud 527 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))) |
108 | | ralunb 4017 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
((𝐴 ∖ {0}) ∪
{0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
109 | 107, 108 | syl6bbr 281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ ((𝐴 ∖ {0}) ∪ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
110 | | undif1 4267 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ {0}) ∪ {0}) =
(𝐴 ∪
{0}) |
111 | 95 | ad2antrr 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ 0 ∈ 𝐴) |
112 | 111 | snssd 4571 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ {0} ⊆ 𝐴) |
113 | | ssequn2 4009 |
. . . . . . . . . . 11
⊢ ({0}
⊆ 𝐴 ↔ (𝐴 ∪ {0}) = 𝐴) |
114 | 112, 113 | sylib 210 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (𝐴 ∪ {0}) =
𝐴) |
115 | 110, 114 | syl5eq 2826 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ ((𝐴 ∖ {0})
∪ {0}) = 𝐴) |
116 | 115 | raleqdv 3340 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
((𝐴 ∖ {0}) ∪
{0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
117 | 86, 109, 116 | 3bitrd 297 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
118 | 117 | rexbidva 3234 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑟 ∈
ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
119 | 18, 118 | bitrd 271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
120 | 119 | ralbidva 3167 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
121 | | nfv 1957 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑤((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 |
122 | | nffvmpt1 6457 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) |
123 | | nfcv 2934 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs
∘ − ) |
124 | | nffvmpt1 6457 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) |
125 | 122, 123,
124 | nfov 6952 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) |
126 | | nfcv 2934 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
< |
127 | | nfcv 2934 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 |
128 | 125, 126,
127 | nfbr 4933 |
. . . . . . . . 9
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 |
129 | 121, 128 | nfim 1943 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑤((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) |
130 | | nfv 1957 |
. . . . . . . 8
⊢
Ⅎ𝑤((𝑥((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) |
131 | | oveq1 6929 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0)) |
132 | 131 | breq1d 4896 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟)) |
133 | | fveq2 6446 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)) |
134 | 133 | oveq1d 6937 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0))) |
135 | 134 | breq1d 4896 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)) |
136 | 132, 135 | imbi12d 336 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))) |
137 | 129, 130,
136 | cbvral 3363 |
. . . . . . 7
⊢
(∀𝑤 ∈
𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)) |
138 | | simpr 479 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
139 | 95 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐴) |
140 | 138, 139 | ovresd 7078 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥(abs ∘ − )0)) |
141 | 54, 53 | syl6ss 3833 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
142 | | ax-resscn 10329 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
143 | 141, 142 | syl6ss 3833 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
144 | 143 | sselda 3821 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
145 | | 0cnd 10369 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ) |
146 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
147 | 146 | cnmetdval 22982 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑥(abs
∘ − )0) = (abs‘(𝑥 − 0))) |
148 | 144, 145,
147 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0))) |
149 | 144 | subid1d 10723 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 − 0) = 𝑥) |
150 | 149 | fveq2d 6450 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝑥 − 0)) = (abs‘𝑥)) |
151 | 140, 148,
150 | 3eqtrd 2818 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (abs‘𝑥)) |
152 | 141 | sselda 3821 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
153 | 54 | sselda 3821 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (0[,)+∞)) |
154 | 153, 62 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝑥) |
155 | 152, 154 | absidd 14569 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝑥) = 𝑥) |
156 | 151, 155 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = 𝑥) |
157 | 156 | breq1d 4896 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ 𝑥 < 𝑟)) |
158 | | eqid 2778 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
159 | 158 | fvmpt2 6552 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
160 | 138, 93, 159 | syl2anc 579 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
161 | 96 | adantr 474 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
162 | 158, 89, 139, 161 | fvmptd3 6564 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) = 𝐶) |
163 | 160, 162 | oveq12d 6940 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (𝑅(abs ∘ − )𝐶)) |
164 | 146 | cnmetdval 22982 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
165 | 93, 161, 164 | syl2anc 579 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
166 | 163, 165 | eqtrd 2814 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (abs‘(𝑅 − 𝐶))) |
167 | 166 | breq1d 4896 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (abs‘(𝑅 − 𝐶)) < 𝑧)) |
168 | 157, 167 | imbi12d 336 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
169 | 168 | ralbidva 3167 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
170 | 137, 169 | syl5bb 275 |
. . . . . 6
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
171 | 170 | rexbidv 3237 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
172 | 171 | ralbidv 3168 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
173 | 93 | fmpttd 6649 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
174 | 173 | biantrurd 528 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
175 | 120, 172,
174 | 3bitr2d 299 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
176 | 79 | eleq1d 2844 |
. . . . . . . 8
⊢ (𝑥 = (1 / 𝑦) → (𝑅 ∈ ℂ ↔ 𝑆 ∈ ℂ)) |
177 | 94 | adantr 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
178 | 176, 177,
47 | rspcdva 3517 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
179 | 178 | ralrimiva 3148 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 𝑆 ∈ ℂ) |
180 | | rpssre 12144 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
181 | 20, 180 | syl6ss 3833 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
182 | | 1red 10377 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
183 | 179, 181,
96, 182 | rlim3 14637 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
184 | | 0xr 10423 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
185 | | 0lt1 10897 |
. . . . . . . . . 10
⊢ 0 <
1 |
186 | | df-ioo 12491 |
. . . . . . . . . . 11
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
187 | | df-ico 12493 |
. . . . . . . . . . 11
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
188 | | xrltletr 12300 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
189 | 186, 187,
188 | ixxss1 12505 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
190 | 184, 185,
189 | mp2an 682 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
191 | | ioorp 12563 |
. . . . . . . . 9
⊢
(0(,)+∞) = ℝ+ |
192 | 190, 191 | sseqtri 3856 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ ℝ+ |
193 | | ssrexv 3886 |
. . . . . . . 8
⊢
((1[,)+∞) ⊆ ℝ+ → (∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
194 | 192, 193 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
195 | | simplr 759 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ+) |
196 | 180, 195 | sseldi 3819 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ) |
197 | 181 | adantr 474 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ⊆
ℝ) |
198 | 197 | sselda 3821 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ) |
199 | | ltle 10465 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦)) |
200 | 196, 198,
199 | syl2anc 579 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦)) |
201 | 200 | imim1d 82 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
202 | 201 | ralimdva 3144 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
203 | 202 | reximdva 3198 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
204 | 194, 203 | syl5 34 |
. . . . . 6
⊢ (𝜑 → (∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
205 | 204 | ralimdv 3145 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+
∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
206 | 183, 205 | sylbid 232 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 → ∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
207 | | ssrexv 3886 |
. . . . . . 7
⊢
(ℝ+ ⊆ ℝ → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
208 | 180, 207 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
209 | 208 | ralimi 3134 |
. . . . 5
⊢
(∀𝑧 ∈
ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
210 | 179, 181,
96 | rlim2lt 14636 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈ ℝ
∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
211 | 209, 210 | syl5ibr 238 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶)) |
212 | 206, 211 | impbid 204 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
213 | | cnxmet 22984 |
. . . . 5
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
214 | | xmetres2 22574 |
. . . . 5
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐴
× 𝐴)) ∈
(∞Met‘𝐴)) |
215 | 213, 143,
214 | sylancr 581 |
. . . 4
⊢ (𝜑 → ((abs ∘ − )
↾ (𝐴 × 𝐴)) ∈
(∞Met‘𝐴)) |
216 | 213 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
217 | | eqid 2778 |
. . . . 5
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴))) |
218 | | rlimcnp.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
219 | 218 | cnfldtopn 22993 |
. . . . 5
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
220 | 217, 219 | metcnp2 22755 |
. . . 4
⊢ ((((abs
∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴) ∧ (abs ∘ − )
∈ (∞Met‘ℂ) ∧ 0 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
221 | 215, 216,
95, 220 | syl3anc 1439 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
222 | 175, 212,
221 | 3bitr4d 303 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0))) |
223 | | rlimcnp.k |
. . . . . 6
⊢ 𝐾 = (𝐽 ↾t 𝐴) |
224 | | eqid 2778 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (𝐴 × 𝐴)) = ((abs ∘ − ) ↾ (𝐴 × 𝐴)) |
225 | 224, 219,
217 | metrest 22737 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
226 | 213, 143,
225 | sylancr 581 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
227 | 223, 226 | syl5eq 2826 |
. . . . 5
⊢ (𝜑 → 𝐾 = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
228 | 227 | oveq1d 6937 |
. . . 4
⊢ (𝜑 → (𝐾 CnP 𝐽) = ((MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴))) CnP 𝐽)) |
229 | 228 | fveq1d 6448 |
. . 3
⊢ (𝜑 → ((𝐾 CnP 𝐽)‘0) = (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0)) |
230 | 229 | eleq2d 2845 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0))) |
231 | 222, 230 | bitr4d 274 |
1
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0))) |