# Metamath Proof Explorer

## 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 {ℝ}^{+}↔\left({A}\in ℝ\wedge 0<{A}\right)$
7 elrp ${⊢}{B}\in {ℝ}^{+}↔\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 {ℝ}^{+}↔\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 {ℝ}^{+}$