Metamath Proof Explorer

Theorem cnblcld

Description: Two ways to write the closed ball centered at zero. (Contributed by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypothesis cnblcld.1 
|- D = ( abs o. - )
Assertion cnblcld 
|- ( R e. RR* -> ( `' abs " ( 0 [,] R ) ) = { x e. CC | ( 0 D x ) <_ R } )

Proof

Step Hyp Ref Expression
1 cnblcld.1 
 |-  D = ( abs o. - )
2 absf 
 |-  abs : CC --> RR
3 ffn 
 |-  ( abs : CC --> RR -> abs Fn CC )
4 elpreima 
 |-  ( abs Fn CC -> ( x e. ( `' abs " ( 0 [,] R ) ) <-> ( x e. CC /\ ( abs ` x ) e. ( 0 [,] R ) ) ) )
5 2 3 4 mp2b 
 |-  ( x e. ( `' abs " ( 0 [,] R ) ) <-> ( x e. CC /\ ( abs ` x ) e. ( 0 [,] R ) ) )
6 df-3an 
 |-  ( ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) <_ R ) <-> ( ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) ) /\ ( abs ` x ) <_ R ) )
7 abscl 
 |-  ( x e. CC -> ( abs ` x ) e. RR )
8 7 rexrd 
 |-  ( x e. CC -> ( abs ` x ) e. RR* )
9 absge0 
 |-  ( x e. CC -> 0 <_ ( abs ` x ) )
10 8 9 jca 
 |-  ( x e. CC -> ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) ) )
11 10 adantl 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) ) )
12 11 biantrurd 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) <_ R <-> ( ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) ) /\ ( abs ` x ) <_ R ) ) )
13 6 12 bitr4id 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) <_ R ) <-> ( abs ` x ) <_ R ) )
14 0xr 
 |-  0 e. RR*
15 simpl 
 |-  ( ( R e. RR* /\ x e. CC ) -> R e. RR* )
16 elicc1 
 |-  ( ( 0 e. RR* /\ R e. RR* ) -> ( ( abs ` x ) e. ( 0 [,] R ) <-> ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) <_ R ) ) )
17 14 15 16 sylancr 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. ( 0 [,] R ) <-> ( ( abs ` x ) e. RR* /\ 0 <_ ( abs ` x ) /\ ( abs ` x ) <_ R ) ) )
18 0cn 
 |-  0 e. CC
19 1 cnmetdval 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 D x ) = ( abs ` ( 0 - x ) ) )
20 abssub 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( abs ` ( 0 - x ) ) = ( abs ` ( x - 0 ) ) )
21 19 20 eqtrd 
 |-  ( ( 0 e. CC /\ x e. CC ) -> ( 0 D x ) = ( abs ` ( x - 0 ) ) )
22 18 21 mpan 
 |-  ( x e. CC -> ( 0 D x ) = ( abs ` ( x - 0 ) ) )
23 subid1 
 |-  ( x e. CC -> ( x - 0 ) = x )
24 23 fveq2d 
 |-  ( x e. CC -> ( abs ` ( x - 0 ) ) = ( abs ` x ) )
25 22 24 eqtrd 
 |-  ( x e. CC -> ( 0 D x ) = ( abs ` x ) )
26 25 adantl 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( 0 D x ) = ( abs ` x ) )
27 26 breq1d 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( 0 D x ) <_ R <-> ( abs ` x ) <_ R ) )
28 13 17 27 3bitr4d 
 |-  ( ( R e. RR* /\ x e. CC ) -> ( ( abs ` x ) e. ( 0 [,] R ) <-> ( 0 D x ) <_ R ) )
29 28 pm5.32da 
 |-  ( R e. RR* -> ( ( x e. CC /\ ( abs ` x ) e. ( 0 [,] R ) ) <-> ( x e. CC /\ ( 0 D x ) <_ R ) ) )
30 5 29 syl5bb 
 |-  ( R e. RR* -> ( x e. ( `' abs " ( 0 [,] R ) ) <-> ( x e. CC /\ ( 0 D x ) <_ R ) ) )
31 30 abbi2dv 
 |-  ( R e. RR* -> ( `' abs " ( 0 [,] R ) ) = { x | ( x e. CC /\ ( 0 D x ) <_ R ) } )
32 df-rab 
 |-  { x e. CC | ( 0 D x ) <_ R } = { x | ( x e. CC /\ ( 0 D x ) <_ R ) }
33 31 32 eqtr4di 
 |-  ( R e. RR* -> ( `' abs " ( 0 [,] R ) ) = { x e. CC | ( 0 D x ) <_ R } )