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 \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{B A}{B} = A$

Step	Hyp	Ref	Expression
1		eqid	$⊢ B A = B A$
2		simp2	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B \in ℂ$
3		simp1	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to A \in ℂ$
4	2 3	mulcld	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to B A \in ℂ$
5		3simpc	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (B \in ℂ \land B \neq 0)$
6		divmul	$⊢ (B A \in ℂ \land A \in ℂ \land (B \in ℂ \land B \neq 0)) \to (\frac{B A}{B} = A \leftrightarrow B A = B A)$
7	4 3 5 6	syl3anc	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to (\frac{B A}{B} = A \leftrightarrow B A = B A)$
8	1 7	mpbiri	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{B A}{B} = A$

Metamath Proof Explorer