Metamath Proof Explorer

Theorem divmulass

Description: An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 simpl1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ∈ ℂ
2 simpl2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → B ∈ ℂ
3 simpr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → D ∈ ℂ ∧ D ≠ 0
4 divass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B D = A ⁢ B D
5 1 2 3 4 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B D = A ⁢ B D
6 5 eqcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B D = A ⁢ B D
7 6 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B D ⁢ C = A ⁢ B D ⁢ C
8 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
9 8 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ B ∈ ℂ
10 9 adantr ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B ∈ ℂ
11 simpl3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → C ∈ ℂ
12 div32 ⊢ A ⁢ B ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 ∧ C ∈ ℂ → A ⁢ B D ⁢ C = A ⁢ B ⁢ C D
13 10 3 11 12 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B D ⁢ C = A ⁢ B ⁢ C D
14 7 13 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ D ∈ ℂ ∧ D ≠ 0 → A ⁢ B D ⁢ C = A ⁢ B ⁢ C D