Step | Hyp | Ref
| Expression |
1 | | isumshft.5 |
. . . . . . . . 9
|
2 | | isumshft.4 |
. . . . . . . . 9
|
3 | 1, 2 | zaddcld 10998 |
. . . . . . . 8
|
4 | | isumshft.2 |
. . . . . . . . . 10
|
5 | 4 | eleq2i 2535 |
. . . . . . . . 9
|
6 | 2 | zcnd 10995 |
. . . . . . . . . . 11
|
7 | | eluzelcn 11121 |
. . . . . . . . . . . 12
|
8 | 7, 4 | eleq2s 2565 |
. . . . . . . . . . 11
|
9 | | isumshft.1 |
. . . . . . . . . . . . . 14
|
10 | | fvex 5881 |
. . . . . . . . . . . . . 14
|
11 | 9, 10 | eqeltri 2541 |
. . . . . . . . . . . . 13
|
12 | 11 | mptex 6143 |
. . . . . . . . . . . 12
|
13 | 12 | shftval 12907 |
. . . . . . . . . . 11
|
14 | 6, 8, 13 | syl2an 477 |
. . . . . . . . . 10
|
15 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
|
16 | | eqid 2457 |
. . . . . . . . . . . . . . . . . 18
|
17 | 16 | fvmpt2i 5962 |
. . . . . . . . . . . . . . . . 17
|
18 | 15, 17 | syl 16 |
. . . . . . . . . . . . . . . 16
|
19 | | eluzelcn 11121 |
. . . . . . . . . . . . . . . . . . . . 21
|
20 | 19, 9 | eleq2s 2565 |
. . . . . . . . . . . . . . . . . . . 20
|
21 | | addcom 9787 |
. . . . . . . . . . . . . . . . . . . 20
|
22 | 6, 20, 21 | syl2an 477 |
. . . . . . . . . . . . . . . . . . 19
|
23 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
|
24 | 23, 9 | syl6eleq 2555 |
. . . . . . . . . . . . . . . . . . . 20
|
25 | | eluzadd 11138 |
. . . . . . . . . . . . . . . . . . . 20
|
26 | 24, 2, 25 | syl2anr 478 |
. . . . . . . . . . . . . . . . . . 19
|
27 | 22, 26 | eqeltrd 2545 |
. . . . . . . . . . . . . . . . . 18
|
28 | 27, 4 | syl6eleqr 2556 |
. . . . . . . . . . . . . . . . 17
|
29 | | isumshft.3 |
. . . . . . . . . . . . . . . . . 18
|
30 | | eqid 2457 |
. . . . . . . . . . . . . . . . . 18
|
31 | 29, 30 | fvmpti 5955 |
. . . . . . . . . . . . . . . . 17
|
32 | 28, 31 | syl 16 |
. . . . . . . . . . . . . . . 16
|
33 | 18, 32 | eqtr4d 2501 |
. . . . . . . . . . . . . . 15
|
34 | 33 | ralrimiva 2871 |
. . . . . . . . . . . . . 14
|
35 | | nffvmpt1 5879 |
. . . . . . . . . . . . . . . 16
|
36 | 35 | nfeq1 2634 |
. . . . . . . . . . . . . . 15
|
37 | | fveq2 5871 |
. . . . . . . . . . . . . . . 16
|
38 | | oveq2 6304 |
. . . . . . . . . . . . . . . . 17
|
39 | 38 | fveq2d 5875 |
. . . . . . . . . . . . . . . 16
|
40 | 37, 39 | eqeq12d 2479 |
. . . . . . . . . . . . . . 15
|
41 | 36, 40 | rspc 3204 |
. . . . . . . . . . . . . 14
|
42 | 34, 41 | mpan9 469 |
. . . . . . . . . . . . 13
|
43 | 42 | ralrimiva 2871 |
. . . . . . . . . . . 12
|
44 | 43 | adantr 465 |
. . . . . . . . . . 11
|
45 | 1 | adantr 465 |
. . . . . . . . . . . . 13
|
46 | 2 | adantr 465 |
. . . . . . . . . . . . 13
|
47 | | simpr 461 |
. . . . . . . . . . . . . 14
|
48 | 47, 4 | syl6eleq 2555 |
. . . . . . . . . . . . 13
|
49 | | eluzsub 11139 |
. . . . . . . . . . . . 13
|
50 | 45, 46, 48, 49 | syl3anc 1228 |
. . . . . . . . . . . 12
|
51 | 50, 9 | syl6eleqr 2556 |
. . . . . . . . . . 11
|
52 | | fveq2 5871 |
. . . . . . . . . . . . 13
|
53 | | oveq2 6304 |
. . . . . . . . . . . . . 14
|
54 | 53 | fveq2d 5875 |
. . . . . . . . . . . . 13
|
55 | 52, 54 | eqeq12d 2479 |
. . . . . . . . . . . 12
|
56 | 55 | rspccva 3209 |
. . . . . . . . . . 11
|
57 | 44, 51, 56 | syl2anc 661 |
. . . . . . . . . 10
|
58 | | pncan3 9851 |
. . . . . . . . . . . 12
|
59 | 6, 8, 58 | syl2an 477 |
. . . . . . . . . . 11
|
60 | 59 | fveq2d 5875 |
. . . . . . . . . 10
|
61 | 14, 57, 60 | 3eqtrrd 2503 |
. . . . . . . . 9
|
62 | 5, 61 | sylan2br 476 |
. . . . . . . 8
|
63 | 3, 62 | seqfeq 12132 |
. . . . . . 7
|
64 | 63 | breq1d 4462 |
. . . . . 6
|
65 | 12 | isershft 13486 |
. . . . . . 7
|
66 | 1, 2, 65 | syl2anc 661 |
. . . . . 6
|
67 | 64, 66 | bitr4d 256 |
. . . . 5
|
68 | 67 | iotabidv 5577 |
. . . 4
|
69 | | df-fv 5601 |
. . . 4
|
70 | | df-fv 5601 |
. . . 4
|
71 | 68, 69, 70 | 3eqtr4g 2523 |
. . 3
|
72 | | eqidd 2458 |
. . . 4
|
73 | | isumshft.6 |
. . . . . 6
|
74 | 73, 30 | fmptd 6055 |
. . . . 5
|
75 | | ffvelrn 6029 |
. . . . 5
|
76 | 74, 75 | sylan 471 |
. . . 4
|
77 | 4, 3, 72, 76 | isum 13541 |
. . 3
|
78 | | eqidd 2458 |
. . . 4
|
79 | 74 | adantr 465 |
. . . . . 6
|
80 | 28 | ralrimiva 2871 |
. . . . . . 7
|
81 | 38 | eleq1d 2526 |
. . . . . . . 8
|
82 | 81 | rspccva 3209 |
. . . . . . 7
|
83 | 80, 82 | sylan 471 |
. . . . . 6
|
84 | | ffvelrn 6029 |
. . . . . 6
|
85 | 79, 83, 84 | syl2anc 661 |
. . . . 5
|
86 | 42, 85 | eqeltrd 2545 |
. . . 4
|
87 | 9, 1, 78, 86 | isum 13541 |
. . 3
|
88 | 71, 77, 87 | 3eqtr4d 2508 |
. 2
|
89 | | sumfc 13531 |
. 2
|
90 | | sumfc 13531 |
. 2
|
91 | 88, 89, 90 | 3eqtr3g 2521 |
1
|