Theorem sqeq0d

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

	Ref	Expression
Hypotheses	expcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
	sqeq0d.1	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = 0 )
Assertion	sqeq0d	⊢ ( 𝜑 → 𝐴 = 0 )

Proof

Step	Hyp	Ref	Expression
1		expcld.1	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
2		sqeq0d.1	⊢ ( 𝜑 → ( 𝐴 ↑ 2 ) = 0 )
3		2nn	⊢ 2 ∈ ℕ
4	3	a1i	⊢ ( 𝜑 → 2 ∈ ℕ )
5	1 4 2	expeq0d	⊢ ( 𝜑 → 𝐴 = 0 )