Step |
Hyp |
Ref |
Expression |
1 |
|
imf |
⊢ ℑ : ℂ ⟶ ℝ |
2 |
|
imcn2 |
⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑦 ∈ ℝ+ ) → ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℂ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ℑ ‘ 𝑤 ) − ( ℑ ‘ 𝑥 ) ) ) < 𝑦 ) ) |
3 |
2
|
rgen2 |
⊢ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℂ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ℑ ‘ 𝑤 ) − ( ℑ ‘ 𝑥 ) ) ) < 𝑦 ) |
4 |
|
ssid |
⊢ ℂ ⊆ ℂ |
5 |
|
ax-resscn |
⊢ ℝ ⊆ ℂ |
6 |
|
elcncf2 |
⊢ ( ( ℂ ⊆ ℂ ∧ ℝ ⊆ ℂ ) → ( ℑ ∈ ( ℂ –cn→ ℝ ) ↔ ( ℑ : ℂ ⟶ ℝ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℂ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ℑ ‘ 𝑤 ) − ( ℑ ‘ 𝑥 ) ) ) < 𝑦 ) ) ) ) |
7 |
4 5 6
|
mp2an |
⊢ ( ℑ ∈ ( ℂ –cn→ ℝ ) ↔ ( ℑ : ℂ ⟶ ℝ ∧ ∀ 𝑥 ∈ ℂ ∀ 𝑦 ∈ ℝ+ ∃ 𝑧 ∈ ℝ+ ∀ 𝑤 ∈ ℂ ( ( abs ‘ ( 𝑤 − 𝑥 ) ) < 𝑧 → ( abs ‘ ( ( ℑ ‘ 𝑤 ) − ( ℑ ‘ 𝑥 ) ) ) < 𝑦 ) ) ) |
8 |
1 3 7
|
mpbir2an |
⊢ ℑ ∈ ( ℂ –cn→ ℝ ) |