Step | Hyp | Ref
| Expression |
1 | | isumshft.5 |
. . . . . . . . 9
   |
2 | | isumshft.4 |
. . . . . . . . 9
   |
3 | 1, 2 | zaddcld 10857 |
. . . . . . . 8
     |
4 | | isumshft.2 |
. . . . . . . . . 10
       |
5 | 4 | eleq2i 2530 |
. . . . . . . . 9

        |
6 | 2 | zcnd 10854 |
. . . . . . . . . . 11
   |
7 | | eluzelz 10976 |
. . . . . . . . . . . . 13
    
 
  |
8 | 7 | zcnd 10854 |
. . . . . . . . . . . 12
    
 
  |
9 | 8, 4 | eleq2s 2560 |
. . . . . . . . . . 11
   |
10 | | isumshft.1 |
. . . . . . . . . . . . . 14
     |
11 | | fvex 5804 |
. . . . . . . . . . . . . 14
     |
12 | 10, 11 | eqeltri 2536 |
. . . . . . . . . . . . 13
 |
13 | 12 | mptex 6052 |
. . . . . . . . . . . 12
   |
14 | 13 | shftval 12676 |
. . . . . . . . . . 11
 
                   |
15 | 6, 9, 14 | syl2an 477 |
. . . . . . . . . 10
 
                   |
16 | | simpr 461 |
. . . . . . . . . . . . . . . . 17
 
   |
17 | | eqid 2452 |
. . . . . . . . . . . . . . . . . 18
     |
18 | 17 | fvmpt2i 5884 |
. . . . . . . . . . . . . . . . 17
           |
19 | 16, 18 | syl 16 |
. . . . . . . . . . . . . . . 16
 
           |
20 | | eluzelz 10976 |
. . . . . . . . . . . . . . . . . . . . . 22
    
  |
21 | 20 | zcnd 10854 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
22 | 21, 10 | eleq2s 2560 |
. . . . . . . . . . . . . . . . . . . 20
   |
23 | | addcom 9661 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
24 | 6, 22, 23 | syl2an 477 |
. . . . . . . . . . . . . . . . . . 19
 
 
     |
25 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
   |
26 | 25, 10 | syl6eleq 2550 |
. . . . . . . . . . . . . . . . . . . 20
       |
27 | | eluzadd 10995 |
. . . . . . . . . . . . . . . . . . . 20
            
    |
28 | 26, 2, 27 | syl2anr 478 |
. . . . . . . . . . . . . . . . . . 19
 
      
    |
29 | 24, 28 | eqeltrd 2540 |
. . . . . . . . . . . . . . . . . 18
 
 
         |
30 | 29, 4 | syl6eleqr 2551 |
. . . . . . . . . . . . . . . . 17
 
 
   |
31 | | isumshft.3 |
. . . . . . . . . . . . . . . . . 18
     |
32 | | eqid 2452 |
. . . . . . . . . . . . . . . . . 18
     |
33 | 31, 32 | fvmpti 5877 |
. . . . . . . . . . . . . . . . 17
        
      |
34 | 30, 33 | syl 16 |
. . . . . . . . . . . . . . . 16
 
      
      |
35 | 19, 34 | eqtr4d 2496 |
. . . . . . . . . . . . . . 15
 
                 |
36 | 35 | ralrimiva 2827 |
. . . . . . . . . . . . . 14
             
    |
37 | | nffvmpt1 5802 |
. . . . . . . . . . . . . . . 16
         |
38 | 37 | nfeq1 2628 |
. . . . . . . . . . . . . . 15
             
   |
39 | | fveq2 5794 |
. . . . . . . . . . . . . . . 16
               |
40 | | oveq2 6203 |
. . . . . . . . . . . . . . . . 17
 
     |
41 | 40 | fveq2d 5798 |
. . . . . . . . . . . . . . . 16
      
            |
42 | 39, 41 | eqeq12d 2474 |
. . . . . . . . . . . . . . 15
             
             
     |
43 | 38, 42 | rspc 3167 |
. . . . . . . . . . . . . 14
  
           
 
                 |
44 | 36, 43 | mpan9 469 |
. . . . . . . . . . . . 13
 
                 |
45 | 44 | ralrimiva 2827 |
. . . . . . . . . . . 12
             
    |
46 | 45 | adantr 465 |
. . . . . . . . . . 11
 
 
                |
47 | 1 | adantr 465 |
. . . . . . . . . . . . 13
 
   |
48 | 2 | adantr 465 |
. . . . . . . . . . . . 13
 
   |
49 | | simpr 461 |
. . . . . . . . . . . . . 14
 
   |
50 | 49, 4 | syl6eleq 2550 |
. . . . . . . . . . . . 13
 
         |
51 | | eluzsub 10996 |
. . . . . . . . . . . . 13
 
               |
52 | 47, 48, 50, 51 | syl3anc 1219 |
. . . . . . . . . . . 12
 
         |
53 | 52, 10 | syl6eleqr 2551 |
. . . . . . . . . . 11
 
     |
54 | | fveq2 5794 |
. . . . . . . . . . . . 13
                   |
55 | | oveq2 6203 |
. . . . . . . . . . . . . 14
   
  
    |
56 | 55 | fveq2d 5798 |
. . . . . . . . . . . . 13
        
              |
57 | 54, 56 | eqeq12d 2474 |
. . . . . . . . . . . 12
               
               
       |
58 | 57 | rspccva 3172 |
. . . . . . . . . . 11
              
 
  
              
     |
59 | 46, 53, 58 | syl2anc 661 |
. . . . . . . . . 10
 
                     |
60 | | pncan3 9724 |
. . . . . . . . . . . 12
 
       |
61 | 6, 9, 60 | syl2an 477 |
. . . . . . . . . . 11
 
 
     |
62 | 61 | fveq2d 5798 |
. . . . . . . . . 10
 
      
            |
63 | 15, 59, 62 | 3eqtrrd 2498 |
. . . . . . . . 9
 
                 |
64 | 5, 63 | sylan2br 476 |
. . . . . . . 8
 
                       |
65 | 3, 64 | seqfeq 11943 |
. . . . . . 7
              
    |
66 | 65 | breq1d 4405 |
. . . . . 6
       
 
          |
67 | 13 | isershft 13254 |
. . . . . . 7
 
     
 
          |
68 | 1, 2, 67 | syl2anc 661 |
. . . . . 6
     
 
          |
69 | 66, 68 | bitr4d 256 |
. . . . 5
       
        |
70 | 69 | iotabidv 5505 |
. . . 4
    
                |
71 | | df-fv 5529 |
. . . 4
 
                 |
72 | | df-fv 5529 |
. . . 4
               |
73 | 70, 71, 72 | 3eqtr4g 2518 |
. . 3

 
     
        |
74 | | eqidd 2453 |
. . . 4
 
               |
75 | | isumshft.6 |
. . . . . 6
 
   |
76 | 75, 32 | fmptd 5971 |
. . . . 5
         |
77 | | ffvelrn 5945 |
. . . . 5
        
        |
78 | 76, 77 | sylan 471 |
. . . 4
 
         |
79 | 4, 3, 74, 78 | isum 13309 |
. . 3
 
                |
80 | | eqidd 2453 |
. . . 4
 
               |
81 | 76 | adantr 465 |
. . . . . 6
 
         |
82 | 30 | ralrimiva 2827 |
. . . . . . 7
  
   |
83 | 40 | eleq1d 2521 |
. . . . . . . 8
   
     |
84 | 83 | rspccva 3172 |
. . . . . . 7
   

     |
85 | 82, 84 | sylan 471 |
. . . . . 6
 
 
   |
86 | | ffvelrn 5945 |
. . . . . 6
          
          |
87 | 81, 85, 86 | syl2anc 661 |
. . . . 5
 
      
    |
88 | 44, 87 | eqeltrd 2540 |
. . . 4
 
         |
89 | 10, 1, 80, 88 | isum 13309 |
. . 3
 
              |
90 | 73, 79, 89 | 3eqtr4d 2503 |
. 2
 
               |
91 | | sumfc 13299 |
. 2

        |
92 | | sumfc 13299 |
. 2

        |
93 | 90, 91, 92 | 3eqtr3g 2516 |
1
 
   |