Metamath Proof Explorer

Theorem div12

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

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

Proof

Step Hyp Ref Expression
1 divcl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
2 1 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
3 mulcom ⊢ A ∈ ℂ ∧ B C ∈ ℂ → A ⁢ B C = B C ⁢ A
4 2 3 sylan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = B C ⁢ A
5 4 3impb ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = B C ⁢ A
6 div13 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ A ∈ ℂ → B C ⁢ A = A C ⁢ B
7 6 3comr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ⁢ A = A C ⁢ B
8 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
9 8 3expb ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
10 mulcom ⊢ A C ∈ ℂ ∧ B ∈ ℂ → A C ⁢ B = B ⁢ A C
11 9 10 stoic3 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 ∧ B ∈ ℂ → A C ⁢ B = B ⁢ A C
12 11 3com23 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ⁢ B = B ⁢ A C
13 5 7 12 3eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = B ⁢ A C