Step | Hyp | Ref
| Expression |
1 | | seqshft2.1 |
. . 3
       |
2 | | eluzfz2 11814 |
. . 3
    
      |
3 | 1, 2 | syl 17 |
. 2
       |
4 | | eleq1 2519 |
. . . . . 6
     
       |
5 | | fveq2 5870 |
. . . . . . 7
               |
6 | | oveq1 6302 |
. . . . . . . 8
       |
7 | 6 | fveq2d 5874 |
. . . . . . 7
                  
    |
8 | 5, 7 | eqeq12d 2468 |
. . . . . 6
                   
   
 
 
         |
9 | 4, 8 | imbi12d 322 |
. . . . 5
        
   
 
 
             
   
 
 
          |
10 | 9 | imbi2d 318 |
. . . 4
  
                      
       
   
 
 
           |
11 | | eleq1 2519 |
. . . . . 6
     
       |
12 | | fveq2 5870 |
. . . . . . 7
               |
13 | | oveq1 6302 |
. . . . . . . 8
       |
14 | 13 | fveq2d 5874 |
. . . . . . 7
                       |
15 | 12, 14 | eqeq12d 2468 |
. . . . . 6
                   
   
 
 
         |
16 | 11, 15 | imbi12d 322 |
. . . . 5
        
   
 
 
             
   
 
 
          |
17 | 16 | imbi2d 318 |
. . . 4
  
                      
       
   
 
 
           |
18 | | eleq1 2519 |
. . . . . 6
       
         |
19 | | fveq2 5870 |
. . . . . . 7
                   |
20 | | oveq1 6302 |
. . . . . . . 8
           |
21 | 20 | fveq2d 5874 |
. . . . . . 7
                           |
22 | 19, 21 | eqeq12d 2468 |
. . . . . 6
                     
       
 
           |
23 | 18, 22 | imbi12d 322 |
. . . . 5
          
   
 
 
               
       
 
            |
24 | 23 | imbi2d 318 |
. . . 4
    
                      
         
       
 
             |
25 | | eleq1 2519 |
. . . . . 6
     
       |
26 | | fveq2 5870 |
. . . . . . 7
               |
27 | | oveq1 6302 |
. . . . . . . 8
       |
28 | 27 | fveq2d 5874 |
. . . . . . 7
                  
    |
29 | 26, 28 | eqeq12d 2468 |
. . . . . 6
                   
   
 
 
         |
30 | 25, 29 | imbi12d 322 |
. . . . 5
        
   
 
 
             
   
 
 
          |
31 | 30 | imbi2d 318 |
. . . 4
  
                      
       
   
 
 
           |
32 | | eluzfz1 11813 |
. . . . . . . . 9
    
      |
33 | 1, 32 | syl 17 |
. . . . . . . 8
       |
34 | | seqshft2.3 |
. . . . . . . . 9
 
    
            |
35 | 34 | ralrimiva 2804 |
. . . . . . . 8
                   |
36 | | fveq2 5870 |
. . . . . . . . . 10
           |
37 | | oveq1 6302 |
. . . . . . . . . . 11
       |
38 | 37 | fveq2d 5874 |
. . . . . . . . . 10
          
    |
39 | 36, 38 | eqeq12d 2468 |
. . . . . . . . 9
           
             |
40 | 39 | rspcv 3148 |
. . . . . . . 8
      
                      
     |
41 | 33, 35, 40 | sylc 62 |
. . . . . . 7
             |
42 | | eluzel2 11171 |
. . . . . . . . 9
    
  |
43 | 1, 42 | syl 17 |
. . . . . . . 8
   |
44 | | seq1 12233 |
. . . . . . . 8
             |
45 | 43, 44 | syl 17 |
. . . . . . 7
             |
46 | | seqshft2.2 |
. . . . . . . . 9
   |
47 | 43, 46 | zaddcld 11051 |
. . . . . . . 8
     |
48 | | seq1 12233 |
. . . . . . . 8
          
          |
49 | 47, 48 | syl 17 |
. . . . . . 7
              
    |
50 | 41, 45, 49 | 3eqtr4d 2497 |
. . . . . 6
                   |
51 | 50 | a1d 26 |
. . . . 5
       
   
 
 
         |
52 | 51 | a1i 11 |
. . . 4
      
             
      |
53 | | peano2fzr 11819 |
. . . . . . . . . 10
            
      |
54 | 53 | adantl 468 |
. . . . . . . . 9
 
            
      |
55 | 54 | expr 620 |
. . . . . . . 8
 
    
              |
56 | 55 | imim1d 78 |
. . . . . . 7
 
    
                                                  |
57 | | oveq1 6302 |
. . . . . . . . . 10
                
      
         
 
               |
58 | | simprl 765 |
. . . . . . . . . . . 12
 
            
      |
59 | | seqp1 12235 |
. . . . . . . . . . . 12
    
              
         |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
 
            
              
         |
61 | 46 | adantr 467 |
. . . . . . . . . . . . . 14
 
            
  |
62 | | eluzadd 11194 |
. . . . . . . . . . . . . 14
            
    |
63 | 58, 61, 62 | syl2anc 667 |
. . . . . . . . . . . . 13
 
            
          |
64 | | seqp1 12235 |
. . . . . . . . . . . . 13
      
 
 
                                |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . 12
 
            
 
                                |
66 | | eluzelz 11175 |
. . . . . . . . . . . . . . 15
    
  |
67 | 58, 66 | syl 17 |
. . . . . . . . . . . . . 14
 
            
  |
68 | | zcn 10949 |
. . . . . . . . . . . . . . 15
   |
69 | | zcn 10949 |
. . . . . . . . . . . . . . 15
   |
70 | | ax-1cn 9602 |
. . . . . . . . . . . . . . . 16
 |
71 | | add32 9852 |
. . . . . . . . . . . . . . . 16
 
           |
72 | 70, 71 | mp3an2 1354 |
. . . . . . . . . . . . . . 15
 
           |
73 | 68, 69, 72 | syl2an 480 |
. . . . . . . . . . . . . 14
 
           |
74 | 67, 61, 73 | syl2anc 667 |
. . . . . . . . . . . . 13
 
            
          |
75 | 74 | fveq2d 5874 |
. . . . . . . . . . . 12
 
            
 
                        |
76 | | simprr 767 |
. . . . . . . . . . . . . . 15
 
            
        |
77 | 35 | adantr 467 |
. . . . . . . . . . . . . . 15
 
            
                  |
78 | | fveq2 5870 |
. . . . . . . . . . . . . . . . 17
          
    |
79 | | oveq1 6302 |
. . . . . . . . . . . . . . . . . 18
           |
80 | 79 | fveq2d 5874 |
. . . . . . . . . . . . . . . . 17
                   |
81 | 78, 80 | eqeq12d 2468 |
. . . . . . . . . . . . . . . 16
             
                 |
82 | 81 | rspcv 3148 |
. . . . . . . . . . . . . . 15
        
                                |
83 | 76, 77, 82 | sylc 62 |
. . . . . . . . . . . . . 14
 
            
                |
84 | 74 | fveq2d 5874 |
. . . . . . . . . . . . . 14
 
            
                  |
85 | 83, 84 | eqtrd 2487 |
. . . . . . . . . . . . 13
 
            
                |
86 | 85 | oveq2d 6311 |
. . . . . . . . . . . 12
 
            
                                        |
87 | 65, 75, 86 | 3eqtr4d 2497 |
. . . . . . . . . . 11
 
            
 
                              |
88 | 60, 87 | eqeq12d 2468 |
. . . . . . . . . 10
 
            
                           
         
 
                |
89 | 57, 88 | syl5ibr 225 |
. . . . . . . . 9
 
            
                
                       |
90 | 89 | expr 620 |
. . . . . . . 8
 
    
                       
                        |
91 | 90 | a2d 29 |
. . . . . . 7
 
    
                                                        |
92 | 56, 91 | syld 45 |
. . . . . 6
 
    
                                                      |
93 | 92 | expcom 437 |
. . . . 5
    
      
                                                 |
94 | 93 | a2d 29 |
. . . 4
    
      
                  
                                |
95 | 10, 17, 24, 31, 52, 94 | uzind4 11224 |
. . 3
    
       
   
 
 
          |
96 | 1, 95 | mpcom 37 |
. 2
       
   
 
 
         |
97 | 3, 96 | mpd 15 |
1
                   |