Metamath Proof Explorer

Theorem divmul2

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

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

Proof

Step Hyp Ref Expression
1 divmul ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B ↔ C ⁢ B = A
2 eqcom ⊢ C ⁢ B = A ↔ A = C ⁢ B
3 1 2 bitrdi ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B ↔ A = C ⁢ B