# 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
`|- ( ( ph /\ x e. S ) -> ( Z .+ x ) = x )`
seqid.2
`|- ( ph -> Z e. S )`
seqid.3
`|- ( ph -> N e. ( ZZ>= ` M ) )`
seqid.4
`|- ( ph -> ( F ` N ) e. S )`
seqid.5
`|- ( ( ph /\ x e. ( M ... ( N - 1 ) ) ) -> ( F ` x ) = Z )`
Assertion seqid
`|- ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` N ) ) = seq N ( .+ , F ) )`

### Proof

Step Hyp Ref Expression
1 seqid.1
` |-  ( ( ph /\ x e. S ) -> ( Z .+ x ) = x )`
2 seqid.2
` |-  ( ph -> Z e. S )`
3 seqid.3
` |-  ( ph -> N e. ( ZZ>= ` M ) )`
4 seqid.4
` |-  ( ph -> ( F ` N ) e. S )`
5 seqid.5
` |-  ( ( ph /\ x e. ( M ... ( N - 1 ) ) ) -> ( F ` x ) = Z )`
6 eluzelz
` |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )`
7 seq1
` |-  ( N e. ZZ -> ( seq N ( .+ , F ) ` N ) = ( F ` N ) )`
8 3 6 7 3syl
` |-  ( ph -> ( seq N ( .+ , F ) ` N ) = ( F ` N ) )`
9 seqeq1
` |-  ( N = M -> seq N ( .+ , F ) = seq M ( .+ , F ) )`
10 9 fveq1d
` |-  ( N = M -> ( seq N ( .+ , F ) ` N ) = ( seq M ( .+ , F ) ` N ) )`
11 10 eqeq1d
` |-  ( N = M -> ( ( seq N ( .+ , F ) ` N ) = ( F ` N ) <-> ( seq M ( .+ , F ) ` N ) = ( F ` N ) ) )`
12 8 11 syl5ibcom
` |-  ( ph -> ( N = M -> ( seq M ( .+ , F ) ` N ) = ( F ` N ) ) )`
13 eluzel2
` |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )`
14 3 13 syl
` |-  ( ph -> M e. ZZ )`
15 seqm1
` |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )`
16 14 15 sylan
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` N ) = ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) )`
17 oveq2
` |-  ( x = Z -> ( Z .+ x ) = ( Z .+ Z ) )`
18 id
` |-  ( x = Z -> x = Z )`
19 17 18 eqeq12d
` |-  ( x = Z -> ( ( Z .+ x ) = x <-> ( Z .+ Z ) = Z ) )`
20 1 ralrimiva
` |-  ( ph -> A. x e. S ( Z .+ x ) = x )`
21 19 20 2 rspcdva
` |-  ( ph -> ( Z .+ Z ) = Z )`
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( Z .+ Z ) = Z )`
23 eluzp1m1
` |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )`
24 14 23 sylan
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` M ) )`
` |-  ( ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) /\ x e. ( M ... ( N - 1 ) ) ) -> ( F ` x ) = Z )`
26 22 24 25 seqid3
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` ( N - 1 ) ) = Z )`
27 26 oveq1d
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( seq M ( .+ , F ) ` ( N - 1 ) ) .+ ( F ` N ) ) = ( Z .+ ( F ` N ) ) )`
28 oveq2
` |-  ( x = ( F ` N ) -> ( Z .+ x ) = ( Z .+ ( F ` N ) ) )`
29 id
` |-  ( x = ( F ` N ) -> x = ( F ` N ) )`
30 28 29 eqeq12d
` |-  ( x = ( F ` N ) -> ( ( Z .+ x ) = x <-> ( Z .+ ( F ` N ) ) = ( F ` N ) ) )`
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> A. x e. S ( Z .+ x ) = x )`
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( F ` N ) e. S )`
33 30 31 32 rspcdva
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( Z .+ ( F ` N ) ) = ( F ` N ) )`
34 16 27 33 3eqtrd
` |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> ( seq M ( .+ , F ) ` N ) = ( F ` N ) )`
35 34 ex
` |-  ( ph -> ( N e. ( ZZ>= ` ( M + 1 ) ) -> ( seq M ( .+ , F ) ` N ) = ( F ` N ) ) )`
36 uzp1
` |-  ( N e. ( ZZ>= ` M ) -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )`
37 3 36 syl
` |-  ( ph -> ( N = M \/ N e. ( ZZ>= ` ( M + 1 ) ) ) )`
38 12 35 37 mpjaod
` |-  ( ph -> ( seq M ( .+ , F ) ` N ) = ( F ` N ) )`
39 eqidd
` |-  ( ( ph /\ x e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` x ) = ( F ` x ) )`
40 3 38 39 seqfeq2
` |-  ( ph -> ( seq M ( .+ , F ) |` ( ZZ>= ` N ) ) = seq N ( .+ , F ) )`