rediv23d

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

	Ref	Expression
Hypotheses	rediv23d.a	$⊢ φ \to A \in ℝ$
	rediv23d.b	$⊢ φ \to B \in ℝ$
	rediv23d.c	$⊢ φ \to C \in ℝ$
	rediv23d.z	$⊢ φ \to C \neq 0$
Assertion	rediv23d	Could not format assertion : No typesetting found for \|- ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) ) with typecode \|-

Step	Hyp	Ref	Expression
1		rediv23d.a	$⊢ φ \to A \in ℝ$
2		rediv23d.b	$⊢ φ \to B \in ℝ$
3		rediv23d.c	$⊢ φ \to C \in ℝ$
4		rediv23d.z	$⊢ φ \to C \neq 0$
5	3 4	sn-rereccld	Could not format ( ph -> ( 1 /R C ) e. RR ) : No typesetting found for \|- ( ph -> ( 1 /R C ) e. RR ) with typecode \|-
6	5	recnd	Could not format ( ph -> ( 1 /R C ) e. CC ) : No typesetting found for \|- ( ph -> ( 1 /R C ) e. CC ) with typecode \|-
7	1	recnd	$⊢ φ \to A \in ℂ$
8	2	recnd	$⊢ φ \to B \in ℂ$
9	6 7 8	mulassd	Could not format ( ph -> ( ( ( 1 /R C ) x. A ) x. B ) = ( ( 1 /R C ) x. ( A x. B ) ) ) : No typesetting found for \|- ( ph -> ( ( ( 1 /R C ) x. A ) x. B ) = ( ( 1 /R C ) x. ( A x. B ) ) ) with typecode \|-
10	1 3 4	redivrec2d	Could not format ( ph -> ( A /R C ) = ( ( 1 /R C ) x. A ) ) : No typesetting found for \|- ( ph -> ( A /R C ) = ( ( 1 /R C ) x. A ) ) with typecode \|-
11	10	oveq1d	Could not format ( ph -> ( ( A /R C ) x. B ) = ( ( ( 1 /R C ) x. A ) x. B ) ) : No typesetting found for \|- ( ph -> ( ( A /R C ) x. B ) = ( ( ( 1 /R C ) x. A ) x. B ) ) with typecode \|-
12	1 2	remulcld	$⊢ φ \to A B \in ℝ$
13	12 3 4	redivrec2d	Could not format ( ph -> ( ( A x. B ) /R C ) = ( ( 1 /R C ) x. ( A x. B ) ) ) : No typesetting found for \|- ( ph -> ( ( A x. B ) /R C ) = ( ( 1 /R C ) x. ( A x. B ) ) ) with typecode \|-
14	9 11 13	3eqtr4rd	Could not format ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) ) : No typesetting found for \|- ( ph -> ( ( A x. B ) /R C ) = ( ( A /R C ) x. B ) ) with typecode \|-

Metamath Proof Explorer