Proof of Theorem seqf1olem1
Step | Hyp | Ref
| Expression |
1 | | seqf1olem.7 |
. 2
                  |
2 | | fvex 5873 |
. . 3
            |
3 | 2 | a1i 11 |
. 2
 
    
             |
4 | | fvex 5873 |
. . . 4
      |
5 | | ovex 6316 |
. . . 4
        |
6 | 4, 5 | ifex 3948 |
. . 3
                       |
7 | 6 | a1i 11 |
. 2
 
    
                        |
8 | | iftrue 3886 |
. . . . . . . . 9
          |
9 | 8 | fveq2d 5867 |
. . . . . . . 8
     
            |
10 | 9 | eqeq2d 2460 |
. . . . . . 7
                    |
11 | 10 | adantl 468 |
. . . . . 6
                            |
12 | | simprr 765 |
. . . . . . . . 9
        
            |
13 | | elfzelz 11797 |
. . . . . . . . . . . . 13
       |
14 | 13 | zred 11037 |
. . . . . . . . . . . 12
       |
15 | 14 | ad2antlr 732 |
. . . . . . . . . . 11
        
        |
16 | | simprl 763 |
. . . . . . . . . . 11
        
        |
17 | 15, 16 | gtned 9767 |
. . . . . . . . . 10
        
        |
18 | | seqf1olem.5 |
. . . . . . . . . . . . . . . . 17
                   |
19 | | f1of 5812 |
. . . . . . . . . . . . . . . . 17
      
       
 
     
       
    |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . . . 16
                   |
21 | 20 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
        
                   
    |
22 | | fzssp1 11838 |
. . . . . . . . . . . . . . . 16
           |
23 | | simplr 761 |
. . . . . . . . . . . . . . . 16
        
            |
24 | 22, 23 | sseldi 3429 |
. . . . . . . . . . . . . . 15
        
              |
25 | 21, 24 | ffvelrnd 6021 |
. . . . . . . . . . . . . 14
        
                  |
26 | | seqf1o.4 |
. . . . . . . . . . . . . . . 16
       |
27 | | elfzp1 11843 |
. . . . . . . . . . . . . . . 16
    
        
                     |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . 15
                               |
29 | 28 | ad2antrr 731 |
. . . . . . . . . . . . . 14
        
              
                     |
30 | 25, 29 | mpbid 214 |
. . . . . . . . . . . . 13
        
                        |
31 | 30 | ord 379 |
. . . . . . . . . . . 12
        
              
         |
32 | 18 | ad2antrr 731 |
. . . . . . . . . . . . . 14
        
                        |
33 | | f1ocnvfv 6175 |
. . . . . . . . . . . . . 14
                 
                        |
34 | 32, 24, 33 | syl2anc 666 |
. . . . . . . . . . . . 13
        
            
          |
35 | | seqf1olem.8 |
. . . . . . . . . . . . . 14
    
   |
36 | 35 | eqeq1i 2455 |
. . . . . . . . . . . . 13

         |
37 | 34, 36 | syl6ibr 231 |
. . . . . . . . . . . 12
        
            
   |
38 | 31, 37 | syld 45 |
. . . . . . . . . . 11
        
              
   |
39 | 38 | necon1ad 2640 |
. . . . . . . . . 10
        
      
           |
40 | 17, 39 | mpd 15 |
. . . . . . . . 9
        
                |
41 | 12, 40 | eqeltrd 2528 |
. . . . . . . 8
        
            |
42 | 12 | eqcomd 2456 |
. . . . . . . . . . . 12
        
            |
43 | | f1ocnvfv 6175 |
. . . . . . . . . . . . 13
                 
                    |
44 | 32, 24, 43 | syl2anc 666 |
. . . . . . . . . . . 12
        
          
        |
45 | 42, 44 | mpd 15 |
. . . . . . . . . . 11
        
             |
46 | 45, 16 | eqbrtrd 4422 |
. . . . . . . . . 10
        
             |
47 | | iftrue 3886 |
. . . . . . . . . 10
                                   |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
        
                                   |
49 | 48, 45 | eqtr2d 2485 |
. . . . . . . 8
        
                              |
50 | 41, 49 | jca 535 |
. . . . . . 7
        
          
                         |
51 | 50 | expr 619 |
. . . . . 6
                                             |
52 | 11, 51 | sylbid 219 |
. . . . 5
                         
                          |
53 | | iffalse 3889 |
. . . . . . . . 9
            |
54 | 53 | fveq2d 5867 |
. . . . . . . 8
                    |
55 | 54 | eqeq2d 2460 |
. . . . . . 7
            
         |
56 | 55 | adantl 468 |
. . . . . 6
                    
         |
57 | | simprr 765 |
. . . . . . . . 9
        
                |
58 | | f1ocnv 5824 |
. . . . . . . . . . . . . . . . . . 19
      
       
 
      
       
    |
59 | 18, 58 | syl 17 |
. . . . . . . . . . . . . . . . . 18
                    |
60 | | f1of1 5811 |
. . . . . . . . . . . . . . . . . 18
                                     |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . . . 17
                    |
62 | | f1f 5777 |
. . . . . . . . . . . . . . . . 17
                        
       
    |
63 | 61, 62 | syl 17 |
. . . . . . . . . . . . . . . 16
                    |
64 | | peano2uz 11209 |
. . . . . . . . . . . . . . . . . 18
    
        |
65 | 26, 64 | syl 17 |
. . . . . . . . . . . . . . . . 17
         |
66 | | eluzfz2 11804 |
. . . . . . . . . . . . . . . . 17
      
     
    |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . . . 16
           |
68 | 63, 67 | ffvelrnd 6021 |
. . . . . . . . . . . . . . 15
     
          |
69 | 35, 68 | syl5eqel 2532 |
. . . . . . . . . . . . . 14
         |
70 | | elfzelz 11797 |
. . . . . . . . . . . . . 14
    
    |
71 | 69, 70 | syl 17 |
. . . . . . . . . . . . 13
   |
72 | 71 | zred 11037 |
. . . . . . . . . . . 12
   |
73 | 72 | ad2antrr 731 |
. . . . . . . . . . 11
        
          |
74 | 14 | ad2antlr 732 |
. . . . . . . . . . . 12
        
          |
75 | | peano2re 9803 |
. . . . . . . . . . . . 13
     |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . 12
        
            |
77 | | simprl 763 |
. . . . . . . . . . . . 13
        
       
  |
78 | 73, 74 | lenltd 9778 |
. . . . . . . . . . . . 13
        
        
   |
79 | 77, 78 | mpbird 236 |
. . . . . . . . . . . 12
        
          |
80 | 74 | ltp1d 10534 |
. . . . . . . . . . . 12
        
            |
81 | 73, 74, 76, 79, 80 | lelttrd 9790 |
. . . . . . . . . . 11
        
            |
82 | 73, 81 | ltned 9768 |
. . . . . . . . . 10
        
            |
83 | 20 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
        
                     
    |
84 | | fzp1elp1 11846 |
. . . . . . . . . . . . . . . 16
          
    |
85 | 84 | ad2antlr 732 |
. . . . . . . . . . . . . . 15
        
                  |
86 | 83, 85 | ffvelrnd 6021 |
. . . . . . . . . . . . . 14
        
                      |
87 | | elfzp1 11843 |
. . . . . . . . . . . . . . . 16
    
          
 
                       |
88 | 26, 87 | syl 17 |
. . . . . . . . . . . . . . 15
                                     |
89 | 88 | ad2antrr 731 |
. . . . . . . . . . . . . 14
        
                  
                         |
90 | 86, 89 | mpbid 214 |
. . . . . . . . . . . . 13
        
                              |
91 | 90 | ord 379 |
. . . . . . . . . . . 12
        
                              |
92 | 18 | ad2antrr 731 |
. . . . . . . . . . . . . 14
        
                          |
93 | | f1ocnvfv 6175 |
. . . . . . . . . . . . . 14
                                   
            |
94 | 92, 85, 93 | syl2anc 666 |
. . . . . . . . . . . . 13
        
                
            |
95 | 35 | eqeq1i 2455 |
. . . . . . . . . . . . 13
  
           |
96 | 94, 95 | syl6ibr 231 |
. . . . . . . . . . . 12
        
                
     |
97 | 91, 96 | syld 45 |
. . . . . . . . . . 11
        
                        |
98 | 97 | necon1ad 2640 |
. . . . . . . . . 10
        
          
             |
99 | 82, 98 | mpd 15 |
. . . . . . . . 9
        
                    |
100 | 57, 99 | eqeltrd 2528 |
. . . . . . . 8
        
              |
101 | 57 | eqcomd 2456 |
. . . . . . . . . . . . . 14
        
                |
102 | | f1ocnvfv 6175 |
. . . . . . . . . . . . . . 15
                                 
          |
103 | 92, 85, 102 | syl2anc 666 |
. . . . . . . . . . . . . 14
        
              
          |
104 | 101, 103 | mpd 15 |
. . . . . . . . . . . . 13
        
                 |
105 | 104 | breq1d 4411 |
. . . . . . . . . . . 12
        
             
     |
106 | | lttr 9707 |
. . . . . . . . . . . . . 14
   
           |
107 | 74, 76, 73, 106 | syl3anc 1267 |
. . . . . . . . . . . . 13
        
              
   |
108 | 80, 107 | mpand 680 |
. . . . . . . . . . . 12
        
          
   |
109 | 105, 108 | sylbid 219 |
. . . . . . . . . . 11
        
                 |
110 | 77, 109 | mtod 181 |
. . . . . . . . . 10
        
       
       |
111 | | iffalse 3889 |
. . . . . . . . . 10
                                     |
112 | 110, 111 | syl 17 |
. . . . . . . . 9
        
                                       |
113 | 104 | oveq1d 6303 |
. . . . . . . . 9
        
                     |
114 | 74 | recnd 9666 |
. . . . . . . . . 10
        
          |
115 | | ax-1cn 9594 |
. . . . . . . . . 10
 |
116 | | pncan 9878 |
. . . . . . . . . 10
 
       |
117 | 114, 115,
116 | sylancl 667 |
. . . . . . . . 9
        
              |
118 | 112, 113,
117 | 3eqtrrd 2489 |
. . . . . . . 8
        
                                |
119 | 100, 118 | jca 535 |
. . . . . . 7
        
            
                         |
120 | 119 | expr 619 |
. . . . . 6
                    
                          |
121 | 56, 120 | sylbid 219 |
. . . . 5
                    
    
                          |
122 | 52, 121 | pm2.61dan 799 |
. . . 4
 
    
                
                          |
123 | 122 | expimpd 607 |
. . 3
      
                
                          |
124 | 47 | eqeq2d 2460 |
. . . . . . 7
                            
        |
125 | 124 | adantl 468 |
. . . . . 6
                                    
        |
126 | | simprr 765 |
. . . . . . . . . . 11
             
              |
127 | 63 | ad2antrr 731 |
. . . . . . . . . . . 12
             
             
            |
128 | | simplr 761 |
. . . . . . . . . . . . 13
             
             |
129 | 22, 128 | sseldi 3429 |
. . . . . . . . . . . 12
             
          
    |
130 | 127, 129 | ffvelrnd 6021 |
. . . . . . . . . . 11
             
               
    |
131 | 126, 130 | eqeltrd 2528 |
. . . . . . . . . 10
             
          
    |
132 | | elfzle1 11799 |
. . . . . . . . . 10
    
    |
133 | 131, 132 | syl 17 |
. . . . . . . . 9
             
         |
134 | | elfzelz 11797 |
. . . . . . . . . . . . 13
    
    |
135 | 131, 134 | syl 17 |
. . . . . . . . . . . 12
             
         |
136 | 135 | zred 11037 |
. . . . . . . . . . 11
             
         |
137 | 72 | ad2antrr 731 |
. . . . . . . . . . 11
             
         |
138 | | eluzelz 11165 |
. . . . . . . . . . . . . . 15
    
  |
139 | 26, 138 | syl 17 |
. . . . . . . . . . . . . 14
   |
140 | 139 | peano2zd 11040 |
. . . . . . . . . . . . 13
     |
141 | 140 | zred 11037 |
. . . . . . . . . . . 12
     |
142 | 141 | ad2antrr 731 |
. . . . . . . . . . 11
             
       
   |
143 | | simprl 763 |
. . . . . . . . . . . 12
             
              |
144 | 126, 143 | eqbrtrd 4422 |
. . . . . . . . . . 11
             
         |
145 | | elfzle2 11800 |
. . . . . . . . . . . . 13
    
      |
146 | 69, 145 | syl 17 |
. . . . . . . . . . . 12

    |
147 | 146 | ad2antrr 731 |
. . . . . . . . . . 11
             
           |
148 | 136, 137,
142, 144, 147 | ltletrd 9792 |
. . . . . . . . . 10
             
           |
149 | 139 | ad2antrr 731 |
. . . . . . . . . . 11
             
         |
150 | | zleltp1 10984 |
. . . . . . . . . . 11
 
       |
151 | 135, 149,
150 | syl2anc 666 |
. . . . . . . . . 10
             
       
     |
152 | 148, 151 | mpbird 236 |
. . . . . . . . 9
             
         |
153 | | eluzel2 11161 |
. . . . . . . . . . . 12
    
  |
154 | 26, 153 | syl 17 |
. . . . . . . . . . 11
   |
155 | 154 | ad2antrr 731 |
. . . . . . . . . 10
             
         |
156 | | elfz 11787 |
. . . . . . . . . 10
 
     
     |
157 | 135, 155,
149, 156 | syl3anc 1267 |
. . . . . . . . 9
             
           
     |
158 | 133, 152,
157 | mpbir2and 932 |
. . . . . . . 8
             
             |
159 | 144, 9 | syl 17 |
. . . . . . . . 9
             
           
            |
160 | 126 | fveq2d 5867 |
. . . . . . . . 9
             
                      |
161 | 18 | ad2antrr 731 |
. . . . . . . . . 10
             
            
       
    |
162 | | f1ocnvfv2 6174 |
. . . . . . . . . 10
                 
                  |
163 | 161, 129,
162 | syl2anc 666 |
. . . . . . . . 9
             
                  |
164 | 159, 160,
163 | 3eqtrrd 2489 |
. . . . . . . 8
             
                    |
165 | 158, 164 | jca 535 |
. . . . . . 7
             
           
              |
166 | 165 | expr 619 |
. . . . . 6
                        
               |
167 | 125, 166 | sylbid 219 |
. . . . 5
                                         
               |
168 | 111 | eqeq2d 2460 |
. . . . . . 7
                            
          |
169 | 168 | adantl 468 |
. . . . . 6
                                    
          |
170 | 154 | zred 11037 |
. . . . . . . . . . 11
   |
171 | 170 | ad2antrr 731 |
. . . . . . . . . 10
             
        
  |
172 | 72 | ad2antrr 731 |
. . . . . . . . . 10
             
        
  |
173 | | simprr 765 |
. . . . . . . . . . . 12
             
                  |
174 | 63 | ad2antrr 731 |
. . . . . . . . . . . . . . 15
             
                            |
175 | | simplr 761 |
. . . . . . . . . . . . . . . 16
             
        
      |
176 | 22, 175 | sseldi 3429 |
. . . . . . . . . . . . . . 15
             
        
        |
177 | 174, 176 | ffvelrnd 6021 |
. . . . . . . . . . . . . 14
             
                      |
178 | | elfzelz 11797 |
. . . . . . . . . . . . . 14
         
         |
179 | 177, 178 | syl 17 |
. . . . . . . . . . . . 13
             
                |
180 | | peano2zm 10977 |
. . . . . . . . . . . . 13
               |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . 12
             
                  |
182 | 173, 181 | eqeltrd 2528 |
. . . . . . . . . . 11
             
           |
183 | 182 | zred 11037 |
. . . . . . . . . 10
             
           |
184 | | elfzle1 11799 |
. . . . . . . . . . . 12
    
    |
185 | 69, 184 | syl 17 |
. . . . . . . . . . 11

  |
186 | 185 | ad2antrr 731 |
. . . . . . . . . 10
             
           |
187 | | simprl 763 |
. . . . . . . . . . . . . 14
             
                |
188 | 179 | zred 11037 |
. . . . . . . . . . . . . . 15
             
                |
189 | 172, 188 | lenltd 9778 |
. . . . . . . . . . . . . 14
             
                       |
190 | 187, 189 | mpbird 236 |
. . . . . . . . . . . . 13
             
                |
191 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . 20
       |
192 | 191 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
193 | 192 | zred 11037 |
. . . . . . . . . . . . . . . . . 18
 
    
  |
194 | 139 | zred 11037 |
. . . . . . . . . . . . . . . . . . . 20
   |
195 | 194 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
196 | 141 | adantr 467 |
. . . . . . . . . . . . . . . . . . 19
 
    
    |
197 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . 20
       |
198 | 197 | adantl 468 |
. . . . . . . . . . . . . . . . . . 19
 
    
  |
199 | 195 | ltp1d 10534 |
. . . . . . . . . . . . . . . . . . 19
 
    
    |
200 | 193, 195,
196, 198, 199 | lelttrd 9790 |
. . . . . . . . . . . . . . . . . 18
 
    
    |
201 | 193, 200 | gtned 9767 |
. . . . . . . . . . . . . . . . 17
 
    
    |
202 | 201 | adantr 467 |
. . . . . . . . . . . . . . . 16
             
             |
203 | 61 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . 18
             
                            |
204 | 67 | ad2antrr 731 |
. . . . . . . . . . . . . . . . . 18
             
                   |
205 | | f1fveq 6161 |
. . . . . . . . . . . . . . . . . 18
                         
     
                      |
206 | 203, 204,
176, 205 | syl12anc 1265 |
. . . . . . . . . . . . . . . . 17
             
                           |
207 | 206 | necon3bid 2667 |
. . . . . . . . . . . . . . . 16
             
                           |
208 | 202, 207 | mpbird 236 |
. . . . . . . . . . . . . . 15
             
             
         |
209 | 35 | neeq1i 2687 |
. . . . . . . . . . . . . . 15
     
              |
210 | 208, 209 | sylibr 216 |
. . . . . . . . . . . . . 14
             
                |
211 | 210 | necomd 2678 |
. . . . . . . . . . . . 13
             
                |
212 | 172, 188 | ltlend 9777 |
. . . . . . . . . . . . 13
             
                              |
213 | 190, 211,
212 | mpbir2and 932 |
. . . . . . . . . . . 12
             
                |
214 | 71 | ad2antrr 731 |
. . . . . . . . . . . . 13
             
        
  |
215 | | zltlem1 10986 |
. . . . . . . . . . . . 13
             
          |
216 | 214, 179,
215 | syl2anc 666 |
. . . . . . . . . . . 12
             
              
          |
217 | 213, 216 | mpbid 214 |
. . . . . . . . . . 11
             
                  |
218 | 217, 173 | breqtrrd 4428 |
. . . . . . . . . 10
             
           |
219 | 171, 172,
183, 186, 218 | letrd 9789 |
. . . . . . . . 9
             
           |
220 | | elfzle2 11800 |
. . . . . . . . . . . 12
         
           |
221 | 177, 220 | syl 17 |
. . . . . . . . . . 11
             
              
   |
222 | 194 | ad2antrr 731 |
. . . . . . . . . . . 12
             
        
  |
223 | | 1re 9639 |
. . . . . . . . . . . . 13
 |
224 | | lesubadd 10083 |
. . . . . . . . . . . . 13
      
              
    |
225 | 223, 224 | mp3an2 1351 |
. . . . . . . . . . . 12
                     
    |
226 | 188, 222,
225 | syl2anc 666 |
. . . . . . . . . . 11
             
                      
    |
227 | 221, 226 | mpbird 236 |
. . . . . . . . . 10
             
               
  |
228 | 173, 227 | eqbrtrd 4422 |
. . . . . . . . 9
             
        
  |
229 | 154 | ad2antrr 731 |
. . . . . . . . . 10
             
        
  |
230 | 139 | ad2antrr 731 |
. . . . . . . . . 10
             
        
  |
231 | 182, 229,
230, 156 | syl3anc 1267 |
. . . . . . . . 9
             
              
    |
232 | 219, 228,
231 | mpbir2and 932 |
. . . . . . . 8
             
               |
233 | 172, 183 | lenltd 9778 |
. . . . . . . . . . 11
             
             |
234 | 218, 233 | mpbid 214 |
. . . . . . . . . 10
             
        
  |
235 | 234, 54 | syl 17 |
. . . . . . . . 9
             
                            |
236 | 173 | oveq1d 6303 |
. . . . . . . . . . 11
             
                      |
237 | 179 | zcnd 11038 |
. . . . . . . . . . . 12
             
                |
238 | | npcan 9881 |
. . . . . . . . . . . 12
                        |
239 | 237, 115,
238 | sylancl 667 |
. . . . . . . . . . 11
             
                         |
240 | 236, 239 | eqtrd 2484 |
. . . . . . . . . 10
             
                  |
241 | 240 | fveq2d 5867 |
. . . . . . . . 9
             
                          |
242 | 18 | ad2antrr 731 |
. . . . . . . . . 10
             
              
       
    |
243 | 242, 176,
162 | syl2anc 666 |
. . . . . . . . 9
             
                    |
244 | 235, 241,
243 | 3eqtrrd 2489 |
. . . . . . . 8
             
        
             |
245 | 232, 244 | jca 535 |
. . . . . . 7
             
                            |
246 | 245 | expr 619 |
. . . . . 6
                     
    
               |
247 | 169, 246 | sylbid 219 |
. . . . 5
                                         
               |
248 | 167, 247 | pm2.61dan 799 |
. . . 4
 
    
                           
               |
249 | 248 | expimpd 607 |
. . 3
      
                                           |
250 | 123, 249 | impbid 194 |
. 2
      
           
    
                          |
251 | 1, 3, 7, 250 | f1od 6516 |
1
               |