Theorem prodf1

Description: The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017)

	Ref	Expression
Hypothesis	prodf1.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	prodf1	$$⊢N\in Z\to seqM\left(\times ,\left(Z\times \left\{1\right\}\right)\right)\left(N\right)=1$$

Proof

Step	Hyp	Ref	Expression
1		prodf1.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		1t1e1	$$⊢1\cdot 1=1$$
3	2	a1i	$$⊢N\in Z\to 1\cdot 1=1$$
4	1	eleq2i	$$⊢N\in Z\leftrightarrow N\in {\mathbb{Z}}_{\ge M}$$
5	4	biimpi	$$⊢N\in Z\to N\in {\mathbb{Z}}_{\ge M}$$
6		ax-1cn	$$⊢1\in ℂ$$
7		elfzuz	$$⊢k\in \left(M\dots N\right)\to k\in {\mathbb{Z}}_{\ge M}$$
8	7 1	eleqtrrdi	$$⊢k\in \left(M\dots N\right)\to k\in Z$$
9	8	adantl	$$⊢\left(N\in Z\wedge k\in \left(M\dots N\right)\right)\to k\in Z$$
10		fvconst2g	$$⊢\left(1\in ℂ\wedge k\in Z\right)\to \left(Z\times \left\{1\right\}\right)\left(k\right)=1$$
11	6 9 10	sylancr	$$⊢\left(N\in Z\wedge k\in \left(M\dots N\right)\right)\to \left(Z\times \left\{1\right\}\right)\left(k\right)=1$$
12	3 5 11	seqid3	$$⊢N\in Z\to seqM\left(\times ,\left(Z\times \left\{1\right\}\right)\right)\left(N\right)=1$$