Metamath Proof Explorer


Theorem sqrtmsq2i

Description: Relationship between square root and squares. (Contributed by NM, 31-Jul-1999)

Ref Expression
Hypotheses sqrtthi.1 A
sqr11.1 B
Assertion sqrtmsq2i 0A0BA=BA=BB

Proof

Step Hyp Ref Expression
1 sqrtthi.1 A
2 sqr11.1 B
3 sqrtsq2 A0AB0BA=BA=B2
4 2 3 mpanr1 A0A0BA=BA=B2
5 1 4 mpanl1 0A0BA=BA=B2
6 2 recni B
7 6 sqvali B2=BB
8 7 eqeq2i A=B2A=BB
9 5 8 bitrdi 0A0BA=BA=BB