Metamath Proof Explorer

Theorem absrei

Description: Absolute value of a real number. (Contributed by NM, 3-Aug-1999)

Ref Expression
Hypothesis sqrtthi.1 
|- A e. RR
Assertion absrei 
|- ( abs ` A ) = ( sqrt ` ( A ^ 2 ) )

Proof

Step Hyp Ref Expression
1 sqrtthi.1 
 |-  A e. RR
2 absre 
 |-  ( A e. RR -> ( abs ` A ) = ( sqrt ` ( A ^ 2 ) ) )
3 1 2 ax-mp 
 |-  ( abs ` A ) = ( sqrt ` ( A ^ 2 ) )