Metamath Proof Explorer


Theorem absvalsq2

Description: Square of value of absolute value function. (Contributed by NM, 1-Feb-2007)

Ref Expression
Assertion absvalsq2 AA2=A2+A2

Proof

Step Hyp Ref Expression
1 absvalsq AA2=AA
2 cjmulval AAA=A2+A2
3 1 2 eqtrd AA2=A2+A2