Theorem fprodreclf

Description: Closure of a finite product of real numbers. A version of fprodrecl using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodreclf.kph	$$⊢Ⅎk\phi$$
	fprodcl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodrecl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
Assertion	fprodreclf	$$⊢\phi \to \prod _{k\in A}B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		fprodreclf.kph	$$⊢Ⅎk\phi$$
2		fprodcl.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fprodrecl.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$
4		ax-resscn	$$⊢ℝ\subseteq ℂ$$
5	4	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
6		remulcl	$$⊢\left(x\in ℝ\wedge y\in ℝ\right)\to xy\in ℝ$$
7	6	adantl	$$⊢\left(\phi \wedge \left(x\in ℝ\wedge y\in ℝ\right)\right)\to xy\in ℝ$$
8		1red	$$⊢\phi \to 1\in ℝ$$
9	1 5 7 2 3 8	fprodcllemf	$$⊢\phi \to \prod _{k\in A}B\in ℝ$$