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

Metamath Proof Explorer

Theorem div11i

Description: One-to-one relationship for division. (Contributed by NM, 20-Aug-2001)

Ref Expression
Hypotheses divclz.1 ⊢ A ∈ ℂ
divclz.2 ⊢ B ∈ ℂ
divmulz.3 ⊢ C ∈ ℂ
divass.4 ⊢ C ≠ 0
Assertion div11i ⊢ A C = B C ↔ A = B

Proof

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