This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem divmulass

Description: An associative law for division and multiplication. (Contributed by AV, 10-Jul-2021)

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

Proof

Step	Hyp	Ref	Expression
1		simpl1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A \in ℂ$
2		simpl2	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to B \in ℂ$
3		simpr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to (D \in ℂ \land D \neq 0)$
4		divass	$⊢ (A \in ℂ \land B \in ℂ \land (D \in ℂ \land D \neq 0)) \to \frac{A B}{D} = A (\frac{B}{D})$
5	1 2 3 4	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to \frac{A B}{D} = A (\frac{B}{D})$
6	5	eqcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A (\frac{B}{D}) = \frac{A B}{D}$
7	6	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A (\frac{B}{D}) C = (\frac{A B}{D}) C$
8		mulcl	$⊢ (A \in ℂ \land B \in ℂ) \to A B \in ℂ$
9	8	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B \in ℂ$
10	9	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A B \in ℂ$
11		simpl3	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to C \in ℂ$
12		div32	$⊢ (A B \in ℂ \land (D \in ℂ \land D \neq 0) \land C \in ℂ) \to (\frac{A B}{D}) C = A B (\frac{C}{D})$
13	10 3 11 12	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to (\frac{A B}{D}) C = A B (\frac{C}{D})$
14	7 13	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A (\frac{B}{D}) C = A B (\frac{C}{D})$