div23

Description: A commutative/associative law for division. (Contributed by NM, 2-Aug-2004)

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

Step	Hyp	Ref	Expression
1		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
2	1	oveq1d	$⊢ (A \in ℂ \land B \in ℂ) \to \frac{A B}{C} = \frac{B A}{C}$
3	2	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{A B}{C} = \frac{B A}{C}$
4		divass	$⊢ (B \in ℂ \land A \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{B A}{C} = B (\frac{A}{C})$
5	4	3com12	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{B A}{C} = B (\frac{A}{C})$
6		simp2	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to B \in ℂ$
7		divcl	$⊢ (A \in ℂ \land C \in ℂ \land C \neq 0) \to \frac{A}{C} \in ℂ$
8	7	3expb	$⊢ (A \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{A}{C} \in ℂ$
9	8	3adant2	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{A}{C} \in ℂ$
10	6 9	mulcomd	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to B (\frac{A}{C}) = (\frac{A}{C}) B$
11	3 5 10	3eqtrd	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{A B}{C} = (\frac{A}{C}) B$

Metamath Proof Explorer