Theorem divass

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

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

Proof

Step	Hyp	Ref	Expression
1		reccl	⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 1 / 𝐶 ) ∈ ℂ )
2		mulass	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 1 / 𝐶 ) ∈ ℂ ) → ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐶 ) ) = ( 𝐴 · ( 𝐵 · ( 1 / 𝐶 ) ) ) )
3	1 2	syl3an3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐶 ) ) = ( 𝐴 · ( 𝐵 · ( 1 / 𝐶 ) ) ) )
4		mulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
5	4	3adant3	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · 𝐵 ) ∈ ℂ )
6		simp3l	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ∈ ℂ )
7		simp3r	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐶 ≠ 0 )
8		divrec	⊢ ( ( ( 𝐴 · 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( ( 𝐴 · 𝐵 ) / 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐶 ) ) )
9	5 6 7 8	syl3anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) / 𝐶 ) = ( ( 𝐴 · 𝐵 ) · ( 1 / 𝐶 ) ) )
10		simp2	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → 𝐵 ∈ ℂ )
11		divrec	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐵 / 𝐶 ) = ( 𝐵 · ( 1 / 𝐶 ) ) )
12	10 6 7 11	syl3anc	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 / 𝐶 ) = ( 𝐵 · ( 1 / 𝐶 ) ) )
13	12	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · ( 𝐵 / 𝐶 ) ) = ( 𝐴 · ( 𝐵 · ( 1 / 𝐶 ) ) ) )
14	3 9 13	3eqtr4d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 · 𝐵 ) / 𝐶 ) = ( 𝐴 · ( 𝐵 / 𝐶 ) ) )