Step |
Hyp |
Ref |
Expression |
1 |
|
imf |
⊢ ℑ : ℂ ⟶ ℝ |
2 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
3 |
|
fss |
⊢ ( ( ℑ : ℂ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → ℑ : ℂ ⟶ ℂ ) |
4 |
1 2 3
|
mp2an |
⊢ ℑ : ℂ ⟶ ℂ |
5 |
|
imsub |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ℑ ‘ ( 𝑧 − 𝐴 ) ) = ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ℑ ‘ ( 𝑧 − 𝐴 ) ) ) = ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) ) |
7 |
|
subcl |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( 𝑧 − 𝐴 ) ∈ ℂ ) |
8 |
|
absimle |
⊢ ( ( 𝑧 − 𝐴 ) ∈ ℂ → ( abs ‘ ( ℑ ‘ ( 𝑧 − 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ) |
9 |
7 8
|
syl |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ℑ ‘ ( 𝑧 − 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ) |
10 |
6 9
|
eqbrtrrd |
⊢ ( ( 𝑧 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) ≤ ( abs ‘ ( 𝑧 − 𝐴 ) ) ) |
11 |
4 10
|
cn1lem |
⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) < 𝑥 ) ) |