Theorem sqrt11

Description: The square root function is one-to-one. (Contributed by Scott Fenton, 11-Jun-2013)

	Ref	Expression
Assertion	sqrt11	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(\sqrt{A}=\sqrt{B}\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		resqrtcl	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \sqrt{A}\in ℝ$$
2		sqrtge0	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to 0\le \sqrt{A}$$
3	1 2	jca	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left(\sqrt{A}\in ℝ\wedge 0\le \sqrt{A}\right)$$
4		resqrtcl	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to \sqrt{B}\in ℝ$$
5		sqrtge0	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to 0\le \sqrt{B}$$
6	4 5	jca	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to \left(\sqrt{B}\in ℝ\wedge 0\le \sqrt{B}\right)$$
7		sq11	$$⊢\left(\left(\sqrt{A}\in ℝ\wedge 0\le \sqrt{A}\right)\wedge \left(\sqrt{B}\in ℝ\wedge 0\le \sqrt{B}\right)\right)\to \left({\sqrt{A}}^2={\sqrt{B}}^2\leftrightarrow \sqrt{A}=\sqrt{B}\right)$$
8	3 6 7	syl2an	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left({\sqrt{A}}^2={\sqrt{B}}^2\leftrightarrow \sqrt{A}=\sqrt{B}\right)$$
9		resqrtth	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to {\sqrt{A}}^2=A$$
10		resqrtth	$$⊢\left(B\in ℝ\wedge 0\le B\right)\to {\sqrt{B}}^2=B$$
11	9 10	eqeqan12d	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left({\sqrt{A}}^2={\sqrt{B}}^2\leftrightarrow A=B\right)$$
12	8 11	bitr3d	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(\sqrt{A}=\sqrt{B}\leftrightarrow A=B\right)$$