Theorem zprodn0

Description: Nonzero series product with index set a subset of the upper integers. (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$$
	zprodn0.5	$$⊢\phi \to A\subseteq Z$$
	zprodn0.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=if\left(k\in A,B,1\right)$$
	zprodn0.7	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
Assertion	zprodn0	$$⊢\phi \to \prod _{k\in A}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		zprodn0.5	$$⊢\phi \to A\subseteq Z$$
6		zprodn0.6	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=if\left(k\in A,B,1\right)$$
7		zprodn0.7	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℂ$$
8	1 2 4 3	ntrivcvgn0	$$⊢\phi \to \exists m\in Z\exists x\left(x\ne 0\wedge seqm\left(\times ,F\right)⇝x\right)$$
9	1 2 8 5 6 7	zprod	$$⊢\phi \to \prod _{k\in A}B=⇝\left(seqM\left(\times ,F\right)\right)$$
10		fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$
11		ffun	$$⊢⇝:\mathrm{dom}⇝⟶ℂ\to \mathrm{Fun}⇝$$
12	10 11	ax-mp	$$⊢\mathrm{Fun}⇝$$
13		funbrfv	$$⊢\mathrm{Fun}⇝\to \left(seqM\left(\times ,F\right)⇝X\to ⇝\left(seqM\left(\times ,F\right)\right)=X\right)$$
14	12 4 13	mpsyl	$$⊢\phi \to ⇝\left(seqM\left(\times ,F\right)\right)=X$$
15	9 14	eqtrd	$$⊢\phi \to \prod _{k\in A}B=X$$