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

Metamath Proof Explorer

Theorem absre

Description: Absolute value of a real number. (Contributed by NM, 17-Mar-2005)

Ref Expression
Assertion absre 
|- ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 absval 
 |-  ( A e. CC -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
3 1 2 syl 
 |-  ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
4 1 sqvald 
 |-  ( A e. RR -> ( A ^ 2 ) = ( A x. A ) )
5 cjre 
 |-  ( A e. RR -> ( * ` A ) = A )
6 5 oveq2d 
 |-  ( A e. RR -> ( A x. ( * ` A ) ) = ( A x. A ) )
7 4 6 eqtr4d 
 |-  ( A e. RR -> ( A ^ 2 ) = ( A x. ( * ` A ) ) )
8 7 fveq2d 
 |-  ( A e. RR -> ( sqrt ` ( A ^ 2 ) ) = ( sqrt ` ( A x. ( * ` A ) ) ) )
9 3 8 eqtr4d 
 |-  ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) )