Theorem divmuldivi

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by NM, 16-Feb-1995)

	Ref	Expression
Hypotheses	divclz.1	|- A e. CC
	divclz.2	|- B e. CC
	divmulz.3	|- C e. CC
	divmuldiv.4	|- D e. CC
	divmuldiv.5	|- B =/= 0
	divmuldiv.6	|- D =/= 0
Assertion	divmuldivi	|- ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) )

Proof

Step	Hyp	Ref	Expression
1		divclz.1	|- A e. CC
2		divclz.2	|- B e. CC
3		divmulz.3	|- C e. CC
4		divmuldiv.4	|- D e. CC
5		divmuldiv.5	|- B =/= 0
6		divmuldiv.6	|- D =/= 0
7	2 5	pm3.2i	|- ( B e. CC /\ B =/= 0 )
8	4 6	pm3.2i	|- ( D e. CC /\ D =/= 0 )
9		divmuldiv	|- ( ( ( A e. CC /\ C e. CC ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) ) )
10	1 3 7 8 9	mp4an	|- ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) )