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

Metamath Proof Explorer

Theorem msq0d

Description: A number is zero iff its square is zero (where square is represented using multiplication). (Contributed by Mario Carneiro, 27-May-2016)

		Ref	Expression
	Hypothesis	msq0d.1	$⊢ φ \to A \in ℂ$
	Assertion	msq0d	$⊢ φ \to (A A = 0 \leftrightarrow A = 0)$

Proof

Step	Hyp	Ref	Expression
1		msq0d.1	$⊢ φ \to A \in ℂ$
2	1 1	mul0ord	$⊢ φ \to (A A = 0 \leftrightarrow (A = 0 \lor A = 0))$
3		oridm	$⊢ (A = 0 \lor A = 0) \leftrightarrow A = 0$
4	2 3	bitrdi	$⊢ φ \to (A A = 0 \leftrightarrow A = 0)$