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 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A B ⁢ C A = C B

Proof

Step Hyp Ref Expression
1 simp1l ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A ∈ ℂ
2 simp3 ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → C ∈ ℂ
3 simp1r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A ≠ 0
4 divcl ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → C A ∈ ℂ
5 2 1 3 4 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → C A ∈ ℂ
6 simp2l ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → B ∈ ℂ
7 simp2r ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → B ≠ 0
8 div23 ⊢ A ∈ ℂ ∧ C A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ⁢ C A B = A B ⁢ C A
9 1 5 6 7 8 syl112anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A ⁢ C A B = A B ⁢ C A
10 divcan2 ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ A ≠ 0 → A ⁢ C A = C
11 2 1 3 10 syl3anc ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A ⁢ C A = C
12 11 oveq1d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A ⁢ C A B = C B
13 9 12 eqtr3d ⊢ A ∈ ℂ ∧ A ≠ 0 ∧ B ∈ ℂ ∧ B ≠ 0 ∧ C ∈ ℂ → A B ⁢ C A = C B