Step | Hyp | Ref
| Expression |
1 | | difss 3699 |
. . 3
⊢ (ℂ
∖ ℝ) ⊆ ℂ |
2 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → 𝑥 ∈
ℂ) |
3 | 2 | imcld 13783 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ∈ ℝ) |
4 | 3 | recnd 9947 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ∈ ℂ) |
5 | | eldifn 3695 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ¬ 𝑥
∈ ℝ) |
6 | | reim0b 13707 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
7 | 2, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑥 ∈
ℝ ↔ (ℑ‘𝑥) = 0)) |
8 | 7 | necon3bbid 2819 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (¬ 𝑥
∈ ℝ ↔ (ℑ‘𝑥) ≠ 0)) |
9 | 5, 8 | mpbid 221 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ≠ 0) |
10 | 4, 9 | absrpcld 14035 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈
ℝ+) |
11 | | cnxmet 22386 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
13 | 4 | abscld 14023 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈ ℝ) |
14 | 13 | rexrd 9968 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈
ℝ*) |
15 | | elbl 22003 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧
(abs‘(ℑ‘𝑥)) ∈ ℝ*) → (𝑦 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ↔ (𝑦 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))))) |
16 | 12, 2, 14, 15 | syl3anc 1318 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
(𝑥(ball‘(abs ∘
− ))(abs‘(ℑ‘𝑥))) ↔ (𝑦 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))))) |
17 | | simprl 790 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → 𝑦 ∈ ℂ) |
18 | 2 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑥 ∈
ℂ) |
19 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℝ) |
20 | 19 | recnd 9947 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℂ) |
21 | 18, 20 | imsubd 13805 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘(𝑥 − 𝑦)) = ((ℑ‘𝑥) − (ℑ‘𝑦))) |
22 | | reim0 13706 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ →
(ℑ‘𝑦) =
0) |
23 | 22 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘𝑦) = 0) |
24 | 23 | oveq2d 6565 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((ℑ‘𝑥) − (ℑ‘𝑦)) = ((ℑ‘𝑥) − 0)) |
25 | 4 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘𝑥) ∈ ℂ) |
26 | 25 | subid1d 10260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((ℑ‘𝑥) − 0) = (ℑ‘𝑥)) |
27 | 21, 24, 26 | 3eqtrd 2648 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘(𝑥 − 𝑦)) = (ℑ‘𝑥)) |
28 | 27 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘(𝑥 − 𝑦))) = (abs‘(ℑ‘𝑥))) |
29 | 18, 20 | subcld 10271 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (𝑥 −
𝑦) ∈
ℂ) |
30 | | absimle 13897 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 − 𝑦) ∈ ℂ →
(abs‘(ℑ‘(𝑥 − 𝑦))) ≤ (abs‘(𝑥 − 𝑦))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘(𝑥 − 𝑦))) ≤ (abs‘(𝑥 − 𝑦))) |
32 | 28, 31 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘𝑥)) ≤ (abs‘(𝑥 − 𝑦))) |
33 | 25 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘𝑥)) ∈ ℝ) |
34 | 29 | abscld 14023 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(𝑥 − 𝑦)) ∈ ℝ) |
35 | 33, 34 | lenltd 10062 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((abs‘(ℑ‘𝑥)) ≤ (abs‘(𝑥 − 𝑦)) ↔ ¬ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥)))) |
36 | 32, 35 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ¬ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥))) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) = (abs ∘ − ) |
38 | 37 | cnmetdval 22384 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑥 − 𝑦))) |
39 | 18, 20, 38 | syl2anc 691 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (𝑥(abs
∘ − )𝑦) =
(abs‘(𝑥 − 𝑦))) |
40 | 39 | breq1d 4593 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) ↔ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥)))) |
41 | 36, 40 | mtbird 314 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ¬ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))) |
42 | 41 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
ℝ → ¬ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) |
43 | 42 | con2d 128 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) → ¬ 𝑦 ∈ ℝ)) |
44 | 43 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℂ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) → ¬ 𝑦 ∈ ℝ)) |
45 | 44 | impr 647 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → ¬ 𝑦 ∈ ℝ) |
46 | 17, 45 | eldifd 3551 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → 𝑦 ∈ (ℂ ∖
ℝ)) |
47 | 46 | ex 449 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ((𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥))) → 𝑦 ∈ (ℂ ∖
ℝ))) |
48 | 16, 47 | sylbid 229 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
(𝑥(ball‘(abs ∘
− ))(abs‘(ℑ‘𝑥))) → 𝑦 ∈ (ℂ ∖
ℝ))) |
49 | 48 | ssrdv 3574 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖
ℝ)) |
50 | | oveq2 6557 |
. . . . . . 7
⊢ (𝑦 =
(abs‘(ℑ‘𝑥)) → (𝑥(ball‘(abs ∘ − ))𝑦) = (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥)))) |
51 | 50 | sseq1d 3595 |
. . . . . 6
⊢ (𝑦 =
(abs‘(ℑ‘𝑥)) → ((𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ) ↔ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖
ℝ))) |
52 | 51 | rspcev 3282 |
. . . . 5
⊢
(((abs‘(ℑ‘𝑥)) ∈ ℝ+ ∧ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖ ℝ)) →
∃𝑦 ∈
ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ)) |
53 | 10, 49, 52 | syl2anc 691 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ∃𝑦
∈ ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ)) |
54 | 53 | rgen 2906 |
. . 3
⊢
∀𝑥 ∈
(ℂ ∖ ℝ)∃𝑦 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑦) ⊆ (ℂ
∖ ℝ) |
55 | | recld2.1 |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
56 | 55 | cnfldtopn 22395 |
. . . . 5
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
57 | 56 | elmopn2 22060 |
. . . 4
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ((ℂ ∖
ℝ) ∈ 𝐽 ↔
((ℂ ∖ ℝ) ⊆ ℂ ∧ ∀𝑥 ∈ (ℂ ∖ ℝ)∃𝑦 ∈ ℝ+
(𝑥(ball‘(abs ∘
− ))𝑦) ⊆
(ℂ ∖ ℝ)))) |
58 | 11, 57 | ax-mp 5 |
. . 3
⊢ ((ℂ
∖ ℝ) ∈ 𝐽
↔ ((ℂ ∖ ℝ) ⊆ ℂ ∧ ∀𝑥 ∈ (ℂ ∖
ℝ)∃𝑦 ∈
ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ))) |
59 | 1, 54, 58 | mpbir2an 957 |
. 2
⊢ (ℂ
∖ ℝ) ∈ 𝐽 |
60 | 55 | cnfldtop 22397 |
. . 3
⊢ 𝐽 ∈ Top |
61 | | ax-resscn 9872 |
. . 3
⊢ ℝ
⊆ ℂ |
62 | 56 | mopnuni 22056 |
. . . . 5
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ℂ = ∪ 𝐽) |
63 | 11, 62 | ax-mp 5 |
. . . 4
⊢ ℂ =
∪ 𝐽 |
64 | 63 | iscld2 20642 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ℝ
⊆ ℂ) → (ℝ ∈ (Clsd‘𝐽) ↔ (ℂ ∖ ℝ) ∈
𝐽)) |
65 | 60, 61, 64 | mp2an 704 |
. 2
⊢ (ℝ
∈ (Clsd‘𝐽)
↔ (ℂ ∖ ℝ) ∈ 𝐽) |
66 | 59, 65 | mpbir 220 |
1
⊢ ℝ
∈ (Clsd‘𝐽) |