# Metamath Proof Explorer

## 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}}{{A}{B}}=\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 {A}{B}\in ℂ$
6 1 2 3 4 mulne0d ${⊢}{\phi }\to {A}{B}\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{{A}{B}}{{B}}}=\frac{{B}}{{A}{B}}$
9 8 eqcomd ${⊢}{\phi }\to \frac{{B}}{{A}{B}}=\frac{\frac{{B}}{{B}}}{\frac{{A}{B}}{{B}}}$
10 2 4 dividd ${⊢}{\phi }\to \frac{{B}}{{B}}=1$
11 1 2 4 divcan4d ${⊢}{\phi }\to \frac{{A}{B}}{{B}}={A}$
12 10 11 oveq12d ${⊢}{\phi }\to \frac{\frac{{B}}{{B}}}{\frac{{A}{B}}{{B}}}=\frac{1}{{A}}$
13 eqidd ${⊢}{\phi }\to \frac{1}{{A}}=\frac{1}{{A}}$
14 9 12 13 3eqtrd ${⊢}{\phi }\to \frac{{B}}{{A}{B}}=\frac{1}{{A}}$