Theorem div12

Description: A commutative/associative law for division. (Contributed by NM, 30-Apr-2005)

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

Proof

Step	Hyp	Ref	Expression
1		divcl	⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
2	1	3expb	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐵 / 𝐶 ) ∈ ℂ )
3		mulcom	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 / 𝐶 ) ∈ ℂ ) → ( 𝐴 · ( 𝐵 / 𝐶 ) ) = ( ( 𝐵 / 𝐶 ) · 𝐴 ) )
4	2 3	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) ) → ( 𝐴 · ( 𝐵 / 𝐶 ) ) = ( ( 𝐵 / 𝐶 ) · 𝐴 ) )
5	4	3impb	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · ( 𝐵 / 𝐶 ) ) = ( ( 𝐵 / 𝐶 ) · 𝐴 ) )
6		div13	⊢ ( ( 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ 𝐴 ∈ ℂ ) → ( ( 𝐵 / 𝐶 ) · 𝐴 ) = ( ( 𝐴 / 𝐶 ) · 𝐵 ) )
7	6	3comr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐵 / 𝐶 ) · 𝐴 ) = ( ( 𝐴 / 𝐶 ) · 𝐵 ) )
8		divcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
9	8	3expb	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 / 𝐶 ) ∈ ℂ )
10		mulcom	⊢ ( ( ( 𝐴 / 𝐶 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 / 𝐶 ) · 𝐵 ) = ( 𝐵 · ( 𝐴 / 𝐶 ) ) )
11	9 10	stoic3	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 / 𝐶 ) · 𝐵 ) = ( 𝐵 · ( 𝐴 / 𝐶 ) ) )
12	11	3com23	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( ( 𝐴 / 𝐶 ) · 𝐵 ) = ( 𝐵 · ( 𝐴 / 𝐶 ) ) )
13	5 7 12	3eqtrd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ ( 𝐶 ∈ ℂ ∧ 𝐶 ≠ 0 ) ) → ( 𝐴 · ( 𝐵 / 𝐶 ) ) = ( 𝐵 · ( 𝐴 / 𝐶 ) ) )