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