Theorem sqrt00

Description: A square root is zero iff its argument is 0. (Contributed by NM, 27-Jul-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		sqrt0	$$⊢\sqrt{0}=0$$
2	1	eqeq2i	$$⊢\sqrt{A}=\sqrt{0}\leftrightarrow \sqrt{A}=0$$
3		0re	$$⊢0\in ℝ$$
4		0le0	$$⊢0\le 0$$
5		sqrt11	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge \left(0\in ℝ\wedge 0\le 0\right)\right)\to \left(\sqrt{A}=\sqrt{0}\leftrightarrow A=0\right)$$
6	3 4 5	mpanr12	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left(\sqrt{A}=\sqrt{0}\leftrightarrow A=0\right)$$
7	2 6	bitr3id	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to \left(\sqrt{A}=0\leftrightarrow A=0\right)$$