Theorem diveq0

Description: A ratio is zero iff the numerator is zero. (Contributed by NM, 20-Apr-2006) (Revised by Mario Carneiro, 27-May-2016)

	Ref	Expression
Assertion	diveq0	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}=0\leftrightarrow A=0\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to A\in ℂ$$
2		0cnd	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to 0\in ℂ$$
3		3simpc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(B\in ℂ\wedge B\ne 0\right)$$
4		divmul2	$$⊢\left(A\in ℂ\wedge 0\in ℂ\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to \left(\frac{A}{B}=0\leftrightarrow A=B\cdot 0\right)$$
5	1 2 3 4	syl3anc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}=0\leftrightarrow A=B\cdot 0\right)$$
6		simp2	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to B\in ℂ$$
7	6	mul01d	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to B\cdot 0=0$$
8	7	eqeq2d	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(A=B\cdot 0\leftrightarrow A=0\right)$$
9	5 8	bitrd	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}=0\leftrightarrow A=0\right)$$