This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ Ⅎ 𝑘 𝜑
fprodcl.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fprodrecl.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
Assertion fprodreclf ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 fprodreclf.kph ⊢ Ⅎ 𝑘 𝜑
2 fprodcl.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
3 fprodrecl.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
4 ax-resscn ⊢ ℝ ⊆ ℂ
5 4 a1i ⊢ ( 𝜑 → ℝ ⊆ ℂ )
6 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
7 6 adantl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) ) → ( 𝑥 · 𝑦 ) ∈ ℝ )
8 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
9 1 5 7 2 3 8 fprodcllemf ⊢ ( 𝜑 → ∏ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )