Theorem iprodn0

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

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

Proof

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