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

Proof

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