divmulasscom

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

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

Proof

Step	Hyp	Ref	Expression
1		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})$
2		mulcom	$⊢ (A \in ℂ \land B \in ℂ) \to A B = B A$
3	2	3adant3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to A B = B A$
4	3	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A B = B A$
5	4	oveq1d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A B (\frac{C}{D}) = B A (\frac{C}{D})$
6		simpl2	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to B \in ℂ$
7		simpl1	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A \in ℂ$
8		simp3	$⊢ (A \in ℂ \land B \in ℂ \land C \in ℂ) \to C \in ℂ$
9	8	anim1i	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to (C \in ℂ \land (D \in ℂ \land D \neq 0))$
10		3anass	$⊢ (C \in ℂ \land D \in ℂ \land D \neq 0) \leftrightarrow (C \in ℂ \land (D \in ℂ \land D \neq 0))$
11	9 10	sylibr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to (C \in ℂ \land D \in ℂ \land D \neq 0)$
12		divcl	$⊢ (C \in ℂ \land D \in ℂ \land D \neq 0) \to \frac{C}{D} \in ℂ$
13	11 12	syl	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to \frac{C}{D} \in ℂ$
14	6 7 13	mulassd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to B A (\frac{C}{D}) = B A (\frac{C}{D})$
15	8	adantr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to C \in ℂ$
16		simpr	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to (D \in ℂ \land D \neq 0)$
17		divass	$⊢ (A \in ℂ \land C \in ℂ \land (D \in ℂ \land D \neq 0)) \to \frac{A C}{D} = A (\frac{C}{D})$
18	7 15 16 17	syl3anc	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to \frac{A C}{D} = A (\frac{C}{D})$
19	18	eqcomd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A (\frac{C}{D}) = \frac{A C}{D}$
20	19	oveq2d	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to B A (\frac{C}{D}) = B (\frac{A C}{D})$
21	14 20	eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to B A (\frac{C}{D}) = B (\frac{A C}{D})$
22	1 5 21	3eqtrd	$⊢ ((A \in ℂ \land B \in ℂ \land C \in ℂ) \land (D \in ℂ \land D \neq 0)) \to A (\frac{B}{D}) C = B (\frac{A C}{D})$

Metamath Proof Explorer

Theorem divmulasscom

Proof