This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abscn2

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

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

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