Metamath Proof Explorer

Theorem divcan1

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

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

Proof

Step Hyp Ref Expression
1 divcl ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ∈ ℂ
2 simp2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ∈ ℂ
3 1 2 mulcomd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ B = B ⁢ A B
4 divcan2 ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → B ⁢ A B = A
5 3 4 eqtrd ⊢ A ∈ ℂ ∧ B ∈ ℂ ∧ B ≠ 0 → A B ⁢ B = A