Metamath Proof Explorer

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}\phantom{\rule{.4em}{0ex}}{\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}\phantom{\rule{.4em}{0ex}}{\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 {x}{y}\in ℝ$
7 6 adantl ${⊢}\left({\phi }\wedge \left({x}\in ℝ\wedge {y}\in ℝ\right)\right)\to {x}{y}\in ℝ$
8 1red ${⊢}{\phi }\to 1\in ℝ$
9 1 5 7 2 3 8 fprodcllemf ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}\in ℝ$