This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ∈ ℂ
mulcan.2 ⊢ 𝐵 ∈ ℂ
mulcan.3 ⊢ 𝐶 ∈ ℂ
mulcan.4 ⊢ 𝐶 ≠ 0
Assertion mulcani ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 mulcan.1 ⊢ 𝐴 ∈ ℂ
2 mulcan.2 ⊢ 𝐵 ∈ ℂ
3 mulcan.3 ⊢ 𝐶 ∈ ℂ
4 mulcan.4 ⊢ 𝐶 ≠ 0
5 3 4 pm3.2i ⊢ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 )
6 mulcan ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ 𝐴 = 𝐵 ) )
7 1 2 5 6 mp3an ⊢ ( ( 𝐶 · 𝐴 ) = ( 𝐶 · 𝐵 ) ↔ 𝐴 = 𝐵 )