Metamath Proof Explorer

Theorem mulcani

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by NM, 26-Jan-1995)

Ref Expression
Hypotheses mulcan.1 ⊢ A ∈ ℂ
mulcan.2 ⊢ B ∈ ℂ
mulcan.3 ⊢ C ∈ ℂ
mulcan.4 ⊢ C ≠ 0
Assertion mulcani ⊢ C ⁢ A = C ⁢ B ↔ A = B

Proof

Step Hyp Ref Expression
1 mulcan.1 ⊢ A ∈ ℂ
2 mulcan.2 ⊢ B ∈ ℂ
3 mulcan.3 ⊢ C ∈ ℂ
4 mulcan.4 ⊢ C ≠ 0
5 3 4 pm3.2i ⊢ C ∈ ℂ ∧ C ≠ 0
6 mulcan ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A = C ⁢ B ↔ A = B
7 1 2 5 6 mp3an ⊢ C ⁢ A = C ⁢ B ↔ A = B