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={\mathbb{Z}}_{\ge M}$$
	iprodcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
	iprodcl.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
	iprodcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	iprodcl.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
Assertion	iprodcl	$$⊢\phi \to \prod _{k\in Z}A\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		iprodcl.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		iprodcl.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		iprodcl.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
4		iprodcl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
5		iprodcl.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
6	1 2 3 4 5	iprod	$$⊢\phi \to \prod _{k\in Z}A=⇝\left(seqM\left(\times ,F\right)\right)$$
7		fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$
8	4 5	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
9	1 3 8	ntrivcvg	$$⊢\phi \to seqM\left(\times ,F\right)\in \mathrm{dom}⇝$$
10		ffvelrn	$$⊢\left(⇝:\mathrm{dom}⇝⟶ℂ\wedge seqM\left(\times ,F\right)\in \mathrm{dom}⇝\right)\to ⇝\left(seqM\left(\times ,F\right)\right)\in ℂ$$
11	7 9 10	sylancr	$$⊢\phi \to ⇝\left(seqM\left(\times ,F\right)\right)\in ℂ$$
12	6 11	eqeltrd	$$⊢\phi \to \prod _{k\in Z}A\in ℂ$$