Metamath Proof Explorer

Theorem div13

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

Ref Expression
Assertion div13 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→AB⁢C=CB⁢A

Proof

Step Hyp Ref Expression
1 mulcom ⊢A∈ℂ∧C∈ℂ→A⁢C=C⁢A
2 1 oveq1d ⊢A∈ℂ∧C∈ℂ→A⁢CB=C⁢AB
3 2 3adant2 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→A⁢CB=C⁢AB
4 div23 ⊢A∈ℂ∧C∈ℂ∧B∈ℂ∧B≠0→A⁢CB=AB⁢C
5 4 3com23 ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→A⁢CB=AB⁢C
6 div23 ⊢C∈ℂ∧A∈ℂ∧B∈ℂ∧B≠0→C⁢AB=CB⁢A
7 6 3coml ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→C⁢AB=CB⁢A
8 3 5 7 3eqtr3d ⊢A∈ℂ∧B∈ℂ∧B≠0∧C∈ℂ→AB⁢C=CB⁢A