Metamath Proof Explorer

Theorem fprodzcl

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

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


Step Hyp Ref Expression
1 fprodcl.1 φ A Fin
2 fprodzcl.2 φ k A B
3 zsscn
4 3 a1i φ
5 zmulcl x y x y
6 5 adantl φ x y x y
7 1zzd φ 1
8 4 6 1 2 7 fprodcllem φ k A B