Proof of Theorem seqf1oglem1
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.7 |
. 2
                  |
2 | | seqf1olem.5 |
. . . . 5
                   |
3 | | f1of 5492 |
. . . . 5
      
       
 
     
       
    |
4 | 2, 3 | syl 14 |
. . . 4
                   |
5 | 4 | adantr 276 |
. . 3
 
    
     
       
    |
6 | | fzelp1 10130 |
. . . . 5
        
    |
7 | 6 | adantl 277 |
. . . 4
 
    
        |
8 | | fzp1elp1 10131 |
. . . . 5
          
    |
9 | 8 | adantl 277 |
. . . 4
 
    
     
    |
10 | | elfzelz 10081 |
. . . . 5
       |
11 | | seqf1olem.8 |
. . . . . . 7
    
   |
12 | | f1ocnv 5505 |
. . . . . . . . . . 11
      
       
 
      
       
    |
13 | 2, 12 | syl 14 |
. . . . . . . . . 10
                    |
14 | | f1of1 5491 |
. . . . . . . . . 10
                                     |
15 | 13, 14 | syl 14 |
. . . . . . . . 9
                    |
16 | | f1f 5451 |
. . . . . . . . 9
                        
       
    |
17 | 15, 16 | syl 14 |
. . . . . . . 8
                    |
18 | | seqf1o.4 |
. . . . . . . . . 10
       |
19 | | peano2uz 9638 |
. . . . . . . . . 10
    
        |
20 | 18, 19 | syl 14 |
. . . . . . . . 9
         |
21 | | eluzfz2 10088 |
. . . . . . . . 9
      
     
    |
22 | 20, 21 | syl 14 |
. . . . . . . 8
           |
23 | 17, 22 | ffvelcdmd 5686 |
. . . . . . 7
     
          |
24 | 11, 23 | eqeltrid 2280 |
. . . . . 6
         |
25 | 24 | elfzelzd 10082 |
. . . . 5
   |
26 | | zdclt 9384 |
. . . . 5
 
 DECID   |
27 | 10, 25, 26 | syl2anr 290 |
. . . 4
 
    
DECID
  |
28 | 7, 9, 27 | ifcldcd 3593 |
. . 3
 
    
 
        
    |
29 | 5, 28 | ffvelcdmd 5686 |
. 2
 
    
              
    |
30 | 17 | adantr 276 |
. . . . 5
 
    
      
            |
31 | | fzelp1 10130 |
. . . . . 6
        
    |
32 | 31 | adantl 277 |
. . . . 5
 
    
        |
33 | 30, 32 | ffvelcdmd 5686 |
. . . 4
 
    
        
    |
34 | 33 | elfzelzd 10082 |
. . 3
 
    
       |
35 | | peano2zm 9345 |
. . . 4
               |
36 | 34, 35 | syl 14 |
. . 3
 
    
         |
37 | 25 | adantr 276 |
. . . 4
 
    
  |
38 | | zdclt 9384 |
. . . 4
        DECID        |
39 | 34, 37, 38 | syl2anc 411 |
. . 3
 
    
DECID        |
40 | 34, 36, 39 | ifcldcd 3593 |
. 2
 
    
                        |
41 | | iftrue 3562 |
. . . . . . . . 9
          |
42 | 41 | fveq2d 5550 |
. . . . . . . 8
     
            |
43 | 42 | eqeq2d 2205 |
. . . . . . 7
                    |
44 | 43 | adantl 277 |
. . . . . 6
                            |
45 | | simprr 531 |
. . . . . . . . 9
        
            |
46 | 5, 7 | ffvelcdmd 5686 |
. . . . . . . . . . . . 13
 
    
            |
47 | 46 | elfzelzd 10082 |
. . . . . . . . . . . 12
 
    
      |
48 | | eluzel2 9587 |
. . . . . . . . . . . . . 14
    
  |
49 | 18, 48 | syl 14 |
. . . . . . . . . . . . 13
   |
50 | 49 | adantr 276 |
. . . . . . . . . . . 12
 
    
  |
51 | | uzssz 9602 |
. . . . . . . . . . . . . 14
     |
52 | 51, 18 | sselid 3177 |
. . . . . . . . . . . . 13
   |
53 | 52 | adantr 276 |
. . . . . . . . . . . 12
 
    
  |
54 | | fzdcel 10096 |
. . . . . . . . . . . 12
     

DECID           |
55 | 47, 50, 53, 54 | syl3anc 1249 |
. . . . . . . . . . 11
 
    
DECID           |
56 | 55 | adantr 276 |
. . . . . . . . . 10
        
      DECID           |
57 | 10 | zred 9429 |
. . . . . . . . . . . 12
       |
58 | 57 | ad2antlr 489 |
. . . . . . . . . . 11
        
        |
59 | | simprl 529 |
. . . . . . . . . . 11
        
        |
60 | 58, 59 | gtned 8122 |
. . . . . . . . . 10
        
        |
61 | 4 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
        
                   
    |
62 | | fzssp1 10123 |
. . . . . . . . . . . . . . . . 17
           |
63 | | simplr 528 |
. . . . . . . . . . . . . . . . 17
        
            |
64 | 62, 63 | sselid 3177 |
. . . . . . . . . . . . . . . 16
        
              |
65 | 61, 64 | ffvelcdmd 5686 |
. . . . . . . . . . . . . . 15
        
                  |
66 | | elfzp1 10128 |
. . . . . . . . . . . . . . . . 17
    
        
                     |
67 | 18, 66 | syl 14 |
. . . . . . . . . . . . . . . 16
                               |
68 | 67 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
        
              
                     |
69 | 65, 68 | mpbid 147 |
. . . . . . . . . . . . . 14
        
                        |
70 | 69 | ord 725 |
. . . . . . . . . . . . 13
        
              
         |
71 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
        
                        |
72 | | f1ocnvfv 5814 |
. . . . . . . . . . . . . . 15
                 
                        |
73 | 71, 64, 72 | syl2anc 411 |
. . . . . . . . . . . . . 14
        
            
          |
74 | 11 | eqeq1i 2201 |
. . . . . . . . . . . . . 14

         |
75 | 73, 74 | imbitrrdi 162 |
. . . . . . . . . . . . 13
        
            
   |
76 | 70, 75 | syld 45 |
. . . . . . . . . . . 12
        
              
   |
77 | 76 | a1d 22 |
. . . . . . . . . . 11
        
      DECID                 
    |
78 | 77 | necon1addc 2440 |
. . . . . . . . . 10
        
      DECID                      |
79 | 56, 60, 78 | mp2d 47 |
. . . . . . . . 9
        
                |
80 | 45, 79 | eqeltrd 2270 |
. . . . . . . 8
        
            |
81 | 45 | eqcomd 2199 |
. . . . . . . . . . . 12
        
            |
82 | | f1ocnvfv 5814 |
. . . . . . . . . . . . 13
                 
                    |
83 | 71, 64, 82 | syl2anc 411 |
. . . . . . . . . . . 12
        
          
        |
84 | 81, 83 | mpd 13 |
. . . . . . . . . . 11
        
             |
85 | 84, 59 | eqbrtrd 4051 |
. . . . . . . . . 10
        
             |
86 | | iftrue 3562 |
. . . . . . . . . 10
                                   |
87 | 85, 86 | syl 14 |
. . . . . . . . 9
        
                                   |
88 | 87, 84 | eqtr2d 2227 |
. . . . . . . 8
        
                              |
89 | 80, 88 | jca 306 |
. . . . . . 7
        
          
                         |
90 | 89 | expr 375 |
. . . . . 6
                                             |
91 | 44, 90 | sylbid 150 |
. . . . 5
                         
                          |
92 | | iffalse 3565 |
. . . . . . . . 9
            |
93 | 92 | fveq2d 5550 |
. . . . . . . 8
                    |
94 | 93 | eqeq2d 2205 |
. . . . . . 7
            
         |
95 | 94 | adantl 277 |
. . . . . 6
                    
         |
96 | | simprr 531 |
. . . . . . . . 9
        
                |
97 | 5, 9 | ffvelcdmd 5686 |
. . . . . . . . . . . . 13
 
    
              |
98 | 97 | elfzelzd 10082 |
. . . . . . . . . . . 12
 
    
        |
99 | | fzdcel 10096 |
. . . . . . . . . . . 12
       

DECID             |
100 | 98, 50, 53, 99 | syl3anc 1249 |
. . . . . . . . . . 11
 
    
DECID             |
101 | 100 | adantr 276 |
. . . . . . . . . 10
        
        DECID             |
102 | 25 | zred 9429 |
. . . . . . . . . . . 12
   |
103 | 102 | ad2antrr 488 |
. . . . . . . . . . 11
        
          |
104 | 57 | ad2antlr 489 |
. . . . . . . . . . . 12
        
          |
105 | | peano2re 8145 |
. . . . . . . . . . . . 13
     |
106 | 104, 105 | syl 14 |
. . . . . . . . . . . 12
        
            |
107 | | simprl 529 |
. . . . . . . . . . . . 13
        
       
  |
108 | 103, 104,
107 | nltled 8130 |
. . . . . . . . . . . 12
        
          |
109 | 104 | ltp1d 8939 |
. . . . . . . . . . . 12
        
            |
110 | 103, 104,
106, 108, 109 | lelttrd 8134 |
. . . . . . . . . . 11
        
            |
111 | 103, 110 | ltned 8123 |
. . . . . . . . . 10
        
            |
112 | 4 | ad2antrr 488 |
. . . . . . . . . . . . . . . 16
        
                     
    |
113 | 8 | ad2antlr 489 |
. . . . . . . . . . . . . . . 16
        
                  |
114 | 112, 113 | ffvelcdmd 5686 |
. . . . . . . . . . . . . . 15
        
                      |
115 | | elfzp1 10128 |
. . . . . . . . . . . . . . . . 17
    
          
 
                       |
116 | 18, 115 | syl 14 |
. . . . . . . . . . . . . . . 16
                                     |
117 | 116 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
        
                  
                         |
118 | 114, 117 | mpbid 147 |
. . . . . . . . . . . . . 14
        
                              |
119 | 118 | ord 725 |
. . . . . . . . . . . . 13
        
                              |
120 | 2 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
        
                          |
121 | | f1ocnvfv 5814 |
. . . . . . . . . . . . . . 15
                                   
            |
122 | 120, 113,
121 | syl2anc 411 |
. . . . . . . . . . . . . 14
        
                
            |
123 | 11 | eqeq1i 2201 |
. . . . . . . . . . . . . 14
  
           |
124 | 122, 123 | imbitrrdi 162 |
. . . . . . . . . . . . 13
        
                
     |
125 | 119, 124 | syld 45 |
. . . . . . . . . . . 12
        
                        |
126 | 125 | a1d 22 |
. . . . . . . . . . 11
        
        DECID                     
      |
127 | 126 | necon1addc 2440 |
. . . . . . . . . 10
        
        DECID                            |
128 | 101, 111,
127 | mp2d 47 |
. . . . . . . . 9
        
                    |
129 | 96, 128 | eqeltrd 2270 |
. . . . . . . 8
        
              |
130 | 96 | eqcomd 2199 |
. . . . . . . . . . . . . 14
        
                |
131 | | f1ocnvfv 5814 |
. . . . . . . . . . . . . . 15
                                 
          |
132 | 120, 113,
131 | syl2anc 411 |
. . . . . . . . . . . . . 14
        
              
          |
133 | 130, 132 | mpd 13 |
. . . . . . . . . . . . 13
        
                 |
134 | 133 | breq1d 4039 |
. . . . . . . . . . . 12
        
             
     |
135 | | lttr 8083 |
. . . . . . . . . . . . . 14
   
           |
136 | 104, 106,
103, 135 | syl3anc 1249 |
. . . . . . . . . . . . 13
        
              
   |
137 | 109, 136 | mpand 429 |
. . . . . . . . . . . 12
        
          
   |
138 | 134, 137 | sylbid 150 |
. . . . . . . . . . 11
        
                 |
139 | 107, 138 | mtod 664 |
. . . . . . . . . 10
        
       
       |
140 | | iffalse 3565 |
. . . . . . . . . 10
                                     |
141 | 139, 140 | syl 14 |
. . . . . . . . 9
        
                                       |
142 | 133 | oveq1d 5925 |
. . . . . . . . 9
        
                     |
143 | 104 | recnd 8038 |
. . . . . . . . . 10
        
          |
144 | | ax-1cn 7955 |
. . . . . . . . . 10
 |
145 | | pncan 8215 |
. . . . . . . . . 10
 
       |
146 | 143, 144,
145 | sylancl 413 |
. . . . . . . . 9
        
              |
147 | 141, 142,
146 | 3eqtrrd 2231 |
. . . . . . . 8
        
                                |
148 | 129, 147 | jca 306 |
. . . . . . 7
        
            
                         |
149 | 148 | expr 375 |
. . . . . 6
                    
                          |
150 | 95, 149 | sylbid 150 |
. . . . 5
                    
    
                          |
151 | | exmiddc 837 |
. . . . . 6
DECID
    |
152 | 27, 151 | syl 14 |
. . . . 5
 
    
    |
153 | 91, 150, 152 | mpjaodan 799 |
. . . 4
 
    
                
                          |
154 | 153 | expimpd 363 |
. . 3
      
                
                          |
155 | 86 | eqeq2d 2205 |
. . . . . . 7
                            
        |
156 | 155 | adantl 277 |
. . . . . 6
                                    
        |
157 | 49 | ad2antrr 488 |
. . . . . . . . 9
             
         |
158 | | eluzelz 9591 |
. . . . . . . . . . 11
    
  |
159 | 18, 158 | syl 14 |
. . . . . . . . . 10
   |
160 | 159 | ad2antrr 488 |
. . . . . . . . 9
             
         |
161 | | simprr 531 |
. . . . . . . . . . 11
             
              |
162 | 17 | ad2antrr 488 |
. . . . . . . . . . . 12
             
             
            |
163 | | simplr 528 |
. . . . . . . . . . . . 13
             
             |
164 | 62, 163 | sselid 3177 |
. . . . . . . . . . . 12
             
          
    |
165 | 162, 164 | ffvelcdmd 5686 |
. . . . . . . . . . 11
             
               
    |
166 | 161, 165 | eqeltrd 2270 |
. . . . . . . . . 10
             
          
    |
167 | 166 | elfzelzd 10082 |
. . . . . . . . 9
             
         |
168 | | elfzle1 10083 |
. . . . . . . . . 10
    
    |
169 | 166, 168 | syl 14 |
. . . . . . . . 9
             
         |
170 | 167 | zred 9429 |
. . . . . . . . . . 11
             
         |
171 | 102 | ad2antrr 488 |
. . . . . . . . . . 11
             
         |
172 | 159 | peano2zd 9432 |
. . . . . . . . . . . . 13
     |
173 | 172 | zred 9429 |
. . . . . . . . . . . 12
     |
174 | 173 | ad2antrr 488 |
. . . . . . . . . . 11
             
       
   |
175 | | simprl 529 |
. . . . . . . . . . . 12
             
              |
176 | 161, 175 | eqbrtrd 4051 |
. . . . . . . . . . 11
             
         |
177 | | elfzle2 10084 |
. . . . . . . . . . . . 13
    
      |
178 | 24, 177 | syl 14 |
. . . . . . . . . . . 12

    |
179 | 178 | ad2antrr 488 |
. . . . . . . . . . 11
             
           |
180 | 170, 171,
174, 176, 179 | ltletrd 8432 |
. . . . . . . . . 10
             
           |
181 | | zleltp1 9362 |
. . . . . . . . . . 11
 
       |
182 | 167, 160,
181 | syl2anc 411 |
. . . . . . . . . 10
             
       
     |
183 | 180, 182 | mpbird 167 |
. . . . . . . . 9
             
         |
184 | 157, 160,
167, 169, 183 | elfzd 10072 |
. . . . . . . 8
             
             |
185 | 176, 42 | syl 14 |
. . . . . . . . 9
             
           
            |
186 | 161 | fveq2d 5550 |
. . . . . . . . 9
             
                      |
187 | 2 | ad2antrr 488 |
. . . . . . . . . 10
             
            
       
    |
188 | | f1ocnvfv2 5813 |
. . . . . . . . . 10
                 
                  |
189 | 187, 164,
188 | syl2anc 411 |
. . . . . . . . 9
             
                  |
190 | 185, 186,
189 | 3eqtrrd 2231 |
. . . . . . . 8
             
                    |
191 | 184, 190 | jca 306 |
. . . . . . 7
             
           
              |
192 | 191 | expr 375 |
. . . . . 6
                        
               |
193 | 156, 192 | sylbid 150 |
. . . . 5
                                         
               |
194 | 140 | eqeq2d 2205 |
. . . . . . 7
                            
          |
195 | 194 | adantl 277 |
. . . . . 6
                                    
          |
196 | 49 | ad2antrr 488 |
. . . . . . . . 9
             
        
  |
197 | 159 | ad2antrr 488 |
. . . . . . . . 9
             
        
  |
198 | | simprr 531 |
. . . . . . . . . 10
             
                  |
199 | 17 | ad2antrr 488 |
. . . . . . . . . . . . 13
             
                            |
200 | | simplr 528 |
. . . . . . . . . . . . . 14
             
        
      |
201 | 62, 200 | sselid 3177 |
. . . . . . . . . . . . 13
             
        
        |
202 | 199, 201 | ffvelcdmd 5686 |
. . . . . . . . . . . 12
             
                      |
203 | 202 | elfzelzd 10082 |
. . . . . . . . . . 11
             
                |
204 | 203, 35 | syl 14 |
. . . . . . . . . 10
             
                  |
205 | 198, 204 | eqeltrd 2270 |
. . . . . . . . 9
             
           |
206 | 49 | zred 9429 |
. . . . . . . . . . 11
   |
207 | 206 | ad2antrr 488 |
. . . . . . . . . 10
             
        
  |
208 | 102 | ad2antrr 488 |
. . . . . . . . . 10
             
        
  |
209 | 205 | zred 9429 |
. . . . . . . . . 10
             
           |
210 | | elfzle1 10083 |
. . . . . . . . . . . 12
    
    |
211 | 24, 210 | syl 14 |
. . . . . . . . . . 11

  |
212 | 211 | ad2antrr 488 |
. . . . . . . . . 10
             
           |
213 | | elfzelz 10081 |
. . . . . . . . . . . . . . . . . . . . 21
       |
214 | 213 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  |
215 | 214 | zred 9429 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
216 | 159 | zred 9429 |
. . . . . . . . . . . . . . . . . . . . 21
   |
217 | 216 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  |
218 | 173 | adantr 276 |
. . . . . . . . . . . . . . . . . . . 20
 
    
    |
219 | | elfzle2 10084 |
. . . . . . . . . . . . . . . . . . . . 21
       |
220 | 219 | adantl 277 |
. . . . . . . . . . . . . . . . . . . 20
 
    
  |
221 | 217 | ltp1d 8939 |
. . . . . . . . . . . . . . . . . . . 20
 
    
    |
222 | 215, 217,
218, 220, 221 | lelttrd 8134 |
. . . . . . . . . . . . . . . . . . 19
 
    
    |
223 | 215, 222 | gtned 8122 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
224 | 223 | adantr 276 |
. . . . . . . . . . . . . . . . 17
             
             |
225 | 15 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
             
                            |
226 | 22 | ad2antrr 488 |
. . . . . . . . . . . . . . . . . . 19
             
                   |
227 | | f1fveq 5807 |
. . . . . . . . . . . . . . . . . . 19
                         
     
                      |
228 | 225, 226,
201, 227 | syl12anc 1247 |
. . . . . . . . . . . . . . . . . 18
             
                           |
229 | 228 | necon3bid 2405 |
. . . . . . . . . . . . . . . . 17
             
                           |
230 | 224, 229 | mpbird 167 |
. . . . . . . . . . . . . . . 16
             
             
         |
231 | 11 | neeq1i 2379 |
. . . . . . . . . . . . . . . 16
     
              |
232 | 230, 231 | sylibr 134 |
. . . . . . . . . . . . . . 15
             
                |
233 | 232 | necomd 2450 |
. . . . . . . . . . . . . 14
             
                |
234 | 25 | ad2antrr 488 |
. . . . . . . . . . . . . . 15
             
        
  |
235 | | zapne 9381 |
. . . . . . . . . . . . . . 15
              #         |
236 | 203, 234,
235 | syl2anc 411 |
. . . . . . . . . . . . . 14
             
               #
        |
237 | 233, 236 | mpbird 167 |
. . . . . . . . . . . . 13
             
              #
  |
238 | 203 | zred 9429 |
. . . . . . . . . . . . . 14
             
                |
239 | | simprl 529 |
. . . . . . . . . . . . . . 15
             
                |
240 | 208, 238,
239 | nltled 8130 |
. . . . . . . . . . . . . 14
             
                |
241 | 208, 238,
240 | leltapd 8648 |
. . . . . . . . . . . . 13
             
                    #
   |
242 | 237, 241 | mpbird 167 |
. . . . . . . . . . . 12
             
                |
243 | | zltlem1 9364 |
. . . . . . . . . . . . 13
             
          |
244 | 234, 203,
243 | syl2anc 411 |
. . . . . . . . . . . 12
             
              
          |
245 | 242, 244 | mpbid 147 |
. . . . . . . . . . 11
             
                  |
246 | 245, 198 | breqtrrd 4057 |
. . . . . . . . . 10
             
           |
247 | 207, 208,
209, 212, 246 | letrd 8133 |
. . . . . . . . 9
             
           |
248 | | elfzle2 10084 |
. . . . . . . . . . . 12
         
           |
249 | 202, 248 | syl 14 |
. . . . . . . . . . 11
             
              
   |
250 | 216 | ad2antrr 488 |
. . . . . . . . . . . 12
             
        
  |
251 | | 1re 8008 |
. . . . . . . . . . . . 13
 |
252 | | lesubadd 8443 |
. . . . . . . . . . . . 13
      
              
    |
253 | 251, 252 | mp3an2 1336 |
. . . . . . . . . . . 12
                     
    |
254 | 238, 250,
253 | syl2anc 411 |
. . . . . . . . . . 11
             
                      
    |
255 | 249, 254 | mpbird 167 |
. . . . . . . . . 10
             
               
  |
256 | 198, 255 | eqbrtrd 4051 |
. . . . . . . . 9
             
        
  |
257 | 196, 197,
205, 247, 256 | elfzd 10072 |
. . . . . . . 8
             
               |
258 | 208, 209,
246 | lensymd 8131 |
. . . . . . . . . 10
             
        
  |
259 | 258, 93 | syl 14 |
. . . . . . . . 9
             
                            |
260 | 198 | oveq1d 5925 |
. . . . . . . . . . 11
             
                      |
261 | 203 | zcnd 9430 |
. . . . . . . . . . . 12
             
                |
262 | | npcan 8218 |
. . . . . . . . . . . 12
                        |
263 | 261, 144,
262 | sylancl 413 |
. . . . . . . . . . 11
             
                         |
264 | 260, 263 | eqtrd 2226 |
. . . . . . . . . 10
             
                  |
265 | 264 | fveq2d 5550 |
. . . . . . . . 9
             
                          |
266 | 2 | ad2antrr 488 |
. . . . . . . . . 10
             
              
       
    |
267 | 266, 201,
188 | syl2anc 411 |
. . . . . . . . 9
             
                    |
268 | 259, 265,
267 | 3eqtrrd 2231 |
. . . . . . . 8
             
        
             |
269 | 257, 268 | jca 306 |
. . . . . . 7
             
                            |
270 | 269 | expr 375 |
. . . . . 6
                     
    
               |
271 | 195, 270 | sylbid 150 |
. . . . 5
                                         
               |
272 | | exmiddc 837 |
. . . . . 6
DECID                    |
273 | 39, 272 | syl 14 |
. . . . 5
 
    
              |
274 | 193, 271,
273 | mpjaodan 799 |
. . . 4
 
    
                           
               |
275 | 274 | expimpd 363 |
. . 3
      
                                           |
276 | 154, 275 | impbid 129 |
. 2
      
           
    
                          |
277 | 1, 29, 40, 276 | f1od 6113 |
1
               |