divcan7

Description: Cancel equal divisors in a division. (Contributed by Jeff Hankins, 29-Sep-2013)

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

Step	Hyp	Ref	Expression
1		divdivdiv	$⊢ ((A \in ℂ \land (C \in ℂ \land C \neq 0)) \land ((B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0))) \to \frac{\frac{A}{C}}{\frac{B}{C}} = \frac{A C}{C B}$
2	1	3impdir	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0)) \to \frac{\frac{A}{C}}{\frac{B}{C}} = \frac{A C}{C B}$
3		mulcom	$⊢ (A \in ℂ \land C \in ℂ) \to A C = C A$
4	3	adantrr	$⊢ (A \in ℂ \land (C \in ℂ \land C \neq 0)) \to A C = C A$
5	4	3adant2	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0)) \to A C = C A$
6	5	oveq1d	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0)) \to \frac{A C}{C B} = \frac{C A}{C B}$
7		divcan5	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0)) \to \frac{C A}{C B} = \frac{A}{B}$
8	2 6 7	3eqtrd	$⊢ (A \in ℂ \land (B \in ℂ \land B \neq 0) \land (C \in ℂ \land C \neq 0)) \to \frac{\frac{A}{C}}{\frac{B}{C}} = \frac{A}{B}$

Metamath Proof Explorer