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 β€˜ 𝐽 )