Metamath Proof Explorer

Theorem seqshft

Description: Shifting the index set of a sequence. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 27-Feb-2014)

Ref Expression
Hypothesis seqshft.1 ⊢ 𝐹 ∈ V
Assertion seqshft ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq 𝑀 ( + , ( 𝐹 shift 𝑁 ) ) = ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) )

Proof

Step Hyp Ref Expression
1 seqshft.1 ⊢ 𝐹 ∈ V
2 seqfn ⊢ ( 𝑀 ∈ ℤ → seq 𝑀 ( + , ( 𝐹 shift 𝑁 ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
3 2 adantr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq 𝑀 ( + , ( 𝐹 shift 𝑁 ) ) Fn ( ℤ≥ ‘ 𝑀 ) )
4 zsubcl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 − 𝑁 ) ∈ ℤ )
5 seqfn ⊢ ( ( 𝑀 − 𝑁 ) ∈ ℤ → seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) Fn ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) )
6 4 5 syl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) Fn ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) )
7 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
8 7 adantl ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℂ )
9 seqex ⊢ seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) ∈ V
10 9 shftfn ⊢ ( ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) Fn ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) ∧ 𝑁 ∈ ℂ ) → ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) } )
11 6 8 10 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) } )
12 simpr ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
13 shftuz ⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑀 − 𝑁 ) ∈ ℤ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) } = ( ℤ≥ ‘ ( ( 𝑀 − 𝑁 ) + 𝑁 ) ) )
14 12 4 13 syl2anc ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) } = ( ℤ≥ ‘ ( ( 𝑀 − 𝑁 ) + 𝑁 ) ) )
15 zcn ⊢ ( 𝑀 ∈ ℤ → 𝑀 ∈ ℂ )
16 npcan ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
17 15 7 16 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( 𝑀 − 𝑁 ) + 𝑁 ) = 𝑀 )
18 17 fveq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ℤ≥ ‘ ( ( 𝑀 − 𝑁 ) + 𝑁 ) ) = ( ℤ≥ ‘ 𝑀 ) )
19 14 18 eqtrd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) } = ( ℤ≥ ‘ 𝑀 ) )
20 19 fneq2d ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) Fn { 𝑥 ∈ ℂ ∣ ( 𝑥 − 𝑁 ) ∈ ( ℤ≥ ‘ ( 𝑀 − 𝑁 ) ) } ↔ ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) Fn ( ℤ≥ ‘ 𝑀 ) ) )
21 11 20 mpbid ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) Fn ( ℤ≥ ‘ 𝑀 ) )
22 negsub ⊢ ( ( 𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
23 15 7 22 syl2an ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
24 23 adantr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑀 + - 𝑁 ) = ( 𝑀 − 𝑁 ) )
25 24 seqeq1d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → seq ( 𝑀 + - 𝑁 ) ( + , 𝐹 ) = seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) )
26 eluzelcn ⊢ ( 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) → 𝑧 ∈ ℂ )
27 negsub ⊢ ( ( 𝑧 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑧 + - 𝑁 ) = ( 𝑧 − 𝑁 ) )
28 26 8 27 syl2anr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( 𝑧 + - 𝑁 ) = ( 𝑧 − 𝑁 ) )
29 25 28 fveq12d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq ( 𝑀 + - 𝑁 ) ( + , 𝐹 ) ‘ ( 𝑧 + - 𝑁 ) ) = ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) ‘ ( 𝑧 − 𝑁 ) ) )
30 simpr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) )
31 znegcl ⊢ ( 𝑁 ∈ ℤ → - 𝑁 ∈ ℤ )
32 31 ad2antlr ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → - 𝑁 ∈ ℤ )
33 elfzelz ⊢ ( 𝑦 ∈ ( 𝑀 ... 𝑧 ) → 𝑦 ∈ ℤ )
34 33 zcnd ⊢ ( 𝑦 ∈ ( 𝑀 ... 𝑧 ) → 𝑦 ∈ ℂ )
35 1 shftval ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 − 𝑁 ) ) )
36 negsub ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝑁 ∈ ℂ ) → ( 𝑦 + - 𝑁 ) = ( 𝑦 − 𝑁 ) )
37 36 ancoms ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝑦 + - 𝑁 ) = ( 𝑦 − 𝑁 ) )
38 37 fveq2d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 𝐹 ‘ ( 𝑦 + - 𝑁 ) ) = ( 𝐹 ‘ ( 𝑦 − 𝑁 ) ) )
39 35 38 eqtr4d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 + - 𝑁 ) ) )
40 7 34 39 syl2an ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑦 ∈ ( 𝑀 ... 𝑧 ) ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 + - 𝑁 ) ) )
41 40 ad4ant24 ⊢ ( ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) ∧ 𝑦 ∈ ( 𝑀 ... 𝑧 ) ) → ( ( 𝐹 shift 𝑁 ) ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑦 + - 𝑁 ) ) )
42 30 32 41 seqshft2 ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , ( 𝐹 shift 𝑁 ) ) ‘ 𝑧 ) = ( seq ( 𝑀 + - 𝑁 ) ( + , 𝐹 ) ‘ ( 𝑧 + - 𝑁 ) ) )
43 9 shftval ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑧 ∈ ℂ ) → ( ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) ‘ 𝑧 ) = ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) ‘ ( 𝑧 − 𝑁 ) ) )
44 8 26 43 syl2an ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) ‘ 𝑧 ) = ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) ‘ ( 𝑧 − 𝑁 ) ) )
45 29 42 44 3eqtr4d ⊢ ( ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) ∧ 𝑧 ∈ ( ℤ≥ ‘ 𝑀 ) ) → ( seq 𝑀 ( + , ( 𝐹 shift 𝑁 ) ) ‘ 𝑧 ) = ( ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) ‘ 𝑧 ) )
46 3 21 45 eqfnfvd ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → seq 𝑀 ( + , ( 𝐹 shift 𝑁 ) ) = ( seq ( 𝑀 − 𝑁 ) ( + , 𝐹 ) shift 𝑁 ) )