Proof of Theorem seqf1olem2
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.6 |
. . . . . . . . . 10
             |
2 | | ffn 5751 |
. . . . . . . . . 10
      
   
        |
3 | 1, 2 | syl 17 |
. . . . . . . . 9
         |
4 | | fzssp1 11870 |
. . . . . . . . 9
           |
5 | | fnssres 5711 |
. . . . . . . . 9
               
               |
6 | 3, 4, 5 | sylancl 673 |
. . . . . . . 8
             |
7 | | fzfid 12218 |
. . . . . . . 8
       |
8 | | fnfi 7875 |
. . . . . . . 8
                         |
9 | 6, 7, 8 | syl2anc 671 |
. . . . . . 7
         |
10 | | elex 3066 |
. . . . . . 7
 
             |
11 | 9, 10 | syl 17 |
. . . . . 6
         |
12 | | seqf1o.1 |
. . . . . . . . 9
 

      |
13 | | seqf1o.2 |
. . . . . . . . 9
 

        |
14 | | seqf1o.3 |
. . . . . . . . 9
 

            |
15 | | seqf1o.4 |
. . . . . . . . 9
       |
16 | | seqf1o.5 |
. . . . . . . . 9

  |
17 | | seqf1olem.5 |
. . . . . . . . 9
                   |
18 | | seqf1olem.7 |
. . . . . . . . 9
                  |
19 | | seqf1olem.8 |
. . . . . . . . 9
    
   |
20 | 12, 13, 14, 15, 16, 17, 1, 18, 19 | seqf1olem1 12284 |
. . . . . . . 8
               |
21 | | f1of 5837 |
. . . . . . . 8
            
              |
22 | 20, 21 | syl 17 |
. . . . . . 7
               |
23 | | fex2 6775 |
. . . . . . 7
                         |
24 | 22, 7, 7, 23 | syl3anc 1276 |
. . . . . 6
   |
25 | 11, 24 | jca 539 |
. . . . 5
       
   |
26 | | seqf1olem.9 |
. . . . 5
                                             |
27 | | fssres 5772 |
. . . . . . 7
                                       |
28 | 1, 4, 27 | sylancl 673 |
. . . . . 6
                 |
29 | 20, 28 | jca 539 |
. . . . 5
                               |
30 | | f1oeq1 5828 |
. . . . . . . 8
             
               |
31 | | feq1 5732 |
. . . . . . . 8
      
        
                 |
32 | 30, 31 | bi2anan9r 890 |
. . . . . . 7
                               
            
                  |
33 | | coeq1 5011 |
. . . . . . . . . . 11
      
            |
34 | | coeq2 5012 |
. . . . . . . . . . 11
                   |
35 | 33, 34 | sylan9eq 2516 |
. . . . . . . . . 10
                     |
36 | 35 | seqeq3d 12253 |
. . . . . . . . 9
                           |
37 | 36 | fveq1d 5890 |
. . . . . . . 8
                                 |
38 | | simpl 463 |
. . . . . . . . . 10
                 |
39 | 38 | seqeq3d 12253 |
. . . . . . . . 9
                       |
40 | 39 | fveq1d 5890 |
. . . . . . . 8
                             |
41 | 37, 40 | eqeq12d 2477 |
. . . . . . 7
                       
               
             |
42 | 32, 41 | imbi12d 326 |
. . . . . 6
                                               
             
                              
              |
43 | 42 | spc2gv 3149 |
. . . . 5
                                                                                
               
              |
44 | 25, 26, 29, 43 | syl3c 63 |
. . . 4
    
                        |
45 | | fvres 5902 |
. . . . . 6
                     |
46 | 45 | adantl 472 |
. . . . 5
 
    
                |
47 | 15, 46 | seqfveq 12269 |
. . . 4
                     |
48 | 44, 47 | eqtrd 2496 |
. . 3
    
                  |
49 | 48 | oveq1d 6330 |
. 2
   
                         
         |
50 | 12 | adantlr 726 |
. . . . 5
        
 
    |
51 | 14 | adantlr 726 |
. . . . 5
        
 
 
        |
52 | | elfzuz3 11826 |
. . . . . . 7
           |
53 | 52 | adantl 472 |
. . . . . 6
 
    
      |
54 | | eluzp1p1 11213 |
. . . . . 6
    
          |
55 | 53, 54 | syl 17 |
. . . . 5
 
    
          |
56 | | elfzuz 11825 |
. . . . . 6
           |
57 | 56 | adantl 472 |
. . . . 5
 
    
      |
58 | | f1of 5837 |
. . . . . . . . . 10
      
       
 
     
       
    |
59 | 17, 58 | syl 17 |
. . . . . . . . 9
                   |
60 | | fco 5762 |
. . . . . . . . 9
                         
   
      
      |
61 | 1, 59, 60 | syl2anc 671 |
. . . . . . . 8
               |
62 | 61, 16 | fssd 5761 |
. . . . . . 7
               |
63 | 62 | ffvelrnda 6045 |
. . . . . 6
 
      
 
      |
64 | 63 | adantlr 726 |
. . . . 5
           
           |
65 | 50, 51, 55, 57, 64 | seqsplit 12278 |
. . . 4
 
    
       
                    
     |
66 | | elfzp12 11902 |
. . . . . . 7
    
                |
67 | 66 | biimpa 491 |
. . . . . 6
           
 
       |
68 | 15, 67 | sylan 478 |
. . . . 5
 
    

         |
69 | | seqeq1 12248 |
. . . . . . . . . . 11
             |
70 | 69 | eqcomd 2468 |
. . . . . . . . . 10
             |
71 | 70 | fveq1d 5890 |
. . . . . . . . 9
                   |
72 | | f1ocnv 5849 |
. . . . . . . . . . . . 13
      
       
 
      
       
    |
73 | | f1of 5837 |
. . . . . . . . . . . . 13
                                     |
74 | 17, 72, 73 | 3syl 18 |
. . . . . . . . . . . 12
                    |
75 | | peano2uz 11241 |
. . . . . . . . . . . . 13
    
        |
76 | | eluzfz2 11836 |
. . . . . . . . . . . . 13
      
     
    |
77 | 15, 75, 76 | 3syl 18 |
. . . . . . . . . . . 12
           |
78 | 74, 77 | ffvelrnd 6046 |
. . . . . . . . . . 11
     
          |
79 | 19, 78 | syl5eqel 2544 |
. . . . . . . . . 10
         |
80 | | elfzelz 11829 |
. . . . . . . . . 10
    
    |
81 | | seq1 12258 |
. . . . . . . . . 10
                 |
82 | 79, 80, 81 | 3syl 18 |
. . . . . . . . 9
                 |
83 | 71, 82 | sylan9eqr 2518 |
. . . . . . . 8
 
                 |
84 | 83 | oveq1d 6330 |
. . . . . . 7
 
                   
         
 
       
     |
85 | | simpr 467 |
. . . . . . . . 9
 
   |
86 | | eluzfz1 11835 |
. . . . . . . . . . 11
    
      |
87 | 15, 86 | syl 17 |
. . . . . . . . . 10
       |
88 | 87 | adantr 471 |
. . . . . . . . 9
 
       |
89 | 85, 88 | eqeltrd 2540 |
. . . . . . . 8
 
       |
90 | 13 | adantlr 726 |
. . . . . . . . . 10
        
 
      |
91 | 16 | adantr 471 |
. . . . . . . . . 10
 
    
  |
92 | 61 | adantr 471 |
. . . . . . . . . 10
 
    
              |
93 | 79 | adantr 471 |
. . . . . . . . . 10
 
    
        |
94 | | peano2uz 11241 |
. . . . . . . . . . 11
    
        |
95 | | fzss1 11866 |
. . . . . . . . . . 11
      
 
              |
96 | 57, 94, 95 | 3syl 18 |
. . . . . . . . . 10
 
    
 
              |
97 | 50, 90, 51, 55, 91, 92, 93, 96 | seqf1olem2a 12283 |
. . . . . . . . 9
 
    
      
 
                     
           |
98 | | 1zzd 10997 |
. . . . . . . . . . 11
 
    
  |
99 | | elfzuz 11825 |
. . . . . . . . . . . . . . . . . 18
    
        |
100 | | fzss1 11866 |
. . . . . . . . . . . . . . . . . 18
    
          |
101 | 79, 99, 100 | 3syl 18 |
. . . . . . . . . . . . . . . . 17
    
      |
102 | 101 | sselda 3444 |
. . . . . . . . . . . . . . . 16
 
    
      |
103 | 22 | ffvelrnda 6045 |
. . . . . . . . . . . . . . . 16
 
    
          |
104 | 102, 103 | syldan 477 |
. . . . . . . . . . . . . . 15
 
    
          |
105 | | fvres 5902 |
. . . . . . . . . . . . . . 15
                                 |
106 | 104, 105 | syl 17 |
. . . . . . . . . . . . . 14
 
    
                        |
107 | | breq1 4419 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
108 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
   |
109 | | oveq1 6322 |
. . . . . . . . . . . . . . . . . . . 20
       |
110 | 107, 108,
109 | ifbieq12d 3920 |
. . . . . . . . . . . . . . . . . . 19
           
     |
111 | 110 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . 18
     
                   |
112 | | fvex 5898 |
. . . . . . . . . . . . . . . . . 18
            |
113 | 111, 18, 112 | fvmpt 5971 |
. . . . . . . . . . . . . . . . 17
                      |
114 | 102, 113 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
          
      |
115 | | elfzle1 11831 |
. . . . . . . . . . . . . . . . . . 19
       |
116 | 115 | adantl 472 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
117 | 79, 80 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
   |
118 | 117 | zred 11069 |
. . . . . . . . . . . . . . . . . . . 20
   |
119 | 118 | adantr 471 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
120 | | elfzelz 11829 |
. . . . . . . . . . . . . . . . . . . . 21
       |
121 | 120 | adantl 472 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  |
122 | 121 | zred 11069 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
123 | 119, 122 | lenltd 9807 |
. . . . . . . . . . . . . . . . . 18
 
    

   |
124 | 116, 123 | mpbid 215 |
. . . . . . . . . . . . . . . . 17
 
    
  |
125 | | iffalse 3902 |
. . . . . . . . . . . . . . . . . 18
            |
126 | 125 | fveq2d 5892 |
. . . . . . . . . . . . . . . . 17
     
 
            |
127 | 124, 126 | syl 17 |
. . . . . . . . . . . . . . . 16
 
    
                   |
128 | 114, 127 | eqtrd 2496 |
. . . . . . . . . . . . . . 15
 
    
            |
129 | 128 | fveq2d 5892 |
. . . . . . . . . . . . . 14
 
    
                    |
130 | 106, 129 | eqtrd 2496 |
. . . . . . . . . . . . 13
 
    
                    
     |
131 | | fvco3 5965 |
. . . . . . . . . . . . . . 15
                  
                            |
132 | 22, 131 | sylan 478 |
. . . . . . . . . . . . . 14
 
    
                            |
133 | 102, 132 | syldan 477 |
. . . . . . . . . . . . 13
 
    
                            |
134 | | fzp1elp1 11878 |
. . . . . . . . . . . . . . 15
          
    |
135 | 102, 134 | syl 17 |
. . . . . . . . . . . . . 14
 
    
     
    |
136 | | fvco3 5965 |
. . . . . . . . . . . . . . 15
                          
 
                  |
137 | 59, 136 | sylan 478 |
. . . . . . . . . . . . . 14
 
     
                       |
138 | 135, 137 | syldan 477 |
. . . . . . . . . . . . 13
 
    
 
                  |
139 | 130, 133,
138 | 3eqtr4d 2506 |
. . . . . . . . . . . 12
 
    
                      |
140 | 139 | adantlr 726 |
. . . . . . . . . . 11
                                   |
141 | 53, 98, 140 | seqshft2 12271 |
. . . . . . . . . 10
 
    
               
            |
142 | | fvco3 5965 |
. . . . . . . . . . . . 13
                        
 
              |
143 | 59, 79, 142 | syl2anc 671 |
. . . . . . . . . . . 12
                 |
144 | 19 | fveq2i 5891 |
. . . . . . . . . . . . . 14
                |
145 | | f1ocnvfv2 6201 |
. . . . . . . . . . . . . . 15
                  
                       |
146 | 17, 77, 145 | syl2anc 671 |
. . . . . . . . . . . . . 14
                |
147 | 144, 146 | syl5eq 2508 |
. . . . . . . . . . . . 13
         |
148 | 147 | fveq2d 5892 |
. . . . . . . . . . . 12
                 |
149 | 143, 148 | eqtr2d 2497 |
. . . . . . . . . . 11
    
          |
150 | 149 | adantr 471 |
. . . . . . . . . 10
 
    
              |
151 | 141, 150 | oveq12d 6333 |
. . . . . . . . 9
 
    
                  
     
                   |
152 | 97, 151 | eqtr4d 2499 |
. . . . . . . 8
 
    
      
 
                         
         |
153 | 89, 152 | syldan 477 |
. . . . . . 7
 
       
 
       
       
                   |
154 | 85 | seqeq1d 12251 |
. . . . . . . . 9
 
             
           |
155 | 154 | fveq1d 5890 |
. . . . . . . 8
 
                
              |
156 | 155 | oveq1d 6330 |
. . . . . . 7
 
               
         
                     |
157 | 84, 153, 156 | 3eqtrd 2500 |
. . . . . 6
 
                   
       
                   |
158 | | eluzel2 11193 |
. . . . . . . . . . . 12
    
  |
159 | 15, 158 | syl 17 |
. . . . . . . . . . 11
   |
160 | | elfzuz 11825 |
. . . . . . . . . . 11
               |
161 | | eluzp1m1 11211 |
. . . . . . . . . . 11
 
   
           |
162 | 159, 160,
161 | syl2an 484 |
. . . . . . . . . 10
 
       
       |
163 | | eluzelz 11197 |
. . . . . . . . . . . . . . . . . . . . 21
    
  |
164 | 15, 163 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
   |
165 | 164 | zcnd 11070 |
. . . . . . . . . . . . . . . . . . 19
   |
166 | | ax-1cn 9623 |
. . . . . . . . . . . . . . . . . . 19
 |
167 | | pncan 9907 |
. . . . . . . . . . . . . . . . . . 19
 
       |
168 | 165, 166,
167 | sylancl 673 |
. . . . . . . . . . . . . . . . . 18
       |
169 | | peano2zm 11009 |
. . . . . . . . . . . . . . . . . . . 20
 
   |
170 | 79, 80, 169 | 3syl 18 |
. . . . . . . . . . . . . . . . . . 19
     |
171 | | elfzuz3 11826 |
. . . . . . . . . . . . . . . . . . . . 21
    
  
       |
172 | 79, 171 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
         |
173 | 117 | zcnd 11070 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
174 | | npcan 9910 |
. . . . . . . . . . . . . . . . . . . . . 22
 
       |
175 | 173, 166,
174 | sylancl 673 |
. . . . . . . . . . . . . . . . . . . . 21
       |
176 | 175 | fveq2d 5892 |
. . . . . . . . . . . . . . . . . . . 20
     
         |
177 | 172, 176 | eleqtrrd 2543 |
. . . . . . . . . . . . . . . . . . 19
             |
178 | | eluzp1m1 11211 |
. . . . . . . . . . . . . . . . . . 19
    
                 
    |
179 | 170, 177,
178 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
        
    |
180 | 168, 179 | eqeltrrd 2541 |
. . . . . . . . . . . . . . . . 17
    
    |
181 | | fzss2 11867 |
. . . . . . . . . . . . . . . . 17
    
 
            |
182 | 180, 181 | syl 17 |
. . . . . . . . . . . . . . . 16
    
 
      |
183 | 182 | sselda 3444 |
. . . . . . . . . . . . . . 15
 
      
      |
184 | 183, 103 | syldan 477 |
. . . . . . . . . . . . . 14
 
      
          |
185 | 184, 105 | syl 17 |
. . . . . . . . . . . . 13
 
      
                        |
186 | 183, 113 | syl 17 |
. . . . . . . . . . . . . . 15
 
      
          
      |
187 | | elfzm11 11894 |
. . . . . . . . . . . . . . . . . . 19
 
        
    |
188 | 159, 117,
187 | syl2anc 671 |
. . . . . . . . . . . . . . . . . 18
        
    |
189 | 188 | biimpa 491 |
. . . . . . . . . . . . . . . . 17
 
      
    |
190 | 189 | simp3d 1028 |
. . . . . . . . . . . . . . . 16
 
      
  |
191 | | iftrue 3899 |
. . . . . . . . . . . . . . . . 17
  
 
     |
192 | 191 | fveq2d 5892 |
. . . . . . . . . . . . . . . 16
     
 
          |
193 | 190, 192 | syl 17 |
. . . . . . . . . . . . . . 15
 
      
                 |
194 | 186, 193 | eqtrd 2496 |
. . . . . . . . . . . . . 14
 
      
          |
195 | 194 | fveq2d 5892 |
. . . . . . . . . . . . 13
 
      
                  |
196 | 185, 195 | eqtr2d 2497 |
. . . . . . . . . . . 12
 
      
                        |
197 | | peano2uz 11241 |
. . . . . . . . . . . . . . 15
    
 
          |
198 | | fzss2 11867 |
. . . . . . . . . . . . . . 15
      
 
              |
199 | 180, 197,
198 | 3syl 18 |
. . . . . . . . . . . . . 14
    
 
        |
200 | 199 | sselda 3444 |
. . . . . . . . . . . . 13
 
      
        |
201 | | fvco3 5965 |
. . . . . . . . . . . . . 14
                        
 
              |
202 | 59, 201 | sylan 478 |
. . . . . . . . . . . . 13
 
      
 
              |
203 | 200, 202 | syldan 477 |
. . . . . . . . . . . 12
 
      
 
              |
204 | 183, 132 | syldan 477 |
. . . . . . . . . . . 12
 
      
                            |
205 | 196, 203,
204 | 3eqtr4d 2506 |
. . . . . . . . . . 11
 
      
 
                  |
206 | 205 | adantlr 726 |
. . . . . . . . . 10
             
           
           |
207 | 162, 206 | seqfveq 12269 |
. . . . . . . . 9
 
              
                    |
208 | | fzp1ss 11876 |
. . . . . . . . . . . 12
             |
209 | 15, 158, 208 | 3syl 18 |
. . . . . . . . . . 11
      
      |
210 | 209 | sselda 3444 |
. . . . . . . . . 10
 
             |
211 | 210, 152 | syldan 477 |
. . . . . . . . 9
 
             
 
       
       
                   |
212 | 207, 211 | oveq12d 6333 |
. . . . . . . 8
 
               
        
 
       
      
                
                      |
213 | 200, 63 | syldan 477 |
. . . . . . . . . . . 12
 
      
 
      |
214 | 213 | adantlr 726 |
. . . . . . . . . . 11
             
           |
215 | 12 | adantlr 726 |
. . . . . . . . . . 11
          
 
    |
216 | 162, 214,
215 | seqcl 12265 |
. . . . . . . . . 10
 
              
    |
217 | 61, 79 | ffvelrnd 6046 |
. . . . . . . . . . . 12
         |
218 | 16, 217 | sseldd 3445 |
. . . . . . . . . . 11
         |
219 | 218 | adantr 471 |
. . . . . . . . . 10
 
               |
220 | 96 | sselda 3444 |
. . . . . . . . . . . . 13
             
      
    |
221 | 220, 64 | syldan 477 |
. . . . . . . . . . . 12
             
           |
222 | 55, 221, 50 | seqcl 12265 |
. . . . . . . . . . 11
 
    
 
       
    |
223 | 210, 222 | syldan 477 |
. . . . . . . . . 10
 
                
    |
224 | 216, 219,
223 | 3jca 1194 |
. . . . . . . . 9
 
               
                 
     |
225 | 14 | caovassg 6494 |
. . . . . . . . 9
 
        
                 
       

                       
     

                       
      |
226 | 224, 225 | syldan 477 |
. . . . . . . 8
 
          

                       
     

                       
      |
227 | 1, 16 | fssd 5761 |
. . . . . . . . . . . . . . . 16
             |
228 | | fssres 5772 |
. . . . . . . . . . . . . . . 16
                                       |
229 | 227, 4, 228 | sylancl 673 |
. . . . . . . . . . . . . . 15
                 |
230 | | fco 5762 |
. . . . . . . . . . . . . . 15
                                               |
231 | 229, 22, 230 | syl2anc 671 |
. . . . . . . . . . . . . 14
                   |
232 | 231 | ffvelrnda 6045 |
. . . . . . . . . . . . 13
 
    
              |
233 | 183, 232 | syldan 477 |
. . . . . . . . . . . 12
 
      
              |
234 | 233 | adantlr 726 |
. . . . . . . . . . 11
             
                 |
235 | 162, 234,
215 | seqcl 12265 |
. . . . . . . . . 10
 
                         |
236 | | elfzuz3 11826 |
. . . . . . . . . . . 12
             |
237 | 236 | adantl 472 |
. . . . . . . . . . 11
 
             |
238 | 102, 232 | syldan 477 |
. . . . . . . . . . . 12
 
    
              |
239 | 238 | adantlr 726 |
. . . . . . . . . . 11
                             |
240 | 237, 239,
215 | seqcl 12265 |
. . . . . . . . . 10
 
                       |
241 | 227, 77 | ffvelrnd 6046 |
. . . . . . . . . . 11
    
    |
242 | 241 | adantr 471 |
. . . . . . . . . 10
 
               |
243 | 235, 240,
242 | 3jca 1194 |
. . . . . . . . 9
 
                     
                         |
244 | 14 | caovassg 6494 |
. . . . . . . . 9
 
                                                      
                                                           
      |
245 | 243, 244 | syldan 477 |
. . . . . . . 8
 
          
                                                  
                
          |
246 | 212, 226,
245 | 3eqtr4d 2506 |
. . . . . . 7
 
          

                       
                      
                
     |
247 | | seqm1 12262 |
. . . . . . . . 9
 
   
                               |
248 | 159, 160,
247 | syl2an 484 |
. . . . . . . 8
 
                       
           |
249 | 248 | oveq1d 6330 |
. . . . . . 7
 
                         
      

                       
     |
250 | 14 | adantlr 726 |
. . . . . . . . . 10
          
 
 
        |
251 | | elfzelz 11829 |
. . . . . . . . . . . . . . 15
         |
252 | 251 | adantl 472 |
. . . . . . . . . . . . . 14
 
         |
253 | 252 | zcnd 11070 |
. . . . . . . . . . . . 13
 
         |
254 | 253, 166,
174 | sylancl 673 |
. . . . . . . . . . . 12
 
             |
255 | 254 | fveq2d 5892 |
. . . . . . . . . . 11
 
                     |
256 | 237, 255 | eleqtrrd 2543 |
. . . . . . . . . 10
 
           
     |
257 | 232 | adantlr 726 |
. . . . . . . . . 10
                             |
258 | 215, 250,
256, 162, 257 | seqsplit 12278 |
. . . . . . . . 9
 
                                                           |
259 | 254 | seqeq1d 12251 |
. . . . . . . . . . 11
 
                       
           |
260 | 259 | fveq1d 5890 |
. . . . . . . . . 10
 
                          
              |
261 | 260 | oveq2d 6331 |
. . . . . . . . 9
 
                     
                                   
                   |
262 | 258, 261 | eqtrd 2496 |
. . . . . . . 8
 
                                       
               |
263 | 262 | oveq1d 6330 |
. . . . . . 7
 
                     
                          
                
     |
264 | 246, 249,
263 | 3eqtr4d 2506 |
. . . . . 6
 
                         
       
                   |
265 | 157, 264 | jaodan 799 |
. . . . 5
 

          

    
 
                         
         |
266 | 68, 265 | syldan 477 |
. . . 4
 
    
        
 
       
       
                   |
267 | 65, 266 | eqtrd 2496 |
. . 3
 
    
       
                
         |
268 | 15 | adantr 471 |
. . . . 5
 

        |
269 | | seqp1 12260 |
. . . . 5
    
       
                      |
270 | 268, 269 | syl 17 |
. . . 4
 

         
                      |
271 | 113 | adantl 472 |
. . . . . . . . . 10
     
                      |
272 | | elfzelz 11829 |
. . . . . . . . . . . . . . . 16
       |
273 | 272 | zred 11069 |
. . . . . . . . . . . . . . 15
       |
274 | 273 | adantl 472 |
. . . . . . . . . . . . . 14
 
    
  |
275 | 164 | zred 11069 |
. . . . . . . . . . . . . . 15
   |
276 | 275 | adantr 471 |
. . . . . . . . . . . . . 14
 
    
  |
277 | | peano2re 9832 |
. . . . . . . . . . . . . . 15
 
   |
278 | 276, 277 | syl 17 |
. . . . . . . . . . . . . 14
 
    
    |
279 | | elfzle2 11832 |
. . . . . . . . . . . . . . 15
       |
280 | 279 | adantl 472 |
. . . . . . . . . . . . . 14
 
    
  |
281 | 276 | ltp1d 10565 |
. . . . . . . . . . . . . 14
 
    
    |
282 | 274, 276,
278, 280, 281 | lelttrd 9819 |
. . . . . . . . . . . . 13
 
    
    |
283 | 282 | adantlr 726 |
. . . . . . . . . . . 12
     
         |
284 | | simplr 767 |
. . . . . . . . . . . 12
     
    
    |
285 | 283, 284 | breqtrrd 4443 |
. . . . . . . . . . 11
     
       |
286 | 285, 192 | syl 17 |
. . . . . . . . . 10
     
         
 
          |
287 | 271, 286 | eqtrd 2496 |
. . . . . . . . 9
     
               |
288 | 287 | fveq2d 5892 |
. . . . . . . 8
     
                                   |
289 | 273 | adantl 472 |
. . . . . . . . . . 11
     
    
  |
290 | 289, 285 | gtned 9796 |
. . . . . . . . . 10
     
       |
291 | 59 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
     
          
            |
292 | | fzelp1 11877 |
. . . . . . . . . . . . . . . 16
        
    |
293 | 292 | adantl 472 |
. . . . . . . . . . . . . . 15
     
    
        |
294 | 291, 293 | ffvelrnd 6046 |
. . . . . . . . . . . . . 14
     
                 |
295 | 15 | ad2antrr 737 |
. . . . . . . . . . . . . . 15
     
    
      |
296 | | elfzp1 11875 |
. . . . . . . . . . . . . . 15
    
        
                     |
297 | 295, 296 | syl 17 |
. . . . . . . . . . . . . 14
     
                                   |
298 | 294, 297 | mpbid 215 |
. . . . . . . . . . . . 13
     
                       |
299 | 298 | ord 383 |
. . . . . . . . . . . 12
     
             
         |
300 | 17 | ad2antrr 737 |
. . . . . . . . . . . . . 14
     
          
       
    |
301 | | f1ocnvfv 6202 |
. . . . . . . . . . . . . 14
                 
                        |
302 | 300, 293,
301 | syl2anc 671 |
. . . . . . . . . . . . 13
     
                      |
303 | 19 | eqeq1i 2467 |
. . . . . . . . . . . . 13

         |
304 | 302, 303 | syl6ibr 235 |
. . . . . . . . . . . 12
     
               |
305 | 299, 304 | syld 45 |
. . . . . . . . . . 11
     
             
   |
306 | 305 | necon1ad 2653 |
. . . . . . . . . 10
     
                 |
307 | 290, 306 | mpd 15 |
. . . . . . . . 9
     
               |
308 | | fvres 5902 |
. . . . . . . . 9
                                 |
309 | 307, 308 | syl 17 |
. . . . . . . 8
     
                             |
310 | 288, 309 | eqtr2d 2497 |
. . . . . . 7
     
              
              |
311 | 59, 292, 201 | syl2an 484 |
. . . . . . . 8
 
    
 
              |
312 | 311 | adantlr 726 |
. . . . . . 7
     
                     |
313 | 132 | adantlr 726 |
. . . . . . 7
     
                                 |
314 | 310, 312,
313 | 3eqtr4d 2506 |
. . . . . 6
     
                         |
315 | 268, 314 | seqfveq 12269 |
. . . . 5
 

                          |
316 | | fvco3 5965 |
. . . . . . . 8
                          
 
                  |
317 | 59, 77, 316 | syl2anc 671 |
. . . . . . 7
      
        
     |
318 | 317 | adantr 471 |
. . . . . 6
 

                      |
319 | | simpr 467 |
. . . . . . . . . 10
 

      |
320 | 19, 319 | syl5eqr 2510 |
. . . . . . . . 9
 

             |
321 | 320 | fveq2d 5892 |
. . . . . . . 8
 

                     |
322 | 146 | adantr 471 |
. . . . . . . 8
 

                 |
323 | 321, 322 | eqtr3d 2498 |
. . . . . . 7
 

            |
324 | 323 | fveq2d 5892 |
. . . . . 6
 

               
    |
325 | 318, 324 | eqtrd 2496 |
. . . . 5
 

             
    |
326 | 315, 325 | oveq12d 6333 |
. . . 4
 

                                  
         |
327 | 270, 326 | eqtrd 2496 |
. . 3
 

         
                
         |
328 | | elfzp1 11875 |
. . . . 5
    
    
             |
329 | 15, 328 | syl 17 |
. . . 4
                   |
330 | 79, 329 | mpbid 215 |
. . 3
           |
331 | 267, 327,
330 | mpjaodan 800 |
. 2
             
                     |
332 | | seqp1 12260 |
. . 3
    
     
        
         |
333 | 15, 332 | syl 17 |
. 2
           
       
     |
334 | 49, 331, 333 | 3eqtr4d 2506 |
1
                     |