Metamath Proof Explorer

Theorem cncmet

Description: The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006) (Revised by Mario Carneiro, 15-Oct-2015)

Ref Expression
Hypothesis cncmet.1 
|- D = ( abs o. - )
Assertion cncmet 
|- D e. ( CMet ` CC )

Proof

Step Hyp Ref Expression
1 cncmet.1 
 |-  D = ( abs o. - )
2 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
3 2 cnfldtopn 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` ( abs o. - ) )
4 1 fveq2i 
 |-  ( MetOpen ` D ) = ( MetOpen ` ( abs o. - ) )
5 3 4 eqtr4i 
 |-  ( TopOpen ` CCfld ) = ( MetOpen ` D )
6 cnmet 
 |-  ( abs o. - ) e. ( Met ` CC )
7 1 6 eqeltri 
 |-  D e. ( Met ` CC )
8 7 a1i 
 |-  ( T. -> D e. ( Met ` CC ) )
9 1rp 
 |-  1 e. RR+
10 9 a1i 
 |-  ( T. -> 1 e. RR+ )
11 2 cnfldtop 
 |-  ( TopOpen ` CCfld ) e. Top
12 metxmet 
 |-  ( D e. ( Met ` CC ) -> D e. ( *Met ` CC ) )
13 7 12 ax-mp 
 |-  D e. ( *Met ` CC )
14 1xr 
 |-  1 e. RR*
15 blssm 
 |-  ( ( D e. ( *Met ` CC ) /\ x e. CC /\ 1 e. RR* ) -> ( x ( ball ` D ) 1 ) C_ CC )
16 13 14 15 mp3an13 
 |-  ( x e. CC -> ( x ( ball ` D ) 1 ) C_ CC )
17 unicntop 
 |-  CC = U. ( TopOpen ` CCfld )
18 17 clscld 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( x ( ball ` D ) 1 ) C_ CC ) -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
19 11 16 18 sylancr 
 |-  ( x e. CC -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) )
20 abscl 
 |-  ( x e. CC -> ( abs ` x ) e. RR )
21 peano2re 
 |-  ( ( abs ` x ) e. RR -> ( ( abs ` x ) + 1 ) e. RR )
22 20 21 syl 
 |-  ( x e. CC -> ( ( abs ` x ) + 1 ) e. RR )
23 df-rab 
 |-  { y e. CC | ( x D y ) <_ 1 } = { y | ( y e. CC /\ ( x D y ) <_ 1 ) }
24 23 eqcomi 
 |-  { y | ( y e. CC /\ ( x D y ) <_ 1 ) } = { y e. CC | ( x D y ) <_ 1 }
25 5 24 blcls 
 |-  ( ( D e. ( *Met ` CC ) /\ x e. CC /\ 1 e. RR* ) -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ { y | ( y e. CC /\ ( x D y ) <_ 1 ) } )
26 13 14 25 mp3an13 
 |-  ( x e. CC -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ { y | ( y e. CC /\ ( x D y ) <_ 1 ) } )
27 abscl 
 |-  ( y e. CC -> ( abs ` y ) e. RR )
28 27 ad2antrl 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( abs ` y ) e. RR )
29 20 adantr 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( abs ` x ) e. RR )
30 28 29 resubcld 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( ( abs ` y ) - ( abs ` x ) ) e. RR )
31 simpl 
 |-  ( ( y e. CC /\ ( x D y ) <_ 1 ) -> y e. CC )
32 id 
 |-  ( x e. CC -> x e. CC )
33 subcl 
 |-  ( ( y e. CC /\ x e. CC ) -> ( y - x ) e. CC )
34 31 32 33 syl2anr 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( y - x ) e. CC )
35 34 abscld 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( abs ` ( y - x ) ) e. RR )
36 1red 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> 1 e. RR )
37 simprl 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> y e. CC )
38 simpl 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> x e. CC )
39 37 38 abs2difd 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( ( abs ` y ) - ( abs ` x ) ) <_ ( abs ` ( y - x ) ) )
40 1 cnmetdval 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x D y ) = ( abs ` ( x - y ) ) )
41 abssub 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x - y ) ) = ( abs ` ( y - x ) ) )
42 40 41 eqtrd 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x D y ) = ( abs ` ( y - x ) ) )
43 42 adantrr 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( x D y ) = ( abs ` ( y - x ) ) )
44 simprr 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( x D y ) <_ 1 )
45 43 44 eqbrtrrd 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( abs ` ( y - x ) ) <_ 1 )
46 30 35 36 39 45 letrd 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( ( abs ` y ) - ( abs ` x ) ) <_ 1 )
47 28 29 36 lesubadd2d 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( ( ( abs ` y ) - ( abs ` x ) ) <_ 1 <-> ( abs ` y ) <_ ( ( abs ` x ) + 1 ) ) )
48 46 47 mpbid 
 |-  ( ( x e. CC /\ ( y e. CC /\ ( x D y ) <_ 1 ) ) -> ( abs ` y ) <_ ( ( abs ` x ) + 1 ) )
49 48 ex 
 |-  ( x e. CC -> ( ( y e. CC /\ ( x D y ) <_ 1 ) -> ( abs ` y ) <_ ( ( abs ` x ) + 1 ) ) )
50 49 ss2abdv 
 |-  ( x e. CC -> { y | ( y e. CC /\ ( x D y ) <_ 1 ) } C_ { y | ( abs ` y ) <_ ( ( abs ` x ) + 1 ) } )
51 26 50 sstrd 
 |-  ( x e. CC -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ { y | ( abs ` y ) <_ ( ( abs ` x ) + 1 ) } )
52 ssabral 
 |-  ( ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ { y | ( abs ` y ) <_ ( ( abs ` x ) + 1 ) } <-> A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ ( ( abs ` x ) + 1 ) )
53 51 52 sylib 
 |-  ( x e. CC -> A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ ( ( abs ` x ) + 1 ) )
54 brralrspcev 
 |-  ( ( ( ( abs ` x ) + 1 ) e. RR /\ A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ ( ( abs ` x ) + 1 ) ) -> E. r e. RR A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ r )
55 22 53 54 syl2anc 
 |-  ( x e. CC -> E. r e. RR A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ r )
56 17 clsss3 
 |-  ( ( ( TopOpen ` CCfld ) e. Top /\ ( x ( ball ` D ) 1 ) C_ CC ) -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ CC )
57 11 16 56 sylancr 
 |-  ( x e. CC -> ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ CC )
58 eqid 
 |-  ( ( TopOpen ` CCfld ) |`t ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ) = ( ( TopOpen ` CCfld ) |`t ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) )
59 2 58 cnheibor 
 |-  ( ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) C_ CC -> ( ( ( TopOpen ` CCfld ) |`t ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp <-> ( ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ E. r e. RR A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ r ) ) )
60 57 59 syl 
 |-  ( x e. CC -> ( ( ( TopOpen ` CCfld ) |`t ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp <-> ( ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) e. ( Clsd ` ( TopOpen ` CCfld ) ) /\ E. r e. RR A. y e. ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ( abs ` y ) <_ r ) ) )
61 19 55 60 mpbir2and 
 |-  ( x e. CC -> ( ( TopOpen ` CCfld ) |`t ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp )
62 61 adantl 
 |-  ( ( T. /\ x e. CC ) -> ( ( TopOpen ` CCfld ) |`t ( ( cls ` ( TopOpen ` CCfld ) ) ` ( x ( ball ` D ) 1 ) ) ) e. Comp )
63 5 8 10 62 relcmpcmet 
 |-  ( T. -> D e. ( CMet ` CC ) )
64 63 mptru 
 |-  D e. ( CMet ` CC )