This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqeq0i

Description: A complex number is zero iff its square is zero. (Contributed by NM, 2-Oct-1999)

		Ref	Expression
	Hypothesis	sqval.1	$⊢ A \in ℂ$
	Assertion	sqeq0i	$⊢ A^{2} = 0 \leftrightarrow A = 0$

Step	Hyp	Ref	Expression
1		sqval.1	$⊢ A \in ℂ$
2		sqeq0	$⊢ A \in ℂ \to (A^{2} = 0 \leftrightarrow A = 0)$
3	1 2	ax-mp	$⊢ A^{2} = 0 \leftrightarrow A = 0$