Metamath Proof Explorer

Theorem mulcan1g

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

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

Proof

Step Hyp Ref Expression
1 mulcl ⊢A∈ℂ∧B∈ℂ→A⁢B∈ℂ
2 1 3adant3 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B∈ℂ
3 mulcl ⊢A∈ℂ∧C∈ℂ→A⁢C∈ℂ
4 3 3adant2 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢C∈ℂ
5 2 4 subeq0ad ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B−A⁢C=0↔A⁢B=A⁢C
6 simp1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A∈ℂ
7 subcl ⊢B∈ℂ∧C∈ℂ→B−C∈ℂ
8 7 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B−C∈ℂ
9 6 8 mul0ord ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B−C=0↔A=0∨B−C=0
10 subdi ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B−C=A⁢B−A⁢C
11 10 eqeq1d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B−C=0↔A⁢B−A⁢C=0
12 subeq0 ⊢B∈ℂ∧C∈ℂ→B−C=0↔B=C
13 12 3adant1 ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→B−C=0↔B=C
14 13 orbi2d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A=0∨B−C=0↔A=0∨B=C
15 9 11 14 3bitr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B−A⁢C=0↔A=0∨B=C
16 5 15 bitr3d ⊢A∈ℂ∧B∈ℂ∧C∈ℂ→A⁢B=A⁢C↔A=0∨B=C