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 e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( B x. A ) / B ) = A )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( B x. A ) = ( B x. A )
2 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
3 simp1 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> A e. CC )
4 2 3 mulcld 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. A ) e. CC )
5 3simpc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B e. CC /\ B =/= 0 ) )
6 divmul 
 |-  ( ( ( B x. A ) e. CC /\ A e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( ( B x. A ) / B ) = A <-> ( B x. A ) = ( B x. A ) ) )
7 4 3 5 6 syl3anc 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( ( B x. A ) / B ) = A <-> ( B x. A ) = ( B x. A ) ) )
8 1 7 mpbiri 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( B x. A ) / B ) = A )