Theorem redivrec2d

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

	Ref	Expression
Hypotheses	redivrec2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	redivrec2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	redivrec2d.z	⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion	redivrec2d	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) = ( ( 1 /ℝ 𝐵 ) · 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		redivrec2d.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		redivrec2d.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		redivrec2d.z	⊢ ( 𝜑 → 𝐵 ≠ 0 )
4	2 3	rerecidd	⊢ ( 𝜑 → ( 𝐵 · ( 1 /ℝ 𝐵 ) ) = 1 )
5	4	oveq1d	⊢ ( 𝜑 → ( ( 𝐵 · ( 1 /ℝ 𝐵 ) ) · 𝐴 ) = ( 1 · 𝐴 ) )
6	2	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
7	2 3	sn-rereccld	⊢ ( 𝜑 → ( 1 /ℝ 𝐵 ) ∈ ℝ )
8	7	recnd	⊢ ( 𝜑 → ( 1 /ℝ 𝐵 ) ∈ ℂ )
9	1	recnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
10	6 8 9	mulassd	⊢ ( 𝜑 → ( ( 𝐵 · ( 1 /ℝ 𝐵 ) ) · 𝐴 ) = ( 𝐵 · ( ( 1 /ℝ 𝐵 ) · 𝐴 ) ) )
11		remullid	⊢ ( 𝐴 ∈ ℝ → ( 1 · 𝐴 ) = 𝐴 )
12	1 11	syl	⊢ ( 𝜑 → ( 1 · 𝐴 ) = 𝐴 )
13	5 10 12	3eqtr3d	⊢ ( 𝜑 → ( 𝐵 · ( ( 1 /ℝ 𝐵 ) · 𝐴 ) ) = 𝐴 )
14	7 1	remulcld	⊢ ( 𝜑 → ( ( 1 /ℝ 𝐵 ) · 𝐴 ) ∈ ℝ )
15	1 14 2 3	redivmuld	⊢ ( 𝜑 → ( ( 𝐴 /ℝ 𝐵 ) = ( ( 1 /ℝ 𝐵 ) · 𝐴 ) ↔ ( 𝐵 · ( ( 1 /ℝ 𝐵 ) · 𝐴 ) ) = 𝐴 ) )
16	13 15	mpbird	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) = ( ( 1 /ℝ 𝐵 ) · 𝐴 ) )