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