# Metamath Proof Explorer

## Theorem fprodm1

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

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

### Proof

Step Hyp Ref Expression
1 fprodm1.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 fprodm1.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {A}\in ℂ$
3 fprodm1.3 ${⊢}{k}={N}\to {A}={B}$
4 fzp1nel ${⊢}¬{N}-1+1\in \left({M}\dots {N}-1\right)$
5 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
6 1 5 syl ${⊢}{\phi }\to {N}\in ℤ$
7 6 zcnd ${⊢}{\phi }\to {N}\in ℂ$
8 1cnd ${⊢}{\phi }\to 1\in ℂ$
9 7 8 npcand ${⊢}{\phi }\to {N}-1+1={N}$
10 9 eleq1d ${⊢}{\phi }\to \left({N}-1+1\in \left({M}\dots {N}-1\right)↔{N}\in \left({M}\dots {N}-1\right)\right)$
11 4 10 mtbii ${⊢}{\phi }\to ¬{N}\in \left({M}\dots {N}-1\right)$
12 disjsn ${⊢}\left({M}\dots {N}-1\right)\cap \left\{{N}\right\}=\varnothing ↔¬{N}\in \left({M}\dots {N}-1\right)$
13 11 12 sylibr ${⊢}{\phi }\to \left({M}\dots {N}-1\right)\cap \left\{{N}\right\}=\varnothing$
14 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
15 1 14 syl ${⊢}{\phi }\to {M}\in ℤ$
16 peano2zm ${⊢}{M}\in ℤ\to {M}-1\in ℤ$
17 15 16 syl ${⊢}{\phi }\to {M}-1\in ℤ$
18 15 zcnd ${⊢}{\phi }\to {M}\in ℂ$
19 18 8 npcand ${⊢}{\phi }\to {M}-1+1={M}$
20 19 fveq2d ${⊢}{\phi }\to {ℤ}_{\ge \left({M}-1+1\right)}={ℤ}_{\ge {M}}$
21 1 20 eleqtrrd ${⊢}{\phi }\to {N}\in {ℤ}_{\ge \left({M}-1+1\right)}$
22 eluzp1m1 ${⊢}\left({M}-1\in ℤ\wedge {N}\in {ℤ}_{\ge \left({M}-1+1\right)}\right)\to {N}-1\in {ℤ}_{\ge \left({M}-1\right)}$
23 17 21 22 syl2anc ${⊢}{\phi }\to {N}-1\in {ℤ}_{\ge \left({M}-1\right)}$
24 fzsuc2 ${⊢}\left({M}\in ℤ\wedge {N}-1\in {ℤ}_{\ge \left({M}-1\right)}\right)\to \left({M}\dots {N}-1+1\right)=\left({M}\dots {N}-1\right)\cup \left\{{N}-1+1\right\}$
25 15 23 24 syl2anc ${⊢}{\phi }\to \left({M}\dots {N}-1+1\right)=\left({M}\dots {N}-1\right)\cup \left\{{N}-1+1\right\}$
26 9 oveq2d ${⊢}{\phi }\to \left({M}\dots {N}-1+1\right)=\left({M}\dots {N}\right)$
27 9 sneqd ${⊢}{\phi }\to \left\{{N}-1+1\right\}=\left\{{N}\right\}$
28 27 uneq2d ${⊢}{\phi }\to \left({M}\dots {N}-1\right)\cup \left\{{N}-1+1\right\}=\left({M}\dots {N}-1\right)\cup \left\{{N}\right\}$
29 25 26 28 3eqtr3d ${⊢}{\phi }\to \left({M}\dots {N}\right)=\left({M}\dots {N}-1\right)\cup \left\{{N}\right\}$
30 fzfid ${⊢}{\phi }\to \left({M}\dots {N}\right)\in \mathrm{Fin}$
31 13 29 30 2 fprodsplit ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}}{A}=\prod _{{k}={M}}^{{N}-1}{A}\prod _{{k}\in \left\{{N}\right\}}{A}$
32 3 eleq1d ${⊢}{k}={N}\to \left({A}\in ℂ↔{B}\in ℂ\right)$
33 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
34 eluzfz2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in \left({M}\dots {N}\right)$
35 1 34 syl ${⊢}{\phi }\to {N}\in \left({M}\dots {N}\right)$
36 32 33 35 rspcdva ${⊢}{\phi }\to {B}\in ℂ$
37 3 prodsn ${⊢}\left({N}\in {ℤ}_{\ge {M}}\wedge {B}\in ℂ\right)\to \prod _{{k}\in \left\{{N}\right\}}{A}={B}$
38 1 36 37 syl2anc ${⊢}{\phi }\to \prod _{{k}\in \left\{{N}\right\}}{A}={B}$
39 38 oveq2d ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}-1}{A}\prod _{{k}\in \left\{{N}\right\}}{A}=\prod _{{k}={M}}^{{N}-1}{A}{B}$
40 31 39 eqtrd ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}}{A}=\prod _{{k}={M}}^{{N}-1}{A}{B}$