**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 = ( 𝑥 ∈ ℂ ↦ ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ) | |

2 | absval | ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) = ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ) | |

3 | abscl | ⊢ ( 𝑥 ∈ ℂ → ( abs ‘ 𝑥 ) ∈ ℝ ) | |

4 | 2 3 | eqeltrrd | ⊢ ( 𝑥 ∈ ℂ → ( √ ‘ ( 𝑥 · ( ∗ ‘ 𝑥 ) ) ) ∈ ℝ ) |

5 | 1 4 | fmpti | ⊢ abs : ℂ ⟶ ℝ |