# Metamath Proof Explorer

## Theorem fprod1p

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

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

### Proof

Step Hyp Ref Expression
1 fprod1p.1 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
2 fprod1p.2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {A}\in ℂ$
3 fprod1p.3 ${⊢}{k}={M}\to {A}={B}$
4 eluzfz1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in \left({M}\dots {N}\right)$
5 1 4 syl ${⊢}{\phi }\to {M}\in \left({M}\dots {N}\right)$
6 elfzelz ${⊢}{M}\in \left({M}\dots {N}\right)\to {M}\in ℤ$
7 5 6 syl ${⊢}{\phi }\to {M}\in ℤ$
8 fzsn ${⊢}{M}\in ℤ\to \left({M}\dots {M}\right)=\left\{{M}\right\}$
9 7 8 syl ${⊢}{\phi }\to \left({M}\dots {M}\right)=\left\{{M}\right\}$
10 9 ineq1d ${⊢}{\phi }\to \left({M}\dots {M}\right)\cap \left({M}+1\dots {N}\right)=\left\{{M}\right\}\cap \left({M}+1\dots {N}\right)$
11 7 zred ${⊢}{\phi }\to {M}\in ℝ$
12 11 ltp1d ${⊢}{\phi }\to {M}<{M}+1$
13 fzdisj ${⊢}{M}<{M}+1\to \left({M}\dots {M}\right)\cap \left({M}+1\dots {N}\right)=\varnothing$
14 12 13 syl ${⊢}{\phi }\to \left({M}\dots {M}\right)\cap \left({M}+1\dots {N}\right)=\varnothing$
15 10 14 eqtr3d ${⊢}{\phi }\to \left\{{M}\right\}\cap \left({M}+1\dots {N}\right)=\varnothing$
16 fzsplit ${⊢}{M}\in \left({M}\dots {N}\right)\to \left({M}\dots {N}\right)=\left({M}\dots {M}\right)\cup \left({M}+1\dots {N}\right)$
17 5 16 syl ${⊢}{\phi }\to \left({M}\dots {N}\right)=\left({M}\dots {M}\right)\cup \left({M}+1\dots {N}\right)$
18 9 uneq1d ${⊢}{\phi }\to \left({M}\dots {M}\right)\cup \left({M}+1\dots {N}\right)=\left\{{M}\right\}\cup \left({M}+1\dots {N}\right)$
19 17 18 eqtrd ${⊢}{\phi }\to \left({M}\dots {N}\right)=\left\{{M}\right\}\cup \left({M}+1\dots {N}\right)$
20 fzfid ${⊢}{\phi }\to \left({M}\dots {N}\right)\in \mathrm{Fin}$
21 15 19 20 2 fprodsplit ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}}{A}=\prod _{{k}\in \left\{{M}\right\}}{A}\prod _{{k}={M}+1}^{{N}}{A}$
22 3 eleq1d ${⊢}{k}={M}\to \left({A}\in ℂ↔{B}\in ℂ\right)$
23 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
24 22 23 5 rspcdva ${⊢}{\phi }\to {B}\in ℂ$
25 3 prodsn ${⊢}\left({M}\in \left({M}\dots {N}\right)\wedge {B}\in ℂ\right)\to \prod _{{k}\in \left\{{M}\right\}}{A}={B}$
26 5 24 25 syl2anc ${⊢}{\phi }\to \prod _{{k}\in \left\{{M}\right\}}{A}={B}$
27 26 oveq1d ${⊢}{\phi }\to \prod _{{k}\in \left\{{M}\right\}}{A}\prod _{{k}={M}+1}^{{N}}{A}={B}\prod _{{k}={M}+1}^{{N}}{A}$
28 21 27 eqtrd ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}}{A}={B}\prod _{{k}={M}+1}^{{N}}{A}$