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	$$⊢\left(A\in ℂ\wedge A\ne 0\right)\to \frac{0}{A}=0$$

Proof

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