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

Metamath Proof Explorer

Theorem mulcan2d

Description: Cancellation law for multiplication. Theorem I.7 of Apostol p. 18. (Contributed by Mario Carneiro, 27-May-2016)

Ref Expression
Hypotheses mulcand.1 ⊢ φ → A ∈ ℂ
mulcand.2 ⊢ φ → B ∈ ℂ
mulcand.3 ⊢ φ → C ∈ ℂ
mulcand.4 ⊢ φ → C ≠ 0
Assertion mulcan2d ⊢ φ → A ⁢ C = B ⁢ C ↔ A = B

Proof

Step Hyp Ref Expression
1 mulcand.1 ⊢ φ → A ∈ ℂ
2 mulcand.2 ⊢ φ → B ∈ ℂ
3 mulcand.3 ⊢ φ → C ∈ ℂ
4 mulcand.4 ⊢ φ → C ≠ 0
5 1 3 mulcomd ⊢ φ → A ⁢ C = C ⁢ A
6 2 3 mulcomd ⊢ φ → B ⁢ C = C ⁢ B
7 5 6 eqeq12d ⊢ φ → A ⁢ C = B ⁢ C ↔ C ⁢ A = C ⁢ B
8 1 2 3 4 mulcand ⊢ φ → C ⁢ A = C ⁢ B ↔ A = B
9 7 8 bitrd ⊢ φ → A ⁢ C = B ⁢ C ↔ A = B