Step | Hyp | Ref
| Expression |
1 | | inss1 3521 |
. . . . 5
   |
2 | 1 | a1i 11 |
. . . 4
  
  |
3 | | ioombl1.e |
. . . 4

  |
4 | | ioombl1.v |
. . . 4
        |
5 | | ovolsscl 19335 |
. . . 4
   
          
    |
6 | 2, 3, 4, 5 | syl3anc 1184 |
. . 3
     
    |
7 | | difss 3434 |
. . . . 5
   |
8 | 7 | a1i 11 |
. . . 4
  
  |
9 | | ovolsscl 19335 |
. . . 4
   
          
    |
10 | 8, 3, 4, 9 | syl3anc 1184 |
. . 3
     
    |
11 | 6, 10 | readdcld 9071 |
. 2
                   |
12 | | ioombl1.b |
. . 3
    |
13 | | ioombl1.a |
. . 3
   |
14 | | ioombl1.c |
. . 3
   |
15 | | ioombl1.s |
. . 3
  
   |
16 | | ioombl1.t |
. . 3
  
   |
17 | | ioombl1.u |
. . 3
  
   |
18 | | ioombl1.f1 |
. . 3
          |
19 | | ioombl1.f2 |
. . 3

     |
20 | | ioombl1.f3 |
. . 3
              |
21 | | ioombl1.p |
. . 3
         |
22 | | ioombl1.q |
. . 3
         |
23 | | ioombl1.g |
. . 3
     
 
   
 
       |
24 | | ioombl1.h |
. . 3
       
     
       |
25 | 12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 | ioombl1lem2 19406 |
. 2
       |
26 | 14 | rpred 10604 |
. . 3
   |
27 | 4, 26 | readdcld 9071 |
. 2
          |
28 | 12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 | ioombl1lem1 19405 |
. . . . . . . . 9
     
             |
29 | 28 | simpld 446 |
. . . . . . . 8
          |
30 | | eqid 2404 |
. . . . . . . . 9
    
  |
31 | 30, 16 | ovolsf 19322 |
. . . . . . . 8
                 |
32 | 29, 31 | syl 16 |
. . . . . . 7
          |
33 | | frn 5556 |
. . . . . . 7
             |
34 | 32, 33 | syl 16 |
. . . . . 6
  
   |
35 | | 0re 9047 |
. . . . . . 7
 |
36 | | pnfxr 10669 |
. . . . . . 7
 |
37 | | icossre 10947 |
. . . . . . 7
    
   |
38 | 35, 36, 37 | mp2an 654 |
. . . . . 6
    |
39 | 34, 38 | syl6ss 3320 |
. . . . 5
   |
40 | | 1nn 9967 |
. . . . . . . 8
 |
41 | | fdm 5554 |
. . . . . . . . 9
          |
42 | 32, 41 | syl 16 |
. . . . . . . 8
   |
43 | 40, 42 | syl5eleqr 2491 |
. . . . . . 7
   |
44 | | ne0i 3594 |
. . . . . . 7
   |
45 | 43, 44 | syl 16 |
. . . . . 6
   |
46 | | dm0rn0 5045 |
. . . . . . 7

  |
47 | 46 | necon3bii 2599 |
. . . . . 6

  |
48 | 45, 47 | sylib 189 |
. . . . 5
   |
49 | 32 | ffvelrnda 5829 |
. . . . . . . . . 10
 

         |
50 | 38, 49 | sseldi 3306 |
. . . . . . . . 9
 

      |
51 | | eqid 2404 |
. . . . . . . . . . . . 13
    
  |
52 | 51, 15 | ovolsf 19322 |
. . . . . . . . . . . 12
                 |
53 | 18, 52 | syl 16 |
. . . . . . . . . . 11
          |
54 | 53 | ffvelrnda 5829 |
. . . . . . . . . 10
 

         |
55 | 38, 54 | sseldi 3306 |
. . . . . . . . 9
 

      |
56 | 25 | adantr 452 |
. . . . . . . . 9
 

      |
57 | | simpr 448 |
. . . . . . . . . . . 12
 

  |
58 | | nnuz 10477 |
. . . . . . . . . . . 12
     |
59 | 57, 58 | syl6eleq 2494 |
. . . . . . . . . . 11
 

      |
60 | | simpl 444 |
. . . . . . . . . . . 12
 

  |
61 | | elfznn 11036 |
. . . . . . . . . . . 12
       |
62 | 30 | ovolfsf 19321 |
. . . . . . . . . . . . . . 15
         
          |
63 | 29, 62 | syl 16 |
. . . . . . . . . . . . . 14
  
          |
64 | 63 | ffvelrnda 5829 |
. . . . . . . . . . . . 13
 

  
         |
65 | 38, 64 | sseldi 3306 |
. . . . . . . . . . . 12
 

  
      |
66 | 60, 61, 65 | syl2an 464 |
. . . . . . . . . . 11
           
      |
67 | 51 | ovolfsf 19321 |
. . . . . . . . . . . . . . . 16
         
          |
68 | 18, 67 | syl 16 |
. . . . . . . . . . . . . . 15
  
          |
69 | 68 | ffvelrnda 5829 |
. . . . . . . . . . . . . 14
 

  
         |
70 | | elrege0 10963 |
. . . . . . . . . . . . . 14
   
                         |
71 | 69, 70 | sylib 189 |
. . . . . . . . . . . . 13
 

   
      
       |
72 | 71 | simpld 446 |
. . . . . . . . . . . 12
 

  
      |
73 | 60, 61, 72 | syl2an 464 |
. . . . . . . . . . 11
           
      |
74 | 28 | simprd 450 |
. . . . . . . . . . . . . . . . . 18
          |
75 | | eqid 2404 |
. . . . . . . . . . . . . . . . . . 19
    
  |
76 | 75 | ovolfsf 19321 |
. . . . . . . . . . . . . . . . . 18
         
          |
77 | 74, 76 | syl 16 |
. . . . . . . . . . . . . . . . 17
  
          |
78 | 77 | ffvelrnda 5829 |
. . . . . . . . . . . . . . . 16
 

  
         |
79 | | elrege0 10963 |
. . . . . . . . . . . . . . . 16
   
                         |
80 | 78, 79 | sylib 189 |
. . . . . . . . . . . . . . 15
 

   
      
       |
81 | 80 | simprd 450 |
. . . . . . . . . . . . . 14
 

  
      |
82 | 80 | simpld 446 |
. . . . . . . . . . . . . . 15
 

  
      |
83 | 65, 82 | addge01d 9570 |
. . . . . . . . . . . . . 14
 

              
   
               |
84 | 81, 83 | mpbid 202 |
. . . . . . . . . . . . 13
 

  
       
      
       |
85 | 12, 13, 3, 4, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24 | ioombl1lem3 19407 |
. . . . . . . . . . . . 13
 

   
              
      |
86 | 84, 85 | breqtrd 4196 |
. . . . . . . . . . . 12
 

  
      
      |
87 | 60, 61, 86 | syl2an 464 |
. . . . . . . . . . 11
           
      
      |
88 | 59, 66, 73, 87 | serle 11333 |
. . . . . . . . . 10
 

  
    
  
       |
89 | 16 | fveq1i 5688 |
. . . . . . . . . 10
             |
90 | 15 | fveq1i 5688 |
. . . . . . . . . 10
             |
91 | 88, 89, 90 | 3brtr4g 4204 |
. . . . . . . . 9
 

          |
92 | | 1z 10267 |
. . . . . . . . . . . . . . . 16
 |
93 | 92 | a1i 11 |
. . . . . . . . . . . . . . 15
   |
94 | | eqidd 2405 |
. . . . . . . . . . . . . . 15
 

  
      
      |
95 | 71 | simprd 450 |
. . . . . . . . . . . . . . 15
 

  
      |
96 | | frn 5556 |
. . . . . . . . . . . . . . . . . . . . 21
             |
97 | 53, 96 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
  
   |
98 | | icossxr 10951 |
. . . . . . . . . . . . . . . . . . . 20
    |
99 | 97, 98 | syl6ss 3320 |
. . . . . . . . . . . . . . . . . . 19
   |
100 | 99 | adantr 452 |
. . . . . . . . . . . . . . . . . 18
 

  |
101 | | ffn 5550 |
. . . . . . . . . . . . . . . . . . . 20
          |
102 | 53, 101 | syl 16 |
. . . . . . . . . . . . . . . . . . 19
   |
103 | | fnfvelrn 5826 |
. . . . . . . . . . . . . . . . . . 19
 
       |
104 | 102, 103 | sylan 458 |
. . . . . . . . . . . . . . . . . 18
 

      |
105 | | supxrub 10859 |
. . . . . . . . . . . . . . . . . 18
          
      |
106 | 100, 104,
105 | syl2anc 643 |
. . . . . . . . . . . . . . . . 17
 

          |
107 | 106 | ralrimiva 2749 |
. . . . . . . . . . . . . . . 16
            |
108 | | breq2 4176 |
. . . . . . . . . . . . . . . . . 18
             
       |
109 | 108 | ralbidv 2686 |
. . . . . . . . . . . . . . . . 17
                       |
110 | 109 | rspcev 3012 |
. . . . . . . . . . . . . . . 16
                
       |
111 | 25, 107, 110 | syl2anc 643 |
. . . . . . . . . . . . . . 15
         |
112 | 58, 15, 93, 94, 72, 95, 111 | isumsup2 12581 |
. . . . . . . . . . . . . 14
       |
113 | 97, 38 | syl6ss 3320 |
. . . . . . . . . . . . . . 15
   |
114 | | fdm 5554 |
. . . . . . . . . . . . . . . . . . 19
          |
115 | 53, 114 | syl 16 |
. . . . . . . . . . . . . . . . . 18
   |
116 | 40, 115 | syl5eleqr 2491 |
. . . . . . . . . . . . . . . . 17
   |
117 | | ne0i 3594 |
. . . . . . . . . . . . . . . . 17
   |
118 | 116, 117 | syl 16 |
. . . . . . . . . . . . . . . 16
   |
119 | | dm0rn0 5045 |
. . . . . . . . . . . . . . . . 17

  |
120 | 119 | necon3bii 2599 |
. . . . . . . . . . . . . . . 16

  |
121 | 118, 120 | sylib 189 |
. . . . . . . . . . . . . . 15
   |
122 | | breq1 4175 |
. . . . . . . . . . . . . . . . . . 19
     
       |
123 | 122 | ralrn 5832 |
. . . . . . . . . . . . . . . . . 18
  
        |
124 | 102, 123 | syl 16 |
. . . . . . . . . . . . . . . . 17
  

       |
125 | 124 | rexbidv 2687 |
. . . . . . . . . . . . . . . 16
   

        |
126 | 111, 125 | mpbird 224 |
. . . . . . . . . . . . . . 15
     |
127 | | supxrre 10862 |
. . . . . . . . . . . . . . 15
 

            |
128 | 113, 121,
126, 127 | syl3anc 1184 |
. . . . . . . . . . . . . 14
           |
129 | 112, 128 | breqtrrd 4198 |
. . . . . . . . . . . . 13
       |
130 | 129 | adantr 452 |
. . . . . . . . . . . 12
 

      |
131 | 15, 130 | syl5eqbrr 4206 |
. . . . . . . . . . 11
 

  
        |
132 | 72 | adantlr 696 |
. . . . . . . . . . 11
       
      |
133 | 95 | adantlr 696 |
. . . . . . . . . . 11
       
      |
134 | 58, 57, 131, 132, 133 | climserle 12411 |
. . . . . . . . . 10
 

  
    
      |
135 | 90, 134 | syl5eqbr 4205 |
. . . . . . . . 9
 

          |
136 | 50, 55, 56, 91, 135 | letrd 9183 |
. . . . . . . 8
 

          |
137 | 136 | ralrimiva 2749 |
. . . . . . 7
            |
138 | | breq2 4176 |
. . . . . . . . 9
             
       |
139 | 138 | ralbidv 2686 |
. . . . . . . 8
                       |
140 | 139 | rspcev 3012 |
. . . . . . 7
                
       |
141 | 25, 137, 140 | syl2anc 643 |
. . . . . 6
         |
142 | | ffn 5550 |
. . . . . . . . 9
          |
143 | 32, 142 | syl 16 |
. . . . . . . 8
   |
144 | | breq1 4175 |
. . . . . . . . 9
     
       |
145 | 144 | ralrn 5832 |
. . . . . . . 8
  
        |
146 | 143, 145 | syl 16 |
. . . . . . 7
  

       |
147 | 146 | rexbidv 2687 |
. . . . . 6
   

        |
148 | 141, 147 | mpbird 224 |
. . . . 5
     |
149 | | suprcl 9924 |
. . . . 5
 

        |
150 | 39, 48, 148, 149 | syl3anc 1184 |
. . . 4
       |
151 | 75, 17 | ovolsf 19322 |
. . . . . . . 8
                 |
152 | 74, 151 | syl 16 |
. . . . . . 7
          |
153 | | frn 5556 |
. . . . . . 7
             |
154 | 152, 153 | syl 16 |
. . . . . 6
  
   |
155 | 154, 38 | syl6ss 3320 |
. . . . 5
   |
156 | | fdm 5554 |
. . . . . . . . 9
          |
157 | 152, 156 | syl 16 |
. . . . . . . 8
   |
158 | 40, 157 | syl5eleqr 2491 |
. . . . . . 7
   |
159 | | ne0i 3594 |
. . . . . . 7
   |
160 | 158, 159 | syl 16 |
. . . . . 6
   |
161 | | dm0rn0 5045 |
. . . . . . 7

  |
162 | 161 | necon3bii 2599 |
. . . . . 6

  |
163 | 160, 162 | sylib 189 |
. . . . 5
   |
164 | 152 | ffvelrnda 5829 |
. . . . . . . . . 10
 

         |
165 | 38, 164 | sseldi 3306 |
. . . . . . . . 9
 

      |
166 | 60, 61, 82 | syl2an 464 |
. . . . . . . . . . 11
           
      |
167 | | elrege0 10963 |
. . . . . . . . . . . . . . . 16
   
                         |
168 | 64, 167 | sylib 189 |
. . . . . . . . . . . . . . 15
 

   
      
       |
169 | 168 | simprd 450 |
. . . . . . . . . . . . . 14
 

  
      |
170 | 82, 65 | addge02d 9571 |
. . . . . . . . . . . . . 14
 

              
   
               |
171 | 169, 170 | mpbid 202 |
. . . . . . . . . . . . 13
 

  
       
      
       |
172 | 171, 85 | breqtrd 4196 |
. . . . . . . . . . . 12
 

  
      
      |
173 | 60, 61, 172 | syl2an 464 |
. . . . . . . . . . 11
           
      
      |
174 | 59, 166, 73, 173 | serle 11333 |
. . . . . . . . . 10
 

  
    
  
       |
175 | 17 | fveq1i 5688 |
. . . . . . . . . 10
             |
176 | 174, 175,
90 | 3brtr4g 4204 |
. . . . . . . . 9
 

          |
177 | 165, 55, 56, 176, 135 | letrd 9183 |
. . . . . . . 8
 

          |
178 | 177 | ralrimiva 2749 |
. . . . . . 7
            |
179 | | breq2 4176 |
. . . . . . . . 9
             
       |
180 | 179 | ralbidv 2686 |
. . . . . . . 8
                       |
181 | 180 | rspcev 3012 |
. . . . . . 7
                
       |
182 | 25, 178, 181 | syl2anc 643 |
. . . . . 6
         |
183 | | ffn 5550 |
. . . . . . . . 9
          |
184 | 152, 183 | syl 16 |
. . . . . . . 8
   |
185 | | breq1 4175 |
. . . . . . . . 9
     
       |
186 | 185 | ralrn 5832 |
. . . . . . . 8
  
        |
187 | 184, 186 | syl 16 |
. . . . . . 7
  

       |
188 | 187 | rexbidv 2687 |
. . . . . 6
   

        |
189 | 182, 188 | mpbird 224 |
. . . . 5
     |
190 | | suprcl 9924 |
. . . . 5
 

        |
191 | 155, 163,
189, 190 | syl3anc 1184 |
. . . 4
       |
192 | | ssralv 3367 |
. . . . . . . . . 10
    

        
                      
            |
193 | 1, 192 | ax-mp 8 |
. . . . . . . . 9
 

        
                      
           |
194 | 21 | breq1i 4179 |
. . . . . . . . . . . . 13

          |
195 | | ovolfcl 19316 |
. . . . . . . . . . . . . . . . . . 19
                                              |
196 | 18, 195 | sylan 458 |
. . . . . . . . . . . . . . . . . 18
 

                                    |
197 | 196 | simp1d 969 |
. . . . . . . . . . . . . . . . 17
 

          |
198 | 21, 197 | syl5eqel 2488 |
. . . . . . . . . . . . . . . 16
 

  |
199 | 198 | adantlr 696 |
. . . . . . . . . . . . . . 15
         |
200 | 1, 3 | syl5ss 3319 |
. . . . . . . . . . . . . . . . 17
  
  |
201 | 200 | sselda 3308 |
. . . . . . . . . . . . . . . 16
 

 
  |
202 | 201 | adantr 452 |
. . . . . . . . . . . . . . 15
         |
203 | | ltle 9119 |
. . . . . . . . . . . . . . 15
 
 
   |
204 | 199, 202,
203 | syl2anc 643 |
. . . . . . . . . . . . . 14
           |
205 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
206 | | opex 4387 |
. . . . . . . . . . . . . . . . . . . 20
     
     
       |
207 | 23 | fvmpt2 5771 |
. . . . . . . . . . . . . . . . . . . 20
             
                     
 
       |
208 | 205, 206,
207 | sylancl 644 |
. . . . . . . . . . . . . . . . . . 19
 

        
 
   
 
       |
209 | 208 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . 18
 

                
     
         |
210 | 13 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . 21
 

  |
211 | | ifcl 3735 |
. . . . . . . . . . . . . . . . . . . . 21
 
   
    |
212 | 210, 198,
211 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . . 20
 

 
 
   |
213 | 196 | simp2d 970 |
. . . . . . . . . . . . . . . . . . . . 21
 

          |
214 | 22, 213 | syl5eqel 2488 |
. . . . . . . . . . . . . . . . . . . 20
 

  |
215 | | ifcl 3735 |
. . . . . . . . . . . . . . . . . . . 20
    
            
 
     |
216 | 212, 214,
215 | syl2anc 643 |
. . . . . . . . . . . . . . . . . . 19
 

    
     
      |
217 | | op1stg 6318 |
. . . . . . . . . . . . . . . . . . 19
     
 
   
 
                  
                
 
     |
218 | 216, 214,
217 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
 

             
 
          
     
      |
219 | 209, 218 | eqtrd 2436 |
. . . . . . . . . . . . . . . . 17
 

                  
      |
220 | 219 | ad2ant2r 728 |
. . . . . . . . . . . . . . . 16
                     
     
      |
221 | 216 | ad2ant2r 728 |
. . . . . . . . . . . . . . . . 17
                  
 
     |
222 | 212 | ad2ant2r 728 |
. . . . . . . . . . . . . . . . 17
                |
223 | 200 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . 18
          
  |
224 | | simplr 732 |
. . . . . . . . . . . . . . . . . 18
             |
225 | 223, 224 | sseldd 3309 |
. . . . . . . . . . . . . . . . 17
           |
226 | 214 | ad2ant2r 728 |
. . . . . . . . . . . . . . . . . 18
           |
227 | | min1 10732 |
. . . . . . . . . . . . . . . . . 18
    
            
 
    
 
   |
228 | 222, 226,
227 | syl2anc 643 |
. . . . . . . . . . . . . . . . 17
                  
 
    
 
   |
229 | 13 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . 19
           |
230 | | inss2 3522 |
. . . . . . . . . . . . . . . . . . . . . 22
   |
231 | 230 | sseli 3304 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
232 | 231 | ad2antlr 708 |
. . . . . . . . . . . . . . . . . . . 20
           |
233 | 13 | rexrd 9090 |
. . . . . . . . . . . . . . . . . . . . . . . 24
   |
234 | | elioo2 10913 |
. . . . . . . . . . . . . . . . . . . . . . . 24
      

    |
235 | 233, 36, 234 | sylancl 644 |
. . . . . . . . . . . . . . . . . . . . . . 23
          |
236 | 12 | eleq2i 2468 |
. . . . . . . . . . . . . . . . . . . . . . 23

     |
237 | | ltpnf 10677 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
   |
238 | 237 | adantr 452 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
     |
239 | 238 | pm4.71i 614 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
      |
240 | | df-3an 938 |
. . . . . . . . . . . . . . . . . . . . . . . 24
  
      |
241 | 239, 240 | bitr4i 244 |
. . . . . . . . . . . . . . . . . . . . . . 23
  

   |
242 | 235, 236,
241 | 3bitr4g 280 |
. . . . . . . . . . . . . . . . . . . . . 22
       |
243 | | simpr 448 |
. . . . . . . . . . . . . . . . . . . . . 22
     |
244 | 242, 243 | syl6bi 220 |
. . . . . . . . . . . . . . . . . . . . 21
     |
245 | 244 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . 20
         
   |
246 | 232, 245 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
           |
247 | 229, 225,
246 | ltled 9177 |
. . . . . . . . . . . . . . . . . 18
           |
248 | | simprr 734 |
. . . . . . . . . . . . . . . . . 18
           |
249 | | breq1 4175 |
. . . . . . . . . . . . . . . . . . 19
      
        |
250 | | breq1 4175 |
. . . . . . . . . . . . . . . . . . 19
      
        |
251 | 249, 250 | ifboth 3730 |
. . . . . . . . . . . . . . . . . 18
 
        |
252 | 247, 248,
251 | syl2anc 643 |
. . . . . . . . . . . . . . . . 17
                |
253 | 221, 222,
225, 228, 252 | letrd 9183 |
. . . . . . . . . . . . . . . 16
                  
 
     |
254 | 220, 253 | eqbrtrd 4192 |
. . . . . . . . . . . . . . 15
                
  |
255 | 254 | expr 599 |
. . . . . . . . . . . . . 14
                   |
256 | 204, 255 | syld 42 |
. . . . . . . . . . . . 13
                   |
257 | 194, 256 | syl5bir 210 |
. . . . . . . . . . . 12
               
           |
258 | 22 | breq2i 4180 |
. . . . . . . . . . . . . 14

          |
259 | 214 | adantlr 696 |
. . . . . . . . . . . . . . 15
         |
260 | | ltle 9119 |
. . . . . . . . . . . . . . 15
 
 
   |
261 | 202, 259,
260 | syl2anc 643 |
. . . . . . . . . . . . . 14
       
   |
262 | 258, 261 | syl5bir 210 |
. . . . . . . . . . . . 13
       
           |
263 | 208 | fveq2d 5691 |
. . . . . . . . . . . . . . . 16
 

                
     
         |
264 | | op2ndg 6319 |
. . . . . . . . . . . . . . . . 17
     
 
   
 
                  
         |
265 | 216, 214,
264 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
 

             
 
        |
266 | 263, 265 | eqtrd 2436 |
. . . . . . . . . . . . . . 15
 

          |
267 | 266 | adantlr 696 |
. . . . . . . . . . . . . 14
                 |
268 | 267 | breq2d 4184 |
. . . . . . . . . . . . 13
       
       
   |
269 | 262, 268 | sylibrd 226 |
. . . . . . . . . . . 12
       
                   |
270 | 257, 269 | anim12d 547 |
. . . . . . . . . . 11
                
                 
            |
271 | 270 | reximdva 2778 |
. . . . . . . . . 10
 

 
 
        
                  
            |
272 | 271 | ralimdva 2744 |
. . . . . . . . 9
               
         
            
            |
273 | 193, 272 | syl5 30 |
. . . . . . . 8
            
         
            
            |
274 | | ovolfioo 19317 |
. . . . . . . . 9
 
    
       

        
            |
275 | 3, 18, 274 | syl2anc 643 |
. . . . . . . 8
     

        
            |
276 | | ovolficc 19318 |
. . . . . . . . 9
   
    
     
  
             
            |
277 | 200, 29, 276 | syl2anc 643 |
. . . . . . . 8
   
  
             
            |
278 | 273, 275,
277 | 3imtr4d 260 |
. . . . . . 7
      
      |
279 | 19, 278 | mpd 15 |
. . . . . 6
  
     |
280 | 16 | ovollb2 19338 |
. . . . . 6
                   
 
      |
281 | 29, 279, 280 | syl2anc 643 |
. . . . 5
     
 
      |
282 | | supxrre 10862 |
. . . . . 6
 

            |
283 | 39, 48, 148, 282 | syl3anc 1184 |
. . . . 5
           |
284 | 281, 283 | breqtrd 4196 |
. . . 4
     
 
      |
285 | | ssralv 3367 |
. . . . . . . . . 10
    

        
                      
            |
286 | 7, 285 | ax-mp 8 |
. . . . . . . . 9
 

        
                      
           |
287 | 198 | adantlr 696 |
. . . . . . . . . . . . . . 15
         |
288 | 7, 3 | syl5ss 3319 |
. . . . . . . . . . . . . . . . 17
  
  |
289 | 288 | sselda 3308 |
. . . . . . . . . . . . . . . 16
 

 
  |
290 | 289 | adantr 452 |
. . . . . . . . . . . . . . 15
         |
291 | 287, 290,
203 | syl2anc 643 |
. . . . . . . . . . . . . 14
           |
292 | 194, 291 | syl5bir 210 |
. . . . . . . . . . . . 13
               
   |
293 | | opex 4387 |
. . . . . . . . . . . . . . . . . 18
            
      |
294 | 24 | fvmpt2 5771 |
. . . . . . . . . . . . . . . . . 18
   
         
 
                    
 
      |
295 | 205, 293,
294 | sylancl 644 |
. . . . . . . . . . . . . . . . 17
 

          
     
       |
296 | 295 | fveq2d 5691 |
. . . . . . . . . . . . . . . 16
 

                       
        |
297 | | op1stg 6318 |
. . . . . . . . . . . . . . . . 17
            
                   
 
       |
298 | 198, 216,
297 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
 

         
     
        |
299 | 296, 298 | eqtrd 2436 |
. . . . . . . . . . . . . . 15
 

          |
300 | 299 | adantlr 696 |
. . . . . . . . . . . . . 14
                 |
301 | 300 | breq1d 4182 |
. . . . . . . . . . . . 13
               
   |
302 | 292, 301 | sylibrd 226 |
. . . . . . . . . . . 12
               
           |
303 | 214 | adantlr 696 |
. . . . . . . . . . . . . . 15
         |
304 | 290, 303,
260 | syl2anc 643 |
. . . . . . . . . . . . . 14
       
   |
305 | 288 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . 19
             |
306 | | simplr 732 |
. . . . . . . . . . . . . . . . . . 19
             |
307 | 305, 306 | sseldd 3309 |
. . . . . . . . . . . . . . . . . 18
           |
308 | 13 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . 18
           |
309 | 198 | ad2ant2r 728 |
. . . . . . . . . . . . . . . . . . 19
           |
310 | 308, 309,
211 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
                |
311 | | eldifn 3430 |
. . . . . . . . . . . . . . . . . . . . 21
  
  |
312 | 311 | ad2antlr 708 |
. . . . . . . . . . . . . . . . . . . 20
        
  |
313 | 307 | biantrurd 495 |
. . . . . . . . . . . . . . . . . . . . 21
               |
314 | 242 | ad2antrr 707 |
. . . . . . . . . . . . . . . . . . . . 21
               |
315 | 313, 314 | bitr4d 248 |
. . . . . . . . . . . . . . . . . . . 20
         
   |
316 | 312, 315 | mtbird 293 |
. . . . . . . . . . . . . . . . . . 19
        
  |
317 | 307, 308 | lenltd 9175 |
. . . . . . . . . . . . . . . . . . 19
             |
318 | 316, 317 | mpbird 224 |
. . . . . . . . . . . . . . . . . 18
           |
319 | | max2 10731 |
. . . . . . . . . . . . . . . . . . 19
 

       |
320 | 309, 308,
319 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
          
 
   |
321 | 307, 308,
310, 318, 320 | letrd 9183 |
. . . . . . . . . . . . . . . . 17
          
 
   |
322 | | simprr 734 |
. . . . . . . . . . . . . . . . 17
           |
323 | | breq2 4176 |
. . . . . . . . . . . . . . . . . 18
               
 
   
    
          
       |
324 | | breq2 4176 |
. . . . . . . . . . . . . . . . . 18
          
 
   
          
       |
325 | 323, 324 | ifboth 3730 |
. . . . . . . . . . . . . . . . 17
 
         
 
   
 
     |
326 | 321, 322,
325 | syl2anc 643 |
. . . . . . . . . . . . . . . 16
             
     
      |
327 | 295 | fveq2d 5691 |
. . . . . . . . . . . . . . . . . 18
 

                       
        |
328 | | op2ndg 6319 |
. . . . . . . . . . . . . . . . . . 19
            
                   
 
        
 
   
 
     |
329 | 198, 216,
328 | syl2anc 643 |
. . . . . . . . . . . . . . . . . 18
 

         
     
                
      |
330 | 327, 329 | eqtrd 2436 |
. . . . . . . . . . . . . . . . 17
 

                  
      |
331 | 330 | ad2ant2r 728 |
. . . . . . . . . . . . . . . 16
                     
     
      |
332 | 326, 331 | breqtrrd 4198 |
. . . . . . . . . . . . . . 15
                   |
333 | 332 | expr 599 |
. . . . . . . . . . . . . 14
       
           |
334 | 304, 333 | syld 42 |
. . . . . . . . . . . . 13
       
           |
335 | 258, 334 | syl5bir 210 |
. . . . . . . . . . . 12
       
                   |
336 | 302, 335 | anim12d 547 |
. . . . . . . . . . 11
                
                 
            |
337 | 336 | reximdva 2778 |
. . . . . . . . . 10
 

 
 
        
                  
            |
338 | 337 | ralimdva 2744 |
. . . . . . . . 9
               
         
            
            |
339 | 286, 338 | syl5 30 |
. . . . . . . 8
            
         
            
            |
340 | | ovolficc 19318 |
. . . . . . . . 9
   
    
         
            
            |
341 | 288, 74, 340 | syl2anc 643 |
. . . . . . . 8
       
            
            |
342 | 339, 275,
341 | 3imtr4d 260 |
. . . . . . 7
             |
343 | 19, 342 | mpd 15 |
. . . . . 6
  
     |
344 | 17 | ovollb2 19338 |
. . . . . 6
                   
 
      |
345 | 74, 343, 344 | syl2anc 643 |
. . . . 5
     
 
      |
346 | | supxrre 10862 |
. . . . . 6
 

            |
347 | 155, 163,
189, 346 | syl3anc 1184 |
. . . . 5
           |
348 | 345, 347 | breqtrd 4196 |
. . . 4
     
 
      |
349 | 6, 10, 150, 191, 284, 348 | le2addd 9600 |
. . 3
                
            |
350 | | eqidd 2405 |
. . . . . 6
 

  
      
      |
351 | 58, 16, 93, 350, 65, 169, 141 | isumsup2 12581 |
. . . . 5
       |
352 | | seqex 11280 |
. . . . . . 7
  
   |
353 | 15, 352 | eqeltri 2474 |
. . . . . 6
 |
354 | 353 | a1i 11 |
. . . . 5
   |
355 | | eqidd 2405 |
. . . . . 6
 

  
      
      |
356 | 58, 17, 93, 355, 82, 81, 182 | isumsup2 12581 |
. . . . 5
       |
357 | 50 | recnd 9070 |
. . . . 5
 

      |
358 | 165 | recnd 9070 |
. . . . 5
 

      |
359 | 65 | recnd 9070 |
. . . . . . . 8
 

  
      |
360 | 60, 61, 359 | syl2an 464 |
. . . . . . 7
           
      |
361 | 82 | recnd 9070 |
. . . . . . . 8
 

  
      |
362 | 60, 61, 361 | syl2an 464 |
. . . . . . 7
           
      |
363 | 85 | eqcomd 2409 |
. . . . . . . 8
 

  
       
      
       |
364 | 60, 61, 363 | syl2an 464 |
. . . . . . 7
           
       
      
       |
365 | 59, 360, 362, 364 | seradd 11320 |
. . . . . 6
 

  
        
       
        |
366 | 89, 175 | oveq12i 6052 |
. . . . . 6
             
    
  
       |
367 | 365, 90, 366 | 3eqtr4g 2461 |
. . . . 5
 

                |
368 | 58, 93, 351, 354, 356, 357, 358, 367 | climadd 12380 |
. . . 4
             |
369 | | climuni 12301 |
. . . 4
                                 |
370 | 368, 129,
369 | syl2anc 643 |
. . 3
                 |
371 | 349, 370 | breqtrd 4196 |
. 2
                
      |
372 | 11, 25, 27, 371, 20 | letrd 9183 |
1
                
         |