Theorem prodf

Description: An infinite product of complex terms is a function from an upper set of integers to CC . (Contributed by Scott Fenton, 4-Dec-2017)

	Ref	Expression
Hypotheses	prodf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	prodf.2	$$⊢\phi \to M\in \mathbb{Z}$$
	prodf.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
Assertion	prodf	$$⊢\phi \to seqM\left(\times ,F\right):Z⟶ℂ$$

Proof

Step	Hyp	Ref	Expression
1		prodf.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		prodf.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		prodf.3	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
4		mulcl	$$⊢\left(k\in ℂ\wedge x\in ℂ\right)\to kx\in ℂ$$
5	4	adantl	$$⊢\left(\phi \wedge \left(k\in ℂ\wedge x\in ℂ\right)\right)\to kx\in ℂ$$
6	1 2 3 5	seqf	$$⊢\phi \to seqM\left(\times ,F\right):Z⟶ℂ$$