Theorem abscn2

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

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

Proof

Step	Hyp	Ref	Expression
1		absf	$$⊢\mathrm{abs}:ℂ⟶ℝ$$
2		ax-resscn	$$⊢ℝ\subseteq ℂ$$
3		fss	$$⊢\left(\mathrm{abs}:ℂ⟶ℝ\wedge ℝ\subseteq ℂ\right)\to \mathrm{abs}:ℂ⟶ℂ$$
4	1 2 3	mp2an	$$⊢\mathrm{abs}:ℂ⟶ℂ$$
5		abs2difabs	$$⊢\left(z\in ℂ\wedge A\in ℂ\right)\to \left|\left|z\right|-\left|A\right|\right|\le \left|z-A\right|$$
6	4 5	cn1lem	$$⊢\left(A\in ℂ\wedge x\in {ℝ}^{+}\right)\to \exists y\in {ℝ}^{+}\forall z\in ℂ\left(\left|z-A\right|<y\to \left|\left|z\right|-\left|A\right|\right|<x\right)$$