# Metamath Proof Explorer

## Theorem fprodeq0

Description: Anything finite product containing a zero term is itself zero. (Contributed by Scott Fenton, 27-Dec-2017)

Ref Expression
Hypotheses fprodeq0.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
fprodeq0.2 ${⊢}{\phi }\to {N}\in {Z}$
fprodeq0.3 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\in ℂ$
fprodeq0.4 ${⊢}\left({\phi }\wedge {k}={N}\right)\to {A}=0$
Assertion fprodeq0 ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \prod _{{k}={M}}^{{K}}{A}=0$

### Proof

Step Hyp Ref Expression
1 fprodeq0.1 ${⊢}{Z}={ℤ}_{\ge {M}}$
2 fprodeq0.2 ${⊢}{\phi }\to {N}\in {Z}$
3 fprodeq0.3 ${⊢}\left({\phi }\wedge {k}\in {Z}\right)\to {A}\in ℂ$
4 fprodeq0.4 ${⊢}\left({\phi }\wedge {k}={N}\right)\to {A}=0$
5 eluzel2 ${⊢}{K}\in {ℤ}_{\ge {N}}\to {N}\in ℤ$
6 5 adantl ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to {N}\in ℤ$
7 6 zred ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to {N}\in ℝ$
8 7 ltp1d ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to {N}<{N}+1$
9 fzdisj ${⊢}{N}<{N}+1\to \left({M}\dots {N}\right)\cap \left({N}+1\dots {K}\right)=\varnothing$
10 8 9 syl ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \left({M}\dots {N}\right)\cap \left({N}+1\dots {K}\right)=\varnothing$
11 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
12 11 1 eleq2s ${⊢}{N}\in {Z}\to {M}\in ℤ$
13 2 12 syl ${⊢}{\phi }\to {M}\in ℤ$
14 13 adantr ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to {M}\in ℤ$
15 eluzelz ${⊢}{K}\in {ℤ}_{\ge {N}}\to {K}\in ℤ$
16 15 adantl ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to {K}\in ℤ$
17 14 16 6 3jca ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \left({M}\in ℤ\wedge {K}\in ℤ\wedge {N}\in ℤ\right)$
18 eluzle ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\le {N}$
19 18 1 eleq2s ${⊢}{N}\in {Z}\to {M}\le {N}$
20 2 19 syl ${⊢}{\phi }\to {M}\le {N}$
21 eluzle ${⊢}{K}\in {ℤ}_{\ge {N}}\to {N}\le {K}$
22 20 21 anim12i ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \left({M}\le {N}\wedge {N}\le {K}\right)$
23 elfz2 ${⊢}{N}\in \left({M}\dots {K}\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\le {N}\wedge {N}\le {K}\right)\right)$
24 17 22 23 sylanbrc ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to {N}\in \left({M}\dots {K}\right)$
25 fzsplit ${⊢}{N}\in \left({M}\dots {K}\right)\to \left({M}\dots {K}\right)=\left({M}\dots {N}\right)\cup \left({N}+1\dots {K}\right)$
26 24 25 syl ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \left({M}\dots {K}\right)=\left({M}\dots {N}\right)\cup \left({N}+1\dots {K}\right)$
27 fzfid ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \left({M}\dots {K}\right)\in \mathrm{Fin}$
28 elfzuz ${⊢}{k}\in \left({M}\dots {K}\right)\to {k}\in {ℤ}_{\ge {M}}$
29 28 1 eleqtrrdi ${⊢}{k}\in \left({M}\dots {K}\right)\to {k}\in {Z}$
30 29 3 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {K}\right)\right)\to {A}\in ℂ$
31 30 adantlr ${⊢}\left(\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in \left({M}\dots {K}\right)\right)\to {A}\in ℂ$
32 10 26 27 31 fprodsplit ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \prod _{{k}={M}}^{{K}}{A}=\prod _{{k}={M}}^{{N}}{A}\prod _{{k}={N}+1}^{{K}}{A}$
33 2 1 eleqtrdi ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
34 elfzuz ${⊢}{k}\in \left({M}\dots {N}\right)\to {k}\in {ℤ}_{\ge {M}}$
35 34 1 eleqtrrdi ${⊢}{k}\in \left({M}\dots {N}\right)\to {k}\in {Z}$
36 35 3 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}\right)\right)\to {A}\in ℂ$
37 33 36 fprodm1s
38 2 4 csbied
39 38 oveq2d
40 fzfid ${⊢}{\phi }\to \left({M}\dots {N}-1\right)\in \mathrm{Fin}$
41 elfzuz ${⊢}{k}\in \left({M}\dots {N}-1\right)\to {k}\in {ℤ}_{\ge {M}}$
42 41 1 eleqtrrdi ${⊢}{k}\in \left({M}\dots {N}-1\right)\to {k}\in {Z}$
43 42 3 sylan2 ${⊢}\left({\phi }\wedge {k}\in \left({M}\dots {N}-1\right)\right)\to {A}\in ℂ$
44 40 43 fprodcl ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}-1}{A}\in ℂ$
45 44 mul01d ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}-1}{A}\cdot 0=0$
46 37 39 45 3eqtrd ${⊢}{\phi }\to \prod _{{k}={M}}^{{N}}{A}=0$
47 46 adantr ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \prod _{{k}={M}}^{{N}}{A}=0$
48 47 oveq1d ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \prod _{{k}={M}}^{{N}}{A}\prod _{{k}={N}+1}^{{K}}{A}=0\cdot \prod _{{k}={N}+1}^{{K}}{A}$
49 fzfid ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \left({N}+1\dots {K}\right)\in \mathrm{Fin}$
50 1 peano2uzs ${⊢}{N}\in {Z}\to {N}+1\in {Z}$
51 2 50 syl ${⊢}{\phi }\to {N}+1\in {Z}$
52 elfzuz ${⊢}{k}\in \left({N}+1\dots {K}\right)\to {k}\in {ℤ}_{\ge \left({N}+1\right)}$
53 1 uztrn2 ${⊢}\left({N}+1\in {Z}\wedge {k}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {k}\in {Z}$
54 51 52 53 syl2an ${⊢}\left({\phi }\wedge {k}\in \left({N}+1\dots {K}\right)\right)\to {k}\in {Z}$
55 54 adantrl ${⊢}\left({\phi }\wedge \left({K}\in {ℤ}_{\ge {N}}\wedge {k}\in \left({N}+1\dots {K}\right)\right)\right)\to {k}\in {Z}$
56 55 3 syldan ${⊢}\left({\phi }\wedge \left({K}\in {ℤ}_{\ge {N}}\wedge {k}\in \left({N}+1\dots {K}\right)\right)\right)\to {A}\in ℂ$
57 56 anassrs ${⊢}\left(\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\wedge {k}\in \left({N}+1\dots {K}\right)\right)\to {A}\in ℂ$
58 49 57 fprodcl ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \prod _{{k}={N}+1}^{{K}}{A}\in ℂ$
59 58 mul02d ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to 0\cdot \prod _{{k}={N}+1}^{{K}}{A}=0$
60 32 48 59 3eqtrd ${⊢}\left({\phi }\wedge {K}\in {ℤ}_{\ge {N}}\right)\to \prod _{{k}={M}}^{{K}}{A}=0$