Metamath Proof Explorer

Theorem abs0

Description: The absolute value of 0. (Contributed by NM, 26-Mar-2005) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion abs0 
|- ( abs ` 0 ) = 0

Proof

Step Hyp Ref Expression
1 0cn 
 |-  0 e. CC
2 absval 
 |-  ( 0 e. CC -> ( abs ` 0 ) = ( sqrt ` ( 0 x. ( * ` 0 ) ) ) )
3 1 2 ax-mp 
 |-  ( abs ` 0 ) = ( sqrt ` ( 0 x. ( * ` 0 ) ) )
4 1 cjcli 
 |-  ( * ` 0 ) e. CC
5 4 mul02i 
 |-  ( 0 x. ( * ` 0 ) ) = 0
6 5 fveq2i 
 |-  ( sqrt ` ( 0 x. ( * ` 0 ) ) ) = ( sqrt ` 0 )
7 sqrt0 
 |-  ( sqrt ` 0 ) = 0
8 3 6 7 3eqtri 
 |-  ( abs ` 0 ) = 0