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

Metamath Proof Explorer

Theorem absf

Description: Mapping domain and codomain of the absolute value function. (Contributed by NM, 30-Aug-2007) (Revised by Mario Carneiro, 7-Nov-2013)

		Ref	Expression
	Assertion	absf	$⊢ abs : ℂ ⟶ ℝ$

Step	Hyp	Ref	Expression
1		df-abs	$⊢ abs = (x \in ℂ ⟼ \sqrt{x \overline{x}})$
2		absval	$⊢ x \in ℂ \to \|x\| = \sqrt{x \overline{x}}$
3		abscl	$⊢ x \in ℂ \to \|x\| \in ℝ$
4	2 3	eqeltrrd	$⊢ x \in ℂ \to \sqrt{x \overline{x}} \in ℝ$
5	1 4	fmpti	$⊢ abs : ℂ ⟶ ℝ$