absfico

Description: Mapping domain and codomain of the absolute value function. (Contributed by Glauco Siliprandi, 3-Mar-2021)

		Ref	Expression
	Assertion	absfico	$⊢ abs : ℂ ⟶ [0, +∞)$

Step	Hyp	Ref	Expression
1		df-abs	$⊢ abs = (x \in ℂ ⟼ \sqrt{x \overline{x}})$
2		0xr	$⊢ 0 \in ℝ^{*}$
3	2	a1i	$⊢ x \in ℂ \to 0 \in ℝ^{*}$
4		pnfxr	$⊢ +∞ \in ℝ^{*}$
5	4	a1i	$⊢ x \in ℂ \to +∞ \in ℝ^{*}$
6		absval	$⊢ x \in ℂ \to \|x\| = \sqrt{x \overline{x}}$
7		abscl	$⊢ x \in ℂ \to \|x\| \in ℝ$
8	6 7	eqeltrrd	$⊢ x \in ℂ \to \sqrt{x \overline{x}} \in ℝ$
9	8	rexrd	$⊢ x \in ℂ \to \sqrt{x \overline{x}} \in ℝ^{*}$
10		cjmulrcl	$⊢ x \in ℂ \to x \overline{x} \in ℝ$
11		cjmulge0	$⊢ x \in ℂ \to 0 \leq x \overline{x}$
12		sqrtge0	$⊢ (x \overline{x} \in ℝ \land 0 \leq x \overline{x}) \to 0 \leq \sqrt{x \overline{x}}$
13	10 11 12	syl2anc	$⊢ x \in ℂ \to 0 \leq \sqrt{x \overline{x}}$
14	8	ltpnfd	$⊢ x \in ℂ \to \sqrt{x \overline{x}} < +∞$
15	3 5 9 13 14	elicod	$⊢ x \in ℂ \to \sqrt{x \overline{x}} \in [0, +∞)$
16	1 15	fmpti	$⊢ abs : ℂ ⟶ [0, +∞)$

Metamath Proof Explorer