# Metamath Proof Explorer

## Theorem seqid3

Description: A sequence that consists entirely of "zeroes" sums to "zero". More precisely, a constant sequence with value an element which is a .+ -idempotent sums (or " .+ 's") to that element. (Contributed by Mario Carneiro, 15-Dec-2014)

Ref Expression
Hypotheses seqid3.1
seqid3.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
seqid3.3 ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {F}\left({x}\right)={Z}$
Assertion seqid3

### Proof

Step Hyp Ref Expression
1 seqid3.1
2 seqid3.2 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
3 seqid3.3 ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {F}\left({x}\right)={Z}$
4 fvex ${⊢}{F}\left({x}\right)\in \mathrm{V}$
5 4 elsn ${⊢}{F}\left({x}\right)\in \left\{{Z}\right\}↔{F}\left({x}\right)={Z}$
6 3 5 sylibr ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}\right)\right)\to {F}\left({x}\right)\in \left\{{Z}\right\}$
7 ovex
8 7 elsn
9 1 8 sylibr
10 elsni ${⊢}{x}\in \left\{{Z}\right\}\to {x}={Z}$
11 elsni ${⊢}{y}\in \left\{{Z}\right\}\to {y}={Z}$
12 10 11 oveqan12d
13 12 eleq1d
14 9 13 syl5ibrcom
15 14 imp
16 2 6 15 seqcl
17 elsni
18 16 17 syl