Metamath Proof Explorer

Theorem divcan1

Description: A cancellation law for division. (Contributed by NM, 5-Jun-2004) (Revised by Mario Carneiro, 27-May-2016)

Ref Expression
Assertion divcan1 
|- ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A )

Proof

Step Hyp Ref Expression
1 divcl 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( A / B ) e. CC )
2 simp2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> B e. CC )
3 1 2 mulcomd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = ( B x. ( A / B ) ) )
4 divcan2 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( B x. ( A / B ) ) = A )
5 3 4 eqtrd 
 |-  ( ( A e. CC /\ B e. CC /\ B =/= 0 ) -> ( ( A / B ) x. B ) = A )