Metamath Proof Explorer

Theorem fprodrecl

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

Ref Expression
Hypotheses fprodcl.1 φ A Fin
fprodrecl.2 φ k A B
Assertion fprodrecl φ k A B


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