Metamath Proof Explorer


Theorem absre

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

Ref Expression
Assertion absre AA=A2

Proof

Step Hyp Ref Expression
1 recn AA
2 absval AA=AA
3 1 2 syl AA=AA
4 1 sqvald AA2=AA
5 cjre AA=A
6 5 oveq2d AAA=AA
7 4 6 eqtr4d AA2=AA
8 7 fveq2d AA2=AA
9 3 8 eqtr4d AA=A2