Step | Hyp | Ref
| Expression |
1 | | seqf1o.6 |
. . 3
               |
2 | | seqf1o.7 |
. . . 4
 
    
      |
3 | | eqid 2462 |
. . . 4
                     |
4 | 2, 3 | fmptd 6074 |
. . 3
                     |
5 | | seqf1o.4 |
. . . . 5
       |
6 | | oveq2 6328 |
. . . . . . . . . . 11
           |
7 | | f1oeq23 5835 |
. . . . . . . . . . 11
                                               |
8 | 6, 6, 7 | syl2anc 671 |
. . . . . . . . . 10
             
               |
9 | 6 | feq2d 5741 |
. . . . . . . . . 10
                     |
10 | 8, 9 | anbi12d 722 |
. . . . . . . . 9
                       
            
            |
11 | | fveq2 5892 |
. . . . . . . . . 10
                   |
12 | | fveq2 5892 |
. . . . . . . . . 10
               |
13 | 11, 12 | eqeq12d 2477 |
. . . . . . . . 9
               
                 |
14 | 10, 13 | imbi12d 326 |
. . . . . . . 8
                                       
                        
       
        |
15 | 14 | 2albidv 1780 |
. . . . . . 7
                                           
                 
                           |
16 | 15 | imbi2d 322 |
. . . . . 6
  
                 
                         
                 
                            |
17 | | oveq2 6328 |
. . . . . . . . . . 11
           |
18 | | f1oeq23 5835 |
. . . . . . . . . . 11
                                               |
19 | 17, 17, 18 | syl2anc 671 |
. . . . . . . . . 10
             
               |
20 | 17 | feq2d 5741 |
. . . . . . . . . 10
                     |
21 | 19, 20 | anbi12d 722 |
. . . . . . . . 9
                       
            
            |
22 | | fveq2 5892 |
. . . . . . . . . 10
                   |
23 | | fveq2 5892 |
. . . . . . . . . 10
               |
24 | 22, 23 | eqeq12d 2477 |
. . . . . . . . 9
               
                 |
25 | 21, 24 | imbi12d 326 |
. . . . . . . 8
                                       
                        
       
        |
26 | 25 | 2albidv 1780 |
. . . . . . 7
                                           
                 
                           |
27 | 26 | imbi2d 322 |
. . . . . 6
  
                 
                         
                 
                            |
28 | | oveq2 6328 |
. . . . . . . . . . 11
               |
29 | | f1oeq23 5835 |
. . . . . . . . . . 11
                                                       |
30 | 28, 28, 29 | syl2anc 671 |
. . . . . . . . . 10
               
                   |
31 | 28 | feq2d 5741 |
. . . . . . . . . 10
                         |
32 | 30, 31 | anbi12d 722 |
. . . . . . . . 9
                         
                               |
33 | | fveq2 5892 |
. . . . . . . . . 10
                       |
34 | | fveq2 5892 |
. . . . . . . . . 10
                   |
35 | 33, 34 | eqeq12d 2477 |
. . . . . . . . 9
                 
                     |
36 | 32, 35 | imbi12d 326 |
. . . . . . . 8
                                         
                              
         
          |
37 | 36 | 2albidv 1780 |
. . . . . . 7
                                             
                                                       |
38 | 37 | imbi2d 322 |
. . . . . 6
    
                 
                         
                                                        |
39 | | oveq2 6328 |
. . . . . . . . . . 11
           |
40 | | f1oeq23 5835 |
. . . . . . . . . . 11
                                               |
41 | 39, 39, 40 | syl2anc 671 |
. . . . . . . . . 10
             
               |
42 | 39 | feq2d 5741 |
. . . . . . . . . 10
                     |
43 | 41, 42 | anbi12d 722 |
. . . . . . . . 9
                       
            
            |
44 | | fveq2 5892 |
. . . . . . . . . 10
                   |
45 | | fveq2 5892 |
. . . . . . . . . 10
               |
46 | 44, 45 | eqeq12d 2477 |
. . . . . . . . 9
               
                 |
47 | 43, 46 | imbi12d 326 |
. . . . . . . 8
                                       
                        
       
        |
48 | 47 | 2albidv 1780 |
. . . . . . 7
                                           
                 
                           |
49 | 48 | imbi2d 322 |
. . . . . 6
  
                 
                         
                 
                            |
50 | | f1of 5841 |
. . . . . . . . . . . . 13
            
              |
51 | 50 | adantr 471 |
. . . . . . . . . . . 12
                                     |
52 | | elfz3 11844 |
. . . . . . . . . . . 12
       |
53 | | fvco3 5970 |
. . . . . . . . . . . 12
                  
                |
54 | 51, 52, 53 | syl2anr 485 |
. . . . . . . . . . 11
                                         |
55 | | ffvelrn 6048 |
. . . . . . . . . . . . . . 15
                  
          |
56 | 50, 52, 55 | syl2anr 485 |
. . . . . . . . . . . . . 14
                         |
57 | | fzsn 11875 |
. . . . . . . . . . . . . . . . 17
         |
58 | 57 | eleq2d 2525 |
. . . . . . . . . . . . . . . 16
         
         |
59 | | elsni 4005 |
. . . . . . . . . . . . . . . 16
             |
60 | 58, 59 | syl6bi 236 |
. . . . . . . . . . . . . . 15
                 |
61 | 60 | imp 435 |
. . . . . . . . . . . . . 14
                 |
62 | 56, 61 | syldan 477 |
. . . . . . . . . . . . 13
                     |
63 | 62 | adantrr 728 |
. . . . . . . . . . . 12
                               |
64 | 63 | fveq2d 5896 |
. . . . . . . . . . 11
                                       |
65 | 54, 64 | eqtrd 2496 |
. . . . . . . . . 10
                                     |
66 | | seq1 12264 |
. . . . . . . . . . 11
                 |
67 | 66 | adantr 471 |
. . . . . . . . . 10
                                         |
68 | | seq1 12264 |
. . . . . . . . . . 11
             |
69 | 68 | adantr 471 |
. . . . . . . . . 10
                                     |
70 | 65, 67, 69 | 3eqtr4d 2506 |
. . . . . . . . 9
                                         |
71 | 70 | ex 440 |
. . . . . . . 8
                                         |
72 | 71 | alrimivv 1785 |
. . . . . . 7
                  
                          |
73 | 72 | a1d 26 |
. . . . . 6
                                               |
74 | | f1oeq1 5832 |
. . . . . . . . . . . 12
             
               |
75 | | feq1 5736 |
. . . . . . . . . . . 12
                     |
76 | 74, 75 | bi2anan9r 890 |
. . . . . . . . . . 11
 
                       
            
            |
77 | | coeq1 5014 |
. . . . . . . . . . . . . . 15
       |
78 | | coeq2 5015 |
. . . . . . . . . . . . . . 15
       |
79 | 77, 78 | sylan9eq 2516 |
. . . . . . . . . . . . . 14
 
       |
80 | 79 | seqeq3d 12259 |
. . . . . . . . . . . . 13
 
             |
81 | 80 | fveq1d 5894 |
. . . . . . . . . . . 12
 
                   |
82 | | simpl 463 |
. . . . . . . . . . . . . 14
 
   |
83 | 82 | seqeq3d 12259 |
. . . . . . . . . . . . 13
 
         |
84 | 83 | fveq1d 5894 |
. . . . . . . . . . . 12
 
               |
85 | 81, 84 | eqeq12d 2477 |
. . . . . . . . . . 11
 
   
       
                     |
86 | 76, 85 | imbi12d 326 |
. . . . . . . . . 10
 
               
                       
                        
       
        |
87 | 86 | cbval2v 2133 |
. . . . . . . . 9
                             
       
                                                 |
88 | | simplll 773 |
. . . . . . . . . . . . . . 15
   
                                                                               |
89 | | seqf1o.1 |
. . . . . . . . . . . . . . 15
 

      |
90 | 88, 89 | sylan 478 |
. . . . . . . . . . . . . 14
                                                                                  
  
   |
91 | | seqf1o.2 |
. . . . . . . . . . . . . . 15
 

        |
92 | 88, 91 | sylan 478 |
. . . . . . . . . . . . . 14
                                                                                  
  
     |
93 | | seqf1o.3 |
. . . . . . . . . . . . . . 15
 

            |
94 | 88, 93 | sylan 478 |
. . . . . . . . . . . . . 14
                                                                                  
    
       |
95 | | simpllr 774 |
. . . . . . . . . . . . . 14
   
                                                                                   |
96 | | seqf1o.5 |
. . . . . . . . . . . . . . 15

  |
97 | 88, 96 | syl 17 |
. . . . . . . . . . . . . 14
   
                                                                               |
98 | | simprl 769 |
. . . . . . . . . . . . . 14
   
                                                                                               |
99 | | simprr 771 |
. . . . . . . . . . . . . 14
   
                                                                                         |
100 | | eqid 2462 |
. . . . . . . . . . . . . 14
                                                 |
101 | | eqid 2462 |
. . . . . . . . . . . . . 14
               |
102 | | simplr 767 |
. . . . . . . . . . . . . . 15
   
                                                                                                                         |
103 | 102, 87 | sylib 201 |
. . . . . . . . . . . . . 14
   
                                                                                                                         |
104 | 90, 92, 94, 95, 97, 98, 99, 100, 101, 103 | seqf1olem2 12291 |
. . . . . . . . . . . . 13
   
                                                                                                 |
105 | 104 | exp31 613 |
. . . . . . . . . . . 12
 
    
                             
       
    
                              
         
          |
106 | 87, 105 | syl5bir 226 |
. . . . . . . . . . 11
 
    
                             
       
    
                              
         
          |
107 | 106 | alrimdv 1786 |
. . . . . . . . . 10
 
    
                             
       
    
                                                     |
108 | 107 | alrimdv 1786 |
. . . . . . . . 9
 
    
                             
       
    
                                                       |
109 | 87, 108 | syl5bi 225 |
. . . . . . . 8
 
    
                             
       
    
                                                       |
110 | 109 | expcom 441 |
. . . . . . 7
    
                   
                                                                                |
111 | 110 | a2d 29 |
. . . . . 6
    
                                             
                                                        |
112 | 16, 27, 38, 49, 73, 111 | uzind4 11251 |
. . . . 5
    
                                              |
113 | 5, 112 | mpcom 37 |
. . . 4
                                             |
114 | | fvex 5902 |
. . . . . . 7
     |
115 | 114, 3 | fnmpti 5732 |
. . . . . 6
               |
116 | | fzfi 12223 |
. . . . . 6
     |
117 | | fnfi 7880 |
. . . . . 6
                                 |
118 | 115, 116,
117 | mp2an 683 |
. . . . 5
           |
119 | | f1of 5841 |
. . . . . . 7
            
              |
120 | 1, 119 | syl 17 |
. . . . . 6
               |
121 | | ovex 6348 |
. . . . . . 7
     |
122 | 121 | a1i 11 |
. . . . . 6
       |
123 | | fex2 6780 |
. . . . . 6
                         |
124 | 120, 122,
122, 123 | syl3anc 1276 |
. . . . 5
   |
125 | | f1oeq1 5832 |
. . . . . . . 8
             
               |
126 | | feq1 5736 |
. . . . . . . 8
                                         |
127 | 125, 126 | bi2anan9r 890 |
. . . . . . 7
            
                                                          |
128 | | coeq1 5014 |
. . . . . . . . . . 11
                           |
129 | | coeq2 5015 |
. . . . . . . . . . 11
                           |
130 | 128, 129 | sylan9eq 2516 |
. . . . . . . . . 10
            
                |
131 | 130 | seqeq3d 12259 |
. . . . . . . . 9
            
                      |
132 | 131 | fveq1d 5894 |
. . . . . . . 8
            
                            |
133 | | simpl 463 |
. . . . . . . . . 10
            

           |
134 | 133 | seqeq3d 12259 |
. . . . . . . . 9
            
                  |
135 | 134 | fveq1d 5894 |
. . . . . . . 8
            
                        |
136 | 132, 135 | eqeq12d 2477 |
. . . . . . 7
            
                
                                   |
137 | 127, 136 | imbi12d 326 |
. . . . . 6
            
                                      
             
                                                         |
138 | 137 | spc2gv 3149 |
. . . . 5
                               
                                                                                               |
139 | 118, 124,
138 | sylancr 674 |
. . . 4
                   
                                                                                               |
140 | 113, 139 | mpd 15 |
. . 3
                                                                       |
141 | 1, 4, 140 | mp2and 690 |
. 2
                    
                |
142 | 120 | ffvelrnda 6050 |
. . . . 5
 
    
          |
143 | | fveq2 5892 |
. . . . . 6
                   |
144 | | fvex 5902 |
. . . . . 6
         |
145 | 143, 3, 144 | fvmpt 5976 |
. . . . 5
                                     |
146 | 142, 145 | syl 17 |
. . . 4
 
    
                            |
147 | | fvco3 5970 |
. . . . 5
                  
                                    |
148 | 120, 147 | sylan 478 |
. . . 4
 
    
                                    |
149 | | seqf1o.8 |
. . . 4
 
    
              |
150 | 146, 148,
149 | 3eqtr4d 2506 |
. . 3
 
    
                      |
151 | 5, 150 | seqfveq 12275 |
. 2
                    
      |
152 | | fveq2 5892 |
. . . . 5
           |
153 | | fvex 5902 |
. . . . 5
     |
154 | 152, 3, 153 | fvmpt 5976 |
. . . 4
                         |
155 | 154 | adantl 472 |
. . 3
 
    
                    |
156 | 5, 155 | seqfveq 12275 |
. 2
                  
      |
157 | 141, 151,
156 | 3eqtr3d 2504 |
1
               |