Theorem imcn2

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

	Ref	Expression
Assertion	imcn2	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|\Im \left(z\right)-\Im \left(A\right)\right|<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		imf	$$⊢\Im :ℂ⟶ℝ$$
2		ax-resscn	$$⊢ℝ\subseteq ℂ$$
3		fss	$$⊢\left(\Im :ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \Im :ℂ⟶ℂ$$
4	1 2 3	mp2an	$$⊢\Im :ℂ⟶ℂ$$
5		imsub	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \Im \left(z-A\right)=\Im \left(z\right)-\Im \left(A\right)$$
6	5	fveq2d	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\Im \left(z-A\right)\right|=\left|\Im \left(z\right)-\Im \left(A\right)\right|$$
7		subcl	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to z-A\in ℂ$$
8		absimle	$$⊢z-A\in ℂ\to \left|\Im \left(z-A\right)\right|\le \left|z-A\right|$$
9	7 8	syl	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\Im \left(z-A\right)\right|\le \left|z-A\right|$$
10	6 9	eqbrtrrd	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\Im \left(z\right)-\Im \left(A\right)\right|\le \left|z-A\right|$$
11	4 10	cn1lem	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|\Im \left(z\right)-\Im \left(A\right)\right|<x\right)$$