This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divass

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

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

Proof

Step Hyp Ref Expression
1 reccl ⊢ C ∈ ℂ ∧ C ≠ 0 → 1 C ∈ ℂ
2 mulass ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ 1 C ∈ ℂ → A ⁢ B ⁢ 1 C = A ⁢ B ⁢ 1 C
3 1 2 syl3an3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B ⁢ 1 C = A ⁢ B ⁢ 1 C
4 mulcl ⊢ A ∈ ℂ ∧ B ∈ ℂ → A ⁢ B ∈ ℂ
5 4 3adant3 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B ∈ ℂ
6 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
7 simp3r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ≠ 0
8 divrec ⊢ A ⁢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = A ⁢ B ⁢ 1 C
9 5 6 7 8 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = A ⁢ B ⁢ 1 C
10 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
11 divrec ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C = B ⁢ 1 C
12 10 6 7 11 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C = B ⁢ 1 C
13 12 oveq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = A ⁢ B ⁢ 1 C
14 3 9 13 3eqtr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ⁢ B C = A ⁢ B C