Theorem rediv23d

Description: A "commutative"/associative law for division. (Contributed by SN, 9-Apr-2026)

	Ref	Expression
Hypotheses	rediv23d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	rediv23d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	rediv23d.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	rediv23d.z	⊢ ( 𝜑 → 𝐶 ≠ 0 )
Assertion	rediv23d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /ℝ 𝐶 ) = ( ( 𝐴 /ℝ 𝐶 ) · 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		rediv23d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		rediv23d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		rediv23d.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		rediv23d.z	⊢ ( 𝜑 → 𝐶 ≠ 0 )
5	3 4	sn-rereccld	⊢ ( 𝜑 → ( 1 /ℝ 𝐶 ) ∈ ℝ )
6	5	recnd	⊢ ( 𝜑 → ( 1 /ℝ 𝐶 ) ∈ ℂ )
7	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
8	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
9	6 7 8	mulassd	⊢ ( 𝜑 → ( ( ( 1 /ℝ 𝐶 ) · 𝐴 ) · 𝐵 ) = ( ( 1 /ℝ 𝐶 ) · ( 𝐴 · 𝐵 ) ) )
10	1 3 4	redivrec2d	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐶 ) = ( ( 1 /ℝ 𝐶 ) · 𝐴 ) )
11	10	oveq1d	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) · 𝐵 ) = ( ( ( 1 /ℝ 𝐶 ) · 𝐴 ) · 𝐵 ) )
12	1 2	remulcld	⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) ∈ ℝ )
13	12 3 4	redivrec2d	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /ℝ 𝐶 ) = ( ( 1 /ℝ 𝐶 ) · ( 𝐴 · 𝐵 ) ) )
14	9 11 13	3eqtr4rd	⊢ ( 𝜑 → ( ( 𝐴 · 𝐵 ) /ℝ 𝐶 ) = ( ( 𝐴 /ℝ 𝐶 ) · 𝐵 ) )