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