Metamath Proof Explorer

Theorem recld2

Description: The real numbers are a closed set in the topology on CC . (Contributed by Mario Carneiro, 17-Feb-2015)

Ref Expression
Hypothesis recld2.1 ⊢ J = TopOpen ⁡ ℂ fld
Assertion recld2 ⊢ ℝ ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 recld2.1 ⊢ J = TopOpen ⁡ ℂ fld
2 difss ⊢ ℂ ∖ ℝ ⊆ ℂ
3 eldifi ⊢ x ∈ ℂ ∖ ℝ → x ∈ ℂ
4 3 imcld ⊢ x ∈ ℂ ∖ ℝ → ℑ ⁡ x ∈ ℝ
5 4 recnd ⊢ x ∈ ℂ ∖ ℝ → ℑ ⁡ x ∈ ℂ
6 eldifn ⊢ x ∈ ℂ ∖ ℝ → ¬ x ∈ ℝ
7 reim0b ⊢ x ∈ ℂ → x ∈ ℝ ↔ ℑ ⁡ x = 0
8 3 7 syl ⊢ x ∈ ℂ ∖ ℝ → x ∈ ℝ ↔ ℑ ⁡ x = 0
9 8 necon3bbid ⊢ x ∈ ℂ ∖ ℝ → ¬ x ∈ ℝ ↔ ℑ ⁡ x ≠ 0
10 6 9 mpbid ⊢ x ∈ ℂ ∖ ℝ → ℑ ⁡ x ≠ 0
11 5 10 absrpcld ⊢ x ∈ ℂ ∖ ℝ → ℑ ⁡ x ∈ ℝ +
12 cnxmet ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ
13 5 abscld ⊢ x ∈ ℂ ∖ ℝ → ℑ ⁡ x ∈ ℝ
14 13 rexrd ⊢ x ∈ ℂ ∖ ℝ → ℑ ⁡ x ∈ ℝ *
15 elbl ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ ∧ x ∈ ℂ ∧ ℑ ⁡ x ∈ ℝ * → y ∈ x ball ⁡ abs ∘ − ℑ ⁡ x ↔ y ∈ ℂ ∧ x abs ∘ − y < ℑ ⁡ x
16 12 3 14 15 mp3an2i ⊢ x ∈ ℂ ∖ ℝ → y ∈ x ball ⁡ abs ∘ − ℑ ⁡ x ↔ y ∈ ℂ ∧ x abs ∘ − y < ℑ ⁡ x
17 simprl ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℂ ∧ x abs ∘ − y < ℑ ⁡ x → y ∈ ℂ
18 3 adantr ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → x ∈ ℂ
19 simpr ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → y ∈ ℝ
20 19 recnd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → y ∈ ℂ
21 eqid ⊢ abs ∘ − = abs ∘ −
22 21 cnmetdval ⊢ x ∈ ℂ ∧ y ∈ ℂ → x abs ∘ − y = x − y
23 18 20 22 syl2anc ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → x abs ∘ − y = x − y
24 5 adantr ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x ∈ ℂ
25 24 abscld ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x ∈ ℝ
26 18 20 subcld ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → x − y ∈ ℂ
27 26 abscld ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → x − y ∈ ℝ
28 18 20 imsubd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x − y = ℑ ⁡ x − ℑ ⁡ y
29 reim0 ⊢ y ∈ ℝ → ℑ ⁡ y = 0
30 29 adantl ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ y = 0
31 30 oveq2d ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x − ℑ ⁡ y = ℑ ⁡ x − 0
32 24 subid1d ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x − 0 = ℑ ⁡ x
33 28 31 32 3eqtrd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x − y = ℑ ⁡ x
34 33 fveq2d ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x − y = ℑ ⁡ x
35 absimle ⊢ x − y ∈ ℂ → ℑ ⁡ x − y ≤ x − y
36 26 35 syl ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x − y ≤ x − y
37 34 36 eqbrtrrd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ℑ ⁡ x ≤ x − y
38 25 27 37 lensymd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ¬ x − y < ℑ ⁡ x
39 23 38 eqnbrtrd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℝ → ¬ x abs ∘ − y < ℑ ⁡ x
40 39 ex ⊢ x ∈ ℂ ∖ ℝ → y ∈ ℝ → ¬ x abs ∘ − y < ℑ ⁡ x
41 40 con2d ⊢ x ∈ ℂ ∖ ℝ → x abs ∘ − y < ℑ ⁡ x → ¬ y ∈ ℝ
42 41 adantr ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℂ → x abs ∘ − y < ℑ ⁡ x → ¬ y ∈ ℝ
43 42 impr ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℂ ∧ x abs ∘ − y < ℑ ⁡ x → ¬ y ∈ ℝ
44 17 43 eldifd ⊢ x ∈ ℂ ∖ ℝ ∧ y ∈ ℂ ∧ x abs ∘ − y < ℑ ⁡ x → y ∈ ℂ ∖ ℝ
45 44 ex ⊢ x ∈ ℂ ∖ ℝ → y ∈ ℂ ∧ x abs ∘ − y < ℑ ⁡ x → y ∈ ℂ ∖ ℝ
46 16 45 sylbid ⊢ x ∈ ℂ ∖ ℝ → y ∈ x ball ⁡ abs ∘ − ℑ ⁡ x → y ∈ ℂ ∖ ℝ
47 46 ssrdv ⊢ x ∈ ℂ ∖ ℝ → x ball ⁡ abs ∘ − ℑ ⁡ x ⊆ ℂ ∖ ℝ
48 oveq2 ⊢ y = ℑ ⁡ x → x ball ⁡ abs ∘ − y = x ball ⁡ abs ∘ − ℑ ⁡ x
49 48 sseq1d ⊢ y = ℑ ⁡ x → x ball ⁡ abs ∘ − y ⊆ ℂ ∖ ℝ ↔ x ball ⁡ abs ∘ − ℑ ⁡ x ⊆ ℂ ∖ ℝ
50 49 rspcev ⊢ ℑ ⁡ x ∈ ℝ + ∧ x ball ⁡ abs ∘ − ℑ ⁡ x ⊆ ℂ ∖ ℝ → ∃ y ∈ ℝ + x ball ⁡ abs ∘ − y ⊆ ℂ ∖ ℝ
51 11 47 50 syl2anc ⊢ x ∈ ℂ ∖ ℝ → ∃ y ∈ ℝ + x ball ⁡ abs ∘ − y ⊆ ℂ ∖ ℝ
52 51 rgen ⊢ ∀ x ∈ ℂ ∖ ℝ ∃ y ∈ ℝ + x ball ⁡ abs ∘ − y ⊆ ℂ ∖ ℝ
53 1 cnfldtopn ⊢ J = MetOpen ⁡ abs ∘ −
54 53 elmopn2 ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ → ℂ ∖ ℝ ∈ J ↔ ℂ ∖ ℝ ⊆ ℂ ∧ ∀ x ∈ ℂ ∖ ℝ ∃ y ∈ ℝ + x ball ⁡ abs ∘ − y ⊆ ℂ ∖ ℝ
55 12 54 ax-mp ⊢ ℂ ∖ ℝ ∈ J ↔ ℂ ∖ ℝ ⊆ ℂ ∧ ∀ x ∈ ℂ ∖ ℝ ∃ y ∈ ℝ + x ball ⁡ abs ∘ − y ⊆ ℂ ∖ ℝ
56 2 52 55 mpbir2an ⊢ ℂ ∖ ℝ ∈ J
57 1 cnfldtop ⊢ J ∈ Top
58 ax-resscn ⊢ ℝ ⊆ ℂ
59 53 mopnuni ⊢ abs ∘ − ∈ ∞Met ⁡ ℂ → ℂ = ⋃ J
60 12 59 ax-mp ⊢ ℂ = ⋃ J
61 60 iscld2 ⊢ J ∈ Top ∧ ℝ ⊆ ℂ → ℝ ∈ Clsd ⁡ J ↔ ℂ ∖ ℝ ∈ J
62 57 58 61 mp2an ⊢ ℝ ∈ Clsd ⁡ J ↔ ℂ ∖ ℝ ∈ J
63 56 62 mpbir ⊢ ℝ ∈ Clsd ⁡ J