Metamath Proof Explorer

Theorem divcan2

Description: A cancellation law for division. (Contributed by NM, 3-Feb-2004) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion divcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A B = A

Proof

Step Hyp Ref Expression
1 eqid ⊢ A B = A B
2 simp1 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A ∈ ℂ
3 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
4 3simpc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ ∧ B ≠ 0
5 divmul ⊢ A ∈ ℂ ∧ A B ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A B ↔ B ⁢ A B = A
6 2 3 4 5 syl3anc ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B = A B ↔ B ⁢ A B = A
7 1 6 mpbii ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A B = A