Metamath Proof Explorer

Theorem mulcan

Description: Cancellation law for multiplication (full theorem form). Theorem I.7 of Apostol p. 18. (Contributed by NM, 29-Jan-1995) (Revised by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
3 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
4 simp3r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ≠ 0
5 1 2 3 4 mulcand ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A = C ⁢ B ↔ A = B