Metamath Proof Explorer

Theorem div11

Description: One-to-one relationship for division. (Contributed by NM, 20-Apr-2006) (Proof shortened by Mario Carneiro, 27-May-2016)

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

Proof

Step Hyp Ref Expression
1 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A ∈ ℂ
2 simp3l ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ∈ ℂ
3 simp3r ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ≠ 0
4 divcl ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
5 1 2 3 4 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C ∈ ℂ
6 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B ∈ ℂ
7 divcl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
8 6 2 3 7 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
9 5 8 2 3 mulcand ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = C ⁢ B C ↔ A C = B C
10 divcan2 ⊢ A ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = A
11 1 2 3 10 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = A
12 divcan2 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = B
13 6 2 3 12 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ B C = B
14 11 13 eqeq12d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → C ⁢ A C = C ⁢ B C ↔ A = B
15 9 14 bitr3d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B C ↔ A = B