Step | Hyp | Ref
| Expression |
1 | | itg2gt0.2 |
. 2
       |
2 | | itg2gt0.1 |
. . . . . . 7
   |
3 | | iccssxr 11742 |
. . . . . . . 8
    |
4 | | volf 22561 |
. . . . . . . . 9
        |
5 | 4 | ffvelrni 6036 |
. . . . . . . 8
          |
6 | 3, 5 | sseldi 3416 |
. . . . . . 7
       |
7 | 2, 6 | syl 17 |
. . . . . 6
       |
8 | 7 | adantr 472 |
. . . . 5
 
           |
9 | | itg2gt0.3 |
. . . . . . . . . . . . . . . 16
          |
10 | | reex 9648 |
. . . . . . . . . . . . . . . 16
 |
11 | | fex 6155 |
. . . . . . . . . . . . . . . 16
         
  |
12 | 9, 10, 11 | sylancl 675 |
. . . . . . . . . . . . . . 15
   |
13 | | cnvexg 6758 |
. . . . . . . . . . . . . . 15
 
  |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . 14
 
  |
15 | | imaexg 6749 |
. . . . . . . . . . . . . 14
              |
16 | 14, 15 | syl 17 |
. . . . . . . . . . . . 13
             |
17 | 16 | adantr 472 |
. . . . . . . . . . . 12
 

            |
18 | | eqid 2471 |
. . . . . . . . . . . 12
                         |
19 | 17, 18 | fmptd 6061 |
. . . . . . . . . . 11
                   |
20 | | ffn 5739 |
. . . . . . . . . . 11
                               |
21 | 19, 20 | syl 17 |
. . . . . . . . . 10
               |
22 | | fniunfv 6170 |
. . . . . . . . . 10
                                             |
23 | 21, 22 | syl 17 |
. . . . . . . . 9
                                 |
24 | | itg2gt0.4 |
. . . . . . . . . . . . . . 15
 MblFn |
25 | | rge0ssre 11766 |
. . . . . . . . . . . . . . . 16
    |
26 | | fss 5749 |
. . . . . . . . . . . . . . . 16
                   |
27 | 9, 25, 26 | sylancl 675 |
. . . . . . . . . . . . . . 15
       |
28 | | mbfima 22667 |
. . . . . . . . . . . . . . 15
  MblFn
                 |
29 | 24, 27, 28 | syl2anc 673 |
. . . . . . . . . . . . . 14
             |
30 | 29 | adantr 472 |
. . . . . . . . . . . . 13
 

            |
31 | 30, 18 | fmptd 6061 |
. . . . . . . . . . . 12
                   |
32 | 31 | ffvelrnda 6037 |
. . . . . . . . . . 11
 

                  |
33 | 32 | ralrimiva 2809 |
. . . . . . . . . 10
                    |
34 | | iunmbl 22585 |
. . . . . . . . . 10
 
                                   |
35 | 33, 34 | syl 17 |
. . . . . . . . 9
                    |
36 | 23, 35 | eqeltrrd 2550 |
. . . . . . . 8
                |
37 | | mblss 22563 |
. . . . . . . 8
                          
  |
38 | 36, 37 | syl 17 |
. . . . . . 7
             
  |
39 | | ovolcl 22509 |
. . . . . . 7
             
                    |
40 | 38, 39 | syl 17 |
. . . . . 6
                     |
41 | 40 | adantr 472 |
. . . . 5
 
          
              |
42 | | 0xr 9705 |
. . . . . 6
 |
43 | 42 | a1i 11 |
. . . . 5
 
       |
44 | | mblvol 22562 |
. . . . . . . 8
            |
45 | 2, 44 | syl 17 |
. . . . . . 7
            |
46 | | mblss 22563 |
. . . . . . . . . . . . . . . 16
   |
47 | 2, 46 | syl 17 |
. . . . . . . . . . . . . . 15

  |
48 | 47 | sselda 3418 |
. . . . . . . . . . . . . 14
 
   |
49 | 9 | ffvelrnda 6037 |
. . . . . . . . . . . . . . . 16
 

         |
50 | | elrege0 11764 |
. . . . . . . . . . . . . . . 16
       
            |
51 | 49, 50 | sylib 201 |
. . . . . . . . . . . . . . 15
 

            |
52 | 51 | simpld 466 |
. . . . . . . . . . . . . 14
 

      |
53 | 48, 52 | syldan 478 |
. . . . . . . . . . . . 13
 
       |
54 | | itg2gt0.5 |
. . . . . . . . . . . . 13
 
       |
55 | | nnrecl 10891 |
. . . . . . . . . . . . 13
           
 
      |
56 | 53, 54, 55 | syl2anc 673 |
. . . . . . . . . . . 12
 
          |
57 | | ffn 5739 |
. . . . . . . . . . . . . . . . . 18
       
  |
58 | 9, 57 | syl 17 |
. . . . . . . . . . . . . . . . 17
   |
59 | 58 | ad2antrr 740 |
. . . . . . . . . . . . . . . 16
       |
60 | | elpreima 6017 |
. . . . . . . . . . . . . . . 16
                          |
61 | 59, 60 | syl 17 |
. . . . . . . . . . . . . . 15
                              |
62 | 48 | adantr 472 |
. . . . . . . . . . . . . . . 16
       |
63 | 62 | biantrurd 516 |
. . . . . . . . . . . . . . 15
              
              |
64 | | nnrecre 10668 |
. . . . . . . . . . . . . . . . . . 19
     |
65 | 64 | adantl 473 |
. . . . . . . . . . . . . . . . . 18
 

    |
66 | 65 | rexrd 9708 |
. . . . . . . . . . . . . . . . 17
 

    |
67 | 66 | adantlr 729 |
. . . . . . . . . . . . . . . 16
         |
68 | | elioopnf 11753 |
. . . . . . . . . . . . . . . 16
  
         
               |
69 | 67, 68 | syl 17 |
. . . . . . . . . . . . . . 15
              
               |
70 | 61, 63, 69 | 3bitr2d 289 |
. . . . . . . . . . . . . 14
                      
        |
71 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
72 | | imaexg 6749 |
. . . . . . . . . . . . . . . . . 18
              |
73 | 14, 72 | syl 17 |
. . . . . . . . . . . . . . . . 17
             |
74 | 73 | adantr 472 |
. . . . . . . . . . . . . . . 16
 
             |
75 | | oveq2 6316 |
. . . . . . . . . . . . . . . . . . 19
       |
76 | 75 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
    
        |
77 | 76 | imaeq2d 5174 |
. . . . . . . . . . . . . . . . 17
                       |
78 | 77, 18 | fvmptg 5961 |
. . . . . . . . . . . . . . . 16
                                         |
79 | 71, 74, 78 | syl2anr 486 |
. . . . . . . . . . . . . . 15
                                 |
80 | 79 | eleq2d 2534 |
. . . . . . . . . . . . . 14
                                   |
81 | 53 | adantr 472 |
. . . . . . . . . . . . . . 15
           |
82 | 81 | biantrurd 516 |
. . . . . . . . . . . . . 14
       
   
               |
83 | 70, 80, 82 | 3bitr4rd 294 |
. . . . . . . . . . . . 13
       
   
                   |
84 | 83 | rexbidva 2889 |
. . . . . . . . . . . 12
 
  
 
   
                    |
85 | 56, 84 | mpbid 215 |
. . . . . . . . . . 11
 
                    |
86 | 85 | ex 441 |
. . . . . . . . . 10
  
                   |
87 | | eluni2 4194 |
. . . . . . . . . . 11
               
              |
88 | | eleq2 2538 |
. . . . . . . . . . . . 13
                 
                   |
89 | 88 | rexrn 6039 |
. . . . . . . . . . . 12
               
            
                   |
90 | 21, 89 | syl 17 |
. . . . . . . . . . 11
               
                    |
91 | 87, 90 | syl5bb 265 |
. . . . . . . . . 10
               
                   |
92 | 86, 91 | sylibrd 242 |
. . . . . . . . 9
   
              |
93 | 92 | ssrdv 3424 |
. . . . . . . 8

               |
94 | | ovolss 22516 |
. . . . . . . 8
 
              
          
           
              |
95 | 93, 38, 94 | syl2anc 673 |
. . . . . . 7
           
              |
96 | 45, 95 | eqbrtrd 4416 |
. . . . . 6
    
                    |
97 | 96 | adantr 472 |
. . . . 5
 
                             |
98 | | mblvol 22562 |
. . . . . . . . 9
                                                   |
99 | 36, 98 | syl 17 |
. . . . . . . 8
                                      |
100 | | peano2nn 10643 |
. . . . . . . . . . . . . . . 16
     |
101 | 100 | adantl 473 |
. . . . . . . . . . . . . . 15
 

    |
102 | | nnrecre 10668 |
. . . . . . . . . . . . . . 15
         |
103 | 101, 102 | syl 17 |
. . . . . . . . . . . . . 14
 

      |
104 | 103 | rexrd 9708 |
. . . . . . . . . . . . 13
 

      |
105 | | nnre 10638 |
. . . . . . . . . . . . . . . 16
   |
106 | 105 | adantl 473 |
. . . . . . . . . . . . . . 15
 

  |
107 | 106 | lep1d 10560 |
. . . . . . . . . . . . . 14
 

    |
108 | | nngt0 10660 |
. . . . . . . . . . . . . . . 16
   |
109 | 108 | adantl 473 |
. . . . . . . . . . . . . . 15
 

  |
110 | 101 | nnred 10646 |
. . . . . . . . . . . . . . 15
 

    |
111 | 101 | nngt0d 10675 |
. . . . . . . . . . . . . . 15
 

    |
112 | | lerec 10511 |
. . . . . . . . . . . . . . 15
                 
     |
113 | 106, 109,
110, 111, 112 | syl22anc 1293 |
. . . . . . . . . . . . . 14
 

  
         |
114 | 107, 113 | mpbid 215 |
. . . . . . . . . . . . 13
 

        |
115 | | iooss1 11696 |
. . . . . . . . . . . . 13
                           |
116 | 104, 114,
115 | syl2anc 673 |
. . . . . . . . . . . 12
 

              |
117 | | imass2 5210 |
. . . . . . . . . . . 12
    
                                |
118 | 116, 117 | syl 17 |
. . . . . . . . . . 11
 

                        |
119 | 71, 73, 78 | syl2anr 486 |
. . . . . . . . . . 11
 

                            |
120 | | imaexg 6749 |
. . . . . . . . . . . . 13
                |
121 | 14, 120 | syl 17 |
. . . . . . . . . . . 12
               |
122 | | oveq2 6316 |
. . . . . . . . . . . . . . 15
           |
123 | 122 | oveq1d 6323 |
. . . . . . . . . . . . . 14
      
          |
124 | 123 | imaeq2d 5174 |
. . . . . . . . . . . . 13
                           |
125 | 124, 18 | fvmptg 5961 |
. . . . . . . . . . . 12
                                                 |
126 | 100, 121,
125 | syl2anr 486 |
. . . . . . . . . . 11
 

                                |
127 | 118, 119,
126 | 3sstr4d 3461 |
. . . . . . . . . 10
 

                                    |
128 | 127 | ralrimiva 2809 |
. . . . . . . . 9
                                      |
129 | | volsup 22588 |
. . . . . . . . 9
                                                     
   
                                   |
130 | 31, 128, 129 | syl2anc 673 |
. . . . . . . 8
                       
                |
131 | 99, 130 | eqtr3d 2507 |
. . . . . . 7
                                         |
132 | 131 | adantr 472 |
. . . . . 6
 
          
                 
                |
133 | 73 | adantr 472 |
. . . . . . . . . . . . 13
 
                 |
134 | 71, 133, 78 | syl2anr 486 |
. . . . . . . . . . . 12
                                     |
135 | 134 | fveq2d 5883 |
. . . . . . . . . . 11
                                             |
136 | 42 | a1i 11 |
. . . . . . . . . . . . . . . . 17
 
                   |
137 | | nnrecgt0 10669 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
138 | 137 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

    |
139 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 |
140 | | ltle 9740 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       
     |
141 | 139, 65, 140 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 

        |
142 | 138, 141 | mpd 15 |
. . . . . . . . . . . . . . . . . . . . . . 23
 

    |
143 | | elxrge0 11767 |
. . . . . . . . . . . . . . . . . . . . . . 23
     
  
     |
144 | 66, 142, 143 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . 22
 

       |
145 | | 0e0iccpnf 11769 |
. . . . . . . . . . . . . . . . . . . . . 22
    |
146 | | ifcl 3914 |
. . . . . . . . . . . . . . . . . . . . . 22
      
                          |
147 | 144, 145,
146 | sylancl 675 |
. . . . . . . . . . . . . . . . . . . . 21
 

                      |
148 | 147 | adantr 472 |
. . . . . . . . . . . . . . . . . . . 20
      
                    |
149 | | eqid 2471 |
. . . . . . . . . . . . . . . . . . . 20
                                       |
150 | 148, 149 | fmptd 6061 |
. . . . . . . . . . . . . . . . . . 19
 

                            |
151 | 150 | adantrr 731 |
. . . . . . . . . . . . . . . . . 18
 
                                             |
152 | | itg2cl 22769 |
. . . . . . . . . . . . . . . . . 18
                                                    |
153 | 151, 152 | syl 17 |
. . . . . . . . . . . . . . . . 17
 
                                          |
154 | | icossicc 11746 |
. . . . . . . . . . . . . . . . . . . 20
       |
155 | | fss 5749 |
. . . . . . . . . . . . . . . . . . . 20
                         |
156 | 9, 154, 155 | sylancl 675 |
. . . . . . . . . . . . . . . . . . 19
          |
157 | | itg2cl 22769 |
. . . . . . . . . . . . . . . . . . 19
              |
158 | 156, 157 | syl 17 |
. . . . . . . . . . . . . . . . . 18
       |
159 | 158 | adantr 472 |
. . . . . . . . . . . . . . . . 17
 
                       |
160 | | 0nrp 11357 |
. . . . . . . . . . . . . . . . . . 19
 |
161 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
                                                 |
162 | 119, 32 | eqeltrrd 2550 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

            |
163 | 162 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                             |
164 | 163 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
                                    |
165 | 161, 139 | syl6eqelr 2558 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   
                                                 |
166 | 65, 138 | elrpd 11361 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
 

    |
167 | 166 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 
                     |
168 | 167 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   
                            |
169 | | itg2const2 22778 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                                        |
170 | 164, 168,
169 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                   
                                                                 |
171 | 165, 170 | mpbird 240 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
                                        |
172 | | elrege0 11764 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
     
        |
173 | 65, 142, 172 | sylanbrc 677 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 

       |
174 | 173 | adantrr 731 |
. . . . . . . . . . . . . . . . . . . . . . . 24
 
                        |
175 | 174 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
                               |
176 | | itg2const 22777 |
. . . . . . . . . . . . . . . . . . . . . . 23
                                                                           |
177 | 164, 171,
175, 176 | syl3anc 1292 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
                                                                   |
178 | 161, 177 | eqtrd 2505 |
. . . . . . . . . . . . . . . . . . . . 21
                   
                                            |
179 | | simplrr 779 |
. . . . . . . . . . . . . . . . . . . . . . 23
                   
                                        |
180 | 171, 179 | elrpd 11361 |
. . . . . . . . . . . . . . . . . . . . . 22
                   
                                        |
181 | 168, 180 | rpmulcld 11380 |
. . . . . . . . . . . . . . . . . . . . 21
                   
                                            |
182 | 178, 181 | eqeltrd 2549 |
. . . . . . . . . . . . . . . . . . . 20
                   
                          |
183 | 182 | ex 441 |
. . . . . . . . . . . . . . . . . . 19
 
                                            |
184 | 160, 183 | mtoi 183 |
. . . . . . . . . . . . . . . . . 18
 
                
                         |
185 | | itg2ge0 22772 |
. . . . . . . . . . . . . . . . . . . . 21
                                                    |
186 | 151, 185 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
 
                
                         |
187 | | xrleloe 11466 |
. . . . . . . . . . . . . . . . . . . . 21
                                                                                                     |
188 | 42, 153, 187 | sylancr 676 |
. . . . . . . . . . . . . . . . . . . 20
 
                                                                                            |
189 | 186, 188 | mpbid 215 |
. . . . . . . . . . . . . . . . . . 19
 
                                                                   |
190 | 189 | ord 384 |
. . . . . . . . . . . . . . . . . 18
 
                                                                   |
191 | 184, 190 | mt3d 130 |
. . . . . . . . . . . . . . . . 17
 
                
                         |
192 | 156 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
 
                          |
193 | 65 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                   |
194 | 58 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
 

  |
195 | 194, 60 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
 

          
              |
196 | 195 | biimpa 492 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
                            |
197 | 196 | simpld 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
              
  |
198 | 52 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
           |
199 | 197, 198 | syldan 478 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                     |
200 | 66 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                   |
201 | 196 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
                          |
202 | | simpr 468 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
       
      
      |
203 | 68, 202 | syl6bi 236 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
  
         
         |
204 | 200, 201,
203 | sylc 61 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                
      |
205 | 193, 199,
204 | ltled 9800 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                
      |
206 | 51 | simprd 470 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
 

      |
207 | 206 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
208 | 197, 207 | syldan 478 |
. . . . . . . . . . . . . . . . . . . . . . . 24
              
      |
209 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                           
       |
210 | | breq1 4398 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
                                       
       |
211 | 209, 210 | ifboth 3908 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   
          
              
      |
212 | 205, 208,
211 | syl2anc 673 |
. . . . . . . . . . . . . . . . . . . . . . 23
                               
      |
213 | 212 | adantlr 729 |
. . . . . . . . . . . . . . . . . . . . . 22
   

           
                
      |
214 | | iffalse 3881 |
. . . . . . . . . . . . . . . . . . . . . . . 24
                              |
215 | 214 | adantl 473 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

                               |
216 | 207 | adantr 472 |
. . . . . . . . . . . . . . . . . . . . . . 23
   

           
      |
217 | 215, 216 | eqbrtrd 4416 |
. . . . . . . . . . . . . . . . . . . . . 22
   

                            
      |
218 | 213, 217 | pm2.61dan 808 |
. . . . . . . . . . . . . . . . . . . . 21
      
              
      |
219 | 218 | ralrimiva 2809 |
. . . . . . . . . . . . . . . . . . . 20
 

                        |
220 | 219 | adantrr 731 |
. . . . . . . . . . . . . . . . . . 19
 
                 
                
      |
221 | 10 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
   |
222 | | ovex 6336 |
. . . . . . . . . . . . . . . . . . . . . . 23
   |
223 | | c0ex 9655 |
. . . . . . . . . . . . . . . . . . . . . . 23
 |
224 | 222, 223 | ifex 3940 |
. . . . . . . . . . . . . . . . . . . . . 22
                  |
225 | 224 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 

                   |
226 | | fvex 5889 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
227 | 226 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . 21
 

      |
228 | | eqidd 2472 |
. . . . . . . . . . . . . . . . . . . . 21
                                         |
229 | 9 | feqmptd 5932 |
. . . . . . . . . . . . . . . . . . . . 21
         |
230 | 221, 225,
227, 228, 229 | ofrfval2 6568 |
. . . . . . . . . . . . . . . . . . . 20
                        
              
       |
231 | 230 | biimpar 493 |
. . . . . . . . . . . . . . . . . . 19
 
                                             |
232 | 220, 231 | syldan 478 |
. . . . . . . . . . . . . . . . . 18
 
                                       |
233 | | itg2le 22776 |
. . . . . . . . . . . . . . . . . 18
                                                       
                             |
234 | 151, 192,
232, 233 | syl3anc 1292 |
. . . . . . . . . . . . . . . . 17
 
                                              |
235 | 136, 153,
159, 191, 234 | xrltletrd 11481 |
. . . . . . . . . . . . . . . 16
 
                
      |
236 | 235 | expr 626 |
. . . . . . . . . . . . . . 15
 

              
       |
237 | 236 | con3d 140 |
. . . . . . . . . . . . . 14
 

                      |
238 | 4 | ffvelrni 6036 |
. . . . . . . . . . . . . . . . 17
                              |
239 | 3, 238 | sseldi 3416 |
. . . . . . . . . . . . . . . 16
                           |
240 | 162, 239 | syl 17 |
. . . . . . . . . . . . . . 15
 

                |
241 | | xrlenlt 9717 |
. . . . . . . . . . . . . . 15
                               
                 |
242 | 240, 42, 241 | sylancl 675 |
. . . . . . . . . . . . . 14
 

              
                 |
243 | 237, 242 | sylibrd 242 |
. . . . . . . . . . . . 13
 

                      |
244 | 243 | imp 436 |
. . . . . . . . . . . 12
                         |
245 | 244 | an32s 821 |
. . . . . . . . . . 11
                         |
246 | 135, 245 | eqbrtrd 4416 |
. . . . . . . . . 10
                            
  |
247 | 246 | ralrimiva 2809 |
. . . . . . . . 9
 
                         
  |
248 | | fveq2 5879 |
. . . . . . . . . . . . 13
                                           |
249 | 248 | breq1d 4405 |
. . . . . . . . . . . 12
                                         
   |
250 | 249 | ralrn 6040 |
. . . . . . . . . . 11
               
               
                    
   |
251 | 19, 20, 250 | 3syl 18 |
. . . . . . . . . 10
                   
                    
   |
252 | 251 | adantr 472 |
. . . . . . . . 9
 
      

               
                    
   |
253 | 247, 252 | mpbird 240 |
. . . . . . . 8
 
                         |
254 | | ffn 5739 |
. . . . . . . . . 10
  
       |
255 | 4, 254 | ax-mp 5 |
. . . . . . . . 9
 |
256 | | frn 5747 |
. . . . . . . . . . 11
                               |
257 | 31, 256 | syl 17 |
. . . . . . . . . 10
               |
258 | 257 | adantr 472 |
. . . . . . . . 9
 
     
          
  |
259 | | breq1 4398 |
. . . . . . . . . 10
    
    
   |
260 | 259 | ralima 6163 |
. . . . . . . . 9
                
                  
               
   |
261 | 255, 258,
260 | sylancr 676 |
. . . . . . . 8
 
      
                  
               
   |
262 | 253, 261 | mpbird 240 |
. . . . . . 7
 
         
               |
263 | | imassrn 5185 |
. . . . . . . . 9
               
 |
264 | | frn 5747 |
. . . . . . . . . . 11
  
    
     |
265 | 4, 264 | ax-mp 5 |
. . . . . . . . . 10
    |
266 | 265, 3 | sstri 3427 |
. . . . . . . . 9
 |
267 | 263, 266 | sstri 3427 |
. . . . . . . 8
                 |
268 | | supxrleub 11637 |
. . . . . . . 8
     
                   
                               
   |
269 | 267, 42, 268 | mp2an 686 |
. . . . . . 7
      
                               
  |
270 | 262, 269 | sylibr 217 |
. . . . . 6
 
          
                |
271 | 132, 270 | eqbrtrd 4416 |
. . . . 5
 
          
              |
272 | 8, 41, 43, 97, 271 | xrletrd 11482 |
. . . 4
 
           |
273 | 272 | ex 441 |
. . 3
         
   |
274 | | xrlenlt 9717 |
. . . 4
           
       |
275 | 7, 42, 274 | sylancl 675 |
. . 3
     
       |
276 | 273, 275 | sylibd 222 |
. 2
     
       |
277 | 1, 276 | mt4d 145 |
1
       |