Theorem sqeq0d

Description: A number is zero iff its square is zero. (Contributed by Mario Carneiro, 28-May-2016)

	Ref	Expression
Hypotheses	expcld.1	$$⊢\phi \to A\in ℂ$$
	sqeq0d.1	$$⊢\phi \to A^2=0$$
Assertion	sqeq0d	$$⊢\phi \to A=0$$

Proof

Step	Hyp	Ref	Expression
1		expcld.1	$$⊢\phi \to A\in ℂ$$
2		sqeq0d.1	$$⊢\phi \to A^2=0$$
3		2nn	$$⊢2\in \mathbb{N}$$
4	3	a1i	$$⊢\phi \to 2\in \mathbb{N}$$
5	1 4 2	expeq0d	$$⊢\phi \to A=0$$