Theorem rerpdivcl

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

	Ref	Expression
Assertion	rerpdivcl	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		rprene0	$$⊢B\in {ℝ}^{+}\to \left(B\in ℝ\wedge B\ne 0\right)$$
2		redivcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge B\ne 0\right)\to \frac{A}{B}\in ℝ$$
3	2	3expb	$$⊢\left(A\in ℝ\wedge \left(B\in ℝ\wedge B\ne 0\right)\right)\to \frac{A}{B}\in ℝ$$
4	1 3	sylan2	$$⊢\left(A\in ℝ\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$