# Metamath Proof Explorer

## Theorem rpmulcl

Description: Closure law for multiplication of positive reals. Part of Axiom 7 of Apostol p. 20. (Contributed by NM, 27-Oct-2007)

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

### Proof

Step Hyp Ref Expression
1 rpre ${⊢}{A}\in {ℝ}^{+}\to {A}\in ℝ$
2 rpre ${⊢}{B}\in {ℝ}^{+}\to {B}\in ℝ$
3 remulcl ${⊢}\left({A}\in ℝ\wedge {B}\in ℝ\right)\to {A}{B}\in ℝ$
4 1 2 3 syl2an ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to {A}{B}\in ℝ$
5 elrp ${⊢}{A}\in {ℝ}^{+}↔\left({A}\in ℝ\wedge 0<{A}\right)$
6 elrp ${⊢}{B}\in {ℝ}^{+}↔\left({B}\in ℝ\wedge 0<{B}\right)$
7 mulgt0 ${⊢}\left(\left({A}\in ℝ\wedge 0<{A}\right)\wedge \left({B}\in ℝ\wedge 0<{B}\right)\right)\to 0<{A}{B}$
8 5 6 7 syl2anb ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to 0<{A}{B}$
9 elrp ${⊢}{A}{B}\in {ℝ}^{+}↔\left({A}{B}\in ℝ\wedge 0<{A}{B}\right)$
10 4 8 9 sylanbrc ${⊢}\left({A}\in {ℝ}^{+}\wedge {B}\in {ℝ}^{+}\right)\to {A}{B}\in {ℝ}^{+}$