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

Metamath Proof Explorer

Theorem divcan3

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

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

Proof

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