# 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 ( 𝜑𝑍𝑆 )
seqid.3 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
seqid.4 ( 𝜑 → ( 𝐹𝑁 ) ∈ 𝑆 )
seqid.5 ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑥 ) = 𝑍 )
Assertion seqid ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ𝑁 ) ) = seq 𝑁 ( + , 𝐹 ) )

### Proof

Step Hyp Ref Expression
1 seqid.1 ( ( 𝜑𝑥𝑆 ) → ( 𝑍 + 𝑥 ) = 𝑥 )
2 seqid.2 ( 𝜑𝑍𝑆 )
3 seqid.3 ( 𝜑𝑁 ∈ ( ℤ𝑀 ) )
4 seqid.4 ( 𝜑 → ( 𝐹𝑁 ) ∈ 𝑆 )
5 seqid.5 ( ( 𝜑𝑥 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑥 ) = 𝑍 )
6 eluzelz ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑁 ∈ ℤ )
7 seq1 ( 𝑁 ∈ ℤ → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) )
8 3 6 7 3syl ( 𝜑 → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) )
9 seqeq1 ( 𝑁 = 𝑀 → seq 𝑁 ( + , 𝐹 ) = seq 𝑀 ( + , 𝐹 ) )
10 9 fveq1d ( 𝑁 = 𝑀 → ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) = ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) )
11 10 eqeq1d ( 𝑁 = 𝑀 → ( ( seq 𝑁 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) ↔ ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) ) )
12 8 11 syl5ibcom ( 𝜑 → ( 𝑁 = 𝑀 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) ) )
13 eluzel2 ( 𝑁 ∈ ( ℤ𝑀 ) → 𝑀 ∈ ℤ )
14 3 13 syl ( 𝜑𝑀 ∈ ℤ )
15 seqm1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹𝑁 ) ) )
16 14 15 sylan ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹𝑁 ) ) )
17 oveq2 ( 𝑥 = 𝑍 → ( 𝑍 + 𝑥 ) = ( 𝑍 + 𝑍 ) )
18 id ( 𝑥 = 𝑍𝑥 = 𝑍 )
19 17 18 eqeq12d ( 𝑥 = 𝑍 → ( ( 𝑍 + 𝑥 ) = 𝑥 ↔ ( 𝑍 + 𝑍 ) = 𝑍 ) )
20 1 ralrimiva ( 𝜑 → ∀ 𝑥𝑆 ( 𝑍 + 𝑥 ) = 𝑥 )
21 19 20 2 rspcdva ( 𝜑 → ( 𝑍 + 𝑍 ) = 𝑍 )
22 21 adantr ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑍 + 𝑍 ) = 𝑍 )
23 eluzp1m1 ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ𝑀 ) )
24 14 23 sylan ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑁 − 1 ) ∈ ( ℤ𝑀 ) )
25 5 adantlr ( ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) ∧ 𝑥 ∈ ( 𝑀 ... ( 𝑁 − 1 ) ) ) → ( 𝐹𝑥 ) = 𝑍 )
26 22 24 25 seqid3 ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) = 𝑍 )
27 26 oveq1d ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( ( seq 𝑀 ( + , 𝐹 ) ‘ ( 𝑁 − 1 ) ) + ( 𝐹𝑁 ) ) = ( 𝑍 + ( 𝐹𝑁 ) ) )
28 oveq2 ( 𝑥 = ( 𝐹𝑁 ) → ( 𝑍 + 𝑥 ) = ( 𝑍 + ( 𝐹𝑁 ) ) )
29 id ( 𝑥 = ( 𝐹𝑁 ) → 𝑥 = ( 𝐹𝑁 ) )
30 28 29 eqeq12d ( 𝑥 = ( 𝐹𝑁 ) → ( ( 𝑍 + 𝑥 ) = 𝑥 ↔ ( 𝑍 + ( 𝐹𝑁 ) ) = ( 𝐹𝑁 ) ) )
31 20 adantr ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ∀ 𝑥𝑆 ( 𝑍 + 𝑥 ) = 𝑥 )
32 4 adantr ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( 𝐹𝑁 ) ∈ 𝑆 )
33 30 31 32 rspcdva ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( 𝑍 + ( 𝐹𝑁 ) ) = ( 𝐹𝑁 ) )
34 16 27 33 3eqtrd ( ( 𝜑𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) )
35 34 ex ( 𝜑 → ( 𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) ) )
36 uzp1 ( 𝑁 ∈ ( ℤ𝑀 ) → ( 𝑁 = 𝑀𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
37 3 36 syl ( 𝜑 → ( 𝑁 = 𝑀𝑁 ∈ ( ℤ ‘ ( 𝑀 + 1 ) ) ) )
38 12 35 37 mpjaod ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ‘ 𝑁 ) = ( 𝐹𝑁 ) )
39 eqidd ( ( 𝜑𝑥 ∈ ( ℤ ‘ ( 𝑁 + 1 ) ) ) → ( 𝐹𝑥 ) = ( 𝐹𝑥 ) )
40 3 38 39 seqfeq2 ( 𝜑 → ( seq 𝑀 ( + , 𝐹 ) ↾ ( ℤ𝑁 ) ) = seq 𝑁 ( + , 𝐹 ) )