Step | Hyp | Ref
| Expression |
1 | | seqf1o.6 |
. . 3
               |
2 | | seqf1o.7 |
. . . 4
 
    
      |
3 | 2 | fmpttd 5705 |
. . 3
                     |
4 | | seqf1o.4 |
. . . . 5
       |
5 | | oveq2 5918 |
. . . . . . . . . . 11
           |
6 | | f1oeq23 5483 |
. . . . . . . . . . 11
                                               |
7 | 5, 5, 6 | syl2anc 411 |
. . . . . . . . . 10
             
               |
8 | 5 | feq2d 5383 |
. . . . . . . . . 10
                     |
9 | 7, 8 | anbi12d 473 |
. . . . . . . . 9
                       
            
            |
10 | | fveq2 5546 |
. . . . . . . . . 10
                   |
11 | | fveq2 5546 |
. . . . . . . . . 10
               |
12 | 10, 11 | eqeq12d 2208 |
. . . . . . . . 9
               
                 |
13 | 9, 12 | imbi12d 234 |
. . . . . . . 8
                                       
                        
       
        |
14 | 13 | 2albidv 1878 |
. . . . . . 7
                                           
                 
                           |
15 | 14 | imbi2d 230 |
. . . . . 6
  
                 
                         
                 
                            |
16 | | oveq2 5918 |
. . . . . . . . . . 11
           |
17 | | f1oeq23 5483 |
. . . . . . . . . . 11
                                               |
18 | 16, 16, 17 | syl2anc 411 |
. . . . . . . . . 10
             
               |
19 | 16 | feq2d 5383 |
. . . . . . . . . 10
                     |
20 | 18, 19 | anbi12d 473 |
. . . . . . . . 9
                       
            
            |
21 | | fveq2 5546 |
. . . . . . . . . 10
                   |
22 | | fveq2 5546 |
. . . . . . . . . 10
               |
23 | 21, 22 | eqeq12d 2208 |
. . . . . . . . 9
               
                 |
24 | 20, 23 | imbi12d 234 |
. . . . . . . 8
                                       
                        
       
        |
25 | 24 | 2albidv 1878 |
. . . . . . 7
                                           
                 
                           |
26 | 25 | imbi2d 230 |
. . . . . 6
  
                 
                         
                 
                            |
27 | | oveq2 5918 |
. . . . . . . . . . 11
               |
28 | | f1oeq23 5483 |
. . . . . . . . . . 11
                                                       |
29 | 27, 27, 28 | syl2anc 411 |
. . . . . . . . . 10
               
                   |
30 | 27 | feq2d 5383 |
. . . . . . . . . 10
                         |
31 | 29, 30 | anbi12d 473 |
. . . . . . . . 9
                         
                               |
32 | | fveq2 5546 |
. . . . . . . . . 10
                       |
33 | | fveq2 5546 |
. . . . . . . . . 10
                   |
34 | 32, 33 | eqeq12d 2208 |
. . . . . . . . 9
                 
                     |
35 | 31, 34 | imbi12d 234 |
. . . . . . . 8
                                         
                              
         
          |
36 | 35 | 2albidv 1878 |
. . . . . . 7
                                             
                                                       |
37 | 36 | imbi2d 230 |
. . . . . 6
    
                 
                         
                                                        |
38 | | oveq2 5918 |
. . . . . . . . . . 11
           |
39 | | f1oeq23 5483 |
. . . . . . . . . . 11
                                               |
40 | 38, 38, 39 | syl2anc 411 |
. . . . . . . . . 10
             
               |
41 | 38 | feq2d 5383 |
. . . . . . . . . 10
                     |
42 | 40, 41 | anbi12d 473 |
. . . . . . . . 9
                       
            
            |
43 | | fveq2 5546 |
. . . . . . . . . 10
                   |
44 | | fveq2 5546 |
. . . . . . . . . 10
               |
45 | 43, 44 | eqeq12d 2208 |
. . . . . . . . 9
               
                 |
46 | 42, 45 | imbi12d 234 |
. . . . . . . 8
                                       
                        
       
        |
47 | 46 | 2albidv 1878 |
. . . . . . 7
                                           
                 
                           |
48 | 47 | imbi2d 230 |
. . . . . 6
  
                 
                         
                 
                            |
49 | | f1of 5492 |
. . . . . . . . . . . . . 14
            
              |
50 | 49 | adantr 276 |
. . . . . . . . . . . . 13
                                     |
51 | | elfz3 10090 |
. . . . . . . . . . . . 13
       |
52 | | fvco3 5620 |
. . . . . . . . . . . . 13
                  
                |
53 | 50, 51, 52 | syl2anr 290 |
. . . . . . . . . . . 12
                                         |
54 | 53 | adantll 476 |
. . . . . . . . . . 11
                          
                |
55 | | ffvelcdm 5683 |
. . . . . . . . . . . . . . . 16
                  
          |
56 | 49, 51, 55 | syl2anr 290 |
. . . . . . . . . . . . . . 15
                         |
57 | | fzsn 10122 |
. . . . . . . . . . . . . . . . . 18
         |
58 | 57 | eleq2d 2263 |
. . . . . . . . . . . . . . . . 17
         
         |
59 | | elsni 3636 |
. . . . . . . . . . . . . . . . 17
             |
60 | 58, 59 | biimtrdi 163 |
. . . . . . . . . . . . . . . 16
                 |
61 | 60 | imp 124 |
. . . . . . . . . . . . . . 15
                 |
62 | 56, 61 | syldan 282 |
. . . . . . . . . . . . . 14
                     |
63 | 62 | adantrr 479 |
. . . . . . . . . . . . 13
                               |
64 | 63 | fveq2d 5550 |
. . . . . . . . . . . 12
                                       |
65 | 64 | adantll 476 |
. . . . . . . . . . 11
                          
              |
66 | 54, 65 | eqtrd 2226 |
. . . . . . . . . 10
                          
            |
67 | | simplr 528 |
. . . . . . . . . . 11
                          
  |
68 | | vex 2763 |
. . . . . . . . . . . . 13
 |
69 | | vex 2763 |
. . . . . . . . . . . . 13
 |
70 | 68, 69 | coex 5203 |
. . . . . . . . . . . 12
   |
71 | 70 | a1i 9 |
. . . . . . . . . . 11
                          
    |
72 | | seqf1og.p |
. . . . . . . . . . . 12
   |
73 | 72 | ad2antrr 488 |
. . . . . . . . . . 11
                          
  |
74 | | seq1g 10524 |
. . . . . . . . . . 11
                     |
75 | 67, 71, 73, 74 | syl3anc 1249 |
. . . . . . . . . 10
                          
                |
76 | 68 | a1i 9 |
. . . . . . . . . . 11
                          
  |
77 | | seq1g 10524 |
. . . . . . . . . . 11
 
             |
78 | 67, 76, 73, 77 | syl3anc 1249 |
. . . . . . . . . 10
                          
            |
79 | 66, 75, 78 | 3eqtr4d 2236 |
. . . . . . . . 9
                          
                |
80 | 79 | ex 115 |
. . . . . . . 8
 

                        
       
       |
81 | 80 | alrimivv 1886 |
. . . . . . 7
 

                 
                          |
82 | 81 | expcom 116 |
. . . . . 6
                                               |
83 | | f1oeq1 5480 |
. . . . . . . . . . . 12
             
               |
84 | | feq1 5378 |
. . . . . . . . . . . 12
                     |
85 | 83, 84 | bi2anan9r 607 |
. . . . . . . . . . 11
 
                       
            
            |
86 | | coeq1 4813 |
. . . . . . . . . . . . . . 15
       |
87 | | coeq2 4814 |
. . . . . . . . . . . . . . 15
       |
88 | 86, 87 | sylan9eq 2246 |
. . . . . . . . . . . . . 14
 
       |
89 | 88 | seqeq3d 10516 |
. . . . . . . . . . . . 13
 
             |
90 | 89 | fveq1d 5548 |
. . . . . . . . . . . 12
 
                   |
91 | | simpl 109 |
. . . . . . . . . . . . . 14
 
   |
92 | 91 | seqeq3d 10516 |
. . . . . . . . . . . . 13
 
         |
93 | 92 | fveq1d 5548 |
. . . . . . . . . . . 12
 
               |
94 | 90, 93 | eqeq12d 2208 |
. . . . . . . . . . 11
 
   
       
                     |
95 | 85, 94 | imbi12d 234 |
. . . . . . . . . 10
 
               
                       
                        
       
        |
96 | 95 | cbval2vw 1944 |
. . . . . . . . 9
                             
       
                                                 |
97 | | simplll 533 |
. . . . . . . . . . . . . . 15
   
                                                                               |
98 | | seqf1o.1 |
. . . . . . . . . . . . . . 15
 

      |
99 | 97, 98 | sylan 283 |
. . . . . . . . . . . . . 14
                                                                                  
  
   |
100 | | seqf1o.2 |
. . . . . . . . . . . . . . 15
 

        |
101 | 97, 100 | sylan 283 |
. . . . . . . . . . . . . 14
                                                                                  
  
     |
102 | | seqf1o.3 |
. . . . . . . . . . . . . . 15
 

            |
103 | 97, 102 | sylan 283 |
. . . . . . . . . . . . . 14
                                                                                  
    
       |
104 | | simpllr 534 |
. . . . . . . . . . . . . 14
   
                                                                                   |
105 | | seqf1o.5 |
. . . . . . . . . . . . . . 15

  |
106 | 97, 105 | syl 14 |
. . . . . . . . . . . . . 14
   
                                                                               |
107 | 97, 72 | syl 14 |
. . . . . . . . . . . . . 14
   
                                                                               |
108 | | simprl 529 |
. . . . . . . . . . . . . 14
   
                                                                                               |
109 | | simprr 531 |
. . . . . . . . . . . . . 14
   
                                                                                         |
110 | | eqid 2193 |
. . . . . . . . . . . . . 14
                                                 |
111 | | eqid 2193 |
. . . . . . . . . . . . . 14
               |
112 | | simplr 528 |
. . . . . . . . . . . . . . 15
   
                                                                                                                         |
113 | 112, 96 | sylib 122 |
. . . . . . . . . . . . . 14
   
                                                                                                                         |
114 | 99, 101, 103, 104, 106, 107, 108, 109, 110, 111, 113 | seqf1oglem2 10581 |
. . . . . . . . . . . . 13
   
                                                                                                 |
115 | 114 | exp31 364 |
. . . . . . . . . . . 12
 
    
                             
       
    
                              
         
          |
116 | 96, 115 | biimtrrid 153 |
. . . . . . . . . . 11
 
    
                             
       
    
                              
         
          |
117 | 116 | alrimdv 1887 |
. . . . . . . . . 10
 
    
                             
       
    
                                                     |
118 | 117 | alrimdv 1887 |
. . . . . . . . 9
 
    
                             
       
    
                                                       |
119 | 96, 118 | biimtrid 152 |
. . . . . . . 8
 
    
                             
       
    
                                                       |
120 | 119 | expcom 116 |
. . . . . . 7
    
                   
                                                                                |
121 | 120 | a2d 26 |
. . . . . 6
    
                                             
                                                        |
122 | 15, 26, 37, 48, 82, 121 | uzind4 9643 |
. . . . 5
    
                                              |
123 | 4, 122 | mpcom 36 |
. . . 4
                                             |
124 | 2 | ralrimiva 2567 |
. . . . . . 7
             |
125 | | eqid 2193 |
. . . . . . . 8
                     |
126 | 125 | fnmpt 5372 |
. . . . . . 7
 
        
                |
127 | 124, 126 | syl 14 |
. . . . . 6
                 |
128 | | eluzel2 9587 |
. . . . . . . 8
    
  |
129 | 4, 128 | syl 14 |
. . . . . . 7
   |
130 | | eluzelz 9591 |
. . . . . . . 8
    
  |
131 | 4, 130 | syl 14 |
. . . . . . 7
   |
132 | 129, 131 | fzfigd 10492 |
. . . . . 6
       |
133 | | fnfi 6985 |
. . . . . 6
                                 |
134 | 127, 132,
133 | syl2anc 411 |
. . . . 5
             |
135 | | f1of 5492 |
. . . . . . 7
            
              |
136 | 1, 135 | syl 14 |
. . . . . 6
               |
137 | 136, 132 | fexd 5780 |
. . . . 5
   |
138 | | f1oeq1 5480 |
. . . . . . . 8
             
               |
139 | | feq1 5378 |
. . . . . . . 8
                                         |
140 | 138, 139 | bi2anan9r 607 |
. . . . . . 7
            
                                                          |
141 | | coeq1 4813 |
. . . . . . . . . . 11
                           |
142 | | coeq2 4814 |
. . . . . . . . . . 11
                           |
143 | 141, 142 | sylan9eq 2246 |
. . . . . . . . . 10
            
                |
144 | 143 | seqeq3d 10516 |
. . . . . . . . 9
            
                      |
145 | 144 | fveq1d 5548 |
. . . . . . . 8
            
                            |
146 | | simpl 109 |
. . . . . . . . . 10
            

           |
147 | 146 | seqeq3d 10516 |
. . . . . . . . 9
            
                  |
148 | 147 | fveq1d 5548 |
. . . . . . . 8
            
                        |
149 | 145, 148 | eqeq12d 2208 |
. . . . . . 7
            
                
                                   |
150 | 140, 149 | imbi12d 234 |
. . . . . 6
            
                                      
             
                                                         |
151 | 150 | spc2gv 2851 |
. . . . 5
                               
                                                                                               |
152 | 134, 137,
151 | syl2anc 411 |
. . . 4
                   
                                                                                               |
153 | 123, 152 | mpd 13 |
. . 3
                                                                       |
154 | 1, 3, 153 | mp2and 433 |
. 2
                    
                |
155 | | fveq2 5546 |
. . . . 5
                   |
156 | 136 | ffvelcdmda 5685 |
. . . . 5
 
    
          |
157 | 155 | eleq1d 2262 |
. . . . . 6
         
           |
158 | 124 | adantr 276 |
. . . . . 6
 
    
            |
159 | 157, 158,
156 | rspcdva 2869 |
. . . . 5
 
    
          |
160 | 125, 155,
156, 159 | fvmptd3 5643 |
. . . 4
 
    
                            |
161 | | fvco3 5620 |
. . . . 5
                  
                                    |
162 | 136, 161 | sylan 283 |
. . . 4
 
    
                                    |
163 | | seqf1o.8 |
. . . 4
 
    
              |
164 | 160, 162,
163 | 3eqtr4d 2236 |
. . 3
 
    
                      |
165 | 134 | elexd 2773 |
. . . 4
             |
166 | | coexg 5202 |
. . . 4
                           |
167 | 165, 137,
166 | syl2anc 411 |
. . 3
               |
168 | | seqf1og.h |
. . 3
   |
169 | 4, 164, 72, 167, 168 | seqfveqg 10539 |
. 2
                    
      |
170 | | fveq2 5546 |
. . . 4
           |
171 | | simpr 110 |
. . . 4
 
    
      |
172 | 170 | eleq1d 2262 |
. . . . 5
     
       |
173 | 172, 158,
171 | rspcdva 2869 |
. . . 4
 
    
      |
174 | 125, 170,
171, 173 | fvmptd3 5643 |
. . 3
 
    
                    |
175 | | seqf1og.g |
. . 3
   |
176 | 4, 174, 72, 134, 175 | seqfveqg 10539 |
. 2
                  
      |
177 | 154, 169,
176 | 3eqtr3d 2234 |
1
               |