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

Metamath Proof Explorer

Theorem div0

Description: Division into zero is zero. (Contributed by NM, 14-Mar-2005) (Proof shortened by SN, 9-Jul-2025)

		Ref	Expression
	Assertion	div0	$⊢ (A \in ℂ \land A \neq 0) \to \frac{0}{A} = 0$

Step	Hyp	Ref	Expression
1		0cn	$⊢ 0 \in ℂ$
2		eqid	$⊢ 0 = 0$
3		diveq0	$⊢ (0 \in ℂ \land A \in ℂ \land A \neq 0) \to (\frac{0}{A} = 0 \leftrightarrow 0 = 0)$
4	2 3	mpbiri	$⊢ (0 \in ℂ \land A \in ℂ \land A \neq 0) \to \frac{0}{A} = 0$
5	1 4	mp3an1	$⊢ (A \in ℂ \land A \neq 0) \to \frac{0}{A} = 0$