| Step | Hyp | Ref
| Expression |
| 1 | | difss 4136 |
. . 3
⊢ (ℂ
∖ ℝ) ⊆ ℂ |
| 2 | | eldifi 4131 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → 𝑥 ∈
ℂ) |
| 3 | 2 | imcld 15234 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ∈ ℝ) |
| 4 | 3 | recnd 11289 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ∈ ℂ) |
| 5 | | eldifn 4132 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ¬ 𝑥
∈ ℝ) |
| 6 | | reim0b 15158 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ → (𝑥 ∈ ℝ ↔
(ℑ‘𝑥) =
0)) |
| 7 | 2, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑥 ∈
ℝ ↔ (ℑ‘𝑥) = 0)) |
| 8 | 7 | necon3bbid 2978 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (¬ 𝑥
∈ ℝ ↔ (ℑ‘𝑥) ≠ 0)) |
| 9 | 5, 8 | mpbid 232 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (ℑ‘𝑥) ≠ 0) |
| 10 | 4, 9 | absrpcld 15487 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈
ℝ+) |
| 11 | | cnxmet 24793 |
. . . . . . . 8
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 12 | 4 | abscld 15475 |
. . . . . . . . 9
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈ ℝ) |
| 13 | 12 | rexrd 11311 |
. . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (abs‘(ℑ‘𝑥)) ∈
ℝ*) |
| 14 | | elbl 24398 |
. . . . . . . 8
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑥 ∈ ℂ ∧
(abs‘(ℑ‘𝑥)) ∈ ℝ*) → (𝑦 ∈ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ↔ (𝑦 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))))) |
| 15 | 11, 2, 13, 14 | mp3an2i 1468 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
(𝑥(ball‘(abs ∘
− ))(abs‘(ℑ‘𝑥))) ↔ (𝑦 ∈ ℂ ∧ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))))) |
| 16 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → 𝑦 ∈ ℂ) |
| 17 | 2 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑥 ∈
ℂ) |
| 18 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℝ) |
| 19 | 18 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → 𝑦 ∈
ℂ) |
| 20 | | eqid 2737 |
. . . . . . . . . . . . . . . 16
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 21 | 20 | cnmetdval 24791 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥(abs ∘ − )𝑦) = (abs‘(𝑥 − 𝑦))) |
| 22 | 17, 19, 21 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (𝑥(abs
∘ − )𝑦) =
(abs‘(𝑥 − 𝑦))) |
| 23 | 4 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘𝑥) ∈ ℂ) |
| 24 | 23 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘𝑥)) ∈ ℝ) |
| 25 | 17, 19 | subcld 11620 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (𝑥 −
𝑦) ∈
ℂ) |
| 26 | 25 | abscld 15475 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(𝑥 − 𝑦)) ∈ ℝ) |
| 27 | 17, 19 | imsubd 15256 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘(𝑥 − 𝑦)) = ((ℑ‘𝑥) − (ℑ‘𝑦))) |
| 28 | | reim0 15157 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ ℝ →
(ℑ‘𝑦) =
0) |
| 29 | 28 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘𝑦) = 0) |
| 30 | 29 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((ℑ‘𝑥) − (ℑ‘𝑦)) = ((ℑ‘𝑥) − 0)) |
| 31 | 23 | subid1d 11609 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ((ℑ‘𝑥) − 0) = (ℑ‘𝑥)) |
| 32 | 27, 30, 31 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (ℑ‘(𝑥 − 𝑦)) = (ℑ‘𝑥)) |
| 33 | 32 | fveq2d 6910 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘(𝑥 − 𝑦))) = (abs‘(ℑ‘𝑥))) |
| 34 | | absimle 15348 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 − 𝑦) ∈ ℂ →
(abs‘(ℑ‘(𝑥 − 𝑦))) ≤ (abs‘(𝑥 − 𝑦))) |
| 35 | 25, 34 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘(𝑥 − 𝑦))) ≤ (abs‘(𝑥 − 𝑦))) |
| 36 | 33, 35 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → (abs‘(ℑ‘𝑥)) ≤ (abs‘(𝑥 − 𝑦))) |
| 37 | 24, 26, 36 | lensymd 11412 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ¬ (abs‘(𝑥 − 𝑦)) < (abs‘(ℑ‘𝑥))) |
| 38 | 22, 37 | eqnbrtrd 5161 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℝ) → ¬ (𝑥(abs ∘ − )𝑦) < (abs‘(ℑ‘𝑥))) |
| 39 | 38 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
ℝ → ¬ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) |
| 40 | 39 | con2d 134 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) → ¬ 𝑦 ∈ ℝ)) |
| 41 | 40 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ 𝑦 ∈
ℂ) → ((𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)) → ¬ 𝑦 ∈ ℝ)) |
| 42 | 41 | impr 454 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → ¬ 𝑦 ∈ ℝ) |
| 43 | 16, 42 | eldifd 3962 |
. . . . . . . 8
⊢ ((𝑥 ∈ (ℂ ∖
ℝ) ∧ (𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥)))) → 𝑦 ∈ (ℂ ∖
ℝ)) |
| 44 | 43 | ex 412 |
. . . . . . 7
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ((𝑦 ∈
ℂ ∧ (𝑥(abs
∘ − )𝑦) <
(abs‘(ℑ‘𝑥))) → 𝑦 ∈ (ℂ ∖
ℝ))) |
| 45 | 15, 44 | sylbid 240 |
. . . . . 6
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑦 ∈
(𝑥(ball‘(abs ∘
− ))(abs‘(ℑ‘𝑥))) → 𝑦 ∈ (ℂ ∖
ℝ))) |
| 46 | 45 | ssrdv 3989 |
. . . . 5
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖
ℝ)) |
| 47 | | oveq2 7439 |
. . . . . . 7
⊢ (𝑦 =
(abs‘(ℑ‘𝑥)) → (𝑥(ball‘(abs ∘ − ))𝑦) = (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥)))) |
| 48 | 47 | sseq1d 4015 |
. . . . . 6
⊢ (𝑦 =
(abs‘(ℑ‘𝑥)) → ((𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ) ↔ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖
ℝ))) |
| 49 | 48 | rspcev 3622 |
. . . . 5
⊢
(((abs‘(ℑ‘𝑥)) ∈ ℝ+ ∧ (𝑥(ball‘(abs ∘ −
))(abs‘(ℑ‘𝑥))) ⊆ (ℂ ∖ ℝ)) →
∃𝑦 ∈
ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ)) |
| 50 | 10, 46, 49 | syl2anc 584 |
. . . 4
⊢ (𝑥 ∈ (ℂ ∖
ℝ) → ∃𝑦
∈ ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ)) |
| 51 | 50 | rgen 3063 |
. . 3
⊢
∀𝑥 ∈
(ℂ ∖ ℝ)∃𝑦 ∈ ℝ+ (𝑥(ball‘(abs ∘ −
))𝑦) ⊆ (ℂ
∖ ℝ) |
| 52 | | recld2.1 |
. . . . . 6
⊢ 𝐽 =
(TopOpen‘ℂfld) |
| 53 | 52 | cnfldtopn 24802 |
. . . . 5
⊢ 𝐽 = (MetOpen‘(abs ∘
− )) |
| 54 | 53 | elmopn2 24455 |
. . . 4
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ((ℂ ∖
ℝ) ∈ 𝐽 ↔
((ℂ ∖ ℝ) ⊆ ℂ ∧ ∀𝑥 ∈ (ℂ ∖ ℝ)∃𝑦 ∈ ℝ+
(𝑥(ball‘(abs ∘
− ))𝑦) ⊆
(ℂ ∖ ℝ)))) |
| 55 | 11, 54 | ax-mp 5 |
. . 3
⊢ ((ℂ
∖ ℝ) ∈ 𝐽
↔ ((ℂ ∖ ℝ) ⊆ ℂ ∧ ∀𝑥 ∈ (ℂ ∖
ℝ)∃𝑦 ∈
ℝ+ (𝑥(ball‘(abs ∘ − ))𝑦) ⊆ (ℂ ∖
ℝ))) |
| 56 | 1, 51, 55 | mpbir2an 711 |
. 2
⊢ (ℂ
∖ ℝ) ∈ 𝐽 |
| 57 | 52 | cnfldtop 24804 |
. . 3
⊢ 𝐽 ∈ Top |
| 58 | | ax-resscn 11212 |
. . 3
⊢ ℝ
⊆ ℂ |
| 59 | 53 | mopnuni 24451 |
. . . . 5
⊢ ((abs
∘ − ) ∈ (∞Met‘ℂ) → ℂ = ∪ 𝐽) |
| 60 | 11, 59 | ax-mp 5 |
. . . 4
⊢ ℂ =
∪ 𝐽 |
| 61 | 60 | iscld2 23036 |
. . 3
⊢ ((𝐽 ∈ Top ∧ ℝ
⊆ ℂ) → (ℝ ∈ (Clsd‘𝐽) ↔ (ℂ ∖ ℝ) ∈
𝐽)) |
| 62 | 57, 58, 61 | mp2an 692 |
. 2
⊢ (ℝ
∈ (Clsd‘𝐽)
↔ (ℂ ∖ ℝ) ∈ 𝐽) |
| 63 | 56, 62 | mpbir 231 |
1
⊢ ℝ
∈ (Clsd‘𝐽) |