divmul13

Description: Swap the denominators in the product of two ratios. (Contributed by NM, 3-May-2005)

		Ref	Expression
	Assertion	divmul13	$⊢ ((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{B}{C}) (\frac{A}{D})$

Step	Hyp	Ref	Expression
1		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
2	1	adantr	$⊢ ((A \in ℂ \land B \in ℂ) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to A B = B A$
3	2	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to \frac{A B}{C D} = \frac{B A}{C D}$
4		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}$
5		divmuldiv	$⊢ ((B \in ℂ \land A \in ℂ) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (\frac{B}{C}) (\frac{A}{D}) = \frac{B A}{C D}$
6	5	ancom1s	$⊢ ((A \in ℂ \land B \in ℂ) \land ((C \in ℂ \land C \neq 0) \land (D \in ℂ \land D \neq 0))) \to (\frac{B}{C}) (\frac{A}{D}) = \frac{B A}{C D}$
7	3 4 6	3eqtr4d	$⊢ ((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{B}{C}) (\frac{A}{D})$

Metamath Proof Explorer