Theorem absfico

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

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

Proof

Step	Hyp	Ref	Expression
1		df-abs	⊢ abs = ( 𝑥 ∈ ℂ ↦ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
2		0xr	⊢ 0 ∈ ℝ*
3	2	a1i	⊢ ( 𝑥 ∈ ℂ → 0 ∈ ℝ* )
4		pnfxr	⊢ +∞ ∈ ℝ*
5	4	a1i	⊢ ( 𝑥 ∈ ℂ → +∞ ∈ ℝ* )
6		absval	⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) = ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
7		abscl	⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ )
8	6 7	eqeltrrd	⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ∈ ℝ )
9	8	rexrd	⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ∈ ℝ* )
10		cjmulrcl	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ∈ ℝ )
11		cjmulge0	⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) )
12		sqrtge0	⊢ ( ( ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) → 0 ≤ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
13	10 11 12	syl2anc	⊢ ( 𝑥 ∈ ℂ → 0 ≤ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) )
14	8	ltpnfd	⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) < +∞ )
15	3 5 9 13 14	elicod	⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ∈ ( 0 [,) +∞ ) )
16	1 15	fmpti	⊢ abs : ℂ ⟶ ( 0 [,) +∞ )