Theorem sqeq0

Description: A complex number is zero iff its square is zero. (Contributed by NM, 11-Mar-2006)

	Ref	Expression
Assertion	sqeq0	$$⊢A\in ℂ\to \left(A^2=0\leftrightarrow A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		2nn	$$⊢2\in \mathbb{N}$$
2		expeq0	$$⊢\left(A\in ℂ\wedge 2\in \mathbb{N}\right)\to \left(A^2=0\leftrightarrow A=0\right)$$
3	1 2	mpan2	$$⊢A\in ℂ\to \left(A^2=0\leftrightarrow A=0\right)$$