divmuldiv

Description: Multiplication of two ratios. Theorem I.14 of Apostol p. 18. (Contributed by NM, 1-Aug-2004)

		Ref	Expression
	Assertion	divmuldiv	$⊢ ((A \in ℂ \land B \in ℂ) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (\frac{A}{C}) (\frac{B}{D}) = \frac{A B}{C D}$

Proof

Step	Hyp	Ref	Expression
1		3anass	$⊢ (A \in ℂ \land C \in ℂ \land C \neq 0) \leftrightarrow (A \in ℂ \land (C \in ℂ \land C \neq 0))$
2		3anass	$⊢ (B \in ℂ \land D \in ℂ \land D \neq 0) \leftrightarrow (B \in ℂ \land (D \in ℂ \land D \neq 0))$
3		divcl	$⊢ (A \in ℂ \land C \in ℂ \land C \neq 0) \to \frac{A}{C} \in ℂ$
4		divcl	$⊢ (B \in ℂ \land D \in ℂ \land D \neq 0) \to \frac{B}{D} \in ℂ$
5		mulcl	$⊢ (\frac{A}{C} \in ℂ \land \frac{B}{D} \in ℂ) \to (\frac{A}{C}) (\frac{B}{D}) \in ℂ$
6	3 4 5	syl2an	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to (\frac{A}{C}) (\frac{B}{D}) \in ℂ$
7		mulcl	$⊢ (C \in ℂ \land D \in ℂ) \to C D \in ℂ$
8	7	ad2ant2r	$⊢ ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0)) \to C D \in ℂ$
9	8	3adantr1	$⊢ ((C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C D \in ℂ$
10	9	3adantl1	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C D \in ℂ$
11		mulne0	$⊢ ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0)) \to C D \neq 0$
12	11	3adantr1	$⊢ ((C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C D \neq 0$
13	12	3adantl1	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C D \neq 0$
14		divcan3	$⊢ ((\frac{A}{C}) (\frac{B}{D}) \in ℂ \land C D \in ℂ \land C D \neq 0) \to \frac{C D (\frac{A}{C}) (\frac{B}{D})}{C D} = (\frac{A}{C}) (\frac{B}{D})$
15	6 10 13 14	syl3anc	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to \frac{C D (\frac{A}{C}) (\frac{B}{D})}{C D} = (\frac{A}{C}) (\frac{B}{D})$
16		simp2	$⊢ (A \in ℂ \land C \in ℂ \land C \neq 0) \to C \in ℂ$
17	16 3	jca	$⊢ (A \in ℂ \land C \in ℂ \land C \neq 0) \to (C \in ℂ \land \frac{A}{C} \in ℂ)$
18		simp2	$⊢ (B \in ℂ \land D \in ℂ \land D \neq 0) \to D \in ℂ$
19	18 4	jca	$⊢ (B \in ℂ \land D \in ℂ \land D \neq 0) \to (D \in ℂ \land \frac{B}{D} \in ℂ)$
20		mul4	$⊢ ((C \in ℂ \land \frac{A}{C} \in ℂ) \land (D \in ℂ \land \frac{B}{D} \in ℂ)) \to C (\frac{A}{C}) D (\frac{B}{D}) = C D (\frac{A}{C}) (\frac{B}{D})$
21	17 19 20	syl2an	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C (\frac{A}{C}) D (\frac{B}{D}) = C D (\frac{A}{C}) (\frac{B}{D})$
22		divcan2	$⊢ (A \in ℂ \land C \in ℂ \land C \neq 0) \to C (\frac{A}{C}) = A$
23		divcan2	$⊢ (B \in ℂ \land D \in ℂ \land D \neq 0) \to D (\frac{B}{D}) = B$
24	22 23	oveqan12d	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C (\frac{A}{C}) D (\frac{B}{D}) = A B$
25	21 24	eqtr3d	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to C D (\frac{A}{C}) (\frac{B}{D}) = A B$
26	25	oveq1d	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to \frac{C D (\frac{A}{C}) (\frac{B}{D})}{C D} = \frac{A B}{C D}$
27	15 26	eqtr3d	$⊢ ((A \in ℂ \land C \in ℂ \land C \neq 0) \land (B \in ℂ \land D \in ℂ \land D \neq 0)) \to (\frac{A}{C}) (\frac{B}{D}) = \frac{A B}{C D}$
28	1 2 27	syl2anbr	$⊢ ((A \in ℂ \land (C \in ℂ \land C \neq 0)) \land (B \in ℂ \land (D \in ℂ \land D \neq 0))) \to (\frac{A}{C}) (\frac{B}{D}) = \frac{A B}{C D}$
29	28	an4s	$⊢ ((A \in ℂ \land B \in ℂ) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (\frac{A}{C}) (\frac{B}{D}) = \frac{A B}{C D}$

Metamath Proof Explorer

Theorem divmuldiv

Proof