Theorem iprod

Description: Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypotheses	zprod.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	zprod.2	$$⊢\phi \to M\in \mathbb{Z}$$
	zprod.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
	iprod.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
	iprod.5	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
Assertion	iprod	$$⊢\phi \to \prod _{k\in Z}B=⇝\left(seqM\left(\times ,F\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		zprod.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		zprod.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		zprod.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
4		iprod.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=B$$
5		iprod.5	$$⊢\left(\phi \wedge k\in Z\right)\to B\in ℂ$$
6		ssidd	$$⊢\phi \to Z\subseteq Z$$
7		iftrue	$$⊢k\in Z\to if\left(k\in Z,B,1\right)=B$$
8	7	adantl	$$⊢\left(\phi \wedge k\in Z\right)\to if\left(k\in Z,B,1\right)=B$$
9	4 8	eqtr4d	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=if\left(k\in Z,B,1\right)$$
10	1 2 3 6 9 5	zprod	$$⊢\phi \to \prod _{k\in Z}B=⇝\left(seqM\left(\times ,F\right)\right)$$