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 ) ) )