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\in ℝ$$
	lt2sq.2	$$⊢B\in ℝ$$
Assertion	sq11i	$$⊢\left(0\le A\wedge 0\le B\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		resqcl.1	$$⊢A\in ℝ$$
2		lt2sq.2	$$⊢B\in ℝ$$
3	1	recni	$$⊢A\in ℂ$$
4	3	sqvali	$$⊢A^2=AA$$
5	2	recni	$$⊢B\in ℂ$$
6	5	sqvali	$$⊢B^2=BB$$
7	4 6	eqeq12i	$$⊢A^2=B^2\leftrightarrow AA=BB$$
8	1 2	msq11i	$$⊢\left(0\le A\wedge 0\le B\right)\to \left(AA=BB\leftrightarrow A=B\right)$$
9	7 8	bitrid	$$⊢\left(0\le A\wedge 0\le B\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$