# Metamath Proof Explorer

## Theorem div12

Description: A commutative/associative law for division. (Contributed by NM, 30-Apr-2005)

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

### Proof

Step Hyp Ref Expression
1 divcl ${⊢}\left({B}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{B}}{{C}}\in ℂ$
2 1 3expb ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{B}}{{C}}\in ℂ$
3 mulcom ${⊢}\left({A}\in ℂ\wedge \frac{{B}}{{C}}\in ℂ\right)\to {A}\left(\frac{{B}}{{C}}\right)=\left(\frac{{B}}{{C}}\right){A}$
4 2 3 sylan2 ${⊢}\left({A}\in ℂ\wedge \left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\right)\to {A}\left(\frac{{B}}{{C}}\right)=\left(\frac{{B}}{{C}}\right){A}$
5 4 3impb ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to {A}\left(\frac{{B}}{{C}}\right)=\left(\frac{{B}}{{C}}\right){A}$
6 div13 ${⊢}\left({B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\wedge {A}\in ℂ\right)\to \left(\frac{{B}}{{C}}\right){A}=\left(\frac{{A}}{{C}}\right){B}$
7 6 3comr ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \left(\frac{{B}}{{C}}\right){A}=\left(\frac{{A}}{{C}}\right){B}$
8 divcl ${⊢}\left({A}\in ℂ\wedge {C}\in ℂ\wedge {C}\ne 0\right)\to \frac{{A}}{{C}}\in ℂ$
9 8 3expb ${⊢}\left({A}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \frac{{A}}{{C}}\in ℂ$
10 mulcom ${⊢}\left(\frac{{A}}{{C}}\in ℂ\wedge {B}\in ℂ\right)\to \left(\frac{{A}}{{C}}\right){B}={B}\left(\frac{{A}}{{C}}\right)$
11 9 10 stoic3 ${⊢}\left({A}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\wedge {B}\in ℂ\right)\to \left(\frac{{A}}{{C}}\right){B}={B}\left(\frac{{A}}{{C}}\right)$
12 11 3com23 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to \left(\frac{{A}}{{C}}\right){B}={B}\left(\frac{{A}}{{C}}\right)$
13 5 7 12 3eqtrd ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge \left({C}\in ℂ\wedge {C}\ne 0\right)\right)\to {A}\left(\frac{{B}}{{C}}\right)={B}\left(\frac{{A}}{{C}}\right)$