divdivdiv

Description: Division of two ratios. Theorem I.15 of Apostol p. 18. (Contributed by NM, 2-Aug-2004)

		Ref	Expression
	Assertion	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}$

Proof

Step	Hyp	Ref	Expression
1		simprrl	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to D \in ℂ$
2		simprll	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to C \in ℂ$
3		simprlr	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to C \neq 0$
4		divcl	$⊢ (D \in ℂ \land C \in ℂ \land C \neq 0) \to \frac{D}{C} \in ℂ$
5	1 2 3 4	syl3anc	$⊢ ((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{D}{C} \in ℂ$
6		simpll	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to A \in ℂ$
7		simplrl	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to B \in ℂ$
8		simplrr	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to B \neq 0$
9		divcl	$⊢ (A \in ℂ \land B \in ℂ \land B \neq 0) \to \frac{A}{B} \in ℂ$
10	6 7 8 9	syl3anc	$⊢ ((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{A}{B} \in ℂ$
11	5 10	mulcomd	$⊢ ((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{D}{C}) (\frac{A}{B}) = (\frac{A}{B}) (\frac{D}{C})$
12		simplr	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (B \in ℂ \land B \neq 0)$
13		simprl	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (C \in ℂ \land C \neq 0)$
14		divmuldiv	$⊢ ((A \in ℂ \land D \in ℂ) \land ((B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0))) \to (\frac{A}{B}) (\frac{D}{C}) = \frac{A D}{B C}$
15	6 1 12 13 14	syl22anc	$⊢ ((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{A}{B}) (\frac{D}{C}) = \frac{A D}{B C}$
16	11 15	eqtrd	$⊢ ((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{D}{C}) (\frac{A}{B}) = \frac{A D}{B C}$
17	16	oveq2d	$⊢ ((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{C}{D}) (\frac{D}{C}) (\frac{A}{B}) = (\frac{C}{D}) (\frac{A D}{B C})$
18		simprr	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (D \in ℂ \land D \neq 0)$
19		divmuldiv	$⊢ ((C \in ℂ \land D \in ℂ) \land ((D \in ℂ \land D \neq 0) \land (C \in ℂ \land C \neq 0))) \to (\frac{C}{D}) (\frac{D}{C}) = \frac{C D}{D C}$
20	2 1 18 13 19	syl22anc	$⊢ ((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{C}{D}) (\frac{D}{C}) = \frac{C D}{D C}$
21	2 1	mulcomd	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to C D = D C$
22	21	oveq1d	$⊢ ((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{C D}{D C} = \frac{D C}{D C}$
23	1 2	mulcld	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to D C \in ℂ$
24		simprrr	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to D \neq 0$
25	1 2 24 3	mulne0d	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to D C \neq 0$
26		divid	$⊢ (D C \in ℂ \land D C \neq 0) \to \frac{D C}{D C} = 1$
27	23 25 26	syl2anc	$⊢ ((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{D C}{D C} = 1$
28	22 27	eqtrd	$⊢ ((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{C D}{D C} = 1$
29	20 28	eqtrd	$⊢ ((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{C}{D}) (\frac{D}{C}) = 1$
30	29	oveq1d	$⊢ ((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{C}{D}) (\frac{D}{C}) (\frac{A}{B}) = 1 (\frac{A}{B})$
31		divcl	$⊢ (C \in ℂ \land D \in ℂ \land D \neq 0) \to \frac{C}{D} \in ℂ$
32	2 1 24 31	syl3anc	$⊢ ((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{C}{D} \in ℂ$
33	32 5 10	mulassd	$⊢ ((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{C}{D}) (\frac{D}{C}) (\frac{A}{B}) = (\frac{C}{D}) (\frac{D}{C}) (\frac{A}{B})$
34	10	mullidd	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to 1 (\frac{A}{B}) = \frac{A}{B}$
35	30 33 34	3eqtr3d	$⊢ ((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{C}{D}) (\frac{D}{C}) (\frac{A}{B}) = \frac{A}{B}$
36	17 35	eqtr3d	$⊢ ((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{C}{D}) (\frac{A D}{B C}) = \frac{A}{B}$
37	6 1	mulcld	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to A D \in ℂ$
38	7 2	mulcld	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to B C \in ℂ$
39		mulne0	$⊢ ((B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0)) \to B C \neq 0$
40	39	ad2ant2lr	$⊢ ((A \in ℂ \land (B \in ℂ \land B \neq 0)) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to B C \neq 0$
41		divcl	$⊢ (A D \in ℂ \land B C \in ℂ \land B C \neq 0) \to \frac{A D}{B C} \in ℂ$
42	37 38 40 41	syl3anc	$⊢ ((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{A D}{B C} \in ℂ$
43		divne0	$⊢ ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0)) \to \frac{C}{D} \neq 0$
44	43	adantl	$⊢ ((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{C}{D} \neq 0$
45		divmul	$⊢ (\frac{A}{B} \in ℂ \land \frac{A D}{B C} \in ℂ \land (\frac{C}{D} \in ℂ \land \frac{C}{D} \neq 0)) \to (\frac{\frac{A}{B}}{\frac{C}{D}} = \frac{A D}{B C} \leftrightarrow (\frac{C}{D}) (\frac{A D}{B C}) = \frac{A}{B})$
46	10 42 32 44 45	syl112anc	$⊢ ((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} \leftrightarrow (\frac{C}{D}) (\frac{A D}{B C}) = \frac{A}{B})$
47	36 46	mpbird	$⊢ ((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}$

Metamath Proof Explorer

Theorem divdivdiv

Proof