Theorem iprodclim

Description: An infinite product equals the value its sequence converges to. (Contributed by Scott Fenton, 18-Dec-2017)

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

Proof

Step	Hyp	Ref	Expression
1		iprodclim.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		iprodclim.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		iprodclim.3	$$⊢\phi \to \exists n\in Z\exists y\left(y\ne 0\wedge seqn\left(\times ,F\right)⇝y\right)$$
4		iprodclim.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
5		iprodclim.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
6		iprodclim.6	$$⊢\phi \to seqM\left(\times ,F\right)⇝B$$
7	1 2 3 4 5	iprod	$$⊢\phi \to \prod _{k\in Z}A=⇝\left(seqM\left(\times ,F\right)\right)$$
8		fclim	$$⊢⇝:\mathrm{dom}⇝⟶ℂ$$
9		ffun	$$⊢⇝:\mathrm{dom}⇝⟶ℂ\to \mathrm{Fun}⇝$$
10	8 9	ax-mp	$$⊢\mathrm{Fun}⇝$$
11		funbrfv	$$⊢\mathrm{Fun}⇝\to \left(seqM\left(\times ,F\right)⇝B\to ⇝\left(seqM\left(\times ,F\right)\right)=B\right)$$
12	10 6 11	mpsyl	$$⊢\phi \to ⇝\left(seqM\left(\times ,F\right)\right)=B$$
13	7 12	eqtrd	$$⊢\phi \to \prod _{k\in Z}A=B$$