# Metamath Proof Explorer

## Theorem iprodn0

Description: Nonzero series product with an upper integer index set (i.e. an infinite product.) (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}$
iprodn0.5 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={B}$
iprodn0.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {B}\in ℂ$
Assertion iprodn0 ${⊢}{\phi }\to \prod _{{k}\in {Z}}{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 iprodn0.5 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)={B}$
6 iprodn0.6 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {B}\in ℂ$
7 ssidd ${⊢}{\phi }\to {Z}\subseteq {Z}$
8 iftrue ${⊢}{k}\in {Z}\to if\left({k}\in {Z},{B},1\right)={B}$
9 8 adantl ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to if\left({k}\in {Z},{B},1\right)={B}$
10 5 9 eqtr4d ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {F}\left({k}\right)=if\left({k}\in {Z},{B},1\right)$
11 1 2 3 4 7 10 6 zprodn0 ${⊢}{\phi }\to \prod _{{k}\in {Z}}{B}={X}$