# Metamath Proof Explorer

## Theorem div23

Description: A commutative/associative law for division. (Contributed by NM, 2-Aug-2004)

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

### Proof

Step Hyp Ref Expression
1 mulcom ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to {A}{B}={B}{A}$
2 1 oveq1d ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\right)\to \frac{{A}{B}}{{C}}=\frac{{B}{A}}{{C}}$
3 2 3adant3 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}{B}}{{C}}=\frac{{B}{A}}{{C}}$
4 divass ${⊢}\left({B}\in ℂ\wedge {A}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{B}{A}}{{C}}={B}\left(\frac{{A}}{{C}}\right)$
5 4 3com12 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{B}{A}}{{C}}={B}\left(\frac{{A}}{{C}}\right)$
6 simp2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to {B}\in ℂ$
7 divcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{A}}{{C}}\in ℂ$
8 7 3expb ${⊢}\left({A}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}}{{C}}\in ℂ$
9 8 3adant2 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}}{{C}}\in ℂ$
10 6 9 mulcomd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to {B}\left(\frac{{A}}{{C}}\right)=\left(\frac{{A}}{{C}}\right){B}$
11 3 5 10 3eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}{B}}{{C}}=\left(\frac{{A}}{{C}}\right){B}$