Step | Hyp | Ref
| Expression |
1 | | voliunlem1.7 |
. . . . 5

  |
2 | 1 | adantr 467 |
. . . 4
 

  |
3 | | voliunlem1.8 |
. . . . 5
        |
4 | 3 | adantr 467 |
. . . 4
 

       |
5 | | difss 3560 |
. . . . 5
    |
6 | | ovolsscl 22439 |
. . . . 5
    
                |
7 | 5, 6 | mp3an1 1351 |
. . . 4
 
          
     |
8 | 2, 4, 7 | syl2anc 667 |
. . 3
 

     
    |
9 | | difss 3560 |
. . . . 5
             |
10 | | ovolsscl 22439 |
. . . . 5
   
         
          
              |
11 | 9, 10 | mp3an1 1351 |
. . . 4
 
          
              |
12 | 2, 4, 11 | syl2anc 667 |
. . 3
 

                   |
13 | | inss1 3652 |
. . . . 5
             |
14 | | ovolsscl 22439 |
. . . . 5
   
         
          
              |
15 | 13, 14 | mp3an1 1351 |
. . . 4
 
          
              |
16 | 2, 4, 15 | syl2anc 667 |
. . 3
 

                   |
17 | | elfznn 11828 |
. . . . . . . . 9
       |
18 | | voliunlem.3 |
. . . . . . . . . . . 12
       |
19 | | ffn 5728 |
. . . . . . . . . . . 12
       |
20 | 18, 19 | syl 17 |
. . . . . . . . . . 11
   |
21 | | fnfvelrn 6019 |
. . . . . . . . . . 11
 
       |
22 | 20, 21 | sylan 474 |
. . . . . . . . . 10
 

      |
23 | | elssuni 4227 |
. . . . . . . . . 10
        
   |
24 | 22, 23 | syl 17 |
. . . . . . . . 9
 

       |
25 | 17, 24 | sylan2 477 |
. . . . . . . 8
 
         
  |
26 | 25 | ralrimiva 2802 |
. . . . . . 7
          
   |
27 | 26 | adantr 467 |
. . . . . 6
 

             |
28 | | iunss 4319 |
. . . . . 6
 
         
             |
29 | 27, 28 | sylibr 216 |
. . . . 5
 

             |
30 | 29 | sscond 3570 |
. . . 4
 

    
            |
31 | 9, 2 | syl5ss 3443 |
. . . 4
 

              |
32 | | ovolss 22438 |
. . . 4
                 
           
     
 
     
             |
33 | 30, 31, 32 | syl2anc 667 |
. . 3
 

     
 
     
             |
34 | 8, 12, 16, 33 | leadd2dd 10228 |
. 2
 

                      
          
                               |
35 | | oveq2 6298 |
. . . . . . . . . . 11
           |
36 | 35 | iuneq1d 4303 |
. . . . . . . . . 10
           
           |
37 | 36 | eleq1d 2513 |
. . . . . . . . 9
  
        
             |
38 | 36 | ineq2d 3634 |
. . . . . . . . . . 11
                           |
39 | 38 | fveq2d 5869 |
. . . . . . . . . 10
                      
              |
40 | | fveq2 5865 |
. . . . . . . . . 10
               |
41 | 39, 40 | eqeq12d 2466 |
. . . . . . . . 9
      
                                            |
42 | 37, 41 | anbi12d 717 |
. . . . . . . 8
                 
                                   
                     |
43 | 42 | imbi2d 318 |
. . . . . . 7
  
 
                                                  
                       |
44 | | oveq2 6298 |
. . . . . . . . . . 11
           |
45 | 44 | iuneq1d 4303 |
. . . . . . . . . 10
           
           |
46 | 45 | eleq1d 2513 |
. . . . . . . . 9
  
        
             |
47 | 45 | ineq2d 3634 |
. . . . . . . . . . 11
                           |
48 | 47 | fveq2d 5869 |
. . . . . . . . . 10
                      
              |
49 | | fveq2 5865 |
. . . . . . . . . 10
               |
50 | 48, 49 | eqeq12d 2466 |
. . . . . . . . 9
      
                                            |
51 | 46, 50 | anbi12d 717 |
. . . . . . . 8
                 
                                   
                     |
52 | 51 | imbi2d 318 |
. . . . . . 7
  
 
                                                  
                       |
53 | | oveq2 6298 |
. . . . . . . . . . 11
               |
54 | 53 | iuneq1d 4303 |
. . . . . . . . . 10
             
             |
55 | 54 | eleq1d 2513 |
. . . . . . . . 9
    
        
               |
56 | 54 | ineq2d 3634 |
. . . . . . . . . . 11
                               |
57 | 56 | fveq2d 5869 |
. . . . . . . . . 10
                        
                |
58 | | fveq2 5865 |
. . . . . . . . . 10
                   |
59 | 57, 58 | eqeq12d 2466 |
. . . . . . . . 9
        
                                                |
60 | 55, 59 | anbi12d 717 |
. . . . . . . 8
                   
                                     
                         |
61 | 60 | imbi2d 318 |
. . . . . . 7
    
 
                                                    
                           |
62 | | 1z 10967 |
. . . . . . . . . . 11
 |
63 | | fzsn 11840 |
. . . . . . . . . . 11
         |
64 | | iuneq1 4292 |
. . . . . . . . . . 11
                          |
65 | 62, 63, 64 | mp2b 10 |
. . . . . . . . . 10
          
       |
66 | | 1ex 9638 |
. . . . . . . . . . 11
 |
67 | | fveq2 5865 |
. . . . . . . . . . 11
           |
68 | 66, 67 | iunxsn 4361 |
. . . . . . . . . 10
            |
69 | 65, 68 | eqtri 2473 |
. . . . . . . . 9
               |
70 | | 1nn 10620 |
. . . . . . . . . 10
 |
71 | | ffvelrn 6020 |
. . . . . . . . . 10
             |
72 | 18, 70, 71 | sylancl 668 |
. . . . . . . . 9
       |
73 | 69, 72 | syl5eqel 2533 |
. . . . . . . 8
             |
74 | 67 | ineq2d 3634 |
. . . . . . . . . . . 12
               |
75 | 74 | fveq2d 5869 |
. . . . . . . . . . 11
                         |
76 | | voliunlem1.6 |
. . . . . . . . . . 11
              |
77 | | fvex 5875 |
. . . . . . . . . . 11
            |
78 | 75, 76, 77 | fvmpt 5948 |
. . . . . . . . . 10
                  |
79 | 70, 78 | ax-mp 5 |
. . . . . . . . 9
        
       |
80 | | seq1 12226 |
. . . . . . . . . 10
             |
81 | 62, 80 | ax-mp 5 |
. . . . . . . . 9
           |
82 | 69 | ineq2i 3631 |
. . . . . . . . . 10
                   |
83 | 82 | fveq2i 5868 |
. . . . . . . . 9
                     
       |
84 | 79, 81, 83 | 3eqtr4ri 2484 |
. . . . . . . 8
                        |
85 | 73, 84 | jctir 541 |
. . . . . . 7
                 
                    |
86 | | peano2nn 10621 |
. . . . . . . . . . . . 13
     |
87 | | ffvelrn 6020 |
. . . . . . . . . . . . 13
                 |
88 | 18, 86, 87 | syl2an 480 |
. . . . . . . . . . . 12
 

        |
89 | | unmbl 22491 |
. . . . . . . . . . . . 13
                                       |
90 | 89 | ex 436 |
. . . . . . . . . . . 12
 
                                     |
91 | 88, 90 | syl5com 31 |
. . . . . . . . . . 11
 

 
                              |
92 | | simpr 463 |
. . . . . . . . . . . . . . 15
 

  |
93 | | nnuz 11194 |
. . . . . . . . . . . . . . 15
     |
94 | 92, 93 | syl6eleq 2539 |
. . . . . . . . . . . . . 14
 

      |
95 | | fzsuc 11843 |
. . . . . . . . . . . . . 14
    
                  |
96 | | iuneq1 4292 |
. . . . . . . . . . . . . 14
                                               |
97 | 94, 95, 96 | 3syl 18 |
. . . . . . . . . . . . 13
 

            
                 |
98 | | iunxun 4363 |
. . . . . . . . . . . . . 14
                           
          |
99 | | ovex 6318 |
. . . . . . . . . . . . . . . 16
   |
100 | | fveq2 5865 |
. . . . . . . . . . . . . . . 16
               |
101 | 99, 100 | iunxsn 4361 |
. . . . . . . . . . . . . . 15
                |
102 | 101 | uneq2i 3585 |
. . . . . . . . . . . . . 14
 
                    
                 |
103 | 98, 102 | eqtri 2473 |
. . . . . . . . . . . . 13
                                   |
104 | 97, 103 | syl6eq 2501 |
. . . . . . . . . . . 12
 

                                |
105 | 104 | eleq1d 2513 |
. . . . . . . . . . 11
 

 
          
 
                   |
106 | 91, 105 | sylibrd 238 |
. . . . . . . . . 10
 

 
                        |
107 | | oveq1 6297 |
. . . . . . . . . . 11
                              
                                                |
108 | | inss1 3652 |
. . . . . . . . . . . . . . 15
               |
109 | 108, 2 | syl5ss 3443 |
. . . . . . . . . . . . . 14
 

                |
110 | | ovolsscl 22439 |
. . . . . . . . . . . . . . . 16
   
           
          
                |
111 | 108, 110 | mp3an1 1351 |
. . . . . . . . . . . . . . 15
 
          
                |
112 | 2, 4, 111 | syl2anc 667 |
. . . . . . . . . . . . . 14
 

                     |
113 | | mblsplit 22486 |
. . . . . . . . . . . . . 14
         
           
                                                                                                 |
114 | 88, 109, 112, 113 | syl3anc 1268 |
. . . . . . . . . . . . 13
 

                                                                             |
115 | | in32 3644 |
. . . . . . . . . . . . . . . 16
                                             |
116 | | inss2 3653 |
. . . . . . . . . . . . . . . . . 18
               |
117 | 86 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
 

    |
118 | 117, 93 | syl6eleq 2539 |
. . . . . . . . . . . . . . . . . . 19
 

        |
119 | | eluzfz2 11807 |
. . . . . . . . . . . . . . . . . . 19
      
          |
120 | 100 | ssiun2s 4322 |
. . . . . . . . . . . . . . . . . . 19
                             |
121 | 118, 119,
120 | 3syl 18 |
. . . . . . . . . . . . . . . . . 18
 

                    |
122 | 116, 121 | syl5ss 3443 |
. . . . . . . . . . . . . . . . 17
 

                      |
123 | | df-ss 3418 |
. . . . . . . . . . . . . . . . 17
                              
                      |
124 | 122, 123 | sylib 200 |
. . . . . . . . . . . . . . . 16
 

                                |
125 | 115, 124 | syl5eq 2497 |
. . . . . . . . . . . . . . 15
 

                                |
126 | 125 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 

                                          |
127 | | indif2 3686 |
. . . . . . . . . . . . . . . 16
                        
                    |
128 | | uncom 3578 |
. . . . . . . . . . . . . . . . . . 19
 
                       
           |
129 | 104, 128 | syl6req 2502 |
. . . . . . . . . . . . . . . . . 18
 

                                |
130 | | voliunlem.5 |
. . . . . . . . . . . . . . . . . . . . . . 23
 Disj
      |
131 | 130 | ad2antrr 732 |
. . . . . . . . . . . . . . . . . . . . . 22
         Disj       |
132 | 117 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
133 | 17 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
134 | 133 | nnred 10624 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
135 | | elfzle2 11803 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
       |
136 | 135 | adantl 468 |
. . . . . . . . . . . . . . . . . . . . . . . 24
           |
137 | 92 | adantr 467 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
           |
138 | | nnleltp1 10991 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
 
       |
139 | 133, 137,
138 | syl2anc 667 |
. . . . . . . . . . . . . . . . . . . . . . . 24
         
     |
140 | 136, 139 | mpbid 214 |
. . . . . . . . . . . . . . . . . . . . . . 23
             |
141 | 134, 140 | gtned 9770 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
142 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
               |
143 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . . 23
           |
144 | 142, 143 | disji2 4389 |
. . . . . . . . . . . . . . . . . . . . . 22
 Disj
          
              |
145 | 131, 132,
133, 141, 144 | syl121anc 1273 |
. . . . . . . . . . . . . . . . . . . . 21
                       |
146 | 145 | iuneq2dv 4300 |
. . . . . . . . . . . . . . . . . . . 20
 

                  
       |
147 | | iunin2 4342 |
. . . . . . . . . . . . . . . . . . . 20
                                     |
148 | | iun0 4334 |
. . . . . . . . . . . . . . . . . . . 20
       |
149 | 146, 147,
148 | 3eqtr3g 2508 |
. . . . . . . . . . . . . . . . . . 19
 

                    |
150 | | uneqdifeq 3856 |
. . . . . . . . . . . . . . . . . . 19
       
                              
                                                                |
151 | 121, 149,
150 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
 

                                                                |
152 | 129, 151 | mpbid 214 |
. . . . . . . . . . . . . . . . 17
 

 
                              |
153 | 152 | ineq2d 3634 |
. . . . . . . . . . . . . . . 16
 

                                    |
154 | 127, 153 | syl5eqr 2499 |
. . . . . . . . . . . . . . 15
 

                                    |
155 | 154 | fveq2d 5869 |
. . . . . . . . . . . . . 14
 

                                              |
156 | 126, 155 | oveq12d 6308 |
. . . . . . . . . . . . 13
 

       
                                                                                  |
157 | | inss1 3652 |
. . . . . . . . . . . . . . . . 17
         |
158 | | ovolsscl 22439 |
. . . . . . . . . . . . . . . . 17
         
          
          |
159 | 157, 158 | mp3an1 1351 |
. . . . . . . . . . . . . . . 16
 
          
          |
160 | 2, 4, 159 | syl2anc 667 |
. . . . . . . . . . . . . . 15
 

               |
161 | 160 | recnd 9669 |
. . . . . . . . . . . . . 14
 

               |
162 | 16 | recnd 9669 |
. . . . . . . . . . . . . 14
 

                   |
163 | 161, 162 | addcomd 9835 |
. . . . . . . . . . . . 13
 

                   
                  
                           |
164 | 114, 156,
163 | 3eqtrd 2489 |
. . . . . . . . . . . 12
 

                         
                           |
165 | | seqp1 12228 |
. . . . . . . . . . . . . 14
    
                        |
166 | 94, 165 | syl 17 |
. . . . . . . . . . . . 13
 

                        |
167 | 100 | ineq2d 3634 |
. . . . . . . . . . . . . . . . 17
                   |
168 | 167 | fveq2d 5869 |
. . . . . . . . . . . . . . . 16
                             |
169 | | fvex 5875 |
. . . . . . . . . . . . . . . 16
              |
170 | 168, 76, 169 | fvmpt 5948 |
. . . . . . . . . . . . . . 15
                        |
171 | 117, 170 | syl 17 |
. . . . . . . . . . . . . 14
 

          
          |
172 | 171 | oveq2d 6306 |
. . . . . . . . . . . . 13
 

                                     |
173 | 166, 172 | eqtrd 2485 |
. . . . . . . . . . . 12
 

                               |
174 | 164, 173 | eqeq12d 2466 |
. . . . . . . . . . 11
 

                           
                      
                                 |
175 | 107, 174 | syl5ibr 225 |
. . . . . . . . . 10
 

                            
                         |
176 | 106, 175 | anim12d 566 |
. . . . . . . . 9
 

                
                  
 
                                          |
177 | 176 | expcom 437 |
. . . . . . . 8
    
                                                   
                          |
178 | 177 | a2d 29 |
. . . . . . 7
  
 
                                 
                   
                          |
179 | 43, 52, 61, 52, 85, 178 | nnind 10627 |
. . . . . 6
                  
                     |
180 | 179 | impcom 432 |
. . . . 5
 

 
                                   |
181 | 180 | simprd 465 |
. . . 4
 

                         |
182 | 181 | eqcomd 2457 |
. . 3
 

                         |
183 | 182 | oveq1d 6305 |
. 2
 

                      
                      |
184 | 180 | simpld 461 |
. . 3
 

            |
185 | | mblsplit 22486 |
. . 3
           
                
                 
              |
186 | 184, 2, 4, 185 | syl3anc 1268 |
. 2
 

                           
               |
187 | 34, 183, 186 | 3brtr4d 4433 |
1
 

                       |