Metamath Proof Explorer


Theorem msq11

Description: The square of a nonnegative number is a one-to-one function. (Contributed by NM, 29-Jul-1999) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion msq11 A0AB0BAA=BBA=B

Proof

Step Hyp Ref Expression
1 le2msq A0AB0BABAABB
2 le2msq B0BA0ABABBAA
3 2 ancoms A0AB0BBABBAA
4 1 3 anbi12d A0AB0BABBAAABBBBAA
5 simpll A0AB0BA
6 simprl A0AB0BB
7 5 6 letri3d A0AB0BA=BABBA
8 5 5 remulcld A0AB0BAA
9 6 6 remulcld A0AB0BBB
10 8 9 letri3d A0AB0BAA=BBAABBBBAA
11 4 7 10 3bitr4rd A0AB0BAA=BBA=B