Theorem redivmul2d

Description: Relationship between division and multiplication. (Contributed by SN, 2-Apr-2026)

	Ref	Expression
Hypotheses	redivmuld.a	$$⊢\phi \to A\in ℝ$$
	redivmuld.b	$$⊢\phi \to B\in ℝ$$
	redivmuld.c	$$⊢\phi \to C\in ℝ$$
	redivmuld.z	$$⊢\phi \to C\ne 0$$
Assertion	redivmul2d	$$⊢\phi \to \left(A{/}_{ℝ}C=B\leftrightarrow A=CB\right)$$

Proof

Step	Hyp	Ref	Expression
1		redivmuld.a	$$⊢\phi \to A\in ℝ$$
2		redivmuld.b	$$⊢\phi \to B\in ℝ$$
3		redivmuld.c	$$⊢\phi \to C\in ℝ$$
4		redivmuld.z	$$⊢\phi \to C\ne 0$$
5	1 2 3 4	redivmuld	$$⊢\phi \to \left(A{/}_{ℝ}C=B\leftrightarrow CB=A\right)$$
6		eqcom	$$⊢CB=A\leftrightarrow A=CB$$
7	5 6	bitrdi	$$⊢\phi \to \left(A{/}_{ℝ}C=B\leftrightarrow A=CB\right)$$