# Metamath Proof Explorer

## Theorem fprodp1

Description: Multiply in the last term in a finite product. (Contributed by Scott Fenton, 24-Dec-2017)

Ref Expression
Hypotheses fprodp1.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
fprodp1.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}+1\right)\right)\to {A}\in ℂ$
fprodp1.3 ${⊢}{k}={N}+1\to {A}={B}$
Assertion fprodp1 ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}+1}{A}=\prod _{{k}={M}}^{{N}}{A}{B}$

### Proof

Step Hyp Ref Expression
1 fprodp1.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 fprodp1.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}+1\right)\right)\to {A}\in ℂ$
3 fprodp1.3 ${⊢}{k}={N}+1\to {A}={B}$
4 peano2uz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}+1\in {ℤ}_{\ge {M}}$
5 1 4 syl ${⊢}{\phi }\to {N}+1\in {ℤ}_{\ge {M}}$
6 5 2 3 fprodm1 ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}+1}{A}=\prod _{{k}={M}}^{{N}+1-1}{A}{B}$
7 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
8 1 7 syl ${⊢}{\phi }\to {N}\in ℤ$
9 8 zcnd ${⊢}{\phi }\to {N}\in ℂ$
10 1cnd ${⊢}{\phi }\to 1\in ℂ$
11 9 10 pncand ${⊢}{\phi }\to {N}+1-1={N}$
12 11 oveq2d ${⊢}{\phi }\to \left({M}\dots {N}+1-1\right)=\left({M}\dots {N}\right)$
13 12 prodeq1d ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}+1-1}{A}=\prod _{{k}={M}}^{{N}}{A}$
14 13 oveq1d ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}+1-1}{A}{B}=\prod _{{k}={M}}^{{N}}{A}{B}$
15 6 14 eqtrd ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}+1}{A}=\prod _{{k}={M}}^{{N}}{A}{B}$