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

Metamath Proof Explorer

Theorem div0OLD

Description: Obsolete version of div0 as of 9-Jul-2025. (Contributed by NM, 14-Mar-2005) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (A \in ℂ \land A \neq 0) \to A \in ℂ$
2	1	mul01d	$⊢ (A \in ℂ \land A \neq 0) \to A \cdot 0 = 0$
3		0cn	$⊢ 0 \in ℂ$
4		divmul	$⊢ (0 \in ℂ \land 0 \in ℂ \land (A \in ℂ \land A \neq 0)) \to (\frac{0}{A} = 0 \leftrightarrow A \cdot 0 = 0)$
5	3 3 4	mp3an12	$⊢ (A \in ℂ \land A \neq 0) \to (\frac{0}{A} = 0 \leftrightarrow A \cdot 0 = 0)$
6	2 5	mpbird	$⊢ (A \in ℂ \land A \neq 0) \to \frac{0}{A} = 0$