# Metamath Proof Explorer

## Theorem iprod

Description: Series product with an upper integer index set (i.e. an infinite product.) (Contributed by Scott Fenton, 5-Dec-2017)

Ref Expression
Hypotheses zprod.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
zprod.2 ${⊢}{\phi }\to {M}\in ℤ$
zprod.3 ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)$
iprod.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={B}$
iprod.5 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {B}\in ℂ$
Assertion iprod ${⊢}{\phi }\to \prod _{{k}\in {Z}}{B}=⇝\left(seq{M}\left(×,{F}\right)\right)$

### Proof

Step Hyp Ref Expression
1 zprod.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 zprod.2 ${⊢}{\phi }\to {M}\in ℤ$
3 zprod.3 ${⊢}{\phi }\to \exists {n}\in {Z}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\ne 0\wedge seq{n}\left(×,{F}\right)⇝{y}\right)$
4 iprod.4 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={B}$
5 iprod.5 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {B}\in ℂ$
6 ssidd ${⊢}{\phi }\to {Z}\subseteq {Z}$
7 iftrue ${⊢}{k}\in {Z}\to if\left({k}\in {Z},{B},1\right)={B}$
8 7 adantl ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to if\left({k}\in {Z},{B},1\right)={B}$
9 4 8 eqtr4d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)=if\left({k}\in {Z},{B},1\right)$
10 1 2 3 6 9 5 zprod ${⊢}{\phi }\to \prod _{{k}\in {Z}}{B}=⇝\left(seq{M}\left(×,{F}\right)\right)$