divmul24d

Description: Swap the numerators in the product of two ratios. (Contributed by Mario Carneiro, 27-May-2016)

	Ref	Expression
Hypotheses	div1d.1	$⊢ φ \to A \in ℂ$
	divcld.2	$⊢ φ \to B \in ℂ$
	divmuld.3	$⊢ φ \to C \in ℂ$
	divmuldivd.4	$⊢ φ \to D \in ℂ$
	divmuldivd.5	$⊢ φ \to B \neq 0$
	divmuldivd.6	$⊢ φ \to D \neq 0$
Assertion	divmul24d	$⊢ φ \to (\frac{A}{B}) (\frac{C}{D}) = (\frac{A}{D}) (\frac{C}{B})$

Step	Hyp	Ref	Expression
1		div1d.1	$⊢ φ \to A \in ℂ$
2		divcld.2	$⊢ φ \to B \in ℂ$
3		divmuld.3	$⊢ φ \to C \in ℂ$
4		divmuldivd.4	$⊢ φ \to D \in ℂ$
5		divmuldivd.5	$⊢ φ \to B \neq 0$
6		divmuldivd.6	$⊢ φ \to D \neq 0$
7	2 5	jca	$⊢ φ \to (B \in ℂ \land B \neq 0)$
8	4 6	jca	$⊢ φ \to (D \in ℂ \land D \neq 0)$
9		divmul24	$⊢ ((A \in ℂ \land C \in ℂ) \land ((B \in ℂ \land B \neq 0) \land (D \in ℂ \land D \neq 0))) \to (\frac{A}{B}) (\frac{C}{D}) = (\frac{A}{D}) (\frac{C}{B})$
10	1 3 7 8 9	syl22anc	$⊢ φ \to (\frac{A}{B}) (\frac{C}{D}) = (\frac{A}{D}) (\frac{C}{B})$

Metamath Proof Explorer