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

Proof

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