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⁢BC=B⁢AC

Proof

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