Theorem rediv23d

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

	Ref	Expression
Hypotheses	rediv23d.a	|- ( ph -> A e. RR )
	rediv23d.b	|- ( ph -> B e. RR )
	rediv23d.c	|- ( ph -> C e. RR )
	rediv23d.z	|- ( ph -> C =/= 0 )
Assertion	rediv23d	|- ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) )

Proof

Step	Hyp	Ref	Expression
1		rediv23d.a	|- ( ph -> A e. RR )
2		rediv23d.b	|- ( ph -> B e. RR )
3		rediv23d.c	|- ( ph -> C e. RR )
4		rediv23d.z	|- ( ph -> C =/= 0 )
5	3 4	sn-rereccld	|- ( ph -> ( 1 /R C ) e. RR )
6	5	recnd	|- ( ph -> ( 1 /R C ) e. CC )
7	1	recnd	|- ( ph -> A e. CC )
8	2	recnd	|- ( ph -> B e. CC )
9	6 7 8	mulassd	|- ( ph -> ( ( ( 1 /R C ) x. A ) x. B ) = ( ( 1 /R C ) x. ( A x. B ) ) )
10	1 3 4	redivrec2d	|- ( ph -> ( A /R C ) = ( ( 1 /R C ) x. A ) )
11	10	oveq1d	|- ( ph -> ( ( A /R C ) x. B ) = ( ( ( 1 /R C ) x. A ) x. B ) )
12	1 2	remulcld	|- ( ph -> ( A x. B ) e. RR )
13	12 3 4	redivrec2d	|- ( ph -> ( ( A x. B ) /R C ) = ( ( 1 /R C ) x. ( A x. B ) ) )
14	9 11 13	3eqtr4rd	|- ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) )