Theorem divmul13d

Description: Swap denominators of two ratios. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	div1d.1	|- ( ph -> A e. CC )
	divcld.2	|- ( ph -> B e. CC )
	divmuld.3	|- ( ph -> C e. CC )
	divmuldivd.4	|- ( ph -> D e. CC )
	divmuldivd.5	|- ( ph -> B =/= 0 )
	divmuldivd.6	|- ( ph -> D =/= 0 )
Assertion	divmul13d	|- ( ph -> ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / D ) ) )

Proof

Step	Hyp	Ref	Expression
1		div1d.1	|- ( ph -> A e. CC )
2		divcld.2	|- ( ph -> B e. CC )
3		divmuld.3	|- ( ph -> C e. CC )
4		divmuldivd.4	|- ( ph -> D e. CC )
5		divmuldivd.5	|- ( ph -> B =/= 0 )
6		divmuldivd.6	|- ( ph -> D =/= 0 )
7	2 5	jca	|- ( ph -> ( B e. CC /\ B =/= 0 ) )
8	4 6	jca	|- ( ph -> ( D e. CC /\ D =/= 0 ) )
9		divmul13	|- ( ( ( A e. CC /\ C e. CC ) /\ ( ( B e. CC /\ B =/= 0 ) /\ ( D e. CC /\ D =/= 0 ) ) ) -> ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / D ) ) )
10	1 3 7 8 9	syl22anc	|- ( ph -> ( ( A / B ) x. ( C / D ) ) = ( ( C / B ) x. ( A / D ) ) )