Theorem divcan2

Description: A cancellation law for division. (Contributed by NM, 3-Feb-2004) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\frac{A}{B}=\frac{A}{B}$$
2		simp1	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to A\in ℂ$$
3		divcl	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \frac{A}{B}\in ℂ$$
4		3simpc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(B\in ℂ\wedge B\ne 0\right)$$
5		divmul	$$⊢\left(A\in ℂ\wedge \frac{A}{B}\in ℂ\wedge \left(B\in ℂ\wedge B\ne 0\right)\right)\to \left(\frac{A}{B}=\frac{A}{B}\leftrightarrow B\left(\frac{A}{B}\right)=A\right)$$
6	2 3 4 5	syl3anc	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to \left(\frac{A}{B}=\frac{A}{B}\leftrightarrow B\left(\frac{A}{B}\right)=A\right)$$
7	1 6	mpbii	$$⊢\left(A\in ℂ\wedge B\in ℂ\wedge B\ne 0\right)\to B\left(\frac{A}{B}\right)=A$$