Metamath Proof Explorer


Theorem sqrtsq

Description: Square root of square. (Contributed by NM, 14-Jan-2006) (Revised by Mario Carneiro, 29-May-2016)

Ref Expression
Assertion sqrtsq A0AA2=A

Proof

Step Hyp Ref Expression
1 eqid A2=A2
2 resqcl AA2
3 sqge0 A0A2
4 2 3 jca AA20A2
5 4 adantr A0AA20A2
6 sqrtsq2 A20A2A0AA2=AA2=A2
7 5 6 mpancom A0AA2=AA2=A2
8 1 7 mpbiri A0AA2=A