Metamath Proof Explorer

Theorem div23

Description: A commutative/associative law for division. (Contributed by NM, 2-Aug-2004)

Ref Expression
Assertion div23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = A C ⁢ B

Proof

Step Hyp Ref Expression
1 mulcom ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B = B ⁢ A
2 1 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B C = B ⁢ A C
3 2 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = B ⁢ A C
4 divass ⊢ B ∈ ℂ ∧ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ⁢ A C = B ⁢ A C
5 4 3com12 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ⁢ A C = B ⁢ A C
6 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
7 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
8 7 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
9 8 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
10 6 9 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ⁢ A C = A C ⁢ B
11 3 5 10 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = A C ⁢ B