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 = ( ZZ>= ` M )
	prodf.2	|- ( ph -> M e. ZZ )
	prodf.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
Assertion	prodf	|- ( ph -> seq M ( x. , F ) : Z --> CC )

Proof

Step	Hyp	Ref	Expression
1		prodf.1	|- Z = ( ZZ>= ` M )
2		prodf.2	|- ( ph -> M e. ZZ )
3		prodf.3	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
4		mulcl	|- ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
5	4	adantl	|- ( ( ph /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
6	1 2 3 5	seqf	|- ( ph -> seq M ( x. , F ) : Z --> CC )