Theorem sn-redivcld

Description: Closure law for real division. (Contributed by SN, 25-Nov-2025)

	Ref	Expression
Hypotheses	redivvald.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	redivvald.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	redivvald.z	⊢ ( 𝜑 → 𝐵 ≠ 0 )
Assertion	sn-redivcld	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		redivvald.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2		redivvald.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3		redivvald.z	⊢ ( 𝜑 → 𝐵 ≠ 0 )
4	1 2 3	redivvald	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) = ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) )
5	1 2 3	rediveud	⊢ ( 𝜑 → ∃! 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 )
6		riotacl	⊢ ( ∃! 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) ∈ ℝ )
7	5 6	syl	⊢ ( 𝜑 → ( ℩ 𝑥 ∈ ℝ ( 𝐵 · 𝑥 ) = 𝐴 ) ∈ ℝ )
8	4 7	eqeltrd	⊢ ( 𝜑 → ( 𝐴 /ℝ 𝐵 ) ∈ ℝ )