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

Metamath Proof Explorer

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 [,) +∞ )