# 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 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\left(\frac{{A}}{{B}}\right)={A}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}\frac{{A}}{{B}}=\frac{{A}}{{B}}$
2 simp1 ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {A}\in ℂ$
3 divcl ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \frac{{A}}{{B}}\in ℂ$
4 3simpc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left({B}\in ℂ\wedge {B}\ne 0\right)$
5 divmul ${⊢}\left({A}\in ℂ\wedge \frac{{A}}{{B}}\in ℂ\wedge \left({B}\in ℂ\wedge {B}\ne 0\right)\right)\to \left(\frac{{A}}{{B}}=\frac{{A}}{{B}}↔{B}\left(\frac{{A}}{{B}}\right)={A}\right)$
6 2 3 4 5 syl3anc ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to \left(\frac{{A}}{{B}}=\frac{{A}}{{B}}↔{B}\left(\frac{{A}}{{B}}\right)={A}\right)$
7 1 6 mpbii ${⊢}\left({A}\in ℂ\wedge {B}\in ℂ\wedge {B}\ne 0\right)\to {B}\left(\frac{{A}}{{B}}\right)={A}$