Metamath Proof Explorer


Theorem sq11i

Description: The square function is one-to-one for nonnegative reals. (Contributed by NM, 27-Oct-1999)

Ref Expression
Hypotheses resqcl.1 A
lt2sq.2 B
Assertion sq11i 0A0BA2=B2A=B

Proof

Step Hyp Ref Expression
1 resqcl.1 A
2 lt2sq.2 B
3 1 recni A
4 3 sqvali A2=AA
5 2 recni B
6 5 sqvali B2=BB
7 4 6 eqeq12i A2=B2AA=BB
8 1 2 msq11i 0A0BAA=BBA=B
9 7 8 syl5bb 0A0BA2=B2A=B