Proof of Theorem uniioombllem4
Step | Hyp | Ref
| Expression |
1 | | inss1 3529 |
. . . 4
   |
2 | 1 | a1i 11 |
. . 3
  
  |
3 | | uniioombl.k |
. . . . . 6
            |
4 | | imassrn 5183 |
. . . . . . 7
             |
5 | 4 | unissi 4006 |
. . . . . 6
  
            |
6 | 3, 5 | eqsstri 3346 |
. . . . 5
    |
7 | 6 | a1i 11 |
. . . 4

     |
8 | | uniioombl.g |
. . . . . . 7
          |
9 | 8 | uniiccdif 19431 |
. . . . . 6
               
        |
10 | 9 | simpld 446 |
. . . . 5
         |
11 | | ovolficcss 19327 |
. . . . . 6
             |
12 | 8, 11 | syl 16 |
. . . . 5
      |
13 | 10, 12 | sstrd 3326 |
. . . 4
      |
14 | 7, 13 | sstrd 3326 |
. . 3

  |
15 | | uniioombl.1 |
. . . . . 6
          |
16 | | uniioombl.2 |
. . . . . 6
 Disj
           |
17 | | uniioombl.3 |
. . . . . 6
  
   |
18 | | uniioombl.a |
. . . . . 6

   |
19 | | uniioombl.e |
. . . . . 6
        |
20 | | uniioombl.c |
. . . . . 6
   |
21 | | uniioombl.s |
. . . . . 6

     |
22 | | uniioombl.t |
. . . . . 6
  
   |
23 | | uniioombl.v |
. . . . . 6
              |
24 | 15, 16, 17, 18, 19, 20, 8, 21, 22, 23 | uniioombllem1 19434 |
. . . . 5
       |
25 | | ssid 3335 |
. . . . . 6
       |
26 | 22 | ovollb 19336 |
. . . . . 6
           
                  |
27 | 8, 25, 26 | sylancl 644 |
. . . . 5
               |
28 | | ovollecl 19340 |
. . . . 5
                
    
          |
29 | 13, 24, 27, 28 | syl3anc 1184 |
. . . 4
           |
30 | | ovolsscl 19343 |
. . . 4
 
                      |
31 | 7, 13, 29, 30 | syl3anc 1184 |
. . 3
        |
32 | | ovolsscl 19343 |
. . 3
   
          
    |
33 | 2, 14, 31, 32 | syl3anc 1184 |
. 2
     
    |
34 | | inss1 3529 |
. . . . 5
   |
35 | 34 | a1i 11 |
. . . 4
  
  |
36 | | ovolsscl 19343 |
. . . 4
   
          
    |
37 | 35, 14, 31, 36 | syl3anc 1184 |
. . 3
     
    |
38 | | ssun2 3479 |
. . . . . 6
                      
                                  
           |
39 | | nnuz 10485 |
. . . . . . . . . . . . . 14
     |
40 | | uniioombl.n |
. . . . . . . . . . . . . . . . 17
   |
41 | 40 | peano2nnd 9981 |
. . . . . . . . . . . . . . . 16
     |
42 | 41, 39 | syl6eleq 2502 |
. . . . . . . . . . . . . . 15
         |
43 | | uzsplit 11081 |
. . . . . . . . . . . . . . 15
      
                
     |
44 | 42, 43 | syl 16 |
. . . . . . . . . . . . . 14
                       |
45 | 39, 44 | syl5eq 2456 |
. . . . . . . . . . . . 13
             
     |
46 | 40 | nncnd 9980 |
. . . . . . . . . . . . . . . 16
   |
47 | | ax-1cn 9012 |
. . . . . . . . . . . . . . . 16
 |
48 | | pncan 9275 |
. . . . . . . . . . . . . . . 16
 
       |
49 | 46, 47, 48 | sylancl 644 |
. . . . . . . . . . . . . . 15
       |
50 | 49 | oveq2d 6064 |
. . . . . . . . . . . . . 14
               |
51 | 50 | uneq1d 3468 |
. . . . . . . . . . . . 13
                               |
52 | 45, 51 | eqtrd 2444 |
. . . . . . . . . . . 12
         
     |
53 | 52 | iuneq1d 4084 |
. . . . . . . . . . 11
                                  |
54 | | iunxun 4140 |
. . . . . . . . . . 11
                       
                               |
55 | 53, 54 | syl6eq 2460 |
. . . . . . . . . 10
                                            |
56 | | ioof 10966 |
. . . . . . . . . . . . . 14
  
     |
57 | | inss2 3530 |
. . . . . . . . . . . . . . . 16
      |
58 | | ressxr 9093 |
. . . . . . . . . . . . . . . . 17
 |
59 | | xpss12 4948 |
. . . . . . . . . . . . . . . . 17
 
       |
60 | 58, 58, 59 | mp2an 654 |
. . . . . . . . . . . . . . . 16
     |
61 | 57, 60 | sstri 3325 |
. . . . . . . . . . . . . . 15
      |
62 | | fss 5566 |
. . . . . . . . . . . . . . 15
                       |
63 | 15, 61, 62 | sylancl 644 |
. . . . . . . . . . . . . 14
         |
64 | | fco 5567 |
. . . . . . . . . . . . . 14
                
        |
65 | 56, 63, 64 | sylancr 645 |
. . . . . . . . . . . . 13
          |
66 | | ffn 5558 |
. . . . . . . . . . . . 13
            |
67 | | fniunfv 5961 |
. . . . . . . . . . . . 13
               |
68 | 65, 66, 67 | 3syl 19 |
. . . . . . . . . . . 12
             |
69 | | fvco3 5767 |
. . . . . . . . . . . . . 14
           
              |
70 | 15, 69 | sylan 458 |
. . . . . . . . . . . . 13
 

                |
71 | 70 | iuneq2dv 4082 |
. . . . . . . . . . . 12
                   |
72 | 68, 71 | eqtr3d 2446 |
. . . . . . . . . . 11
               |
73 | 18, 72 | syl5eq 2456 |
. . . . . . . . . 10
            |
74 | | uniioombl.l |
. . . . . . . . . . . 12
            |
75 | | ffun 5560 |
. . . . . . . . . . . . . 14
            |
76 | | funiunfv 5962 |
. . . . . . . . . . . . . 14
  
                         |
77 | 65, 75, 76 | 3syl 19 |
. . . . . . . . . . . . 13
               
          |
78 | | elfznn 11044 |
. . . . . . . . . . . . . . 15
       |
79 | 15, 78, 69 | syl2an 464 |
. . . . . . . . . . . . . 14
 
      
              |
80 | 79 | iuneq2dv 4082 |
. . . . . . . . . . . . 13
                             |
81 | 77, 80 | eqtr3d 2446 |
. . . . . . . . . . . 12
            
               |
82 | 74, 81 | syl5eq 2456 |
. . . . . . . . . . 11
                 |
83 | 82 | uneq1d 3468 |
. . . . . . . . . 10
  
   
                                              |
84 | 55, 73, 83 | 3eqtr4d 2454 |
. . . . . . . . 9
                     |
85 | 84 | ineq2d 3510 |
. . . . . . . 8
         
               |
86 | | indi 3555 |
. . . . . . . 8
      
                 
   
              |
87 | 85, 86 | syl6eq 2460 |
. . . . . . 7
           
               |
88 | | fss 5566 |
. . . . . . . . . . . . . . 15
                       |
89 | 8, 61, 88 | sylancl 644 |
. . . . . . . . . . . . . 14
         |
90 | | fco 5567 |
. . . . . . . . . . . . . 14
                
        |
91 | 56, 89, 90 | sylancr 645 |
. . . . . . . . . . . . 13
          |
92 | | ffun 5560 |
. . . . . . . . . . . . 13
            |
93 | | funiunfv 5962 |
. . . . . . . . . . . . 13
  
                         |
94 | 91, 92, 93 | 3syl 19 |
. . . . . . . . . . . 12
               
          |
95 | | elfznn 11044 |
. . . . . . . . . . . . . 14
       |
96 | | fvco3 5767 |
. . . . . . . . . . . . . 14
           
              |
97 | 8, 95, 96 | syl2an 464 |
. . . . . . . . . . . . 13
 
      
              |
98 | 97 | iuneq2dv 4082 |
. . . . . . . . . . . 12
                             |
99 | 94, 98 | eqtr3d 2446 |
. . . . . . . . . . 11
            
               |
100 | 3, 99 | syl5eq 2456 |
. . . . . . . . . 10
                 |
101 | 100 | ineq2d 3510 |
. . . . . . . . 9
                 
                 
                 |
102 | | incom 3501 |
. . . . . . . . 9
                   
   
             |
103 | | iunin2 4123 |
. . . . . . . . . . . . 13
                
                 
                  |
104 | | incom 3501 |
. . . . . . . . . . . . . . 15
                          
          |
105 | 104 | a1i 11 |
. . . . . . . . . . . . . 14
    
 
                          
           |
106 | 105 | iuneq2i 4079 |
. . . . . . . . . . . . 13
                
                         
          |
107 | | incom 3501 |
. . . . . . . . . . . . 13
 
   
                             
   
             |
108 | 103, 106,
107 | 3eqtr4ri 2443 |
. . . . . . . . . . . 12
 
   
                                    
          |
109 | 108 | a1i 11 |
. . . . . . . . . . 11
      
                        
   
                       |
110 | 109 | iuneq2i 4079 |
. . . . . . . . . 10
                      
                               
          |
111 | | iunin2 4123 |
. . . . . . . . . 10
                      
                         
                |
112 | 110, 111 | eqtr3i 2434 |
. . . . . . . . 9
                      
                         
                |
113 | 101, 102,
112 | 3eqtr4g 2469 |
. . . . . . . 8
  
   
                                  
           |
114 | 113 | uneq2d 3469 |
. . . . . . 7
                                                
            |
115 | 87, 114 | eqtrd 2444 |
. . . . . 6
                            
            |
116 | 38, 115 | syl5sseqr 3365 |
. . . . 5
                       
         
   |
117 | 116, 1 | syl6ss 3328 |
. . . 4
                       
           |
118 | | ovolsscl 19343 |
. . . 4
                        
                                         
            |
119 | 117, 14, 31, 118 | syl3anc 1184 |
. . 3
           
   
                        |
120 | 37, 119 | readdcld 9079 |
. 2
                                   
             |
121 | 20 | rpred 10612 |
. . 3
   |
122 | 37, 121 | readdcld 9079 |
. 2
            |
123 | 115 | fveq2d 5699 |
. . 3
     
                               
             |
124 | 35, 14 | sstrd 3326 |
. . . 4
  
  |
125 | 117, 14 | sstrd 3326 |
. . . 4
                       
           |
126 | | ovolun 19356 |
. . . 4
    
                               
                                   
                                         
          
                                  
             |
127 | 124, 37, 125, 119, 126 | syl22anc 1185 |
. . 3
                              
          
                                  
             |
128 | 123, 127 | eqbrtrd 4200 |
. 2
     
 
                                  
             |
129 | | fzfid 11275 |
. . . . 5
       |
130 | | iunss 4100 |
. . . . . . . 8
 
     
   
                           
   
                       |
131 | 117, 130 | sylib 189 |
. . . . . . 7
                       
           |
132 | 131 | r19.21bi 2772 |
. . . . . 6
 
                     
           |
133 | 14 | adantr 452 |
. . . . . 6
 
       |
134 | 31 | adantr 452 |
. . . . . 6
 
            |
135 | | ovolsscl 19343 |
. . . . . 6
                  
                                   
            |
136 | 132, 133,
134, 135 | syl3anc 1184 |
. . . . 5
 
                         
            |
137 | 129, 136 | fsumrecl 12491 |
. . . 4
               
                        |
138 | 132, 133 | sstrd 3326 |
. . . . . . 7
 
                     
           |
139 | 138, 136 | jca 519 |
. . . . . 6
 
      
               
                             
             |
140 | 139 | ralrimiva 2757 |
. . . . 5
                        
                             
             |
141 | | ovolfiniun 19358 |
. . . . 5
                             
                             
                                      
                        
                        |
142 | 129, 140,
141 | syl2anc 643 |
. . . 4
           
   
                                                
            |
143 | | uniioombl.m |
. . . . . . . 8
   |
144 | 121, 143 | nndivred 10012 |
. . . . . . 7
     |
145 | 144 | adantr 452 |
. . . . . 6
 
         |
146 | 82 | ineq2d 3510 |
. . . . . . . . . . . . 13
         
          
                |
147 | 146 | adantr 452 |
. . . . . . . . . . . 12
 
             
          
                |
148 | 104 | a1i 11 |
. . . . . . . . . . . . . 14
             
                 
           |
149 | 148 | iuneq2i 4079 |
. . . . . . . . . . . . 13
                                                 |
150 | | iunin2 4123 |
. . . . . . . . . . . . 13
                                 
               |
151 | 149, 150 | eqtri 2432 |
. . . . . . . . . . . 12
                                 
               |
152 | 147, 151 | syl6eqr 2462 |
. . . . . . . . . . 11
 
             
               
           |
153 | | fzfid 11275 |
. . . . . . . . . . . 12
 
           |
154 | | ffvelrn 5835 |
. . . . . . . . . . . . . . . . . . . . 21
             
     |
155 | 15, 78, 154 | syl2an 464 |
. . . . . . . . . . . . . . . . . . . 20
 
        
     |
156 | 57, 155 | sseldi 3314 |
. . . . . . . . . . . . . . . . . . 19
 
             |
157 | | 1st2nd2 6353 |
. . . . . . . . . . . . . . . . . . 19
      
                         |
158 | 156, 157 | syl 16 |
. . . . . . . . . . . . . . . . . 18
 
                              |
159 | 158 | fveq2d 5699 |
. . . . . . . . . . . . . . . . 17
 
                                      |
160 | | df-ov 6051 |
. . . . . . . . . . . . . . . . 17
                                            |
161 | 159, 160 | syl6eqr 2462 |
. . . . . . . . . . . . . . . 16
 
                                   |
162 | | ioombl 19420 |
. . . . . . . . . . . . . . . 16
                     |
163 | 161, 162 | syl6eqel 2500 |
. . . . . . . . . . . . . . 15
 
               |
164 | 163 | adantlr 696 |
. . . . . . . . . . . . . 14
                       |
165 | | ffvelrn 5835 |
. . . . . . . . . . . . . . . . . . . . 21
             
     |
166 | 8, 95, 165 | syl2an 464 |
. . . . . . . . . . . . . . . . . . . 20
 
        
     |
167 | 57, 166 | sseldi 3314 |
. . . . . . . . . . . . . . . . . . 19
 
             |
168 | | 1st2nd2 6353 |
. . . . . . . . . . . . . . . . . . 19
      
                         |
169 | 167, 168 | syl 16 |
. . . . . . . . . . . . . . . . . 18
 
                              |
170 | 169 | fveq2d 5699 |
. . . . . . . . . . . . . . . . 17
 
                                      |
171 | | df-ov 6051 |
. . . . . . . . . . . . . . . . 17
                                            |
172 | 170, 171 | syl6eqr 2462 |
. . . . . . . . . . . . . . . 16
 
                                   |
173 | | ioombl 19420 |
. . . . . . . . . . . . . . . 16
                     |
174 | 172, 173 | syl6eqel 2500 |
. . . . . . . . . . . . . . 15
 
               |
175 | 174 | adantr 452 |
. . . . . . . . . . . . . 14
                       |
176 | | inmbl 19397 |
. . . . . . . . . . . . . 14
                                       |
177 | 164, 175,
176 | syl2anc 643 |
. . . . . . . . . . . . 13
                     
           |
178 | 177 | ralrimiva 2757 |
. . . . . . . . . . . 12
 
                               |
179 | | finiunmbl 19399 |
. . . . . . . . . . . 12
                    
                                    |
180 | 153, 178,
179 | syl2anc 643 |
. . . . . . . . . . 11
 
                               |
181 | 152, 180 | eqeltrd 2486 |
. . . . . . . . . 10
 
             
   |
182 | | inss2 3530 |
. . . . . . . . . . 11
           |
183 | 15 | uniiccdif 19431 |
. . . . . . . . . . . . . . 15
               
        |
184 | 183 | simpld 446 |
. . . . . . . . . . . . . 14
         |
185 | | ovolficcss 19327 |
. . . . . . . . . . . . . . 15
             |
186 | 15, 185 | syl 16 |
. . . . . . . . . . . . . 14
      |
187 | 184, 186 | sstrd 3326 |
. . . . . . . . . . . . 13
      |
188 | 18, 187 | syl5eqss 3360 |
. . . . . . . . . . . 12

  |
189 | 188 | adantr 452 |
. . . . . . . . . . 11
 
       |
190 | 182, 189 | syl5ss 3327 |
. . . . . . . . . 10
 
             
   |
191 | | inss1 3529 |
. . . . . . . . . . . 12
                   |
192 | 191 | a1i 11 |
. . . . . . . . . . 11
 
             
           |
193 | | ioossre 10936 |
. . . . . . . . . . . 12
                     |
194 | 172, 193 | syl6eqss 3366 |
. . . . . . . . . . 11
 
               |
195 | 172 | fveq2d 5699 |
. . . . . . . . . . . . 13
 
                                             |
196 | | ovolfcl 19324 |
. . . . . . . . . . . . . . 15
                                              |
197 | 8, 95, 196 | syl2an 464 |
. . . . . . . . . . . . . 14
 
                                         |
198 | | ovolioo 19423 |
. . . . . . . . . . . . . 14
                                                                                |
199 | 197, 198 | syl 16 |
. . . . . . . . . . . . 13
 
                                                  |
200 | 195, 199 | eqtrd 2444 |
. . . . . . . . . . . 12
 
                                      |
201 | 197 | simp2d 970 |
. . . . . . . . . . . . 13
 
               |
202 | 197 | simp1d 969 |
. . . . . . . . . . . . 13
 
               |
203 | 201, 202 | resubcld 9429 |
. . . . . . . . . . . 12
 
                         |
204 | 200, 203 | eqeltrd 2486 |
. . . . . . . . . . 11
 
                    |
205 | | ovolsscl 19343 |
. . . . . . . . . . 11
          
        
                                  
    |
206 | 192, 194,
204, 205 | syl3anc 1184 |
. . . . . . . . . 10
 
                      |
207 | | mblsplit 19389 |
. . . . . . . . . 10
          

        
                                              
         
                
                |
208 | 181, 190,
206, 207 | syl3anc 1184 |
. . . . . . . . 9
 
                                  
         
                
                |
209 | | imassrn 5183 |
. . . . . . . . . . . . . . 15
             |
210 | 209 | unissi 4006 |
. . . . . . . . . . . . . 14
  
            |
211 | 210, 74, 18 | 3sstr4i 3355 |
. . . . . . . . . . . . 13
 |
212 | | sslin 3535 |
. . . . . . . . . . . . 13
         
         
   |
213 | 211, 212 | mp1i 12 |
. . . . . . . . . . . 12
 
             
         
   |
214 | | dfss1 3513 |
. . . . . . . . . . . 12
         
         
          
         
              |
215 | 213, 214 | sylib 189 |
. . . . . . . . . . 11
 
              
         
              |
216 | 215 | fveq2d 5699 |
. . . . . . . . . 10
 
                  
         
               
    |
217 | | indifdir 3565 |
. . . . . . . . . . . . 13
                                   |
218 | | incom 3501 |
. . . . . . . . . . . . . 14
                  
  |
219 | | incom 3501 |
. . . . . . . . . . . . . 14
                  
  |
220 | 218, 219 | difeq12i 3431 |
. . . . . . . . . . . . 13
                               
             |
221 | 217, 220 | eqtri 2432 |
. . . . . . . . . . . 12
                     
             |
222 | 84 | eqcomd 2417 |
. . . . . . . . . . . . . . . 16
  
   
              |
223 | 82 | ineq1d 3509 |
. . . . . . . . . . . . . . . . . 18
  
   
                          
                   |
224 | | fveq2 5695 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
225 | 224 | fveq2d 5699 |
. . . . . . . . . . . . . . . . . . . . 21
                   |
226 | 225 | cbvdisjv 4161 |
. . . . . . . . . . . . . . . . . . . 20
Disj          Disj            |
227 | 16, 226 | sylib 189 |
. . . . . . . . . . . . . . . . . . 19
 Disj
           |
228 | 78 | ssriv 3320 |
. . . . . . . . . . . . . . . . . . . 20
     |
229 | 228 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
    
  |
230 | | uzss 10470 |
. . . . . . . . . . . . . . . . . . . . 21
      
   
        |
231 | 42, 230 | syl 16 |
. . . . . . . . . . . . . . . . . . . 20
             |
232 | 231, 39 | syl6sseqr 3363 |
. . . . . . . . . . . . . . . . . . 19
         |
233 | | uzdisj 11082 |
. . . . . . . . . . . . . . . . . . . 20
            
    |
234 | 50 | ineq1d 3509 |
. . . . . . . . . . . . . . . . . . . 20
                               |
235 | 233, 234 | syl5reqr 2459 |
. . . . . . . . . . . . . . . . . . 19
               |
236 | | disjiun 4170 |
. . . . . . . . . . . . . . . . . . 19
 Disj
                   
    
   
      
                                |
237 | 227, 229,
232, 235, 236 | syl13anc 1186 |
. . . . . . . . . . . . . . . . . 18
               
                   |
238 | 223, 237 | eqtrd 2444 |
. . . . . . . . . . . . . . . . 17
  
   
              |
239 | | uneqdifeq 3684 |
. . . . . . . . . . . . . . . . 17
 

                                                          |
240 | 211, 238,
239 | sylancr 645 |
. . . . . . . . . . . . . . . 16
       
              
   
              |
241 | 222, 240 | mpbid 202 |
. . . . . . . . . . . . . . 15
                     |
242 | 241 | adantr 452 |
. . . . . . . . . . . . . 14
 
                         |
243 | 242 | ineq2d 3510 |
. . . . . . . . . . . . 13
 
             
           
                   |
244 | | incom 3501 |
. . . . . . . . . . . . 13
                    
    |
245 | 106, 103 | eqtri 2432 |
. . . . . . . . . . . . 13
                
                 
                  |
246 | 243, 244,
245 | 3eqtr4g 2469 |
. . . . . . . . . . . 12
 
       
                         
           |
247 | 221, 246 | syl5eqr 2458 |
. . . . . . . . . . 11
 
              
            
   
                       |
248 | 247 | fveq2d 5699 |
. . . . . . . . . 10
 
                  
                     
                        |
249 | 216, 248 | oveq12d 6066 |
. . . . . . . . 9
 
                    
                          
                          
                      
             |
250 | 208, 249 | eqtrd 2444 |
. . . . . . . 8
 
                                            
                         |
251 | 206, 145 | resubcld 9429 |
. . . . . . . . . . 11
 
                  
       |
252 | | inss2 3530 |
. . . . . . . . . . . . . 14
                           |
253 | 252 | a1i 11 |
. . . . . . . . . . . . 13
                     
                   |
254 | 194 | adantr 452 |
. . . . . . . . . . . . 13
                       |
255 | 204 | adantr 452 |
. . . . . . . . . . . . 13
                            |
256 | | ovolsscl 19343 |
. . . . . . . . . . . . 13
          
                        
                                       |
257 | 253, 254,
255, 256 | syl3anc 1184 |
. . . . . . . . . . . 12
                                      |
258 | 153, 257 | fsumrecl 12491 |
. . . . . . . . . . 11
 
                       
            |
259 | | uniioombl.n2 |
. . . . . . . . . . . . . 14
                             
                      
        |
260 | 259 | r19.21bi 2772 |
. . . . . . . . . . . . 13
 
                           
                      
        |
261 | 258, 206,
145 | absdifltd 12199 |
. . . . . . . . . . . . 13
 
                            
                      
                    
                       
                            
                                 |
262 | 260, 261 | mpbid 202 |
. . . . . . . . . . . 12
 
                   
                       
                            
                                |
263 | 262 | simpld 446 |
. . . . . . . . . . 11
 
                  
                       
            |
264 | 251, 258,
263 | ltled 9185 |
. . . . . . . . . 10
 
                  
                       
            |
265 | 152 | fveq2d 5699 |
. . . . . . . . . . 11
 
                                      
            |
266 | | mblvol 19387 |
. . . . . . . . . . . . . . . . 17
         
        
           
                      
            |
267 | 177, 266 | syl 16 |
. . . . . . . . . . . . . . . 16
                                                            |
268 | 267, 257 | eqeltrd 2486 |
. . . . . . . . . . . . . . 15
                                     |
269 | 177, 268 | jca 519 |
. . . . . . . . . . . . . 14
                      
                    
             |
270 | 269 | ralrimiva 2757 |
. . . . . . . . . . . . 13
 
                                         
             |
271 | | inss1 3529 |
. . . . . . . . . . . . . . . 16
                           |
272 | 271 | rgenw 2741 |
. . . . . . . . . . . . . . 15
                            |
273 | 227 | adantr 452 |
. . . . . . . . . . . . . . 15
 
     Disj            |
274 | | disjss2 4153 |
. . . . . . . . . . . . . . 15
 
        
                 Disj
         Disj          
            |
275 | 272, 273,
274 | mpsyl 61 |
. . . . . . . . . . . . . 14
 
     Disj                      |
276 | | disjss1 4156 |
. . . . . . . . . . . . . 14
    
Disj                    Disj              
            |
277 | 228, 275,
276 | mpsyl 61 |
. . . . . . . . . . . . 13
 
     Disj                          |
278 | | volfiniun 19402 |
. . . . . . . . . . . . 13
                     
                    
           Disj                                                                      
            |
279 | 153, 270,
277, 278 | syl3anc 1184 |
. . . . . . . . . . . 12
 
                                                  
            |
280 | | mblvol 19387 |
. . . . . . . . . . . . 13
 
             
        
                 
                            
            |
281 | 180, 280 | syl 16 |
. . . . . . . . . . . 12
 
                                                                |
282 | 267 | sumeq2dv 12460 |
. . . . . . . . . . . 12
 
                      
                            
            |
283 | 279, 281,
282 | 3eqtr3d 2452 |
. . . . . . . . . . 11
 
                                                    
            |
284 | 265, 283 | eqtrd 2444 |
. . . . . . . . . 10
 
                                      
            |
285 | 264, 284 | breqtrrd 4206 |
. . . . . . . . 9
 
                  
                 
    |
286 | 284, 258 | eqeltrd 2486 |
. . . . . . . . . 10
 
                      |
287 | 206, 145,
286 | lesubaddd 9587 |
. . . . . . . . 9
 
                   
                 
              
 
                      |
288 | 285, 287 | mpbid 202 |
. . . . . . . 8
 
                                         |
289 | 250, 288 | eqbrtrrd 4202 |
. . . . . . 7
 
                  
                      
          
                     |
290 | 136, 145,
286 | leadd2d 9585 |
. . . . . . 7
 
              
                                                
                                             |
291 | 289, 290 | mpbird 224 |
. . . . . 6
 
                         
              |
292 | 129, 136,
145, 291 | fsumle 12541 |
. . . . 5
               
                                |
293 | 144 | recnd 9078 |
. . . . . . 7
     |
294 | | fsumconst 12536 |
. . . . . . 7
      
                        |
295 | 129, 293,
294 | syl2anc 643 |
. . . . . 6
                       |
296 | | nnnn0 10192 |
. . . . . . . 8
   |
297 | | hashfz1 11593 |
. . . . . . . 8

          |
298 | 143, 296,
297 | 3syl 19 |
. . . . . . 7
           |
299 | 298 | oveq1d 6063 |
. . . . . 6
                   |
300 | 121 | recnd 9078 |
. . . . . . 7
   |
301 | 143 | nncnd 9980 |
. . . . . . 7
   |
302 | 143 | nnne0d 10008 |
. . . . . . 7
   |
303 | 300, 301,
302 | divcan2d 9756 |
. . . . . 6
       |
304 | 295, 299,
303 | 3eqtrd 2448 |
. . . . 5
           |
305 | 292, 304 | breqtrd 4204 |
. . . 4
               
                        |
306 | 119, 137,
121, 142, 305 | letrd 9191 |
. . 3
           
   
                        |
307 | 119, 121,
37, 306 | leadd2dd 9605 |
. 2
                                   
          
           |
308 | 33, 120, 122, 128, 307 | letrd 9191 |
1
     
 
           |