Theorem iprodcl

Description: The product of a non-trivially converging infinite sequence is a complex number. (Contributed by Scott Fenton, 18-Dec-2017)

	Ref	Expression
Hypotheses	iprodcl.1	|- Z = ( ZZ>= ` M )
	iprodcl.2	|- ( ph -> M e. ZZ )
	iprodcl.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
	iprodcl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
	iprodcl.5	|- ( ( ph /\ k e. Z ) -> A e. CC )
Assertion	iprodcl	|- ( ph -> prod_ k e. Z A e. CC )

Proof

Step	Hyp	Ref	Expression
1		iprodcl.1	|- Z = ( ZZ>= ` M )
2		iprodcl.2	|- ( ph -> M e. ZZ )
3		iprodcl.3	|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , F ) ~~> y ) )
4		iprodcl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
5		iprodcl.5	|- ( ( ph /\ k e. Z ) -> A e. CC )
6	1 2 3 4 5	iprod	|- ( ph -> prod_ k e. Z A = ( ~~> ` seq M ( x. , F ) ) )
7		fclim	|- ~~> : dom ~~> --> CC
8	4 5	eqeltrd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
9	1 3 8	ntrivcvg	|- ( ph -> seq M ( x. , F ) e. dom ~~> )
10		ffvelrn	|- ( ( ~~> : dom ~~> --> CC /\ seq M ( x. , F ) e. dom ~~> ) -> ( ~~> ` seq M ( x. , F ) ) e. CC )
11	7 9 10	sylancr	|- ( ph -> ( ~~> ` seq M ( x. , F ) ) e. CC )
12	6 11	eqeltrd	|- ( ph -> prod_ k e. Z A e. CC )