Metamath Proof Explorer

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}={ℤ}_{\ge {M}}$
zprodn0.2 ${⊢}{\phi }\to {M}\in ℤ$
zprodn0.3 ${⊢}{\phi }\to {X}\ne 0$
zprodn0.4 ${⊢}{\phi }\to seq{M}\left(×,{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}={ℤ}_{\ge {M}}$
2 zprodn0.2 ${⊢}{\phi }\to {M}\in ℤ$
3 zprodn0.3 ${⊢}{\phi }\to {X}\ne 0$
4 zprodn0.4 ${⊢}{\phi }\to seq{M}\left(×,{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}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\ne 0\wedge seq{m}\left(×,{F}\right)⇝{x}\right)$
9 1 2 8 5 6 7 zprod ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}=⇝\left(seq{M}\left(×,{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(seq{M}\left(×,{F}\right)⇝{X}\to ⇝\left(seq{M}\left(×,{F}\right)\right)={X}\right)$
14 12 4 13 mpsyl ${⊢}{\phi }\to ⇝\left(seq{M}\left(×,{F}\right)\right)={X}$
15 9 14 eqtrd ${⊢}{\phi }\to \prod _{{k}\in {A}}{B}={X}$