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

Proof

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