Theorem rpdivcl

Description: Closure law for division of positive reals. (Contributed by FL, 27-Dec-2007)

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

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
2		rprene0	$$⊢B\in {ℝ}^{+}\to \left(B\in ℝ\wedge B\ne 0\right)$$
3		redivcl	$$⊢\left(A\in ℝ\wedge B\in ℝ\wedge B\ne 0\right)\to \frac{A}{B}\in ℝ$$
4	3	3expb	$$⊢\left(A\in ℝ\wedge \left(B\in ℝ\wedge B\ne 0\right)\right)\to \frac{A}{B}\in ℝ$$
5	1 2 4	syl2an	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in ℝ$$
6		elrp	$$⊢A\in {ℝ}^{+}\leftrightarrow \left(A\in ℝ\wedge 0<A\right)$$
7		elrp	$$⊢B\in {ℝ}^{+}\leftrightarrow \left(B\in ℝ\wedge 0<B\right)$$
8		divgt0	$$⊢\left(\left(A\in ℝ\wedge 0<A\right)\wedge \left(B\in ℝ\wedge 0<B\right)\right)\to 0<\frac{A}{B}$$
9	6 7 8	syl2anb	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to 0<\frac{A}{B}$$
10		elrp	$$⊢\frac{A}{B}\in {ℝ}^{+}\leftrightarrow \left(\frac{A}{B}\in ℝ\wedge 0<\frac{A}{B}\right)$$
11	5 9 10	sylanbrc	$$⊢\left(A\in {ℝ}^{+}\wedge B\in {ℝ}^{+}\right)\to \frac{A}{B}\in {ℝ}^{+}$$