This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
Assertion recld2 ℝ ∈ ( Clsd ‘ 𝐽 )

Proof

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