Theorem fprodzcl

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

	Ref	Expression
Hypotheses	fprodcl.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodzcl.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \mathbb{Z}$$
Assertion	fprodzcl	$$⊢\phi \to \prod _{k\in A}B\in \mathbb{Z}$$

Proof

Step	Hyp	Ref	Expression
1		fprodcl.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		fprodzcl.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \mathbb{Z}$$
3		zsscn	$$⊢\mathbb{Z}\subseteq ℂ$$
4	3	a1i	$$⊢\phi \to \mathbb{Z}\subseteq ℂ$$
5		zmulcl	$$⊢\left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\to xy\in \mathbb{Z}$$
6	5	adantl	$$⊢\left(\phi \wedge \left(x\in \mathbb{Z}\wedge y\in \mathbb{Z}\right)\right)\to xy\in \mathbb{Z}$$
7		1zzd	$$⊢\phi \to 1\in \mathbb{Z}$$
8	4 6 1 2 7	fprodcllem	$$⊢\phi \to \prod _{k\in A}B\in \mathbb{Z}$$