Step | Hyp | Ref
| Expression |
1 | | poimir.0 |
. . . . . . 7
   |
2 | 1 | adantr 467 |
. . . . . 6
 

  |
3 | | oveq1 6295 |
. . . . . . . . . . . . . 14
                                                                                                               |
4 | 3 | fveq2d 5867 |
. . . . . . . . . . . . 13
                                                                                                                       |
5 | 4 | fveq1d 5865 |
. . . . . . . . . . . 12
                                                
                                                                              |
6 | 5 | breq2d 4413 |
. . . . . . . . . . 11
                                                               
                                                                 |
7 | | fveq1 5862 |
. . . . . . . . . . . 12
                                                                                                 |
8 | 7 | neeq1d 2682 |
. . . . . . . . . . 11
                                                                                                   |
9 | 6, 8 | anbi12d 716 |
. . . . . . . . . 10
                                                  
             
                                                                                                                       |
10 | 9 | ralbidv 2826 |
. . . . . . . . 9
                                                        
             
                                                                         
                                                   |
11 | 10 | rabbidv 3035 |
. . . . . . . 8
                                                            
             
                                                                               
                                                   |
12 | 11 | uneq2d 3587 |
. . . . . . 7
                                                               
             
                                                                                                                                        |
13 | 12 | supeq1d 7957 |
. . . . . 6
                                                      
     
     
                                
     
                                                             
                                                      |
14 | 1 | nnnn0d 10922 |
. . . . . . . . . . 11
   |
15 | | 0elfz 11886 |
. . . . . . . . . . 11

      |
16 | 14, 15 | syl 17 |
. . . . . . . . . 10
       |
17 | 16 | snssd 4116 |
. . . . . . . . 9
         |
18 | | ssrab2 3513 |
. . . . . . . . . . 11
     
     
     
                  
     |
19 | | 1eluzge0 11199 |
. . . . . . . . . . . 12
     |
20 | | fzss1 11834 |
. . . . . . . . . . . 12
    
          |
21 | 19, 20 | ax-mp 5 |
. . . . . . . . . . 11
         |
22 | 18, 21 | sstri 3440 |
. . . . . . . . . 10
     
     
     
                  
     |
23 | 22 | a1i 11 |
. . . . . . . . 9
                 
             
            |
24 | 17, 23 | unssd 3609 |
. . . . . . . 8
                    
             
             |
25 | | ltso 9711 |
. . . . . . . . 9
 |
26 | | snfi 7647 |
. . . . . . . . . . 11
   |
27 | | fzfi 12182 |
. . . . . . . . . . . 12
     |
28 | | rabfi 7793 |
. . . . . . . . . . . 12
          
     
     
                     |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . 11
     
     
     
                    |
30 | | unfi 7835 |
. . . . . . . . . . 11
                    
             
               
     
     
                      |
31 | 26, 29, 30 | mp2an 677 |
. . . . . . . . . 10
                                          |
32 | | c0ex 9634 |
. . . . . . . . . . . 12
 |
33 | 32 | snid 3995 |
. . . . . . . . . . 11
   |
34 | | elun1 3600 |
. . . . . . . . . . 11
                                              |
35 | | ne0i 3736 |
. . . . . . . . . . 11
         
     
     
                                                               |
36 | 33, 34, 35 | mp2b 10 |
. . . . . . . . . 10
                                          |
37 | | 0red 9641 |
. . . . . . . . . . . . 13
     |
38 | 37 | snssd 4116 |
. . . . . . . . . . . 12
       |
39 | 1, 38 | ax-mp 5 |
. . . . . . . . . . 11
 
 |
40 | | elfzelz 11797 |
. . . . . . . . . . . . . 14
       |
41 | 40 | ssriv 3435 |
. . . . . . . . . . . . 13
     |
42 | | zssre 10941 |
. . . . . . . . . . . . 13
 |
43 | 41, 42 | sstri 3440 |
. . . . . . . . . . . 12
     |
44 | 18, 43 | sstri 3440 |
. . . . . . . . . . 11
     
     
     
                  
 |
45 | 39, 44 | unssi 3608 |
. . . . . . . . . 10
                                          |
46 | 31, 36, 45 | 3pm3.2i 1185 |
. . . . . . . . 9
                                         
                                                 
     
     
                      |
47 | | fisupcl 7982 |
. . . . . . . . 9
          
     
     
                                       
             
               
     
     
                                
     
     
                                                                 |
48 | 25, 46, 47 | mp2an 677 |
. . . . . . . 8
                     
             
                            
             
        |
49 | | ssel 3425 |
. . . . . . . 8
                                             
           
     
     
                                                                         
     
     
                             |
50 | 24, 48, 49 | mpisyl 21 |
. . . . . . 7
                                                    |
51 | 50 | ad2antrr 731 |
. . . . . 6
                                                                    |
52 | | elfznn 11825 |
. . . . . . . . 9
       |
53 | | nngt0 10635 |
. . . . . . . . . . . 12
   |
54 | 53 | adantr 467 |
. . . . . . . . . . 11
         |
55 | | simpr 463 |
. . . . . . . . . . . . . 14
 
     
                        |
56 | 55 | ralimi 2780 |
. . . . . . . . . . . . 13
 
     
     
                              |
57 | | elfznn 11825 |
. . . . . . . . . . . . . 14
       |
58 | | nnre 10613 |
. . . . . . . . . . . . . . . . . . . 20
   |
59 | | nnre 10613 |
. . . . . . . . . . . . . . . . . . . 20
   |
60 | | lenlt 9709 |
. . . . . . . . . . . . . . . . . . . 20
 
     |
61 | 58, 59, 60 | syl2an 480 |
. . . . . . . . . . . . . . . . . . 19
 
     |
62 | | elfz1b 11861 |
. . . . . . . . . . . . . . . . . . . . 21
    
    |
63 | 62 | biimpri 210 |
. . . . . . . . . . . . . . . . . . . 20
 
       |
64 | 63 | 3expia 1209 |
. . . . . . . . . . . . . . . . . . 19
 
         |
65 | 61, 64 | sylbird 239 |
. . . . . . . . . . . . . . . . . 18
 
 
       |
66 | | fveq2 5863 |
. . . . . . . . . . . . . . . . . . . . 21
           |
67 | 66 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . . . . 20
             |
68 | 67 | rspcev 3149 |
. . . . . . . . . . . . . . . . . . 19
                       |
69 | 68 | expcom 437 |
. . . . . . . . . . . . . . . . . 18
          
            |
70 | 65, 69 | sylan9 662 |
. . . . . . . . . . . . . . . . 17
        
              |
71 | 70 | an32s 812 |
. . . . . . . . . . . . . . . 16
         
             |
72 | | nne 2627 |
. . . . . . . . . . . . . . . . . 18
           |
73 | 72 | rexbii 2888 |
. . . . . . . . . . . . . . . . 17
          
           |
74 | | rexnal 2835 |
. . . . . . . . . . . . . . . . 17
                      |
75 | 73, 74 | bitr3i 255 |
. . . . . . . . . . . . . . . 16
          
            |
76 | 71, 75 | syl6ib 230 |
. . . . . . . . . . . . . . 15
         
             |
77 | 76 | con4d 109 |
. . . . . . . . . . . . . 14
                       |
78 | 57, 77 | sylan2 477 |
. . . . . . . . . . . . 13
            
 
            |
79 | 56, 78 | syl5 33 |
. . . . . . . . . . . 12
            
 
     
     
                     |
80 | 79 | ralrimiva 2801 |
. . . . . . . . . . 11
                         
             
    
   |
81 | | ralunb 3614 |
. . . . . . . . . . . 12
 
                                         
 
                                             |
82 | | breq1 4404 |
. . . . . . . . . . . . . 14
 
   |
83 | 32, 82 | ralsn 4009 |
. . . . . . . . . . . . 13
 
     |
84 | | oveq2 6296 |
. . . . . . . . . . . . . . 15
           |
85 | 84 | raleqdv 2992 |
. . . . . . . . . . . . . 14
  
     
     
                  
     
     
                     |
86 | 85 | ralrab 3199 |
. . . . . . . . . . . . 13
 
                
             
                         
             
    
   |
87 | 83, 86 | anbi12i 702 |
. . . . . . . . . . . 12
     
                 
             
       
 
                                    
    |
88 | 81, 87 | bitri 253 |
. . . . . . . . . . 11
 
                                         
 
                                    
    |
89 | 54, 80, 88 | sylanbrc 669 |
. . . . . . . . . 10
                                                    |
90 | | breq1 4404 |
. . . . . . . . . . 11
                                                         
     
     
                         |
91 | 90 | rspcva 3147 |
. . . . . . . . . 10
                                                                  
             
                                                             
     
     
                        |
92 | 48, 89, 91 | sylancr 668 |
. . . . . . . . 9
                                                      |
93 | 52, 92 | sylan 474 |
. . . . . . . 8
                                                          |
94 | 93 | 3adant2 1026 |
. . . . . . 7
                                                                      |
95 | 94 | adantl 468 |
. . . . . 6
                          
                     
             
           |
96 | 40 | zred 11037 |
. . . . . . . . . . 11
       |
97 | 96 | 3ad2ant1 1028 |
. . . . . . . . . 10
                         |
98 | 97 | adantl 468 |
. . . . . . . . 9
                          
  |
99 | | simpr1 1013 |
. . . . . . . . . . 11
                          
      |
100 | | simpll 759 |
. . . . . . . . . . . . 13
                          
  |
101 | | simplr 761 |
. . . . . . . . . . . . . . . . 17
                      
  |
102 | | elfzelz 11797 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
103 | 102 | zred 11037 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
104 | | nndivre 10642 |
. . . . . . . . . . . . . . . . . . . . . 22
 
     |
105 | 103, 104 | sylan 474 |
. . . . . . . . . . . . . . . . . . . . 21
     
     |
106 | | elfzle1 11799 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
107 | 103, 106 | jca 535 |
. . . . . . . . . . . . . . . . . . . . . 22
         |
108 | | nnrp 11308 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
109 | 108 | rpregt0d 11344 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
110 | | divge0 10471 |
. . . . . . . . . . . . . . . . . . . . . 22
  
   
    |
111 | 107, 109,
110 | syl2an 480 |
. . . . . . . . . . . . . . . . . . . . 21
     

    |
112 | | elfzle2 11800 |
. . . . . . . . . . . . . . . . . . . . . . 23
       |
113 | 112 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
     

  |
114 | 103 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
115 | | 1red 9655 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
116 | 108 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
     
   |
117 | 114, 115,
116 | ledivmuld 11388 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
         |
118 | | nncn 10614 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
119 | 118 | mulid1d 9657 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
120 | 119 | breq2d 4413 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
 
   |
121 | 120 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
   
   |
122 | 117, 121 | bitrd 257 |
. . . . . . . . . . . . . . . . . . . . . 22
     
       |
123 | 113, 122 | mpbird 236 |
. . . . . . . . . . . . . . . . . . . . 21
     
  
  |
124 | | 0re 9640 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
125 | | 1re 9639 |
. . . . . . . . . . . . . . . . . . . . . 22
 |
126 | 124, 125 | elicc2i 11697 |
. . . . . . . . . . . . . . . . . . . . 21
     ![[,] [,]](_icc.gif) 
    
     |
127 | 105, 111,
123, 126 | syl3anbrc 1191 |
. . . . . . . . . . . . . . . . . . . 20
     
     ![[,] [,]](_icc.gif)    |
128 | 127 | ancoms 455 |
. . . . . . . . . . . . . . . . . . 19
 
         ![[,] [,]](_icc.gif)    |
129 | | elsni 3992 |
. . . . . . . . . . . . . . . . . . . . 21
     |
130 | 129 | oveq2d 6304 |
. . . . . . . . . . . . . . . . . . . 20
         |
131 | 130 | eleq1d 2512 |
. . . . . . . . . . . . . . . . . . 19
        ![[,] [,]](_icc.gif)      ![[,] [,]](_icc.gif)     |
132 | 128, 131 | syl5ibrcom 226 |
. . . . . . . . . . . . . . . . . 18
 
            ![[,] [,]](_icc.gif)     |
133 | 132 | impr 624 |
. . . . . . . . . . . . . . . . 17
               ![[,] [,]](_icc.gif)    |
134 | 101, 133 | sylan 474 |
. . . . . . . . . . . . . . . 16
   
                                 ![[,] [,]](_icc.gif)    |
135 | | simprr 765 |
. . . . . . . . . . . . . . . 16
                      
              |
136 | | vex 3047 |
. . . . . . . . . . . . . . . . . 18
 |
137 | 136 | fconst 5767 |
. . . . . . . . . . . . . . . . 17
                   |
138 | 137 | a1i 11 |
. . . . . . . . . . . . . . . 16
                      
                    |
139 | | fzfid 12183 |
. . . . . . . . . . . . . . . 16
                      
      |
140 | | inidm 3640 |
. . . . . . . . . . . . . . . 16
               |
141 | 134, 135,
138, 139, 139, 140 | off 6543 |
. . . . . . . . . . . . . . 15
                      
 
                   ![[,] [,]](_icc.gif)    |
142 | | poimir.i |
. . . . . . . . . . . . . . . . 17
   ![[,] [,]](_icc.gif)        |
143 | 142 | eleq2i 2520 |
. . . . . . . . . . . . . . . 16
           
 
            ![[,] [,]](_icc.gif)         |
144 | | ovex 6316 |
. . . . . . . . . . . . . . . . 17
  ![[,] [,]](_icc.gif)   |
145 | | ovex 6316 |
. . . . . . . . . . . . . . . . 17
     |
146 | 144, 145 | elmap 7497 |
. . . . . . . . . . . . . . . 16
               ![[,] [,]](_icc.gif)      
 
                   ![[,] [,]](_icc.gif)    |
147 | 143, 146 | bitri 253 |
. . . . . . . . . . . . . . 15
           
 
                   ![[,] [,]](_icc.gif)    |
148 | 141, 147 | sylibr 216 |
. . . . . . . . . . . . . 14
                      
 
           |
149 | 148 | 3adantr3 1168 |
. . . . . . . . . . . . 13
                          
 
           |
150 | | 3anass 988 |
. . . . . . . . . . . . . . . 16
                                                 |
151 | | ancom 452 |
. . . . . . . . . . . . . . . 16
                  
     
                          |
152 | 150, 151 | bitri 253 |
. . . . . . . . . . . . . . 15
                                         
       |
153 | | ffn 5726 |
. . . . . . . . . . . . . . . . . 18
            
      |
154 | 153 | ad2antrl 733 |
. . . . . . . . . . . . . . . . 17
                             |
155 | | fnconstg 5769 |
. . . . . . . . . . . . . . . . . 18
               |
156 | 136, 155 | mp1i 13 |
. . . . . . . . . . . . . . . . 17
                                     |
157 | | fzfid 12183 |
. . . . . . . . . . . . . . . . 17
                             |
158 | | simplrr 770 |
. . . . . . . . . . . . . . . . 17
   
             
                 |
159 | 136 | fvconst2 6118 |
. . . . . . . . . . . . . . . . . 18
                   |
160 | 159 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   
             
                         |
161 | 154, 156,
157, 157, 140, 158, 160 | ofval 6537 |
. . . . . . . . . . . . . . . 16
   
             
                              |
162 | 161 | anasss 652 |
. . . . . . . . . . . . . . 15
                 
                              |
163 | 152, 162 | sylan2b 478 |
. . . . . . . . . . . . . 14
                          
                   |
164 | | nnne0 10639 |
. . . . . . . . . . . . . . . 16
   |
165 | 118, 164 | dividd 10378 |
. . . . . . . . . . . . . . 15
     |
166 | 165 | ad2antlr 732 |
. . . . . . . . . . . . . 14
                          
    |
167 | 163, 166 | eqtrd 2484 |
. . . . . . . . . . . . 13
                          
                 |
168 | | ovex 6316 |
. . . . . . . . . . . . . 14
            |
169 | | eleq1 2516 |
. . . . . . . . . . . . . . . . 17
            
 
            |
170 | | fveq1 5862 |
. . . . . . . . . . . . . . . . . 18
                                 |
171 | 170 | eqeq1d 2452 |
. . . . . . . . . . . . . . . . 17
                                   |
172 | 169, 171 | 3anbi23d 1341 |
. . . . . . . . . . . . . . . 16
                                                          |
173 | 172 | anbi2d 709 |
. . . . . . . . . . . . . . 15
             
    
       
    
                              |
174 | | fveq2 5863 |
. . . . . . . . . . . . . . . . 17
                   
             |
175 | 174 | fveq1d 5865 |
. . . . . . . . . . . . . . . 16
                                         |
176 | 175 | breq2d 4413 |
. . . . . . . . . . . . . . 15
            
       
                      |
177 | 173, 176 | imbi12d 322 |
. . . . . . . . . . . . . 14
               
   
     
                                           
                       |
178 | | poimir.3 |
. . . . . . . . . . . . . 14
 
    
                |
179 | 168, 177,
178 | vtocl 3099 |
. . . . . . . . . . . . 13
 
    
 
                         
     
               |
180 | 100, 99, 149, 167, 179 | syl13anc 1269 |
. . . . . . . . . . . 12
                          
                     |
181 | | simpr 463 |
. . . . . . . . . . . . 13
 

  |
182 | | simp3 1009 |
. . . . . . . . . . . . 13
                             |
183 | | neeq1 2685 |
. . . . . . . . . . . . . . 15
             |
184 | 164, 183 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
             |
185 | 184 | imp 431 |
. . . . . . . . . . . . 13
             |
186 | 181, 182,
185 | syl2an 480 |
. . . . . . . . . . . 12
                          
      |
187 | | vex 3047 |
. . . . . . . . . . . . 13
 |
188 | | fveq2 5863 |
. . . . . . . . . . . . . . 15
                                         |
189 | 188 | breq2d 4413 |
. . . . . . . . . . . . . 14
 
     
            
                      |
190 | 66 | neeq1d 2682 |
. . . . . . . . . . . . . 14
             |
191 | 189, 190 | anbi12d 716 |
. . . . . . . . . . . . 13
                                
             
        |
192 | 187, 191 | ralsn 4009 |
. . . . . . . . . . . 12
 
       
             
          
             
       |
193 | 180, 186,
192 | sylanbrc 669 |
. . . . . . . . . . 11
                          
   
     
                    |
194 | 40 | zcnd 11038 |
. . . . . . . . . . . . . . . . . . 19
       |
195 | | 1cnd 9656 |
. . . . . . . . . . . . . . . . . . 19
       |
196 | 194, 195 | subeq0ad 9993 |
. . . . . . . . . . . . . . . . . 18
           |
197 | 196 | biimpcd 228 |
. . . . . . . . . . . . . . . . 17
       
   |
198 | | 1z 10964 |
. . . . . . . . . . . . . . . . . . . . 21
 |
199 | | fzsn 11837 |
. . . . . . . . . . . . . . . . . . . . 21
         |
200 | 198, 199 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . . 20
       |
201 | | oveq2 6296 |
. . . . . . . . . . . . . . . . . . . 20
           |
202 | | sneq 3977 |
. . . . . . . . . . . . . . . . . . . 20
  
    |
203 | 200, 201,
202 | 3eqtr4a 2510 |
. . . . . . . . . . . . . . . . . . 19
         |
204 | 203 | raleqdv 2992 |
. . . . . . . . . . . . . . . . . 18
  
     
     
                  
       
             
        |
205 | 204 | biimprd 227 |
. . . . . . . . . . . . . . . . 17
  
       
             
    
           
             
        |
206 | 197, 205 | syl6 34 |
. . . . . . . . . . . . . . . 16
            
     
                                                     |
207 | | ralun 3615 |
. . . . . . . . . . . . . . . . . . . 20
                                  
   
     
                  
            
     
                    |
208 | | npcan1 10041 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
209 | 194, 208 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
210 | | elfzuz 11793 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
211 | 209, 210 | eqeltrd 2528 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
212 | | peano2zm 10977 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
213 | | uzid 11170 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
             |
214 | | peano2uz 11209 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
        
            |
215 | 40, 212, 213, 214 | 4syl 19 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                 |
216 | 209, 215 | eqeltrrd 2529 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
217 | | fzsplit2 11821 |
. . . . . . . . . . . . . . . . . . . . . . 23
                
                      |
218 | 211, 216,
217 | syl2anc 666 |
. . . . . . . . . . . . . . . . . . . . . 22
                           |
219 | 209 | oveq1d 6303 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   |
220 | | fzsn 11837 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
         |
221 | 40, 220 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
             |
222 | 219, 221 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . . . 23
                 |
223 | 222 | uneq2d 3587 |
. . . . . . . . . . . . . . . . . . . . . 22
                                 |
224 | 218, 223 | eqtrd 2484 |
. . . . . . . . . . . . . . . . . . . . 21
                     |
225 | 224 | raleqdv 2992 |
. . . . . . . . . . . . . . . . . . . 20
      
     
     
                  
                                       |
226 | 207, 225 | syl5ibr 225 |
. . . . . . . . . . . . . . . . . . 19
                    
             
    
   
     
                  
           
             
        |
227 | 226 | expd 438 |
. . . . . . . . . . . . . . . . . 18
      
       
     
                      
     
                                                     |
228 | 227 | com12 32 |
. . . . . . . . . . . . . . . . 17
 
       
     
                      
 
       
             
    
           
             
         |
229 | 228 | adantl 468 |
. . . . . . . . . . . . . . . 16
                
     
                  
    
 
       
             
    
           
             
         |
230 | 206, 229 | jaoi 381 |
. . . . . . . . . . . . . . 15
                        
             
                
     
                                                     |
231 | 230 | imdistand 697 |
. . . . . . . . . . . . . 14
                        
             
            
   
     
                  
    
           
             
         |
232 | 231 | com12 32 |
. . . . . . . . . . . . 13
              
             
                
             
             
                       
             
         |
233 | | elun 3573 |
. . . . . . . . . . . . . 14
           
     
     
                   
                                               |
234 | | ovex 6316 |
. . . . . . . . . . . . . . . 16
   |
235 | 234 | elsnc 3991 |
. . . . . . . . . . . . . . 15
         |
236 | | oveq2 6296 |
. . . . . . . . . . . . . . . . 17
               |
237 | 236 | raleqdv 2992 |
. . . . . . . . . . . . . . . 16
    
     
     
                  
       
     
                     |
238 | 237 | elrab 3195 |
. . . . . . . . . . . . . . 15
                   
             
     
       
       
     
                     |
239 | 235, 238 | orbi12i 524 |
. . . . . . . . . . . . . 14
                        
             
      
                  
     
                      |
240 | 233, 239 | bitri 253 |
. . . . . . . . . . . . 13
           
     
     
                   
                  
     
                      |
241 | | oveq2 6296 |
. . . . . . . . . . . . . . 15
           |
242 | 241 | raleqdv 2992 |
. . . . . . . . . . . . . 14
  
     
     
                  
     
     
                     |
243 | 242 | elrab 3195 |
. . . . . . . . . . . . 13
                 
             
     
    
           
             
        |
244 | 232, 240,
243 | 3imtr4g 274 |
. . . . . . . . . . . 12
              
             
                                                 
                
             
         |
245 | | elun2 3601 |
. . . . . . . . . . . 12
                 
             
                         
             
         |
246 | 244, 245 | syl6 34 |
. . . . . . . . . . 11
              
             
                                                 
                                            |
247 | 99, 193, 246 | syl2anc 666 |
. . . . . . . . . 10
                          
           
     
     
                                       
             
          |
248 | | fimaxre2 10549 |
. . . . . . . . . . . . 13
                     
             
               
     
     
                                                                   |
249 | 45, 31, 248 | mp2an 677 |
. . . . . . . . . . . 12
                     
             
         |
250 | 45, 36, 249 | 3pm3.2i 1185 |
. . . . . . . . . . 11
                                                  
     
     
                    
                    
             
          |
251 | 250 | suprubii 10579 |
. . . . . . . . . 10
         
     
     
                                                                   |
252 | 247, 251 | syl6 34 |
. . . . . . . . 9
                          
           
     
     
                                                                    |
253 | | ltm1 10442 |
. . . . . . . . . 10
     |
254 | | peano2rem 9938 |
. . . . . . . . . . 11
     |
255 | 45, 48 | sselii 3428 |
. . . . . . . . . . . 12
                     
             
          |
256 | | ltletr 9722 |
. . . . . . . . . . . 12
   
          
     
     
                                                                        
            
     
     
                         |
257 | 255, 256 | mp3an3 1352 |
. . . . . . . . . . 11
   
    
          
     
     
                    |