# Metamath Proof Explorer

## Theorem prodf1f

Description: A one-valued infinite product is equal to the constant one function. (Contributed by Scott Fenton, 5-Dec-2017)

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

### Proof

Step Hyp Ref Expression
1 prodf1.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 1 prodf1 ${⊢}{k}\in {Z}\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({k}\right)=1$
3 1ex ${⊢}1\in \mathrm{V}$
4 3 fvconst2 ${⊢}{k}\in {Z}\to \left({Z}×\left\{1\right\}\right)\left({k}\right)=1$
5 2 4 eqtr4d ${⊢}{k}\in {Z}\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({k}\right)=\left({Z}×\left\{1\right\}\right)\left({k}\right)$
6 5 rgen ${⊢}\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({k}\right)=\left({Z}×\left\{1\right\}\right)\left({k}\right)$
7 seqfn ${⊢}{M}\in ℤ\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)Fn{ℤ}_{\ge {M}}$
8 1 fneq2i ${⊢}seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)Fn{Z}↔seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)Fn{ℤ}_{\ge {M}}$
9 7 8 sylibr ${⊢}{M}\in ℤ\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)Fn{Z}$
10 3 fconst ${⊢}\left({Z}×\left\{1\right\}\right):{Z}⟶\left\{1\right\}$
11 ffn ${⊢}\left({Z}×\left\{1\right\}\right):{Z}⟶\left\{1\right\}\to \left({Z}×\left\{1\right\}\right)Fn{Z}$
12 10 11 ax-mp ${⊢}\left({Z}×\left\{1\right\}\right)Fn{Z}$
13 eqfnfv ${⊢}\left(seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)Fn{Z}\wedge \left({Z}×\left\{1\right\}\right)Fn{Z}\right)\to \left(seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)={Z}×\left\{1\right\}↔\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({k}\right)=\left({Z}×\left\{1\right\}\right)\left({k}\right)\right)$
14 9 12 13 sylancl ${⊢}{M}\in ℤ\to \left(seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)={Z}×\left\{1\right\}↔\forall {k}\in {Z}\phantom{\rule{.4em}{0ex}}seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)\left({k}\right)=\left({Z}×\left\{1\right\}\right)\left({k}\right)\right)$
15 6 14 mpbiri ${⊢}{M}\in ℤ\to seq{M}\left(×,\left({Z}×\left\{1\right\}\right)\right)={Z}×\left\{1\right\}$