Theorem recn2

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

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

Proof

Step	Hyp	Ref	Expression
1		ref	$$⊢\Re :ℂ⟶ℝ$$
2		ax-resscn	$$⊢ℝ\subseteq ℂ$$
3		fss	$$⊢\left(\Re :ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \Re :ℂ⟶ℂ$$
4	1 2 3	mp2an	$$⊢\Re :ℂ⟶ℂ$$
5		resub	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \Re \left(z-A\right)=\Re \left(z\right)-\Re \left(A\right)$$
6	5	fveq2d	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\Re \left(z-A\right)\right|=\left|\Re \left(z\right)-\Re \left(A\right)\right|$$
7		subcl	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to z-A\in ℂ$$
8		absrele	$$⊢z-A\in ℂ\to \left|\Re \left(z-A\right)\right|\le \left|z-A\right|$$
9	7 8	syl	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\Re \left(z-A\right)\right|\le \left|z-A\right|$$
10	6 9	eqbrtrrd	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\Re \left(z\right)-\Re \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|\Re \left(z\right)-\Re \left(A\right)\right|<x\right)$$