divmul13i

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

Step	Hyp	Ref	Expression
1		divclz.1	$⊢ A \in ℂ$
2		divclz.2	$⊢ B \in ℂ$
3		divmulz.3	$⊢ C \in ℂ$
4		divmuldiv.4	$⊢ D \in ℂ$
5		divmuldiv.5	$⊢ B \neq 0$
6		divmuldiv.6	$⊢ D \neq 0$
7	3 1	mulcomi	$⊢ C A = A C$
8	7	oveq1i	$⊢ \frac{C A}{B D} = \frac{A C}{B D}$
9	3 2 1 4 5 6	divmuldivi	$⊢ (\frac{C}{B}) (\frac{A}{D}) = \frac{C A}{B D}$
10	1 2 3 4 5 6	divmuldivi	$⊢ (\frac{A}{B}) (\frac{C}{D}) = \frac{A C}{B D}$
11	8 9 10	3eqtr4ri	$⊢ (\frac{A}{B}) (\frac{C}{D}) = (\frac{C}{B}) (\frac{A}{D})$

Metamath Proof Explorer