Step | Hyp | Ref
| Expression |
1 | | seqhomo.3 |
. . 3
       |
2 | | eluzfz2 10088 |
. . 3
    
      |
3 | 1, 2 | syl 14 |
. 2
       |
4 | | eleq1 2256 |
. . . . . 6
     
       |
5 | | 2fveq3 5551 |
. . . . . . 7
                       |
6 | | fveq2 5546 |
. . . . . . 7
                   |
7 | 5, 6 | eqeq12d 2208 |
. . . . . 6
                   
  
                  |
8 | 4, 7 | imbi12d 234 |
. . . . 5
                         
    
  
                   |
9 | 8 | imbi2d 230 |
. . . 4
  
                         
                            |
10 | | eleq1 2256 |
. . . . . 6
     
       |
11 | | 2fveq3 5551 |
. . . . . . 7
                       |
12 | | fveq2 5546 |
. . . . . . 7
                   |
13 | 11, 12 | eqeq12d 2208 |
. . . . . 6
                   
  
                  |
14 | 10, 13 | imbi12d 234 |
. . . . 5
                         
    
  
                   |
15 | 14 | imbi2d 230 |
. . . 4
  
                         
                            |
16 | | eleq1 2256 |
. . . . . 6
       
         |
17 | | 2fveq3 5551 |
. . . . . . 7
                           |
18 | | fveq2 5546 |
. . . . . . 7
                       |
19 | 17, 18 | eqeq12d 2208 |
. . . . . 6
                     
  
                      |
20 | 16, 19 | imbi12d 234 |
. . . . 5
                           
                          
      |
21 | 20 | imbi2d 230 |
. . . 4
    
                         
                          
       |
22 | | eleq1 2256 |
. . . . . 6
     
       |
23 | | 2fveq3 5551 |
. . . . . . 7
                       |
24 | | fveq2 5546 |
. . . . . . 7
                   |
25 | 23, 24 | eqeq12d 2208 |
. . . . . 6
                   
  
                  |
26 | 22, 25 | imbi12d 234 |
. . . . 5
                         
    
  
                   |
27 | 26 | imbi2d 230 |
. . . 4
  
                         
                            |
28 | | 2fveq3 5551 |
. . . . . . . 8
                   |
29 | | fveq2 5546 |
. . . . . . . 8
           |
30 | 28, 29 | eqeq12d 2208 |
. . . . . . 7
             
               |
31 | | seqhomo.5 |
. . . . . . . 8
 
    
              |
32 | 31 | ralrimiva 2567 |
. . . . . . 7
                     |
33 | | eluzfz1 10087 |
. . . . . . . 8
    
      |
34 | 1, 33 | syl 14 |
. . . . . . 7
       |
35 | 30, 32, 34 | rspcdva 2869 |
. . . . . 6
               |
36 | | eluzel2 9587 |
. . . . . . . . 9
    
  |
37 | 1, 36 | syl 14 |
. . . . . . . 8
   |
38 | | seqhomog.f |
. . . . . . . 8
   |
39 | | seqhomog.p |
. . . . . . . 8
   |
40 | | seq1g 10524 |
. . . . . . . 8
 
             |
41 | 37, 38, 39, 40 | syl3anc 1249 |
. . . . . . 7
             |
42 | 41 | fveq2d 5550 |
. . . . . 6
                     |
43 | | seqhomog.g |
. . . . . . 7
   |
44 | | seqhomog.q |
. . . . . . 7
   |
45 | | seq1g 10524 |
. . . . . . 7
 
               |
46 | 37, 43, 44, 45 | syl3anc 1249 |
. . . . . 6
               |
47 | 35, 42, 46 | 3eqtr4d 2236 |
. . . . 5
                     |
48 | 47 | a1d 22 |
. . . 4
                           |
49 | | peano2fzr 10093 |
. . . . . . . 8
            
      |
50 | 49 | adantl 277 |
. . . . . . 7
 
            
      |
51 | 50 | expr 375 |
. . . . . 6
 
    
              |
52 | 51 | imim1d 75 |
. . . . 5
 
    
                                                      |
53 | | oveq1 5917 |
. . . . . 6
                                                           |
54 | | simprl 529 |
. . . . . . . . . 10
 
            
      |
55 | 38 | adantr 276 |
. . . . . . . . . 10
 
            
  |
56 | 39 | adantr 276 |
. . . . . . . . . 10
 
            
  |
57 | | seqp1g 10527 |
. . . . . . . . . 10
     
               
         |
58 | 54, 55, 56, 57 | syl3anc 1249 |
. . . . . . . . 9
 
            
              
         |
59 | 58 | fveq2d 5550 |
. . . . . . . 8
 
            
  
              
              |
60 | | seqhomo.4 |
. . . . . . . . . . 11
 

     
                |
61 | 60 | ralrimivva 2576 |
. . . . . . . . . 10
  
                    |
62 | 61 | adantr 276 |
. . . . . . . . 9
 
            


                    |
63 | | elfzuz3 10078 |
. . . . . . . . . . . . . 14
           |
64 | | fzss2 10120 |
. . . . . . . . . . . . . 14
    
          |
65 | 50, 63, 64 | 3syl 17 |
. . . . . . . . . . . . 13
 
            
          |
66 | 65 | sselda 3179 |
. . . . . . . . . . . 12
                    
      |
67 | | seqhomo.2 |
. . . . . . . . . . . . 13
 
    
      |
68 | 67 | adantlr 477 |
. . . . . . . . . . . 12
                    
      |
69 | 66, 68 | syldan 282 |
. . . . . . . . . . 11
                    
      |
70 | | seqhomo.1 |
. . . . . . . . . . . 12
 

      |
71 | 70 | adantlr 477 |
. . . . . . . . . . 11
                       |
72 | 54, 69, 71, 55, 56 | seqclg 10533 |
. . . . . . . . . 10
 
            
        |
73 | | fveq2 5546 |
. . . . . . . . . . . 12
          
    |
74 | 73 | eleq1d 2262 |
. . . . . . . . . . 11
       
         |
75 | 67 | ralrimiva 2567 |
. . . . . . . . . . . 12
             |
76 | 75 | adantr 276 |
. . . . . . . . . . 11
 
            
            |
77 | | simprr 531 |
. . . . . . . . . . 11
 
            
        |
78 | 74, 76, 77 | rspcdva 2869 |
. . . . . . . . . 10
 
            
        |
79 | | fvoveq1 5933 |
. . . . . . . . . . . 12
  
       
           
    |
80 | | fveq2 5546 |
. . . . . . . . . . . . 13
  
            
       |
81 | 80 | oveq1d 5925 |
. . . . . . . . . . . 12
  
                                    |
82 | 79, 81 | eqeq12d 2208 |
. . . . . . . . . . 11
  
        
             
     
                           |
83 | | oveq2 5918 |
. . . . . . . . . . . . 13
    
        
       
         |
84 | 83 | fveq2d 5550 |
. . . . . . . . . . . 12
    
           
           
          |
85 | | fveq2 5546 |
. . . . . . . . . . . . 13
    
                  |
86 | 85 | oveq2d 5926 |
. . . . . . . . . . . 12
    
                                              |
87 | 84, 86 | eqeq12d 2208 |
. . . . . . . . . . 11
    
            
                         
                                       |
88 | 82, 87 | rspc2v 2877 |
. . . . . . . . . 10
                

                           
             
             
       |
89 | 72, 78, 88 | syl2anc 411 |
. . . . . . . . 9
 
            
 

                 
     
                                       |
90 | 62, 89 | mpd 13 |
. . . . . . . 8
 
            
     
                                      |
91 | | 2fveq3 5551 |
. . . . . . . . . . 11
                       |
92 | | fveq2 5546 |
. . . . . . . . . . 11
          
    |
93 | 91, 92 | eqeq12d 2208 |
. . . . . . . . . 10
               
                   |
94 | 32 | adantr 276 |
. . . . . . . . . 10
 
            
                    |
95 | 93, 94, 77 | rspcdva 2869 |
. . . . . . . . 9
 
            
                  |
96 | 95 | oveq2d 5926 |
. . . . . . . 8
 
            
                                              |
97 | 59, 90, 96 | 3eqtrd 2230 |
. . . . . . 7
 
            
  
              
                |
98 | 43 | adantr 276 |
. . . . . . . 8
 
            
  |
99 | 44 | adantr 276 |
. . . . . . . 8
 
            
  |
100 | | seqp1g 10527 |
. . . . . . . 8
     
                               |
101 | 54, 98, 99, 100 | syl3anc 1249 |
. . . . . . 7
 
            
                              |
102 | 97, 101 | eqeq12d 2208 |
. . . . . 6
 
            
                    
 
                                         |
103 | 53, 102 | imbitrrid 156 |
. . . . 5
 
            
                                      
     |
104 | 52, 103 | animpimp2impd 559 |
. . . 4
    
      
  
                        
  
                        |
105 | 9, 15, 21, 27, 48, 104 | uzind4i 9647 |
. . 3
    
                            |
106 | 1, 105 | mpcom 36 |
. 2
                           |
107 | 3, 106 | mpd 13 |
1
                     |