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) (Proof shortened by SN, 9-Jul-2025)

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

Proof

Step Hyp Ref Expression
1 divcl ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
2 1 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
3 2 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ∈ ℂ
4 divmul3 ⊢ A ∈ ℂ ∧ B C ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B C ↔ A = B C ⁢ C
5 3 4 syld3an2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B C ↔ A = B C ⁢ C
6 divcan1 ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ⁢ C = B
7 6 3expb ⊢ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ⁢ C = B
8 7 3adant1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → B C ⁢ C = B
9 8 eqeq2d ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A = B C ⁢ C ↔ A = B
10 5 9 bitrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ C ∈ ℂ ∧ C ≠ 0 → A C = B C ↔ A = B