Description: A nonnegative number is its own absolute value. (Contributed by NM, 2Aug1999)
Ref  Expression  

Hypothesis  sqrtthi.1   A e. RR 

Assertion  absidi   ( 0 <_ A > ( abs ` A ) = A ) 
Step  Hyp  Ref  Expression 

1  sqrtthi.1   A e. RR 

2  absid   ( ( A e. RR /\ 0 <_ A ) > ( abs ` A ) = A ) 

3  1 2  mpan   ( 0 <_ A > ( abs ` A ) = A ) 