Step | Hyp | Ref
| Expression |
1 | | rpreccl 11733 |
. . . . . . . . 9
⊢ (𝑟 ∈ ℝ+
→ (1 / 𝑟) ∈
ℝ+) |
2 | 1 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (1 /
𝑟) ∈
ℝ+) |
3 | | rpreccl 11733 |
. . . . . . . . . 10
⊢ (𝑡 ∈ ℝ+
→ (1 / 𝑡) ∈
ℝ+) |
4 | 3 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 /
𝑡) ∈
ℝ+) |
5 | | rpcnne0 11726 |
. . . . . . . . . . . 12
⊢ (𝑡 ∈ ℝ+
→ (𝑡 ∈ ℂ
∧ 𝑡 ≠
0)) |
6 | 5 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (𝑡 ∈ ℂ ∧ 𝑡 ≠ 0)) |
7 | | recrec 10601 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℂ ∧ 𝑡 ≠ 0) → (1 / (1 / 𝑡)) = 𝑡) |
8 | 6, 7 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → (1 / (1 /
𝑡)) = 𝑡) |
9 | 8 | eqcomd 2616 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝑡 = (1 / (1 / 𝑡))) |
10 | | oveq2 6557 |
. . . . . . . . . . 11
⊢ (𝑟 = (1 / 𝑡) → (1 / 𝑟) = (1 / (1 / 𝑡))) |
11 | 10 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑟 = (1 / 𝑡) → (𝑡 = (1 / 𝑟) ↔ 𝑡 = (1 / (1 / 𝑡)))) |
12 | 11 | rspcev 3282 |
. . . . . . . . 9
⊢ (((1 /
𝑡) ∈
ℝ+ ∧ 𝑡
= (1 / (1 / 𝑡))) →
∃𝑟 ∈
ℝ+ 𝑡 = (1
/ 𝑟)) |
13 | 4, 9, 12 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
∃𝑟 ∈
ℝ+ 𝑡 = (1
/ 𝑟)) |
14 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → 𝑡 = (1 / 𝑟)) |
15 | 14 | breq1d 4593 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (𝑡 < 𝑦 ↔ (1 / 𝑟) < 𝑦)) |
16 | 15 | imbi1d 330 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → ((𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
17 | 16 | ralbidv 2969 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 = (1 / 𝑟)) → (∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
18 | 2, 13, 17 | rexxfrd 4807 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
19 | 18 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
20 | | simplr 788 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑟 ∈ ℝ+) |
21 | | rlimcnp.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆
ℝ+) |
22 | 21 | sselda 3568 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+) |
23 | 22 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ+) |
24 | | elrp 11710 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ℝ+
↔ (𝑟 ∈ ℝ
∧ 0 < 𝑟)) |
25 | | elrp 11710 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ+
↔ (𝑦 ∈ ℝ
∧ 0 < 𝑦)) |
26 | | ltrec1 10789 |
. . . . . . . . . . . . . 14
⊢ (((𝑟 ∈ ℝ ∧ 0 <
𝑟) ∧ (𝑦 ∈ ℝ ∧ 0 <
𝑦)) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
27 | 24, 25, 26 | syl2anb 495 |
. . . . . . . . . . . . 13
⊢ ((𝑟 ∈ ℝ+
∧ 𝑦 ∈
ℝ+) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
28 | 20, 23, 27 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑟) < 𝑦 ↔ (1 / 𝑦) < 𝑟)) |
29 | 28 | imbi1d 330 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
30 | 29 | ralbidva 2968 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
31 | 30 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
32 | | rpcn 11717 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ∈
ℂ) |
33 | | rpne0 11724 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℝ+
→ 𝑦 ≠
0) |
34 | 32, 33 | recrecd 10677 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / (1 / 𝑦)) =
𝑦) |
35 | 22, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) = 𝑦) |
36 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ 𝐵) |
37 | 35, 36 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / (1 / 𝑦)) ∈ 𝐵) |
38 | | rpreccl 11733 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ+
→ (1 / 𝑦) ∈
ℝ+) |
39 | 22, 38 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈
ℝ+) |
40 | | rlimcnp.d |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
41 | 40 | ralrimiva 2949 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
42 | 41 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
43 | | eleq1 2676 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1 / 𝑦) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑦) ∈ 𝐴)) |
44 | | oveq2 6557 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (1 / 𝑦) → (1 / 𝑥) = (1 / (1 / 𝑦))) |
45 | 44 | eleq1d 2672 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1 / 𝑦) → ((1 / 𝑥) ∈ 𝐵 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)) |
46 | 43, 45 | bibi12d 334 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → ((𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵) ↔ ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵))) |
47 | 46 | rspcv 3278 |
. . . . . . . . . . . . . 14
⊢ ((1 /
𝑦) ∈
ℝ+ → (∀𝑥 ∈ ℝ+ (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵))) |
48 | 39, 42, 47 | sylc 63 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ((1 / 𝑦) ∈ 𝐴 ↔ (1 / (1 / 𝑦)) ∈ 𝐵)) |
49 | 37, 48 | mpbird 246 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ 𝐴) |
50 | 39 | rpne0d 11753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ≠ 0) |
51 | | eldifsn 4260 |
. . . . . . . . . . . 12
⊢ ((1 /
𝑦) ∈ (𝐴 ∖ {0}) ↔ ((1 / 𝑦) ∈ 𝐴 ∧ (1 / 𝑦) ≠ 0)) |
52 | 49, 50, 51 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → (1 / 𝑦) ∈ (𝐴 ∖ {0})) |
53 | | eldifi 3694 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ∈ 𝐴) |
54 | 53 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ 𝐴) |
55 | | rge0ssre 12151 |
. . . . . . . . . . . . . . . 16
⊢
(0[,)+∞) ⊆ ℝ |
56 | | rlimcnp.a |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐴 ⊆ (0[,)+∞)) |
57 | 56 | ssdifssd 3710 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐴 ∖ {0}) ⊆
(0[,)+∞)) |
58 | 57 | sselda 3568 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ (0[,)+∞)) |
59 | 55, 58 | sseldi 3566 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ) |
60 | | 0re 9919 |
. . . . . . . . . . . . . . . . . . 19
⊢ 0 ∈
ℝ |
61 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . . 19
⊢ +∞
∈ ℝ* |
62 | | elico2 12108 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((0
∈ ℝ ∧ +∞ ∈ ℝ*) → (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 <
+∞))) |
63 | 60, 61, 62 | mp2an 704 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (0[,)+∞) ↔
(𝑥 ∈ ℝ ∧ 0
≤ 𝑥 ∧ 𝑥 <
+∞)) |
64 | 63 | simp2bi 1070 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (0[,)+∞) → 0
≤ 𝑥) |
65 | 58, 64 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 ≤ 𝑥) |
66 | | eldifsni 4261 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (𝐴 ∖ {0}) → 𝑥 ≠ 0) |
67 | 66 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ≠ 0) |
68 | 59, 65, 67 | ne0gt0d 10053 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 0 < 𝑥) |
69 | 59, 68 | elrpd 11745 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 ∈ ℝ+) |
70 | 69, 40 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (𝑥 ∈ 𝐴 ↔ (1 / 𝑥) ∈ 𝐵)) |
71 | 54, 70 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / 𝑥) ∈ 𝐵) |
72 | | rpcn 11717 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℂ) |
73 | | rpne0 11724 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ≠
0) |
74 | 72, 73 | recrecd 10677 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℝ+
→ (1 / (1 / 𝑥)) =
𝑥) |
75 | 69, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → (1 / (1 / 𝑥)) = 𝑥) |
76 | 75 | eqcomd 2616 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → 𝑥 = (1 / (1 / 𝑥))) |
77 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (1 / 𝑥) → (1 / 𝑦) = (1 / (1 / 𝑥))) |
78 | 77 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (𝑦 = (1 / 𝑥) → (𝑥 = (1 / 𝑦) ↔ 𝑥 = (1 / (1 / 𝑥)))) |
79 | 78 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ (((1 /
𝑥) ∈ 𝐵 ∧ 𝑥 = (1 / (1 / 𝑥))) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦)) |
80 | 71, 76, 79 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐴 ∖ {0})) → ∃𝑦 ∈ 𝐵 𝑥 = (1 / 𝑦)) |
81 | | breq1 4586 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 / 𝑦) → (𝑥 < 𝑟 ↔ (1 / 𝑦) < 𝑟)) |
82 | | rlimcnp.s |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (1 / 𝑦) → 𝑅 = 𝑆) |
83 | 82 | oveq1d 6564 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = (1 / 𝑦) → (𝑅 − 𝐶) = (𝑆 − 𝐶)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = (1 / 𝑦) → (abs‘(𝑅 − 𝐶)) = (abs‘(𝑆 − 𝐶))) |
85 | 84 | breq1d 4593 |
. . . . . . . . . . . . 13
⊢ (𝑥 = (1 / 𝑦) → ((abs‘(𝑅 − 𝐶)) < 𝑧 ↔ (abs‘(𝑆 − 𝐶)) < 𝑧)) |
86 | 81, 85 | imbi12d 333 |
. . . . . . . . . . . 12
⊢ (𝑥 = (1 / 𝑦) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
87 | 86 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 = (1 / 𝑦)) → ((𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
88 | 52, 80, 87 | ralxfrd 4805 |
. . . . . . . . . 10
⊢ (𝜑 → (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
89 | 88 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑦 ∈ 𝐵 ((1 / 𝑦) < 𝑟 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
90 | 31, 89 | bitr4d 270 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
91 | | elsni 4142 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ {0} → 𝑥 = 0) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑥 = 0) |
93 | | rlimcnp.c |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 0 → 𝑅 = 𝐶) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 𝑅 = 𝐶) |
95 | 94 | oveq1d 6564 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = (𝐶 − 𝐶)) |
96 | | rlimcnp.0 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 0 ∈ 𝐴) |
97 | | rlimcnp.r |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑅 ∈ ℂ) |
98 | 97 | ralrimiva 2949 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
99 | 93 | eleq1d 2672 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 0 → (𝑅 ∈ ℂ ↔ 𝐶 ∈ ℂ)) |
100 | 99 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . 19
⊢ (0 ∈
𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → 𝐶 ∈ ℂ)) |
101 | 96, 98, 100 | sylc 63 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐶 ∈ ℂ) |
102 | 101 | subidd 10259 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐶 − 𝐶) = 0) |
103 | 102 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝐶 − 𝐶) = 0) |
104 | 95, 103 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑅 − 𝐶) = 0) |
105 | 104 | abs00bd 13879 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) →
(abs‘(𝑅 − 𝐶)) = 0) |
106 | | rpgt0 11720 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ ℝ+
→ 0 < 𝑧) |
107 | 106 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → 0 < 𝑧) |
108 | 105, 107 | eqbrtrd 4605 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) →
(abs‘(𝑅 − 𝐶)) < 𝑧) |
109 | 108 | a1d 25 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑥 ∈ {0}) → (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
110 | 109 | ralrimiva 2949 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
111 | 110 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ ∀𝑥 ∈ {0}
(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)) |
112 | 111 | biantrud 527 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧)))) |
113 | | ralunb 3756 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
((𝐴 ∖ {0}) ∪
{0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ (∀𝑥 ∈ (𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ∧ ∀𝑥 ∈ {0} (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
114 | 112, 113 | syl6bbr 277 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
(𝐴 ∖ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ ((𝐴 ∖ {0}) ∪ {0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
115 | | undif1 3995 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ {0}) ∪ {0}) =
(𝐴 ∪
{0}) |
116 | 96 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ 0 ∈ 𝐴) |
117 | 116 | snssd 4281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ {0} ⊆ 𝐴) |
118 | | ssequn2 3748 |
. . . . . . . . . . 11
⊢ ({0}
⊆ 𝐴 ↔ (𝐴 ∪ {0}) = 𝐴) |
119 | 117, 118 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (𝐴 ∪ {0}) =
𝐴) |
120 | 115, 119 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ ((𝐴 ∖ {0})
∪ {0}) = 𝐴) |
121 | 120 | raleqdv 3121 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑥 ∈
((𝐴 ∖ {0}) ∪
{0})(𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
122 | 90, 114, 121 | 3bitrd 293 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑧 ∈ ℝ+) ∧ 𝑟 ∈ ℝ+)
→ (∀𝑦 ∈
𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
123 | 122 | rexbidva 3031 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑟 ∈
ℝ+ ∀𝑦 ∈ 𝐵 ((1 / 𝑟) < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
124 | 19, 123 | bitrd 267 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ℝ+) →
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
125 | 124 | ralbidva 2968 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
126 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝑤((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 |
127 | | nffvmpt1 6111 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) |
128 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(abs
∘ − ) |
129 | | nffvmpt1 6111 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) |
130 | 127, 128,
129 | nfov 6575 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) |
131 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥
< |
132 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝑧 |
133 | 130, 131,
132 | nfbr 4629 |
. . . . . . . . 9
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 |
134 | 126, 133 | nfim 1813 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝑤((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) |
135 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑤((𝑥((abs ∘ − ) ↾
(𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) |
136 | | oveq1 6556 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0)) |
137 | 136 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟)) |
138 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑤 = 𝑥 → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤) = ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)) |
139 | 138 | oveq1d 6564 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0))) |
140 | 139 | breq1d 4593 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)) |
141 | 137, 140 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑤 = 𝑥 → (((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧))) |
142 | 134, 135,
141 | cbvral 3143 |
. . . . . . 7
⊢
(∀𝑤 ∈
𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)) |
143 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
144 | 96 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ 𝐴) |
145 | 143, 144 | ovresd 6699 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (𝑥(abs ∘ − )0)) |
146 | 56, 55 | syl6ss 3580 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
147 | | ax-resscn 9872 |
. . . . . . . . . . . . . . 15
⊢ ℝ
⊆ ℂ |
148 | 146, 147 | syl6ss 3580 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
149 | 148 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℂ) |
150 | | 0cnd 9912 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ∈ ℂ) |
151 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (abs
∘ − ) = (abs ∘ − ) |
152 | 151 | cnmetdval 22384 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℂ ∧ 0 ∈
ℂ) → (𝑥(abs
∘ − )0) = (abs‘(𝑥 − 0))) |
153 | 149, 150,
152 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥(abs ∘ − )0) = (abs‘(𝑥 − 0))) |
154 | 149 | subid1d 10260 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 − 0) = 𝑥) |
155 | 154 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘(𝑥 − 0)) = (abs‘𝑥)) |
156 | 145, 153,
155 | 3eqtrd 2648 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = (abs‘𝑥)) |
157 | 146 | sselda 3568 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
158 | 56 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (0[,)+∞)) |
159 | 158, 64 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 0 ≤ 𝑥) |
160 | 157, 159 | absidd 14009 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (abs‘𝑥) = 𝑥) |
161 | 156, 160 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) = 𝑥) |
162 | 161 | breq1d 4593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 ↔ 𝑥 < 𝑟)) |
163 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝐴 ↦ 𝑅) = (𝑥 ∈ 𝐴 ↦ 𝑅) |
164 | 163 | fvmpt2 6200 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑅 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
165 | 143, 97, 164 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥) = 𝑅) |
166 | 101 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
167 | 93, 163 | fvmptg 6189 |
. . . . . . . . . . . . 13
⊢ ((0
∈ 𝐴 ∧ 𝐶 ∈ ℂ) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) = 𝐶) |
168 | 144, 166,
167 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅)‘0) = 𝐶) |
169 | 165, 168 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (𝑅(abs ∘ − )𝐶)) |
170 | 151 | cnmetdval 22384 |
. . . . . . . . . . . 12
⊢ ((𝑅 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
171 | 97, 166, 170 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑅(abs ∘ − )𝐶) = (abs‘(𝑅 − 𝐶))) |
172 | 169, 171 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) = (abs‘(𝑅 − 𝐶))) |
173 | 172 | breq1d 4593 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧 ↔ (abs‘(𝑅 − 𝐶)) < 𝑧)) |
174 | 162, 173 | imbi12d 333 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
175 | 174 | ralbidva 2968 |
. . . . . . 7
⊢ (𝜑 → (∀𝑥 ∈ 𝐴 ((𝑥((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑥)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
176 | 142, 175 | syl5bb 271 |
. . . . . 6
⊢ (𝜑 → (∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
177 | 176 | rexbidv 3034 |
. . . . 5
⊢ (𝜑 → (∃𝑟 ∈ ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
178 | 177 | ralbidv 2969 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ∀𝑧 ∈ ℝ+ ∃𝑟 ∈ ℝ+
∀𝑥 ∈ 𝐴 (𝑥 < 𝑟 → (abs‘(𝑅 − 𝐶)) < 𝑧))) |
179 | 97, 163 | fmptd 6292 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ) |
180 | 179 | biantrurd 528 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
181 | 125, 178,
180 | 3bitr2d 295 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
182 | 98 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ) |
183 | 82 | eleq1d 2672 |
. . . . . . . . 9
⊢ (𝑥 = (1 / 𝑦) → (𝑅 ∈ ℂ ↔ 𝑆 ∈ ℂ)) |
184 | 183 | rspcv 3278 |
. . . . . . . 8
⊢ ((1 /
𝑦) ∈ 𝐴 → (∀𝑥 ∈ 𝐴 𝑅 ∈ ℂ → 𝑆 ∈ ℂ)) |
185 | 49, 182, 184 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → 𝑆 ∈ ℂ) |
186 | 185 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ 𝐵 𝑆 ∈ ℂ) |
187 | | rpssre 11719 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
188 | 21, 187 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
189 | | 1red 9934 |
. . . . . 6
⊢ (𝜑 → 1 ∈
ℝ) |
190 | 186, 188,
101, 189 | rlim3 14077 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
191 | | 0xr 9965 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
192 | | 0lt1 10429 |
. . . . . . . . . 10
⊢ 0 <
1 |
193 | | df-ioo 12050 |
. . . . . . . . . . 11
⊢ (,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 < 𝑧 ∧ 𝑧 < 𝑦)}) |
194 | | df-ico 12052 |
. . . . . . . . . . 11
⊢ [,) =
(𝑥 ∈
ℝ*, 𝑦
∈ ℝ* ↦ {𝑧 ∈ ℝ* ∣ (𝑥 ≤ 𝑧 ∧ 𝑧 < 𝑦)}) |
195 | | xrltletr 11864 |
. . . . . . . . . . 11
⊢ ((0
∈ ℝ* ∧ 1 ∈ ℝ* ∧ 𝑤 ∈ ℝ*)
→ ((0 < 1 ∧ 1 ≤ 𝑤) → 0 < 𝑤)) |
196 | 193, 194,
195 | ixxss1 12064 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 0 < 1) → (1[,)+∞) ⊆
(0(,)+∞)) |
197 | 191, 192,
196 | mp2an 704 |
. . . . . . . . 9
⊢
(1[,)+∞) ⊆ (0(,)+∞) |
198 | | ioorp 12122 |
. . . . . . . . 9
⊢
(0(,)+∞) = ℝ+ |
199 | 197, 198 | sseqtri 3600 |
. . . . . . . 8
⊢
(1[,)+∞) ⊆ ℝ+ |
200 | | ssrexv 3630 |
. . . . . . . 8
⊢
((1[,)+∞) ⊆ ℝ+ → (∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
201 | 199, 200 | ax-mp 5 |
. . . . . . 7
⊢
(∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
202 | | simplr 788 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ+) |
203 | 187, 202 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑡 ∈ ℝ) |
204 | 188 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) → 𝐵 ⊆
ℝ) |
205 | 204 | sselda 3568 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → 𝑦 ∈ ℝ) |
206 | | ltle 10005 |
. . . . . . . . . . 11
⊢ ((𝑡 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦)) |
207 | 203, 205,
206 | syl2anc 691 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → (𝑡 < 𝑦 → 𝑡 ≤ 𝑦)) |
208 | 207 | imim1d 80 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ℝ+) ∧ 𝑦 ∈ 𝐵) → ((𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
209 | 208 | ralimdva 2945 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑡 ∈ ℝ+) →
(∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
210 | 209 | reximdva 3000 |
. . . . . . 7
⊢ (𝜑 → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
211 | 201, 210 | syl5 33 |
. . . . . 6
⊢ (𝜑 → (∃𝑡 ∈ (1[,)+∞)∀𝑦 ∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
212 | 211 | ralimdv 2946 |
. . . . 5
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
(1[,)+∞)∀𝑦
∈ 𝐵 (𝑡 ≤ 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ+
∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
213 | 190, 212 | sylbid 229 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 → ∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
214 | | ssrexv 3630 |
. . . . . . 7
⊢
(ℝ+ ⊆ ℝ → (∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
215 | 187, 214 | ax-mp 5 |
. . . . . 6
⊢
(∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
216 | 215 | ralimi 2936 |
. . . . 5
⊢
(∀𝑧 ∈
ℝ+ ∃𝑡 ∈ ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → ∀𝑧 ∈ ℝ+ ∃𝑡 ∈ ℝ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧)) |
217 | 186, 188,
101 | rlim2lt 14076 |
. . . . 5
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈ ℝ
∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
218 | 216, 217 | syl5ibr 235 |
. . . 4
⊢ (𝜑 → (∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧) → (𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶)) |
219 | 213, 218 | impbid 201 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ ∀𝑧 ∈ ℝ+
∃𝑡 ∈
ℝ+ ∀𝑦 ∈ 𝐵 (𝑡 < 𝑦 → (abs‘(𝑆 − 𝐶)) < 𝑧))) |
220 | | cnxmet 22386 |
. . . . 5
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
221 | | xmetres2 21976 |
. . . . 5
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝐴
× 𝐴)) ∈
(∞Met‘𝐴)) |
222 | 220, 148,
221 | sylancr 694 |
. . . 4
⊢ (𝜑 → ((abs ∘ − )
↾ (𝐴 × 𝐴)) ∈
(∞Met‘𝐴)) |
223 | 220 | a1i 11 |
. . . 4
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
224 | | eqid 2610 |
. . . . 5
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝐴 × 𝐴))) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴))) |
225 | | rlimcnp.j |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
226 | 225 | cnfldtopn 22395 |
. . . . 5
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
227 | 224, 226 | metcnp2 22157 |
. . . 4
⊢ ((((abs
∘ − ) ↾ (𝐴 × 𝐴)) ∈ (∞Met‘𝐴) ∧ (abs ∘ − )
∈ (∞Met‘ℂ) ∧ 0 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
228 | 222, 223,
96, 227 | syl3anc 1318 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0) ↔ ((𝑥 ∈ 𝐴 ↦ 𝑅):𝐴⟶ℂ ∧ ∀𝑧 ∈ ℝ+
∃𝑟 ∈
ℝ+ ∀𝑤 ∈ 𝐴 ((𝑤((abs ∘ − ) ↾ (𝐴 × 𝐴))0) < 𝑟 → (((𝑥 ∈ 𝐴 ↦ 𝑅)‘𝑤)(abs ∘ − )((𝑥 ∈ 𝐴 ↦ 𝑅)‘0)) < 𝑧)))) |
229 | 181, 219,
228 | 3bitr4d 299 |
. 2
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0))) |
230 | | rlimcnp.k |
. . . . . 6
⊢ 𝐾 = (𝐽 ↾t 𝐴) |
231 | | eqid 2610 |
. . . . . . . 8
⊢ ((abs
∘ − ) ↾ (𝐴 × 𝐴)) = ((abs ∘ − ) ↾ (𝐴 × 𝐴)) |
232 | 231, 226,
224 | metrest 22139 |
. . . . . . 7
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝐴 ⊆ ℂ) → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
233 | 220, 148,
232 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → (𝐽 ↾t 𝐴) = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
234 | 230, 233 | syl5eq 2656 |
. . . . 5
⊢ (𝜑 → 𝐾 = (MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴)))) |
235 | 234 | oveq1d 6564 |
. . . 4
⊢ (𝜑 → (𝐾 CnP 𝐽) = ((MetOpen‘((abs ∘ − )
↾ (𝐴 × 𝐴))) CnP 𝐽)) |
236 | 235 | fveq1d 6105 |
. . 3
⊢ (𝜑 → ((𝐾 CnP 𝐽)‘0) = (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0)) |
237 | 236 | eleq2d 2673 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0) ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ (((MetOpen‘((abs ∘
− ) ↾ (𝐴
× 𝐴))) CnP 𝐽)‘0))) |
238 | 229, 237 | bitr4d 270 |
1
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ↦ 𝑆) ⇝𝑟 𝐶 ↔ (𝑥 ∈ 𝐴 ↦ 𝑅) ∈ ((𝐾 CnP 𝐽)‘0))) |