Metamath Proof Explorer

Theorem divmul3

Description: Relationship between division and multiplication. (Contributed by NM, 13-Feb-2006)

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

Proof

Step Hyp Ref Expression
1 divmul2 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> A = ( C x. B ) ) )
2 mulcom 
 |-  ( ( B e. CC /\ C e. CC ) -> ( B x. C ) = ( C x. B ) )
3 2 adantrr 
 |-  ( ( B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B x. C ) = ( C x. B ) )
4 3 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( B x. C ) = ( C x. B ) )
5 4 eqeq2d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( A = ( B x. C ) <-> A = ( C x. B ) ) )
6 1 5 bitr4d 
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> A = ( B x. C ) ) )