Theorem divdivdivi

Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (Contributed by NM, 22-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
	divdivdiv.7	|- C =/= 0
Assertion	divdivdivi	|- ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) )

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		divdivdiv.7	|- C =/= 0
8	2 5	pm3.2i	|- ( B e. CC /\ B =/= 0 )
9	3 7	pm3.2i	|- ( C e. CC /\ C =/= 0 )
10	4 6	pm3.2i	|- ( D e. CC /\ D =/= 0 )
11		divdivdiv	|- ( ( ( A e. CC /\ ( B e. CC /\ B =/= 0 ) ) /\ ( ( C e. CC /\ C =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) ) )
12	1 8 9 10 11	mp4an	|- ( ( A / B ) / ( C / D ) ) = ( ( A x. D ) / ( B x. C ) )