Theorem divmul13i

Description: Swap denominators of two ratios. (Contributed by NM, 6-Aug-1999)

	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	divmul13i	|- ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / 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	3 1	mulcomi	|- ( C x. A ) = ( A x. C )
8	7	oveq1i	|- ( ( C x. A ) / ( B x. D ) ) = ( ( A x. C ) / ( B x. D ) )
9	3 2 1 4 5 6	divmuldivi	|- ( ( C / B ) x. ( A / D ) ) = ( ( C x. A ) / ( B x. D ) )
10	1 2 3 4 5 6	divmuldivi	|- ( ( A / B ) x. ( C / D ) ) = ( ( A x. C ) / ( B x. D ) )
11	8 9 10	3eqtr4ri	|- ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / D ) )