Theorem absfico

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

	Ref	Expression
Assertion	absfico	$$⊢\mathrm{abs}:ℂ⟶\left[0,\mathrm{+\infty }\right)$$

Proof

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