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 )
22 21 adantr 
 |-  ( ( 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 ) )
25 5 adantlr 
 |-  ( ( ( 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 ) ) )
31 20 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> A. x e. S ( Z .+ x ) = x )
32 4 adantr 
 |-  ( ( 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 ) )