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 𝑁 ( + , 𝐹 ) )