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 : CC --> ( 0 [,) +oo )

Proof

Step Hyp Ref Expression
1 df-abs 
 |-  abs = ( x e. CC |-> ( sqrt ` ( x x. ( * ` x ) ) ) )
2 0xr 
 |-  0 e. RR*
3 2 a1i 
 |-  ( x e. CC -> 0 e. RR* )
4 pnfxr 
 |-  +oo e. RR*
5 4 a1i 
 |-  ( x e. CC -> +oo e. RR* )
6 absval 
 |-  ( x e. CC -> ( abs ` x ) = ( sqrt ` ( x x. ( * ` x ) ) ) )
7 abscl 
 |-  ( x e. CC -> ( abs ` x ) e. RR )
8 6 7 eqeltrrd 
 |-  ( x e. CC -> ( sqrt ` ( x x. ( * ` x ) ) ) e. RR )
9 8 rexrd 
 |-  ( x e. CC -> ( sqrt ` ( x x. ( * ` x ) ) ) e. RR* )
10 cjmulrcl 
 |-  ( x e. CC -> ( x x. ( * ` x ) ) e. RR )
11 cjmulge0 
 |-  ( x e. CC -> 0 <_ ( x x. ( * ` x ) ) )
12 sqrtge0 
 |-  ( ( ( x x. ( * ` x ) ) e. RR /\ 0 <_ ( x x. ( * ` x ) ) ) -> 0 <_ ( sqrt ` ( x x. ( * ` x ) ) ) )
13 10 11 12 syl2anc 
 |-  ( x e. CC -> 0 <_ ( sqrt ` ( x x. ( * ` x ) ) ) )
14 8 ltpnfd 
 |-  ( x e. CC -> ( sqrt ` ( x x. ( * ` x ) ) ) < +oo )
15 3 5 9 13 14 elicod 
 |-  ( x e. CC -> ( sqrt ` ( x x. ( * ` x ) ) ) e. ( 0 [,) +oo ) )
16 1 15 fmpti 
 |-  abs : CC --> ( 0 [,) +oo )