Metamath Proof Explorer

Theorem divmul3

Description: Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 divmul2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B ↔ A = C ⁢ B
2 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
3 2 adantrr ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ⁢ C = C ⁢ B
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ⁢ C = C ⁢ B
5 4 eqeq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A = B ⁢ C ↔ A = C ⁢ B
6 1 5 bitr4d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B ↔ A = B ⁢ C