Theorem redivmul2d

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

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

Proof

Step	Hyp	Ref	Expression
1		redivmuld.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		redivmuld.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		redivmuld.c	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
4		redivmuld.z	⊢ ( 𝜑 → 𝐶 ≠ 0 )
5	1 2 3 4	redivmuld	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = 𝐵 ↔ ( 𝐶 · 𝐵 ) = 𝐴 ) )
6		eqcom	⊢ ( ( 𝐶 · 𝐵 ) = 𝐴 ↔ 𝐴 = ( 𝐶 · 𝐵 ) )
7	5 6	bitrdi	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐶 ) = 𝐵 ↔ 𝐴 = ( 𝐶 · 𝐵 ) ) )