# Metamath Proof Explorer

## Theorem fprodrpcl

Description: Closure of a finite product of positive reals. (Contributed by Scott Fenton, 14-Dec-2017)

Ref Expression
Hypotheses fprodcl.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
fprodrpcl.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {ℝ}^{+}$
Assertion fprodrpcl ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in {ℝ}^{+}$

### Proof

Step Hyp Ref Expression
1 fprodcl.1 ${⊢}{\phi }\to {A}\in \mathrm{Fin}$
2 fprodrpcl.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in {ℝ}^{+}$
3 rpssre ${⊢}{ℝ}^{+}\subseteq ℝ$
4 ax-resscn ${⊢}ℝ\subseteq ℂ$
5 3 4 sstri ${⊢}{ℝ}^{+}\subseteq ℂ$
6 5 a1i ${⊢}{\phi }\to {ℝ}^{+}\subseteq ℂ$
7 rpmulcl ${⊢}\left({x}\in {ℝ}^{+}\wedge {y}\in {ℝ}^{+}\right)\to {x}{y}\in {ℝ}^{+}$
8 7 adantl ${⊢}\left({\phi }\wedge \left({x}\in {ℝ}^{+}\wedge {y}\in {ℝ}^{+}\right)\right)\to {x}{y}\in {ℝ}^{+}$
9 1rp ${⊢}1\in {ℝ}^{+}$
10 9 a1i ${⊢}{\phi }\to 1\in {ℝ}^{+}$
11 6 8 1 2 10 fprodcllem ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in {ℝ}^{+}$