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 ) ) )

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 ) ) )

Step

Hyp

Ref

Expression

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

 |-  ( ( C x. B ) = A <-> A = ( C x. B ) )

1 2

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