Theorem rerpdivcl

Description: Closure law for division of a real by a positive real. (Contributed by NM, 10-Nov-2008)

	Ref	Expression
Assertion	rerpdivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		rprene0	⊢ ( 𝐵 ∈ ℝ+ → ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) )
2		redivcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
3	2	3expb	⊢ ( ( 𝐴 ∈ ℝ ∧ ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) ∈ ℝ )
4	1 3	sylan2	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )