Theorem div32

Description: A commutative/associative law for division. (Contributed by Mario Carneiro, 27-May-2016)

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

Proof

Step	Hyp	Ref	Expression
1		div23	|- ( ( A e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A x. C ) / B ) = ( ( A / B ) x. C ) )
2		divass	|- ( ( A e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A x. C ) / B ) = ( A x. ( C / B ) ) )
3	1 2	eqtr3d	|- ( ( A e. CC /\ C e. CC /\ ( B e. CC /\ B =/= 0 ) ) -> ( ( A / B ) x. C ) = ( A x. ( C / B ) ) )
4	3	3com23	|- ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) /\ C e. CC ) -> ( ( A / B ) x. C ) = ( A x. ( C / B ) ) )