Metamath Proof Explorer

Theorem absf

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 : CC --> RR

Proof

Step Hyp Ref Expression
1 df-abs 
 |-  abs = ( x e. CC |-> ( sqrt ` ( x x. ( * ` x ) ) ) )
2 absval 
 |-  ( x e. CC -> ( abs ` x ) = ( sqrt ` ( x x. ( * ` x ) ) ) )
3 abscl 
 |-  ( x e. CC -> ( abs ` x ) e. RR )
4 2 3 eqeltrrd 
 |-  ( x e. CC -> ( sqrt ` ( x x. ( * ` x ) ) ) e. RR )
5 1 4 fmpti 
 |-  abs : CC --> RR