Step | Hyp | Ref
| Expression |
1 | | seqsplit.3 |
. . 3
    
    |
2 | | eluzfz2 10088 |
. . 3
    
 
        |
3 | 1, 2 | syl 14 |
. 2
         |
4 | | eleq1 2256 |
. . . . . 6
         
           |
5 | | fveq2 5546 |
. . . . . . 7
              
    |
6 | | fveq2 5546 |
. . . . . . . 8
                  
    |
7 | 6 | oveq2d 5926 |
. . . . . . 7
         
 
                     
     |
8 | 5, 7 | eqeq12d 2208 |
. . . . . 6
                
 
      
     
        
 
     
      |
9 | 4, 8 | imbi12d 234 |
. . . . 5
            
          
 
       
 
            
        
 
     
       |
10 | 9 | imbi2d 230 |
. . . 4
    
                   
 
         
              
        
 
     
        |
11 | | eleq1 2256 |
. . . . . 6
       
         |
12 | | fveq2 5546 |
. . . . . . 7
               |
13 | | fveq2 5546 |
. . . . . . . 8
                   |
14 | 13 | oveq2d 5926 |
. . . . . . 7
       
 
                         |
15 | 12, 14 | eqeq12d 2208 |
. . . . . 6
              
 
      
            
 
          |
16 | 11, 15 | imbi12d 234 |
. . . . 5
          
          
 
       
      
            
 
           |
17 | 16 | imbi2d 230 |
. . . 4
  
                   
 
         
                   
 
            |
18 | | eleq1 2256 |
. . . . . 6
         
           |
19 | | fveq2 5546 |
. . . . . . 7
                   |
20 | | fveq2 5546 |
. . . . . . . 8
                       |
21 | 20 | oveq2d 5926 |
. . . . . . 7
         
 
                           |
22 | 19, 21 | eqeq12d 2208 |
. . . . . 6
                
 
      
              
 
            |
23 | 18, 22 | imbi12d 234 |
. . . . 5
            
          
 
       
                       
 
             |
24 | 23 | imbi2d 230 |
. . . 4
    
                   
 
         
                       
 
              |
25 | | eleq1 2256 |
. . . . . 6
       
         |
26 | | fveq2 5546 |
. . . . . . 7
               |
27 | | fveq2 5546 |
. . . . . . . 8
                   |
28 | 27 | oveq2d 5926 |
. . . . . . 7
       
 
                         |
29 | 26, 28 | eqeq12d 2208 |
. . . . . 6
              
 
      
            
 
          |
30 | 25, 29 | imbi12d 234 |
. . . . 5
          
          
 
       
      
            
 
           |
31 | 30 | imbi2d 230 |
. . . 4
  
                   
 
         
                   
 
            |
32 | | seqsplit.4 |
. . . . . . 7
       |
33 | | seqsplitg.f |
. . . . . . 7
   |
34 | | seqsplitg.p |
. . . . . . 7
   |
35 | | seqp1g 10527 |
. . . . . . 7
     
      
        
         |
36 | 32, 33, 34, 35 | syl3anc 1249 |
. . . . . 6
           
       
     |
37 | | eluzel2 9587 |
. . . . . . . . 9
    
 
    |
38 | 1, 37 | syl 14 |
. . . . . . . 8
     |
39 | | seq1g 10524 |
. . . . . . . 8
   
        
          |
40 | 38, 33, 34, 39 | syl3anc 1249 |
. . . . . . 7
              
    |
41 | 40 | oveq2d 5926 |
. . . . . 6
   
   
 
               
         |
42 | 36, 41 | eqtr4d 2229 |
. . . . 5
           
   
 
           |
43 | 42 | a1i13 24 |
. . . 4
            
     
        
 
     
       |
44 | | peano2fzr 10093 |
. . . . . . . 8
     
          
 
      |
45 | 44 | adantl 277 |
. . . . . . 7
 
                         |
46 | 45 | expr 375 |
. . . . . 6
 
      
                  |
47 | 46 | imim1d 75 |
. . . . 5
 
      
                    
 
                  
          
 
           |
48 | | oveq1 5917 |
. . . . . 6
             
 
             
              
 
                |
49 | | simprl 529 |
. . . . . . . . 9
 
                         |
50 | | peano2uz 9638 |
. . . . . . . . . . 11
    
        |
51 | 32, 50 | syl 14 |
. . . . . . . . . 10
         |
52 | 51 | adantr 276 |
. . . . . . . . 9
 
                 
       |
53 | | uztrn 9599 |
. . . . . . . . 9
     
  
            |
54 | 49, 52, 53 | syl2anc 411 |
. . . . . . . 8
 
                       |
55 | 33 | adantr 276 |
. . . . . . . 8
 
                   |
56 | 34 | adantr 276 |
. . . . . . . 8
 
                   |
57 | | seqp1g 10527 |
. . . . . . . 8
     
               
         |
58 | 54, 55, 56, 57 | syl3anc 1249 |
. . . . . . 7
 
                               
         |
59 | | seqp1g 10527 |
. . . . . . . . . 10
     
 
                   
         |
60 | 49, 55, 56, 59 | syl3anc 1249 |
. . . . . . . . 9
 
                                   
         |
61 | 60 | oveq2d 5926 |
. . . . . . . 8
 
                       
 
                  
                |
62 | | simpl 109 |
. . . . . . . . 9
 
                   |
63 | | eluzelz 9591 |
. . . . . . . . . . . . . . . 16
    
  |
64 | 32, 63 | syl 14 |
. . . . . . . . . . . . . . 15
   |
65 | | peano2uzr 9640 |
. . . . . . . . . . . . . . 15
 
   
  
      |
66 | 64, 1, 65 | syl2anc 411 |
. . . . . . . . . . . . . 14
       |
67 | | fzss2 10120 |
. . . . . . . . . . . . . 14
    
          |
68 | 66, 67 | syl 14 |
. . . . . . . . . . . . 13
    
      |
69 | 68 | sselda 3179 |
. . . . . . . . . . . 12
 
    
      |
70 | | seqsplit.5 |
. . . . . . . . . . . 12
 
    
      |
71 | 69, 70 | syldan 282 |
. . . . . . . . . . 11
 
    
      |
72 | | seqsplit.1 |
. . . . . . . . . . 11
 

      |
73 | 32, 71, 72, 33, 34 | seqclg 10533 |
. . . . . . . . . 10
         |
74 | 73 | adantr 276 |
. . . . . . . . 9
 
                         |
75 | | elfzuz3 10078 |
. . . . . . . . . . . . . 14
             |
76 | | fzss2 10120 |
. . . . . . . . . . . . . 14
    
 
            |
77 | 45, 75, 76 | 3syl 17 |
. . . . . . . . . . . . 13
 
                               |
78 | | fzss1 10119 |
. . . . . . . . . . . . . . 15
      
 
          |
79 | 32, 50, 78 | 3syl 17 |
. . . . . . . . . . . . . 14
      
      |
80 | 79 | adantr 276 |
. . . . . . . . . . . . 13
 
                             |
81 | 77, 80 | sstrd 3189 |
. . . . . . . . . . . 12
 
                             |
82 | 81 | sselda 3179 |
. . . . . . . . . . 11
       
                  
      |
83 | 70 | adantlr 477 |
. . . . . . . . . . 11
       
                
      |
84 | 82, 83 | syldan 282 |
. . . . . . . . . 10
       
                  
      |
85 | 72 | adantlr 477 |
. . . . . . . . . 10
       
                   |
86 | 49, 84, 85, 55, 56 | seqclg 10533 |
. . . . . . . . 9
 
                           |
87 | | fveq2 5546 |
. . . . . . . . . . 11
          
    |
88 | 87 | eleq1d 2262 |
. . . . . . . . . 10
       
         |
89 | 70 | ralrimiva 2567 |
. . . . . . . . . . 11
             |
90 | 89 | adantr 276 |
. . . . . . . . . 10
 
                             |
91 | | simpr 110 |
. . . . . . . . . . 11
     
                     |
92 | | ssel2 3174 |
. . . . . . . . . . 11
       
                     |
93 | 79, 91, 92 | syl2an 289 |
. . . . . . . . . 10
 
                         |
94 | 88, 90, 93 | rspcdva 2869 |
. . . . . . . . 9
 
                         |
95 | | seqsplit.2 |
. . . . . . . . . 10
 

            |
96 | 95 | caovassg 6069 |
. . . . . . . . 9
 
                              
 
                    
        
          |
97 | 62, 74, 86, 94, 96 | syl13anc 1251 |
. . . . . . . 8
 
                    
   
 
      
         
      
                |
98 | 61, 97 | eqtr4d 2229 |
. . . . . . 7
 
                       
 
            
   
 
      
         |
99 | 58, 98 | eqeq12d 2208 |
. . . . . 6
 
                                
 
        
      
              
 
                 |
100 | 48, 99 | imbitrrid 156 |
. . . . 5
 
                              
 
                     
 
            |
101 | 47, 100 | animpimp2impd 559 |
. . . 4
    
 
        
            
 
                                 
 
              |
102 | 10, 17, 24, 31, 43, 101 | uzind4 9643 |
. . 3
    
 
         
          
 
           |
103 | 1, 102 | mpcom 36 |
. 2
         
          
 
          |
104 | 3, 103 | mpd 13 |
1
         
   
 
         |