# Metamath Proof Explorer

## Theorem fprodcvg

Description: The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
prodrb.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
fprodcvg.4 ${⊢}{\phi }\to {A}\subseteq \left({M}\dots {N}\right)$
Assertion fprodcvg ${⊢}{\phi }\to seq{M}\left(×,{F}\right)⇝seq{M}\left(×,{F}\right)\left({N}\right)$

### Proof

Step Hyp Ref Expression
1 prodmo.1 ${⊢}{F}=\left({k}\in ℤ⟼if\left({k}\in {A},{B},1\right)\right)$
2 prodmo.2 ${⊢}\left({\phi }\wedge {k}\in {A}\right)\to {B}\in ℂ$
3 prodrb.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
4 fprodcvg.4 ${⊢}{\phi }\to {A}\subseteq \left({M}\dots {N}\right)$
5 eqid ${⊢}{ℤ}_{\ge {N}}={ℤ}_{\ge {N}}$
6 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
7 3 6 syl ${⊢}{\phi }\to {N}\in ℤ$
8 seqex ${⊢}seq{M}\left(×,{F}\right)\in \mathrm{V}$
9 8 a1i ${⊢}{\phi }\to seq{M}\left(×,{F}\right)\in \mathrm{V}$
10 eqid ${⊢}{ℤ}_{\ge {M}}={ℤ}_{\ge {M}}$
11 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
12 3 11 syl ${⊢}{\phi }\to {M}\in ℤ$
13 eluzelz ${⊢}{k}\in {ℤ}_{\ge {M}}\to {k}\in ℤ$
14 13 adantl ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {k}\in ℤ$
15 iftrue ${⊢}{k}\in {A}\to if\left({k}\in {A},{B},1\right)={B}$
16 15 adantl ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},1\right)={B}$
17 2 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to {B}\in ℂ$
18 16 17 eqeltrd ${⊢}\left(\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\wedge {k}\in {A}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
19 18 ex ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to \left({k}\in {A}\to if\left({k}\in {A},{B},1\right)\in ℂ\right)$
20 iffalse ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},1\right)=1$
21 ax-1cn ${⊢}1\in ℂ$
22 20 21 eqeltrdi ${⊢}¬{k}\in {A}\to if\left({k}\in {A},{B},1\right)\in ℂ$
23 19 22 pm2.61d1 ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
24 1 fvmpt2 ${⊢}\left({k}\in ℤ\wedge if\left({k}\in {A},{B},1\right)\in ℂ\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
25 14 23 24 syl2anc ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
26 25 23 eqeltrd ${⊢}\left({\phi }\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {F}\left({k}\right)\in ℂ$
27 10 12 26 prodf ${⊢}{\phi }\to seq{M}\left(×,{F}\right):{ℤ}_{\ge {M}}⟶ℂ$
28 27 3 ffvelrnd ${⊢}{\phi }\to seq{M}\left(×,{F}\right)\left({N}\right)\in ℂ$
29 mulid1 ${⊢}{m}\in ℂ\to {m}\cdot 1={m}$
30 29 adantl ${⊢}\left(\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\wedge {m}\in ℂ\right)\to {m}\cdot 1={m}$
31 3 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to {N}\in {ℤ}_{\ge {M}}$
32 simpr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to {n}\in {ℤ}_{\ge {N}}$
33 12 adantr ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to {M}\in ℤ$
34 26 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in {ℤ}_{\ge {M}}\right)\to {F}\left({k}\right)\in ℂ$
35 10 33 34 prodf ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to seq{M}\left(×,{F}\right):{ℤ}_{\ge {M}}⟶ℂ$
36 35 31 ffvelrnd ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to seq{M}\left(×,{F}\right)\left({N}\right)\in ℂ$
37 elfzuz ${⊢}{m}\in \left({N}+1\dots {n}\right)\to {m}\in {ℤ}_{\ge \left({N}+1\right)}$
38 eluzelz ${⊢}{m}\in {ℤ}_{\ge \left({N}+1\right)}\to {m}\in ℤ$
39 38 adantl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {m}\in ℤ$
40 4 sseld ${⊢}{\phi }\to \left({m}\in {A}\to {m}\in \left({M}\dots {N}\right)\right)$
41 fznuz ${⊢}{m}\in \left({M}\dots {N}\right)\to ¬{m}\in {ℤ}_{\ge \left({N}+1\right)}$
42 40 41 syl6 ${⊢}{\phi }\to \left({m}\in {A}\to ¬{m}\in {ℤ}_{\ge \left({N}+1\right)}\right)$
43 42 con2d ${⊢}{\phi }\to \left({m}\in {ℤ}_{\ge \left({N}+1\right)}\to ¬{m}\in {A}\right)$
44 43 imp ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to ¬{m}\in {A}$
45 39 44 eldifd ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {m}\in \left(ℤ\setminus {A}\right)$
46 fveqeq2 ${⊢}{k}={m}\to \left({F}\left({k}\right)=1↔{F}\left({m}\right)=1\right)$
47 eldifi ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to {k}\in ℤ$
48 eldifn ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to ¬{k}\in {A}$
49 48 20 syl ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to if\left({k}\in {A},{B},1\right)=1$
50 49 21 eqeltrdi ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to if\left({k}\in {A},{B},1\right)\in ℂ$
51 47 50 24 syl2anc ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to {F}\left({k}\right)=if\left({k}\in {A},{B},1\right)$
52 51 49 eqtrd ${⊢}{k}\in \left(ℤ\setminus {A}\right)\to {F}\left({k}\right)=1$
53 46 52 vtoclga ${⊢}{m}\in \left(ℤ\setminus {A}\right)\to {F}\left({m}\right)=1$
54 45 53 syl ${⊢}\left({\phi }\wedge {m}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {F}\left({m}\right)=1$
55 37 54 sylan2 ${⊢}\left({\phi }\wedge {m}\in \left({N}+1\dots {n}\right)\right)\to {F}\left({m}\right)=1$
56 55 adantlr ${⊢}\left(\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\wedge {m}\in \left({N}+1\dots {n}\right)\right)\to {F}\left({m}\right)=1$
57 30 31 32 36 56 seqid2 ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to seq{M}\left(×,{F}\right)\left({N}\right)=seq{M}\left(×,{F}\right)\left({n}\right)$
58 57 eqcomd ${⊢}\left({\phi }\wedge {n}\in {ℤ}_{\ge {N}}\right)\to seq{M}\left(×,{F}\right)\left({n}\right)=seq{M}\left(×,{F}\right)\left({N}\right)$
59 5 7 9 28 58 climconst ${⊢}{\phi }\to seq{M}\left(×,{F}\right)⇝seq{M}\left(×,{F}\right)\left({N}\right)$