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 ` CCfld )
Assertion recld2 
|- RR e. ( Clsd ` J )

Proof

Step Hyp Ref Expression
1 recld2.1 
 |-  J = ( TopOpen ` CCfld )
2 difss 
 |-  ( CC \ RR ) C_ CC
3 eldifi 
 |-  ( x e. ( CC \ RR ) -> x e. CC )
4 3 imcld 
 |-  ( x e. ( CC \ RR ) -> ( Im ` x ) e. RR )
5 4 recnd 
 |-  ( x e. ( CC \ RR ) -> ( Im ` x ) e. CC )
6 eldifn 
 |-  ( x e. ( CC \ RR ) -> -. x e. RR )
7 reim0b 
 |-  ( x e. CC -> ( x e. RR <-> ( Im ` x ) = 0 ) )
8 3 7 syl 
 |-  ( x e. ( CC \ RR ) -> ( x e. RR <-> ( Im ` x ) = 0 ) )
9 8 necon3bbid 
 |-  ( x e. ( CC \ RR ) -> ( -. x e. RR <-> ( Im ` x ) =/= 0 ) )
10 6 9 mpbid 
 |-  ( x e. ( CC \ RR ) -> ( Im ` x ) =/= 0 )
11 5 10 absrpcld 
 |-  ( x e. ( CC \ RR ) -> ( abs ` ( Im ` x ) ) e. RR+ )
12 cnxmet 
 |-  ( abs o. - ) e. ( *Met ` CC )
13 5 abscld 
 |-  ( x e. ( CC \ RR ) -> ( abs ` ( Im ` x ) ) e. RR )
14 13 rexrd 
 |-  ( x e. ( CC \ RR ) -> ( abs ` ( Im ` x ) ) e. RR* )
15 elbl 
 |-  ( ( ( abs o. - ) e. ( *Met ` CC ) /\ x e. CC /\ ( abs ` ( Im ` x ) ) e. RR* ) -> ( y e. ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) <-> ( y e. CC /\ ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) ) )
16 12 3 14 15 mp3an2i 
 |-  ( x e. ( CC \ RR ) -> ( y e. ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) <-> ( y e. CC /\ ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) ) )
17 simprl 
 |-  ( ( x e. ( CC \ RR ) /\ ( y e. CC /\ ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) ) -> y e. CC )
18 3 adantr 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> x e. CC )
19 simpr 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> y e. RR )
20 19 recnd 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> y e. CC )
21 eqid 
 |-  ( abs o. - ) = ( abs o. - )
22 21 cnmetdval 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x ( abs o. - ) y ) = ( abs ` ( x - y ) ) )
23 18 20 22 syl2anc 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( x ( abs o. - ) y ) = ( abs ` ( x - y ) ) )
24 5 adantr 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( Im ` x ) e. CC )
25 24 abscld 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( abs ` ( Im ` x ) ) e. RR )
26 18 20 subcld 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( x - y ) e. CC )
27 26 abscld 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( abs ` ( x - y ) ) e. RR )
28 18 20 imsubd 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( Im ` ( x - y ) ) = ( ( Im ` x ) - ( Im ` y ) ) )
29 reim0 
 |-  ( y e. RR -> ( Im ` y ) = 0 )
30 29 adantl 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( Im ` y ) = 0 )
31 30 oveq2d 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( ( Im ` x ) - ( Im ` y ) ) = ( ( Im ` x ) - 0 ) )
32 24 subid1d 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( ( Im ` x ) - 0 ) = ( Im ` x ) )
33 28 31 32 3eqtrd 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( Im ` ( x - y ) ) = ( Im ` x ) )
34 33 fveq2d 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( abs ` ( Im ` ( x - y ) ) ) = ( abs ` ( Im ` x ) ) )
35 absimle 
 |-  ( ( x - y ) e. CC -> ( abs ` ( Im ` ( x - y ) ) ) <_ ( abs ` ( x - y ) ) )
36 26 35 syl 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( abs ` ( Im ` ( x - y ) ) ) <_ ( abs ` ( x - y ) ) )
37 34 36 eqbrtrrd 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> ( abs ` ( Im ` x ) ) <_ ( abs ` ( x - y ) ) )
38 25 27 37 lensymd 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> -. ( abs ` ( x - y ) ) < ( abs ` ( Im ` x ) ) )
39 23 38 eqnbrtrd 
 |-  ( ( x e. ( CC \ RR ) /\ y e. RR ) -> -. ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) )
40 39 ex 
 |-  ( x e. ( CC \ RR ) -> ( y e. RR -> -. ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) )
41 40 con2d 
 |-  ( x e. ( CC \ RR ) -> ( ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) -> -. y e. RR ) )
42 41 adantr 
 |-  ( ( x e. ( CC \ RR ) /\ y e. CC ) -> ( ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) -> -. y e. RR ) )
43 42 impr 
 |-  ( ( x e. ( CC \ RR ) /\ ( y e. CC /\ ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) ) -> -. y e. RR )
44 17 43 eldifd 
 |-  ( ( x e. ( CC \ RR ) /\ ( y e. CC /\ ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) ) -> y e. ( CC \ RR ) )
45 44 ex 
 |-  ( x e. ( CC \ RR ) -> ( ( y e. CC /\ ( x ( abs o. - ) y ) < ( abs ` ( Im ` x ) ) ) -> y e. ( CC \ RR ) ) )
46 16 45 sylbid 
 |-  ( x e. ( CC \ RR ) -> ( y e. ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) -> y e. ( CC \ RR ) ) )
47 46 ssrdv 
 |-  ( x e. ( CC \ RR ) -> ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) C_ ( CC \ RR ) )
48 oveq2 
 |-  ( y = ( abs ` ( Im ` x ) ) -> ( x ( ball ` ( abs o. - ) ) y ) = ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) )
49 48 sseq1d 
 |-  ( y = ( abs ` ( Im ` x ) ) -> ( ( x ( ball ` ( abs o. - ) ) y ) C_ ( CC \ RR ) <-> ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) C_ ( CC \ RR ) ) )
50 49 rspcev 
 |-  ( ( ( abs ` ( Im ` x ) ) e. RR+ /\ ( x ( ball ` ( abs o. - ) ) ( abs ` ( Im ` x ) ) ) C_ ( CC \ RR ) ) -> E. y e. RR+ ( x ( ball ` ( abs o. - ) ) y ) C_ ( CC \ RR ) )
51 11 47 50 syl2anc 
 |-  ( x e. ( CC \ RR ) -> E. y e. RR+ ( x ( ball ` ( abs o. - ) ) y ) C_ ( CC \ RR ) )
52 51 rgen 
 |-  A. x e. ( CC \ RR ) E. y e. RR+ ( x ( ball ` ( abs o. - ) ) y ) C_ ( CC \ RR )
53 1 cnfldtopn 
 |-  J = ( MetOpen ` ( abs o. - ) )
54 53 elmopn2 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> ( ( CC \ RR ) e. J <-> ( ( CC \ RR ) C_ CC /\ A. x e. ( CC \ RR ) E. y e. RR+ ( x ( ball ` ( abs o. - ) ) y ) C_ ( CC \ RR ) ) ) )
55 12 54 ax-mp 
 |-  ( ( CC \ RR ) e. J <-> ( ( CC \ RR ) C_ CC /\ A. x e. ( CC \ RR ) E. y e. RR+ ( x ( ball ` ( abs o. - ) ) y ) C_ ( CC \ RR ) ) )
56 2 52 55 mpbir2an 
 |-  ( CC \ RR ) e. J
57 1 cnfldtop 
 |-  J e. Top
58 ax-resscn 
 |-  RR C_ CC
59 53 mopnuni 
 |-  ( ( abs o. - ) e. ( *Met ` CC ) -> CC = U. J )
60 12 59 ax-mp 
 |-  CC = U. J
61 60 iscld2 
 |-  ( ( J e. Top /\ RR C_ CC ) -> ( RR e. ( Clsd ` J ) <-> ( CC \ RR ) e. J ) )
62 57 58 61 mp2an 
 |-  ( RR e. ( Clsd ` J ) <-> ( CC \ RR ) e. J )
63 56 62 mpbir 
 |-  RR e. ( Clsd ` J )