Theorem divmulass

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

	Ref	Expression
Assertion	divmulass	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 / 𝐷 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simpl1	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → 𝐴 ∈ ℂ )
2		simpl2	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → 𝐵 ∈ ℂ )
3		simpr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) )
4		divass	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) / 𝐷 ) = ( 𝐴 · ( 𝐵 / 𝐷 ) ) )
5	1 2 3 4	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) / 𝐷 ) = ( 𝐴 · ( 𝐵 / 𝐷 ) ) )
6	5	eqcomd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 · ( 𝐵 / 𝐷 ) ) = ( ( 𝐴 · 𝐵 ) / 𝐷 ) )
7	6	oveq1d	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( ( ( 𝐴 · 𝐵 ) / 𝐷 ) · 𝐶 ) )
8		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
9	8	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
10	9	adantr	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
11		simpl3	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → 𝐶 ∈ ℂ )
12		div32	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ∧ 𝐶 ∈ ℂ ) → ( ( ( 𝐴 · 𝐵 ) / 𝐷 ) · 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 / 𝐷 ) ) )
13	10 3 11 12	syl3anc	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( ( 𝐴 · 𝐵 ) / 𝐷 ) · 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 / 𝐷 ) ) )
14	7 13	eqtrd	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ) ∧ ( 𝐷 ∈ ℂ ∧ 𝐷 ≠ 0 ) ) → ( ( 𝐴 · ( 𝐵 / 𝐷 ) ) · 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 𝐶 / 𝐷 ) ) )