Metamath Proof Explorer


Theorem divmul2

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

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

Proof

Step Hyp Ref Expression
1 divmul
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> ( C x. B ) = A ) )
2 eqcom
 |-  ( ( C x. B ) = A <-> A = ( C x. B ) )
3 1 2 bitrdi
 |-  ( ( A e. CC /\ B e. CC /\ ( C e. CC /\ C =/= 0 ) ) -> ( ( A / C ) = B <-> A = ( C x. B ) ) )