Theorem imcn2

Description: The imaginary part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

	Ref	Expression
Assertion	imcn2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑥 ∈ ℝ+ ) → ∃ 𝑦 ∈ ℝ+ ∀ 𝑧 ∈ ℂ ( ( abs ‘ ( 𝑧 − 𝐴 ) ) < 𝑦 → ( abs ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) < 𝑥 ) )

Proof

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 ‘ ( ( ℑ ‘ 𝑧 ) − ( ℑ ‘ 𝐴 ) ) ) < 𝑥 ) )