Theorem prodfclim1

Description: The constant one product converges to one. (Contributed by Scott Fenton, 5-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		prodf1.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2	1	prodf1f	$$⊢M\in \mathbb{Z}\to seqM\left(\times ,\left(Z\times \left\{1\right\}\right)\right)=Z\times \left\{1\right\}$$
3		ax-1cn	$$⊢1\in ℂ$$
4	1	eqimss2i	$$⊢{\mathbb{Z}}_{\ge M}\subseteq Z$$
5	1	fvexi	$$⊢Z\in \mathrm{V}$$
6	4 5	climconst2	$$⊢\left(1\in ℂ\wedge M\in \mathbb{Z}\right)\to \left(Z\times \left\{1\right\}\right)⇝1$$
7	3 6	mpan	$$⊢M\in \mathbb{Z}\to \left(Z\times \left\{1\right\}\right)⇝1$$
8	2 7	eqbrtrd	$$⊢M\in \mathbb{Z}\to seqM\left(\times ,\left(Z\times \left\{1\right\}\right)\right)⇝1$$