Theorem fprodclf

Description: Closure of a finite product of complex numbers. A version of fprodcl using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

	Ref	Expression
Hypotheses	fprodclf.kph	$$⊢Ⅎk\phi$$
	fprodclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
	fprodclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
Assertion	fprodclf	$$⊢\phi \to \prod _{k\in A}B\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		fprodclf.kph	$$⊢Ⅎk\phi$$
2		fprodclf.a	$$⊢\phi \to A\in \mathrm{Fin}$$
3		fprodclf.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
4		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
5		mulcl	$$⊢\left(x\in ℂ\wedge y\in ℂ\right)\to xy\in ℂ$$
6	5	adantl	$$⊢\left(\phi \wedge \left(x\in ℂ\wedge y\in ℂ\right)\right)\to xy\in ℂ$$
7		1cnd	$$⊢\phi \to 1\in ℂ$$
8	1 4 6 2 3 7	fprodcllemf	$$⊢\phi \to \prod _{k\in A}B\in ℂ$$