Metamath Proof Explorer


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 ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ+ ) → ( 𝐴 / 𝐵 ) ∈ ℝ )