Theorem cnsqrt00

Description: A square root of a complex number is zero iff its argument is 0. Version of sqrt00 for complex numbers. (Contributed by AV, 26-Jan-2023)

	Ref	Expression
Assertion	cnsqrt00	$$⊢A\in ℂ\to \left(\sqrt{A}=0\leftrightarrow A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢\sqrt{A}=0\to {\sqrt{A}}^2=0^2$$
2		sqrtth	$$⊢A\in ℂ\to {\sqrt{A}}^2=A$$
3		sq0	$$⊢0^2=0$$
4	3	a1i	$$⊢A\in ℂ\to 0^2=0$$
5	2 4	eqeq12d	$$⊢A\in ℂ\to \left({\sqrt{A}}^2=0^2\leftrightarrow A=0\right)$$
6	1 5	imbitrid	$$⊢A\in ℂ\to \left(\sqrt{A}=0\to A=0\right)$$
7		fveq2	$$⊢A=0\to \sqrt{A}=\sqrt{0}$$
8		sqrt0	$$⊢\sqrt{0}=0$$
9	7 8	eqtrdi	$$⊢A=0\to \sqrt{A}=0$$
10	6 9	impbid1	$$⊢A\in ℂ\to \left(\sqrt{A}=0\leftrightarrow A=0\right)$$