Metamath Proof Explorer

Theorem imcn2

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

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

Proof

Step Hyp Ref Expression
1 imf 
 |-  Im : CC --> RR
2 ax-resscn 
 |-  RR C_ CC
3 fss 
 |-  ( ( Im : CC --> RR /\ RR C_ CC ) -> Im : CC --> CC )
4 1 2 3 mp2an 
 |-  Im : CC --> CC
5 imsub 
 |-  ( ( z e. CC /\ A e. CC ) -> ( Im ` ( z - A ) ) = ( ( Im ` z ) - ( Im ` A ) ) )
6 5 fveq2d 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( Im ` ( z - A ) ) ) = ( abs ` ( ( Im ` z ) - ( Im ` A ) ) ) )
7 subcl 
 |-  ( ( z e. CC /\ A e. CC ) -> ( z - A ) e. CC )
8 absimle 
 |-  ( ( z - A ) e. CC -> ( abs ` ( Im ` ( z - A ) ) ) <_ ( abs ` ( z - A ) ) )
9 7 8 syl 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( Im ` ( z - A ) ) ) <_ ( abs ` ( z - A ) ) )
10 6 9 eqbrtrrd 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( Im ` z ) - ( Im ` A ) ) ) <_ ( abs ` ( z - A ) ) )
11 4 10 cn1lem 
 |-  ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Im ` z ) - ( Im ` A ) ) ) < x ) )