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 φ
fprodcl.a φ A Fin
fprodrecl.b φ k A B
Assertion fprodreclf φ k A B


Step Hyp Ref Expression
1 fprodreclf.kph k φ
2 fprodcl.a φ A Fin
3 fprodrecl.b φ k A B
4 ax-resscn
5 4 a1i φ
6 remulcl x y x y
7 6 adantl φ x y x y
8 1red φ 1
9 1 5 7 2 3 8 fprodcllemf φ k A B