fprodrpcl

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

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

Metamath Proof Explorer