divass

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

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

Step	Hyp	Ref	Expression
1		reccl	$⊢ (C \in ℂ \land C \neq 0) \to \frac{1}{C} \in ℂ$
2		mulass	$⊢ (A \in ℂ \land B \in ℂ \land \frac{1}{C} \in ℂ) \to A B (\frac{1}{C}) = A B (\frac{1}{C})$
3	1 2	syl3an3	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to A B (\frac{1}{C}) = A B (\frac{1}{C})$
4		mulcl	$⊢ (A \in ℂ \land B \in ℂ) \to A B \in ℂ$
5	4	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to A B \in ℂ$
6		simp3l	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to C \in ℂ$
7		simp3r	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to C \neq 0$
8		divrec	$⊢ (A B \in ℂ \land C \in ℂ \land C \neq 0) \to \frac{A B}{C} = A B (\frac{1}{C})$
9	5 6 7 8	syl3anc	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{A B}{C} = A B (\frac{1}{C})$
10		simp2	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to B \in ℂ$
11		divrec	$⊢ (B \in ℂ \land C \in ℂ \land C \neq 0) \to \frac{B}{C} = B (\frac{1}{C})$
12	10 6 7 11	syl3anc	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{B}{C} = B (\frac{1}{C})$
13	12	oveq2d	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to A (\frac{B}{C}) = A B (\frac{1}{C})$
14	3 9 13	3eqtr4d	$⊢ (A \in ℂ \land B \in ℂ \land (C \in ℂ \land C \neq 0)) \to \frac{A B}{C} = A (\frac{B}{C})$

Metamath Proof Explorer