# Metamath Proof Explorer

## Theorem prodf1

Description: The value of the partial products in a one-valued infinite product. (Contributed by Scott Fenton, 5-Dec-2017)

Ref Expression
Hypothesis prodf1.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
Assertion prodf1 ${⊢}{N}\in {Z}\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({N}\right)=1$

### Proof

Step Hyp Ref Expression
1 prodf1.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 1t1e1 ${⊢}1\cdot 1=1$
3 2 a1i ${⊢}{N}\in {Z}\to 1\cdot 1=1$
4 1 eleq2i ${⊢}{N}\in {Z}↔{N}\in {ℤ}_{\ge {M}}$
5 4 biimpi ${⊢}{N}\in {Z}\to {N}\in {ℤ}_{\ge {M}}$
6 ax-1cn ${⊢}1\in ℂ$
7 elfzuz ${⊢}{k}\in \left({M}\dots {N}\right)\to {k}\in {ℤ}_{\ge {M}}$
8 7 1 eleqtrrdi ${⊢}{k}\in \left({M}\dots {N}\right)\to {k}\in {Z}$
9 8 adantl ${⊢}\left({N}\in {Z}\wedge {k}\in \left({M}\dots {N}\right)\right)\to {k}\in {Z}$
10 fvconst2g ${⊢}\left(1\in ℂ\wedge {k}\in {Z}\right)\to \left({Z}×\left\{1\right\}\right)\left({k}\right)=1$
11 6 9 10 sylancr ${⊢}\left({N}\in {Z}\wedge {k}\in \left({M}\dots {N}\right)\right)\to \left({Z}×\left\{1\right\}\right)\left({k}\right)=1$
12 3 5 11 seqid3 ${⊢}{N}\in {Z}\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({N}\right)=1$