Theorem sqrtsq2

Description: Relationship between square root and squares. (Contributed by NM, 31-Jul-1999) (Revised by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	sqrtsq2	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(\sqrt{A}=B\leftrightarrow A=B^2\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		sq11	$$⊢\left(\left(\sqrt{A}\in ℝ\wedge 0\le \sqrt{A}\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left({\sqrt{A}}^2=B^2\leftrightarrow \sqrt{A}=B\right)$$
5	3 4	sylan	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left({\sqrt{A}}^2=B^2\leftrightarrow \sqrt{A}=B\right)$$
6		resqrtth	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to {\sqrt{A}}^2=A$$
7	6	adantr	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to {\sqrt{A}}^2=A$$
8	7	eqeq1d	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left({\sqrt{A}}^2=B^2\leftrightarrow A=B^2\right)$$
9	5 8	bitr3d	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(B\in ℝ\wedge 0\le B\right)\right)\to \left(\sqrt{A}=B\leftrightarrow A=B^2\right)$$