Step | Hyp | Ref
| Expression |
1 | | ssrab2 3238 |
. . 3
⊢ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ⊆ ℂ |
2 | 1 | a1i 9 |
. 2
⊢ (𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ⊆ ℂ) |
3 | | breq1 4001 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝑤 # 𝐴 ↔ 𝑥 # 𝐴)) |
4 | 3 | elrab 2891 |
. . . . . . . . 9
⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ↔ (𝑥 ∈ ℂ ∧ 𝑥 # 𝐴)) |
5 | 4 | biimpi 120 |
. . . . . . . 8
⊢ (𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} → (𝑥 ∈ ℂ ∧ 𝑥 # 𝐴)) |
6 | 5 | adantl 277 |
. . . . . . 7
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (𝑥 ∈ ℂ ∧ 𝑥 # 𝐴)) |
7 | 6 | simpld 112 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → 𝑥 ∈ ℂ) |
8 | | simpl 109 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → 𝐴 ∈ ℂ) |
9 | 7, 8 | subcld 8242 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (𝑥 − 𝐴) ∈ ℂ) |
10 | 6 | simprd 114 |
. . . . . 6
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → 𝑥 # 𝐴) |
11 | 7, 8, 10 | subap0d 8575 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (𝑥 − 𝐴) # 0) |
12 | 9, 11 | absrpclapd 11165 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (abs‘(𝑥 − 𝐴)) ∈
ℝ+) |
13 | | breq1 4001 |
. . . . . . 7
⊢ (𝑤 = 𝑧 → (𝑤 # 𝐴 ↔ 𝑧 # 𝐴)) |
14 | | cnxmet 13611 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
15 | 9 | abscld 11158 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (abs‘(𝑥 − 𝐴)) ∈ ℝ) |
16 | 15 | rexrd 7981 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (abs‘(𝑥 − 𝐴)) ∈
ℝ*) |
17 | | elbl 13471 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧ (abs‘(𝑥 − 𝐴)) ∈ ℝ*) → (𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴))) ↔ (𝑧 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑧) < (abs‘(𝑥 − 𝐴))))) |
18 | 14, 7, 16, 17 | mp3an2i 1342 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴))) ↔ (𝑧 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑧) < (abs‘(𝑥 − 𝐴))))) |
19 | 18 | biimpa 296 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (𝑧 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑧) < (abs‘(𝑥 − 𝐴)))) |
20 | 19 | simpld 112 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → 𝑧 ∈
ℂ) |
21 | 8 | adantr 276 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → 𝐴 ∈
ℂ) |
22 | 20, 21 | subcld 8242 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (𝑧 − 𝐴) ∈ ℂ) |
23 | 22 | abscld 11158 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑧 − 𝐴)) ∈
ℝ) |
24 | 7 | adantr 276 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → 𝑥 ∈
ℂ) |
25 | 24, 20 | subcld 8242 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (𝑥 − 𝑧) ∈ ℂ) |
26 | 25 | abscld 11158 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑥 − 𝑧)) ∈
ℝ) |
27 | 15 | adantr 276 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑥 − 𝐴)) ∈
ℝ) |
28 | 26, 23 | readdcld 7961 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
((abs‘(𝑥 −
𝑧)) + (abs‘(𝑧 − 𝐴))) ∈ ℝ) |
29 | | eqid 2175 |
. . . . . . . . . . . . . . 15
⊢ (abs
∘ − ) = (abs ∘ − ) |
30 | 29 | cnmetdval 13609 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ ℂ ∧ 𝑧 ∈ ℂ) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧))) |
31 | 24, 20, 30 | syl2anc 411 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (𝑥(abs ∘ − )𝑧) = (abs‘(𝑥 − 𝑧))) |
32 | 19 | simprd 114 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (𝑥(abs ∘ − )𝑧) < (abs‘(𝑥 − 𝐴))) |
33 | 31, 32 | eqbrtrrd 4022 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑥 − 𝑧)) < (abs‘(𝑥 − 𝐴))) |
34 | 24, 21, 20 | abs3difd 11177 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑥 − 𝐴)) ≤ ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝐴)))) |
35 | 26, 27, 28, 33, 34 | ltletrd 8354 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑥 − 𝑧)) < ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝐴)))) |
36 | 23, 26 | ltaddposd 8460 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (0 <
(abs‘(𝑧 − 𝐴)) ↔ (abs‘(𝑥 − 𝑧)) < ((abs‘(𝑥 − 𝑧)) + (abs‘(𝑧 − 𝐴))))) |
37 | 35, 36 | mpbird 167 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → 0 <
(abs‘(𝑧 − 𝐴))) |
38 | 23, 37 | gt0ap0d 8560 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
(abs‘(𝑧 − 𝐴)) # 0) |
39 | | abs00ap 11039 |
. . . . . . . . . 10
⊢ ((𝑧 − 𝐴) ∈ ℂ → ((abs‘(𝑧 − 𝐴)) # 0 ↔ (𝑧 − 𝐴) # 0)) |
40 | 22, 39 | syl 14 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) →
((abs‘(𝑧 −
𝐴)) # 0 ↔ (𝑧 − 𝐴) # 0)) |
41 | 38, 40 | mpbid 147 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → (𝑧 − 𝐴) # 0) |
42 | | subap0 8574 |
. . . . . . . . 9
⊢ ((𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑧 − 𝐴) # 0 ↔ 𝑧 # 𝐴)) |
43 | 20, 21, 42 | syl2anc 411 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → ((𝑧 − 𝐴) # 0 ↔ 𝑧 # 𝐴)) |
44 | 41, 43 | mpbid 147 |
. . . . . . 7
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → 𝑧 # 𝐴) |
45 | 13, 20, 44 | elrabd 2893 |
. . . . . 6
⊢ (((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) ∧ 𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) → 𝑧 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) |
46 | 45 | ex 115 |
. . . . 5
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (𝑧 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴))) → 𝑧 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴})) |
47 | 46 | ssrdv 3159 |
. . . 4
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴))) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) |
48 | | oveq2 5873 |
. . . . . 6
⊢ (𝑟 = (abs‘(𝑥 − 𝐴)) → (𝑥(ball‘(abs ∘ − ))𝑟) = (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴)))) |
49 | 48 | sseq1d 3182 |
. . . . 5
⊢ (𝑟 = (abs‘(𝑥 − 𝐴)) → ((𝑥(ball‘(abs ∘ − ))𝑟) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ↔ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴))) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴})) |
50 | 49 | rspcev 2839 |
. . . 4
⊢
(((abs‘(𝑥
− 𝐴)) ∈
ℝ+ ∧ (𝑥(ball‘(abs ∘ −
))(abs‘(𝑥 −
𝐴))) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) |
51 | 12, 47, 50 | syl2anc 411 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) → ∃𝑟 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) |
52 | 51 | ralrimiva 2548 |
. 2
⊢ (𝐴 ∈ ℂ →
∀𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}∃𝑟 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}) |
53 | | eqid 2175 |
. . . 4
⊢
(MetOpen‘(abs ∘ − )) = (MetOpen‘(abs ∘
− )) |
54 | 53 | elmopn2 13529 |
. . 3
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ({𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ −
)) ↔ ({𝑤 ∈
ℂ ∣ 𝑤 # 𝐴} ⊆ ℂ ∧
∀𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}∃𝑟 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}))) |
55 | 14, 54 | ax-mp 5 |
. 2
⊢ ({𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ −
)) ↔ ({𝑤 ∈
ℂ ∣ 𝑤 # 𝐴} ⊆ ℂ ∧
∀𝑥 ∈ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴}∃𝑟 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑟) ⊆ {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴})) |
56 | 2, 52, 55 | sylanbrc 417 |
1
⊢ (𝐴 ∈ ℂ → {𝑤 ∈ ℂ ∣ 𝑤 # 𝐴} ∈ (MetOpen‘(abs ∘ −
))) |