Theorem sq11

Description: The square function is one-to-one for nonnegative reals. (Contributed by NM, 8-Apr-2001) (Proof shortened by Mario Carneiro, 28-May-2016)

	Ref	Expression
Assertion	sq11	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A\in ℝ$$
2	1	recnd	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A\in ℂ$$
3		sqval	$$⊢A\in ℂ\to A^2=AA$$
4	2 3	syl	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to A^2=AA$$
5		simpl	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to B\in ℝ$$
6	5	recnd	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to B\in ℂ$$
7		sqval	$$⊢B\in ℂ\to B^2=BB$$
8	6 7	syl	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to B^2=BB$$
9	4 8	eqeqan12d	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(A^2=B^2\leftrightarrow AA=BB\right)$$
10		msq11	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(AA=BB\leftrightarrow A=B\right)$$
11	9 10	bitrd	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(A^2=B^2\leftrightarrow A=B\right)$$