divdivdivd

Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (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$
	divdivdivd.7	$⊢ φ \to C \neq 0$
Assertion	divdivdivd	$⊢ φ \to \frac{\frac{A}{B}}{\frac{C}{D}} = \frac{A D}{B C}$

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		divdivdivd.7	$⊢ φ \to C \neq 0$
8	2 5	jca	$⊢ φ \to (B \in ℂ \land B \neq 0)$
9	3 7	jca	$⊢ φ \to (C \in ℂ \land C \neq 0)$
10	4 6	jca	$⊢ φ \to (D \in ℂ \land D \neq 0)$
11		divdivdiv	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to \frac{\frac{A}{B}}{\frac{C}{D}} = \frac{A D}{B C}$
12	1 8 9 10 11	syl22anc	$⊢ φ \to \frac{\frac{A}{B}}{\frac{C}{D}} = \frac{A D}{B C}$

Metamath Proof Explorer