Step | Hyp | Ref
| Expression |
1 | | seqfn 13611 |
. . 3
⊢ (𝑀 ∈ ℤ → seq𝑀( + , (𝐹 shift 𝑁)) Fn (ℤ≥‘𝑀)) |
2 | 1 | adantr 484 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → seq𝑀( + , (𝐹 shift 𝑁)) Fn (ℤ≥‘𝑀)) |
3 | | zsubcl 12244 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 − 𝑁) ∈ ℤ) |
4 | | seqfn 13611 |
. . . . 5
⊢ ((𝑀 − 𝑁) ∈ ℤ → seq(𝑀 − 𝑁)( + , 𝐹) Fn (ℤ≥‘(𝑀 − 𝑁))) |
5 | 3, 4 | syl 17 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
seq(𝑀 − 𝑁)( + , 𝐹) Fn (ℤ≥‘(𝑀 − 𝑁))) |
6 | | zcn 12206 |
. . . . 5
⊢ (𝑁 ∈ ℤ → 𝑁 ∈
ℂ) |
7 | 6 | adantl 485 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℂ) |
8 | | seqex 13601 |
. . . . 5
⊢ seq(𝑀 − 𝑁)( + , 𝐹) ∈ V |
9 | 8 | shftfn 14661 |
. . . 4
⊢
((seq(𝑀 −
𝑁)( + , 𝐹) Fn (ℤ≥‘(𝑀 − 𝑁)) ∧ 𝑁 ∈ ℂ) → (seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁) Fn {𝑥 ∈ ℂ ∣ (𝑥 − 𝑁) ∈
(ℤ≥‘(𝑀 − 𝑁))}) |
10 | 5, 7, 9 | syl2anc 587 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁) Fn {𝑥 ∈ ℂ ∣ (𝑥 − 𝑁) ∈
(ℤ≥‘(𝑀 − 𝑁))}) |
11 | | simpr 488 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → 𝑁 ∈
ℤ) |
12 | | shftuz 14657 |
. . . . . 6
⊢ ((𝑁 ∈ ℤ ∧ (𝑀 − 𝑁) ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝑁) ∈
(ℤ≥‘(𝑀 − 𝑁))} = (ℤ≥‘((𝑀 − 𝑁) + 𝑁))) |
13 | 11, 3, 12 | syl2anc 587 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝑁) ∈
(ℤ≥‘(𝑀 − 𝑁))} = (ℤ≥‘((𝑀 − 𝑁) + 𝑁))) |
14 | | zcn 12206 |
. . . . . . 7
⊢ (𝑀 ∈ ℤ → 𝑀 ∈
ℂ) |
15 | | npcan 11112 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑀 − 𝑁) + 𝑁) = 𝑀) |
16 | 14, 6, 15 | syl2an 599 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → ((𝑀 − 𝑁) + 𝑁) = 𝑀) |
17 | 16 | fveq2d 6740 |
. . . . 5
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(ℤ≥‘((𝑀 − 𝑁) + 𝑁)) = (ℤ≥‘𝑀)) |
18 | 13, 17 | eqtrd 2778 |
. . . 4
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → {𝑥 ∈ ℂ ∣ (𝑥 − 𝑁) ∈
(ℤ≥‘(𝑀 − 𝑁))} = (ℤ≥‘𝑀)) |
19 | 18 | fneq2d 6491 |
. . 3
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
((seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁) Fn {𝑥 ∈ ℂ ∣ (𝑥 − 𝑁) ∈
(ℤ≥‘(𝑀 − 𝑁))} ↔ (seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁) Fn (ℤ≥‘𝑀))) |
20 | 10, 19 | mpbid 235 |
. 2
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) →
(seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁) Fn (ℤ≥‘𝑀)) |
21 | | negsub 11151 |
. . . . . . 7
⊢ ((𝑀 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑀 + -𝑁) = (𝑀 − 𝑁)) |
22 | 14, 6, 21 | syl2an 599 |
. . . . . 6
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑀 + -𝑁) = (𝑀 − 𝑁)) |
23 | 22 | adantr 484 |
. . . . 5
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → (𝑀 + -𝑁) = (𝑀 − 𝑁)) |
24 | 23 | seqeq1d 13605 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → seq(𝑀 + -𝑁)( + , 𝐹) = seq(𝑀 − 𝑁)( + , 𝐹)) |
25 | | eluzelcn 12475 |
. . . . 5
⊢ (𝑧 ∈
(ℤ≥‘𝑀) → 𝑧 ∈ ℂ) |
26 | | negsub 11151 |
. . . . 5
⊢ ((𝑧 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑧 + -𝑁) = (𝑧 − 𝑁)) |
27 | 25, 7, 26 | syl2anr 600 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → (𝑧 + -𝑁) = (𝑧 − 𝑁)) |
28 | 24, 27 | fveq12d 6743 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → (seq(𝑀 + -𝑁)( + , 𝐹)‘(𝑧 + -𝑁)) = (seq(𝑀 − 𝑁)( + , 𝐹)‘(𝑧 − 𝑁))) |
29 | | simpr 488 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → 𝑧 ∈ (ℤ≥‘𝑀)) |
30 | | znegcl 12237 |
. . . . 5
⊢ (𝑁 ∈ ℤ → -𝑁 ∈
ℤ) |
31 | 30 | ad2antlr 727 |
. . . 4
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → -𝑁 ∈ ℤ) |
32 | | elfzelz 13137 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑀...𝑧) → 𝑦 ∈ ℤ) |
33 | 32 | zcnd 12308 |
. . . . . 6
⊢ (𝑦 ∈ (𝑀...𝑧) → 𝑦 ∈ ℂ) |
34 | | seqshft.1 |
. . . . . . . 8
⊢ 𝐹 ∈ V |
35 | 34 | shftval 14662 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐹 shift 𝑁)‘𝑦) = (𝐹‘(𝑦 − 𝑁))) |
36 | | negsub 11151 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 𝑁 ∈ ℂ) → (𝑦 + -𝑁) = (𝑦 − 𝑁)) |
37 | 36 | ancoms 462 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑦 + -𝑁) = (𝑦 − 𝑁)) |
38 | 37 | fveq2d 6740 |
. . . . . . 7
⊢ ((𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝐹‘(𝑦 + -𝑁)) = (𝐹‘(𝑦 − 𝑁))) |
39 | 35, 38 | eqtr4d 2781 |
. . . . . 6
⊢ ((𝑁 ∈ ℂ ∧ 𝑦 ∈ ℂ) → ((𝐹 shift 𝑁)‘𝑦) = (𝐹‘(𝑦 + -𝑁))) |
40 | 6, 33, 39 | syl2an 599 |
. . . . 5
⊢ ((𝑁 ∈ ℤ ∧ 𝑦 ∈ (𝑀...𝑧)) → ((𝐹 shift 𝑁)‘𝑦) = (𝐹‘(𝑦 + -𝑁))) |
41 | 40 | ad4ant24 754 |
. . . 4
⊢ ((((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) ∧ 𝑦 ∈ (𝑀...𝑧)) → ((𝐹 shift 𝑁)‘𝑦) = (𝐹‘(𝑦 + -𝑁))) |
42 | 29, 31, 41 | seqshft2 13627 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → (seq𝑀( + , (𝐹 shift 𝑁))‘𝑧) = (seq(𝑀 + -𝑁)( + , 𝐹)‘(𝑧 + -𝑁))) |
43 | 8 | shftval 14662 |
. . . 4
⊢ ((𝑁 ∈ ℂ ∧ 𝑧 ∈ ℂ) →
((seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁)‘𝑧) = (seq(𝑀 − 𝑁)( + , 𝐹)‘(𝑧 − 𝑁))) |
44 | 7, 25, 43 | syl2an 599 |
. . 3
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → ((seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁)‘𝑧) = (seq(𝑀 − 𝑁)( + , 𝐹)‘(𝑧 − 𝑁))) |
45 | 28, 42, 44 | 3eqtr4d 2788 |
. 2
⊢ (((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ 𝑧 ∈
(ℤ≥‘𝑀)) → (seq𝑀( + , (𝐹 shift 𝑁))‘𝑧) = ((seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁)‘𝑧)) |
46 | 2, 20, 45 | eqfnfvd 6874 |
1
⊢ ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → seq𝑀( + , (𝐹 shift 𝑁)) = (seq(𝑀 − 𝑁)( + , 𝐹) shift 𝑁)) |