Theorem redivmul2d

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

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

Proof

Step	Hyp	Ref	Expression
1		redivmuld.a	|- ( ph -> A e. RR )
2		redivmuld.b	|- ( ph -> B e. RR )
3		redivmuld.c	|- ( ph -> C e. RR )
4		redivmuld.z	|- ( ph -> C =/= 0 )
5	1 2 3 4	redivmuld	|- ( ph -> ( ( A /R C ) = B <-> ( C x. B ) = A ) )
6		eqcom	|- ( ( C x. B ) = A <-> A = ( C x. B ) )
7	5 6	bitrdi	|- ( ph -> ( ( A /R C ) = B <-> A = ( C x. B ) ) )