Metamath Proof Explorer

Theorem cjcn2

Description: The complex conjugate function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

Ref Expression
Assertion cjcn2 
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 cjf 
 |-  * : CC --> CC
2 cjcl 
 |-  ( z e. CC -> ( * ` z ) e. CC )
3 cjcl 
 |-  ( A e. CC -> ( * ` A ) e. CC )
4 subcl 
 |-  ( ( ( * ` z ) e. CC /\ ( * ` A ) e. CC ) -> ( ( * ` z ) - ( * ` A ) ) e. CC )
5 2 3 4 syl2an 
 |-  ( ( z e. CC /\ A e. CC ) -> ( ( * ` z ) - ( * ` A ) ) e. CC )
6 5 abscld 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) e. RR )
7 cjsub 
 |-  ( ( z e. CC /\ A e. CC ) -> ( * ` ( z - A ) ) = ( ( * ` z ) - ( * ` A ) ) )
8 7 fveq2d 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( * ` ( z - A ) ) ) = ( abs ` ( ( * ` z ) - ( * ` A ) ) ) )
9 subcl 
 |-  ( ( z e. CC /\ A e. CC ) -> ( z - A ) e. CC )
10 9 abscjd 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( * ` ( z - A ) ) ) = ( abs ` ( z - A ) ) )
11 8 10 eqtr3d 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) = ( abs ` ( z - A ) ) )
12 6 11 eqled 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) <_ ( abs ` ( z - A ) ) )
13 1 12 cn1lem 
 |-  ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( * ` z ) - ( * ` A ) ) ) < x ) )