Metamath Proof Explorer

Theorem mulcan2g

Description: A generalized form of the cancellation law for multiplication. (Contributed by Scott Fenton, 17-Jun-2013)

Ref Expression
Assertion mulcan2g ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = B ⁢ C ↔ A = B ∨ C = 0

Proof

Step Hyp Ref Expression
1 mulcom ⊢ A ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
2 1 3adant2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = C ⁢ A
3 mulcom ⊢ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
4 3 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → B ⁢ C = C ⁢ B
5 2 4 eqeq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = B ⁢ C ↔ C ⁢ A = C ⁢ B
6 mulcan1g ⊢ C ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℂ → C ⁢ A = C ⁢ B ↔ C = 0 ∨ A = B
7 6 3coml ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A = C ⁢ B ↔ C = 0 ∨ A = B
8 orcom ⊢ C = 0 ∨ A = B ↔ A = B ∨ C = 0
9 7 8 bitrdi ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → C ⁢ A = C ⁢ B ↔ A = B ∨ C = 0
10 5 9 bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ → A ⁢ C = B ⁢ C ↔ A = B ∨ C = 0