Metamath Proof Explorer

Theorem cjcncf

Description: Complex conjugate is continuous. (Contributed by Paul Chapman, 21-Oct-2007) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion cjcncf 
|- * e. ( CC -cn-> CC )

Proof

Step Hyp Ref Expression
1 cjf 
 |-  * : CC --> CC
2 cjcn2 
 |-  ( ( x e. CC /\ y e. RR+ ) -> E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( * ` w ) - ( * ` x ) ) ) < y ) )
3 2 rgen2 
 |-  A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( * ` w ) - ( * ` x ) ) ) < y )
4 ssid 
 |-  CC C_ CC
5 elcncf2 
 |-  ( ( CC C_ CC /\ CC C_ CC ) -> ( * e. ( CC -cn-> CC ) <-> ( * : CC --> CC /\ A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( * ` w ) - ( * ` x ) ) ) < y ) ) ) )
6 4 4 5 mp2an 
 |-  ( * e. ( CC -cn-> CC ) <-> ( * : CC --> CC /\ A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( * ` w ) - ( * ` x ) ) ) < y ) ) )
7 1 3 6 mpbir2an 
 |-  * e. ( CC -cn-> CC )