Theorem divcan8d

Description: A cancellation law for division. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	divcan8d.a	$$⊢\phi \to A\in ℂ$$
	divcan8d.b	$$⊢\phi \to B\in ℂ$$
	divcan8d.a0	$$⊢\phi \to A\ne 0$$
	divcan8d.b0	$$⊢\phi \to B\ne 0$$
Assertion	divcan8d	$$⊢\phi \to \frac{B}{AB}=\frac{1}{A}$$

Proof

Step	Hyp	Ref	Expression
1		divcan8d.a	$$⊢\phi \to A\in ℂ$$
2		divcan8d.b	$$⊢\phi \to B\in ℂ$$
3		divcan8d.a0	$$⊢\phi \to A\ne 0$$
4		divcan8d.b0	$$⊢\phi \to B\ne 0$$
5	1 2	mulcld	$$⊢\phi \to AB\in ℂ$$
6	1 2 3 4	mulne0d	$$⊢\phi \to AB\ne 0$$
7	1 2 6	mulne0bbd	$$⊢\phi \to B\ne 0$$
8	2 5 2 6 7	divcan7d	$$⊢\phi \to \frac{\frac{B}{B}}{\frac{AB}{B}}=\frac{B}{AB}$$
9	8	eqcomd	$$⊢\phi \to \frac{B}{AB}=\frac{\frac{B}{B}}{\frac{AB}{B}}$$
10	2 4	dividd	$$⊢\phi \to \frac{B}{B}=1$$
11	1 2 4	divcan4d	$$⊢\phi \to \frac{AB}{B}=A$$
12	10 11	oveq12d	$$⊢\phi \to \frac{\frac{B}{B}}{\frac{AB}{B}}=\frac{1}{A}$$
13		eqidd	$$⊢\phi \to \frac{1}{A}=\frac{1}{A}$$
14	9 12 13	3eqtrd	$$⊢\phi \to \frac{B}{AB}=\frac{1}{A}$$