Step | Hyp | Ref
| Expression |
1 | | difss 3737 |
. . 3
⊢ (ℂ
∖ ℝ) ⊆ ℂ |
2 | | eldifi 3732 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → 𝑥 ∈
ℂ) |
3 | 2 | imcld 13935 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ∈ ℝ) |
4 | 3 | recnd 10068 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ∈ ℂ) |
5 | | eldifn 3733 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ¬ 𝑥
∈ ℝ) |
6 | | reim0b 13859 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
7 | 2, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑥 ∈
ℝ ↔ (ℑ‘𝑥) = 0)) |
8 | 7 | necon3bbid 2831 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (¬ 𝑥
∈ ℝ ↔ (ℑ‘𝑥) ≠ 0)) |
9 | 5, 8 | mpbid 222 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ≠ 0) |
10 | 4, 9 | absrpcld 14187 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈
ℝ+) |
11 | | cnxmet 22576 |
. . . . . . . . 9
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
12 | 11 | a1i 11 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs ∘ − ) ∈
(∞Met‘ℂ)) |
13 | 4 | abscld 14175 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈ ℝ) |
14 | 13 | rexrd 10089 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈
ℝ*) |
15 | | elbl 22193 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧
(abs‘(ℑ‘𝑥)) ∈ ℝ*) → (𝑦 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ↔ (𝑦 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))))) |
16 | 12, 2, 14, 15 | syl3anc 1326 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
(𝑥(ball‘(abs ∘
− ))(abs‘(ℑ‘𝑥))) ↔ (𝑦 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))))) |
17 | | simprl 794 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → 𝑦 ∈ ℂ) |
18 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑥 ∈
ℂ) |
19 | | simpr 477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℝ) |
20 | 19 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℂ) |
21 | 18, 20 | imsubd 13957 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘(𝑥 − 𝑦)) = ((ℑ‘𝑥) − (ℑ‘𝑦))) |
22 | | reim0 13858 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ →
(ℑ‘𝑦) =
0) |
23 | 22 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘𝑦) = 0) |
24 | 23 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((ℑ‘𝑥) − (ℑ‘𝑦)) = ((ℑ‘𝑥) − 0)) |
25 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘𝑥) ∈ ℂ) |
26 | 25 | subid1d 10381 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((ℑ‘𝑥) − 0) = (ℑ‘𝑥)) |
27 | 21, 24, 26 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘(𝑥 − 𝑦)) = (ℑ‘𝑥)) |
28 | 27 | fveq2d 6195 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘(𝑥 − 𝑦))) = (abs‘(ℑ‘𝑥))) |
29 | 18, 20 | subcld 10392 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (𝑥 −
𝑦) ∈
ℂ) |
30 | | absimle 14049 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 − 𝑦) ∈ ℂ →
(abs‘(ℑ‘(𝑥 − 𝑦))) ≤ (abs‘(𝑥 − 𝑦))) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘(𝑥 − 𝑦))) ≤ (abs‘(𝑥 − 𝑦))) |
32 | 28, 31 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘𝑥)) ≤ (abs‘(𝑥 − 𝑦))) |
33 | 25 | abscld 14175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘𝑥)) ∈ ℝ) |
34 | 29 | abscld 14175 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(𝑥 − 𝑦)) ∈ ℝ) |
35 | 33, 34 | lenltd 10183 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((abs‘(ℑ‘𝑥)) ≤ (abs‘(𝑥 − 𝑦)) ↔ ¬ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥)))) |
36 | 32, 35 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ¬ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥))) |
37 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) = (abs ∘ − ) |
38 | 37 | cnmetdval 22574 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑥 − 𝑦))) |
39 | 18, 20, 38 | syl2anc 693 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (𝑥(abs
∘ − )𝑦) =
(abs‘(𝑥 − 𝑦))) |
40 | 39 | breq1d 4663 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) ↔ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥)))) |
41 | 36, 40 | mtbird 315 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ¬ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))) |
42 | 41 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
ℝ → ¬ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) |
43 | 42 | con2d 129 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) → ¬ 𝑦 ∈ ℝ)) |
44 | 43 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℂ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) → ¬ 𝑦 ∈ ℝ)) |
45 | 44 | impr 649 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → ¬ 𝑦 ∈ ℝ) |
46 | 17, 45 | eldifd 3585 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → 𝑦 ∈ (ℂ ∖
ℝ)) |
47 | 46 | ex 450 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ((𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥))) → 𝑦 ∈ (ℂ ∖
ℝ))) |
48 | 16, 47 | sylbid 230 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
(𝑥(ball‘(abs ∘
− ))(abs‘(ℑ‘𝑥))) → 𝑦 ∈ (ℂ ∖
ℝ))) |
49 | 48 | ssrdv 3609 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖
ℝ)) |
50 | | oveq2 6658 |
. . . . . . 7
⊢ (𝑦 =
(abs‘(ℑ‘𝑥)) → (𝑥(ball‘(abs ∘ − ))𝑦) = (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥)))) |
51 | 50 | sseq1d 3632 |
. . . . . 6
⊢ (𝑦 =
(abs‘(ℑ‘𝑥)) → ((𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ) ↔ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖
ℝ))) |
52 | 51 | rspcev 3309 |
. . . . 5
⊢
(((abs‘(ℑ‘𝑥)) ∈ ℝ+ ∧ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖ ℝ)) →
∃𝑦 ∈
ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ)) |
53 | 10, 49, 52 | syl2anc 693 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ∃𝑦
∈ ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ)) |
54 | 53 | rgen 2922 |
. . 3
⊢
∀𝑥 ∈
(ℂ ∖ ℝ)∃𝑦 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑦) ⊆ (ℂ
∖ ℝ) |
55 | | recld2.1 |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
56 | 55 | cnfldtopn 22585 |
. . . . 5
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
57 | 56 | elmopn2 22250 |
. . . 4
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ((ℂ ∖
ℝ) ∈ 𝐽 ↔
((ℂ ∖ ℝ) ⊆ ℂ ∧ ∀𝑥 ∈ (ℂ ∖ ℝ)∃𝑦 ∈ ℝ+
(𝑥(ball‘(abs ∘
− ))𝑦) ⊆
(ℂ ∖ ℝ)))) |
58 | 11, 57 | ax-mp 5 |
. . 3
⊢ ((ℂ
∖ ℝ) ∈ 𝐽
↔ ((ℂ ∖ ℝ) ⊆ ℂ ∧ ∀𝑥 ∈ (ℂ ∖
ℝ)∃𝑦 ∈
ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ))) |
59 | 1, 54, 58 | mpbir2an 955 |
. 2
⊢ (ℂ
∖ ℝ) ∈ 𝐽 |
60 | 55 | cnfldtop 22587 |
. . 3
⊢ 𝐽 ∈ Top |
61 | | ax-resscn 9993 |
. . 3
⊢ ℝ
⊆ ℂ |
62 | 56 | mopnuni 22246 |
. . . . 5
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ℂ = ∪ 𝐽) |
63 | 11, 62 | ax-mp 5 |
. . . 4
⊢ ℂ =
∪ 𝐽 |
64 | 63 | iscld2 20832 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ℝ
⊆ ℂ) → (ℝ ∈ (Clsd‘𝐽) ↔ (ℂ ∖ ℝ) ∈
𝐽)) |
65 | 60, 61, 64 | mp2an 708 |
. 2
⊢ (ℝ
∈ (Clsd‘𝐽)
↔ (ℂ ∖ ℝ) ∈ 𝐽) |
66 | 59, 65 | mpbir 221 |
1
⊢ ℝ
∈ (Clsd‘𝐽) |