Step | Hyp | Ref
| Expression |
1 | | nnuz 11194 |
. . . 4
     |
2 | | 1zzd 10968 |
. . . 4
   |
3 | | uniioombl.c |
. . . 4
   |
4 | | eqidd 2452 |
. . . 4
 

          |
5 | | uniioombl.t |
. . . . . 6
   
   |
6 | | eqidd 2452 |
. . . . . 6
 

  
      
      |
7 | | uniioombl.g |
. . . . . . . . . 10
          |
8 | | eqid 2451 |
. . . . . . . . . . 11
    
  |
9 | 8 | ovolfsf 22424 |
. . . . . . . . . 10
         
          |
10 | 7, 9 | syl 17 |
. . . . . . . . 9
  
          |
11 | 10 | ffvelrnda 6022 |
. . . . . . . 8
 

  
         |
12 | | elrege0 11738 |
. . . . . . . 8
   
                         |
13 | 11, 12 | sylib 200 |
. . . . . . 7
 

   
      
       |
14 | 13 | simpld 461 |
. . . . . 6
 

  
      |
15 | 13 | simprd 465 |
. . . . . 6
 

  
      |
16 | | uniioombl.1 |
. . . . . . . 8
          |
17 | | uniioombl.2 |
. . . . . . . 8
 Disj
          |
18 | | uniioombl.3 |
. . . . . . . 8
   
   |
19 | | uniioombl.a |
. . . . . . . 8

   |
20 | | uniioombl.e |
. . . . . . . 8
        |
21 | | uniioombl.s |
. . . . . . . 8

     |
22 | | uniioombl.v |
. . . . . . . 8
              |
23 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22 | uniioombllem1 22538 |
. . . . . . 7
       |
24 | 8, 5 | ovolsf 22425 |
. . . . . . . . . . . . 13
                 |
25 | 7, 24 | syl 17 |
. . . . . . . . . . . 12
          |
26 | | frn 5735 |
. . . . . . . . . . . 12
       
     |
27 | 25, 26 | syl 17 |
. . . . . . . . . . 11
  
   |
28 | | icossxr 11719 |
. . . . . . . . . . 11
    |
29 | 27, 28 | syl6ss 3444 |
. . . . . . . . . 10
   |
30 | | supxrub 11610 |
. . . . . . . . . 10
         |
31 | 29, 30 | sylan 474 |
. . . . . . . . 9
 
       |
32 | 31 | ralrimiva 2802 |
. . . . . . . 8
 
      |
33 | | ffn 5728 |
. . . . . . . . . 10
       
  |
34 | 25, 33 | syl 17 |
. . . . . . . . 9
   |
35 | | breq1 4405 |
. . . . . . . . . 10
     
       
       |
36 | 35 | ralrn 6025 |
. . . . . . . . 9
  
    
           |
37 | 34, 36 | syl 17 |
. . . . . . . 8
  
   
            |
38 | 32, 37 | mpbid 214 |
. . . . . . 7
            |
39 | | breq2 4406 |
. . . . . . . . 9
             
       |
40 | 39 | ralbidv 2827 |
. . . . . . . 8
                       |
41 | 40 | rspcev 3150 |
. . . . . . 7
                
       |
42 | 23, 38, 41 | syl2anc 667 |
. . . . . 6
         |
43 | 1, 5, 2, 6, 14, 15, 42 | isumsup2 13904 |
. . . . 5
       |
44 | | rge0ssre 11740 |
. . . . . . 7
    |
45 | 27, 44 | syl6ss 3444 |
. . . . . 6
   |
46 | | 1nn 10620 |
. . . . . . . . 9
 |
47 | | fdm 5733 |
. . . . . . . . . 10
          |
48 | 25, 47 | syl 17 |
. . . . . . . . 9
   |
49 | 46, 48 | syl5eleqr 2536 |
. . . . . . . 8
   |
50 | | ne0i 3737 |
. . . . . . . 8
   |
51 | 49, 50 | syl 17 |
. . . . . . 7
   |
52 | | dm0rn0 5051 |
. . . . . . . 8

  |
53 | 52 | necon3bii 2676 |
. . . . . . 7

  |
54 | 51, 53 | sylib 200 |
. . . . . 6
   |
55 | | breq2 4406 |
. . . . . . . . 9
     
       |
56 | 55 | ralbidv 2827 |
. . . . . . . 8
       
       |
57 | 56 | rspcev 3150 |
. . . . . . 7
                |
58 | 23, 32, 57 | syl2anc 667 |
. . . . . 6
     |
59 | | supxrre 11613 |
. . . . . 6
 

            |
60 | 45, 54, 58, 59 | syl3anc 1268 |
. . . . 5
           |
61 | 43, 60 | breqtrrd 4429 |
. . . 4
       |
62 | 1, 2, 3, 4, 61 | climi2 13575 |
. . 3
                        |
63 | 1 | r19.2uz 13414 |
. . 3
  
                                    |
64 | 62, 63 | syl 17 |
. 2
                  |
65 | | 1zzd 10968 |
. . . . . . . . 9
                           |
66 | 3 | ad2antrr 732 |
. . . . . . . . . 10
                           |
67 | | simplrl 770 |
. . . . . . . . . . 11
                           |
68 | 67 | nnrpd 11339 |
. . . . . . . . . 10
                           |
69 | 66, 68 | rpdivcld 11358 |
. . . . . . . . 9
                             |
70 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
         |
71 | 70 | inex1 4544 |
. . . . . . . . . . . . . . 15
                   |
72 | 71 | rgenw 2749 |
. . . . . . . . . . . . . 14
                    |
73 | | eqid 2451 |
. . . . . . . . . . . . . . 15
                             
           |
74 | 73 | fnmpt 5704 |
. . . . . . . . . . . . . 14
 
        
                               |
75 | 72, 74 | mp1i 13 |
. . . . . . . . . . . . 13
    
                               
            |
76 | | elfznn 11828 |
. . . . . . . . . . . . 13
       |
77 | | fvco2 5940 |
. . . . . . . . . . . . 13
           
                       
                                             |
78 | 75, 76, 77 | syl2an 480 |
. . . . . . . . . . . 12
                                             
                                             |
79 | 76 | adantl 468 |
. . . . . . . . . . . . . 14
                                   |
80 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
81 | 80 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                   |
82 | 81 | ineq1d 3633 |
. . . . . . . . . . . . . . 15
         
                 
           |
83 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
         |
84 | 83 | inex1 4544 |
. . . . . . . . . . . . . . 15
                   |
85 | 82, 73, 84 | fvmpt 5948 |
. . . . . . . . . . . . . 14
           
                     
           |
86 | 79, 85 | syl 17 |
. . . . . . . . . . . . 13
                                           
                     
           |
87 | 86 | fveq2d 5869 |
. . . . . . . . . . . 12
                                               
                          
            |
88 | 78, 87 | eqtrd 2485 |
. . . . . . . . . . 11
                                             
                          
            |
89 | | simpr 463 |
. . . . . . . . . . . 12
    
                        |
90 | 89, 1 | syl6eleq 2539 |
. . . . . . . . . . 11
    
                            |
91 | | inss2 3653 |
. . . . . . . . . . . . . 14
                           |
92 | 91 | a1i 11 |
. . . . . . . . . . . . 13
                                         
                   |
93 | | inss2 3653 |
. . . . . . . . . . . . . . . . . . 19
      |
94 | 7 | adantr 467 |
. . . . . . . . . . . . . . . . . . . 20
 
                    
     |
95 | | elfznn 11828 |
. . . . . . . . . . . . . . . . . . . 20
       |
96 | | ffvelrn 6020 |
. . . . . . . . . . . . . . . . . . . 20
             
     |
97 | 94, 95, 96 | syl2an 480 |
. . . . . . . . . . . . . . . . . . 19
                            
     |
98 | 93, 97 | sseldi 3430 |
. . . . . . . . . . . . . . . . . 18
                                 |
99 | | 1st2nd2 6830 |
. . . . . . . . . . . . . . . . . 18
      
                         |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . . . . 17
                                                  |
101 | 100 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                                                          |
102 | | df-ov 6293 |
. . . . . . . . . . . . . . . 16
                                            |
103 | 101, 102 | syl6eqr 2503 |
. . . . . . . . . . . . . . 15
                                                       |
104 | | ioossre 11696 |
. . . . . . . . . . . . . . 15
                     |
105 | 103, 104 | syl6eqss 3482 |
. . . . . . . . . . . . . 14
                                   |
106 | 105 | ad2antrr 732 |
. . . . . . . . . . . . 13
                                           |
107 | 103 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                                                                 |
108 | | ovolfcl 22419 |
. . . . . . . . . . . . . . . . . 18
                                              |
109 | 94, 95, 108 | syl2an 480 |
. . . . . . . . . . . . . . . . 17
                                                             |
110 | | ovolioo 22521 |
. . . . . . . . . . . . . . . . 17
                                                                                |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
                                                                      |
112 | 107, 111 | eqtrd 2485 |
. . . . . . . . . . . . . . 15
                                                          |
113 | 109 | simp2d 1021 |
. . . . . . . . . . . . . . . 16
                                   |
114 | 109 | simp1d 1020 |
. . . . . . . . . . . . . . . 16
                                   |
115 | 113, 114 | resubcld 10047 |
. . . . . . . . . . . . . . 15
                                             |
116 | 112, 115 | eqeltrd 2529 |
. . . . . . . . . . . . . 14
                                        |
117 | 116 | ad2antrr 732 |
. . . . . . . . . . . . 13
                                                |
118 | | ovolsscl 22439 |
. . . . . . . . . . . . 13
          
                        
                                       |
119 | 92, 106, 117, 118 | syl3anc 1268 |
. . . . . . . . . . . 12
                                                          |
120 | 119 | recnd 9669 |
. . . . . . . . . . 11
                                                          |
121 | 88, 90, 120 | fsumser 13796 |
. . . . . . . . . 10
    
                                        
                       
                 |
122 | 121 | eqcomd 2457 |
. . . . . . . . 9
    
                                   
                                 
            |
123 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
124 | 123 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                   |
125 | 124 | ineq1d 3633 |
. . . . . . . . . . . . 13
         
                 
           |
126 | 125 | cbvmptv 4495 |
. . . . . . . . . . . 12
                             
           |
127 | | eqeq1 2455 |
. . . . . . . . . . . . . 14
 
   |
128 | | infeq1 7992 |
. . . . . . . . . . . . . . 15
 inf   inf     |
129 | | supeq1 7959 |
. . . . . . . . . . . . . . 15
           |
130 | 128, 129 | opeq12d 4174 |
. . . . . . . . . . . . . 14
 inf       
 inf  
    
   |
131 | 127, 130 | ifbieq2d 3906 |
. . . . . . . . . . . . 13
       
inf       
      
  inf            |
132 | 131 | cbvmptv 4495 |
. . . . . . . . . . . 12
       
inf       
          
inf       
    |
133 | 16, 17, 18, 19, 20, 3, 7, 21, 5,
22, 126, 132 | uniioombllem2 22540 |
. . . . . . . . . . 11
 

             
                             |
134 | 95, 133 | sylan2 477 |
. . . . . . . . . 10
 
                  
                             |
135 | 134 | adantlr 721 |
. . . . . . . . 9
                                      
                             |
136 | 1, 65, 69, 122, 135 | climi2 13575 |
. . . . . . . 8
                                                      
                      
        |
137 | | 1z 10967 |
. . . . . . . . 9
 |
138 | 1 | rexuz3 13411 |
. . . . . . . . 9
  
                            
                      
                                   
                      
         |
139 | 137, 138 | ax-mp 5 |
. . . . . . . 8
  
                           
                      
                                   
                      
        |
140 | 136, 139 | sylib 200 |
. . . . . . 7
                                                      
                      
        |
141 | 140 | ralrimiva 2802 |
. . . . . 6
 
                                                    
                      
        |
142 | | fzfi 12185 |
. . . . . . 7
     |
143 | | rexfiuz 13410 |
. . . . . . 7
      
                                  
                      
                                         
                      
         |
144 | 142, 143 | ax-mp 5 |
. . . . . 6
  
                                 
                      
                                         
                      
        |
145 | 141, 144 | sylibr 216 |
. . . . 5
 
                                                    
                      
        |
146 | 1 | rexuz3 13411 |
. . . . . 6
  
                                  
                      
                                         
                      
         |
147 | 137, 146 | ax-mp 5 |
. . . . 5
  
                                 
                      
                                         
                      
        |
148 | 145, 147 | sylibr 216 |
. . . 4
 
                                                    
                      
        |
149 | 1 | r19.2uz 13414 |
. . . 4
  
                                 
                      
     
                             
                      
        |
150 | 148, 149 | syl 17 |
. . 3
 
                            
                 
                      
        |
151 | 16 | adantr 467 |
. . . . 5
 
                
                             
                      
            
     |
152 | 17 | adantr 467 |
. . . . 5
 
                
                             
                      
         Disj           |
153 | 20 | adantr 467 |
. . . . 5
 
                
                             
                      
                |
154 | 3 | adantr 467 |
. . . . 5
 
                
                             
                      
           |
155 | 7 | adantr 467 |
. . . . 5
 
                
                             
                      
            
     |
156 | 21 | adantr 467 |
. . . . 5
 
                
                             
                      
              |
157 | 22 | adantr 467 |
. . . . 5
 
                
                             
                      
                      |
158 | | simprll 772 |
. . . . 5
 
                
                             
                      
           |
159 | | simprlr 773 |
. . . . 5
 
                
                             
                      
                         |
160 | | eqid 2451 |
. . . . 5
  
                    |
161 | | simprrl 774 |
. . . . 5
 
                
                             
                      
           |
162 | | simprrr 775 |
. . . . . 6
 
                
                             
                      
                                     
                      
        |
163 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
164 | 163 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                   |
165 | 164 | ineq1d 3633 |
. . . . . . . . . . . . 13
         
                 
           |
166 | 165 | fveq2d 5869 |
. . . . . . . . . . . 12
                                    
            |
167 | 166 | cbvsumv 13762 |
. . . . . . . . . . 11
                  
                            
           |
168 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
169 | 168 | fveq2d 5869 |
. . . . . . . . . . . . . 14
                   |
170 | 169 | ineq2d 3634 |
. . . . . . . . . . . . 13
         
                 
           |
171 | 170 | fveq2d 5869 |
. . . . . . . . . . . 12
                                    
            |
172 | 171 | sumeq2sdv 13770 |
. . . . . . . . . . 11
                   
                            
            |
173 | 167, 172 | syl5eq 2497 |
. . . . . . . . . 10
                   
                            
            |
174 | 169 | ineq1d 3633 |
. . . . . . . . . . 11
         
             |
175 | 174 | fveq2d 5869 |
. . . . . . . . . 10
                            
    |
176 | 173, 175 | oveq12d 6308 |
. . . . . . . . 9
                    
                      
                      
                      
     |
177 | 176 | fveq2d 5869 |
. . . . . . . 8
                       
                      
                          
                      
      |
178 | 177 | breq1d 4412 |
. . . . . . 7
                        
                      
                            
                      
         |
179 | 178 | cbvralv 3019 |
. . . . . 6
 
         
                 
                      
                                  
                      
        |
180 | 162, 179 | sylib 200 |
. . . . 5
 
                
                             
                      
                                     
                      
        |
181 | | eqid 2451 |
. . . . 5
  
                    |
182 | 151, 152,
18, 19, 153, 154, 155, 156, 5, 157, 158, 159, 160, 161, 180, 181 | uniioombllem5 22545 |
. . . 4
 
                
                             
                      
                     
              |
183 | 182 | anassrs 654 |
. . 3
                               
                 
                      
                       
           |
184 | 150, 183 | rexlimddv 2883 |
. 2
 
                             
              |
185 | 64, 184 | rexlimddv 2883 |
1
                
           |