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 ) )