# Metamath Proof Explorer

## Theorem seqid

Description: Discarding the first few terms of a sequence that starts with all zeroes (or any element which is a left-identity for .+ ) has no effect on its sum. (Contributed by Mario Carneiro, 13-Jul-2013) (Revised by Mario Carneiro, 27-May-2014)

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

### Proof

Step Hyp Ref Expression
1 seqid.1
2 seqid.2 ${⊢}{\phi }\to {Z}\in {S}$
3 seqid.3 ${⊢}{\phi }\to {N}\in {ℤ}_{\ge {M}}$
4 seqid.4 ${⊢}{\phi }\to {F}\left({N}\right)\in {S}$
5 seqid.5 ${⊢}\left({\phi }\wedge {x}\in \left({M}\dots {N}-1\right)\right)\to {F}\left({x}\right)={Z}$
6 eluzelz ${⊢}{N}\in {ℤ}_{\ge {M}}\to {N}\in ℤ$
7 seq1
8 3 6 7 3syl
9 seqeq1
10 9 fveq1d
11 10 eqeq1d
12 8 11 syl5ibcom
13 eluzel2 ${⊢}{N}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
14 3 13 syl ${⊢}{\phi }\to {M}\in ℤ$
15 seqm1
16 14 15 sylan
17 oveq2
18 id ${⊢}{x}={Z}\to {x}={Z}$
19 17 18 eqeq12d
20 1 ralrimiva
21 19 20 2 rspcdva
23 eluzp1m1 ${⊢}\left({M}\in ℤ\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge {M}}$
24 14 23 sylan ${⊢}\left({\phi }\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {N}-1\in {ℤ}_{\ge {M}}$
25 5 adantlr ${⊢}\left(\left({\phi }\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\wedge {x}\in \left({M}\dots {N}-1\right)\right)\to {F}\left({x}\right)={Z}$
26 22 24 25 seqid3
27 26 oveq1d
28 oveq2
29 id ${⊢}{x}={F}\left({N}\right)\to {x}={F}\left({N}\right)$
30 28 29 eqeq12d
32 4 adantr ${⊢}\left({\phi }\wedge {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)\to {F}\left({N}\right)\in {S}$
36 uzp1 ${⊢}{N}\in {ℤ}_{\ge {M}}\to \left({N}={M}\vee {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
37 3 36 syl ${⊢}{\phi }\to \left({N}={M}\vee {N}\in {ℤ}_{\ge \left({M}+1\right)}\right)$
39 eqidd ${⊢}\left({\phi }\wedge {x}\in {ℤ}_{\ge \left({N}+1\right)}\right)\to {F}\left({x}\right)={F}\left({x}\right)$