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