# Metamath Proof Explorer

## Theorem dmdcan

Description: Cancellation law for division and multiplication. (Contributed by Scott Fenton, 7-Jun-2013) (Proof shortened by Fan Zheng, 3-Jul-2016)

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

### Proof

Step Hyp Ref Expression
1 simp1l ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to {A}\in ℂ$
2 simp3 ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to {C}\in ℂ$
3 simp1r ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to {A}\ne 0$
4 divcl ${⊢}\left({C}\in ℂ\wedge {A}\in ℂ\wedge {A}\ne 0\right)\to \frac{{C}}{{A}}\in ℂ$
5 2 1 3 4 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to \frac{{C}}{{A}}\in ℂ$
6 simp2l ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to {B}\in ℂ$
7 simp2r ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to {B}\ne 0$
8 div23 ${⊢}\left({A}\in ℂ\wedge \frac{{C}}{{A}}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \frac{{A}\left(\frac{{C}}{{A}}\right)}{{B}}=\left(\frac{{A}}{{B}}\right)\left(\frac{{C}}{{A}}\right)$
9 1 5 6 7 8 syl112anc ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to \frac{{A}\left(\frac{{C}}{{A}}\right)}{{B}}=\left(\frac{{A}}{{B}}\right)\left(\frac{{C}}{{A}}\right)$
10 divcan2 ${⊢}\left({C}\in ℂ\wedge {A}\in ℂ\wedge {A}\ne 0\right)\to {A}\left(\frac{{C}}{{A}}\right)={C}$
11 2 1 3 10 syl3anc ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to {A}\left(\frac{{C}}{{A}}\right)={C}$
12 11 oveq1d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to \frac{{A}\left(\frac{{C}}{{A}}\right)}{{B}}=\frac{{C}}{{B}}$
13 9 12 eqtr3d ${⊢}\left(\left({A}\in ℂ\wedge {A}\ne 0\right)\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\wedge {C}\in ℂ\right)\to \left(\frac{{A}}{{B}}\right)\left(\frac{{C}}{{A}}\right)=\frac{{C}}{{B}}$