Step | Hyp | Ref
| Expression |
1 | | fveq2 5865 |
. . . . . 6

voln*  voln*    |
2 | 1 | fveq1d 5867 |
. . . . 5

 voln*           voln*            |
3 | 2 | adantl 468 |
. . . 4
 

 voln*           voln*            |
4 | | ovnsubadd.2 |
. . . . . . . . . . . 12
          |
5 | 4 | adantr 467 |
. . . . . . . . . . 11
 

         |
6 | | simpr 463 |
. . . . . . . . . . 11
 

  |
7 | 5, 6 | ffvelrnd 6023 |
. . . . . . . . . 10
 

         |
8 | | elpwi 3960 |
. . . . . . . . . 10
           
    |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
 

    
   |
10 | 9 | ralrimiva 2802 |
. . . . . . . 8
          |
11 | | iunss 4319 |
. . . . . . . 8
 
               |
12 | 10, 11 | sylibr 216 |
. . . . . . 7
          |
13 | 12 | adantr 467 |
. . . . . 6
 

         |
14 | | oveq2 6298 |
. . . . . . 7

      |
15 | 14 | adantl 468 |
. . . . . 6
 

      |
16 | 13, 15 | sseqtrd 3468 |
. . . . 5
 

         |
17 | 16 | ovn0val 38372 |
. . . 4
 

 voln*            |
18 | 3, 17 | eqtrd 2485 |
. . 3
 

 voln*            |
19 | | nnex 10615 |
. . . . . 6
 |
20 | 19 | a1i 11 |
. . . . 5
   |
21 | | ovnsubadd.1 |
. . . . . . . 8
   |
22 | 21 | adantr 467 |
. . . . . . 7
 

  |
23 | 22, 9 | ovncl 38389 |
. . . . . 6
 

 voln*              |
24 | | eqid 2451 |
. . . . . 6
  voln*            voln*           |
25 | 23, 24 | fmptd 6046 |
. . . . 5
   voln*                   |
26 | 20, 25 | sge0ge0 38226 |
. . . 4

Σ^   voln*             |
27 | 26 | adantr 467 |
. . 3
 

Σ^   voln*             |
28 | 18, 27 | eqbrtrd 4423 |
. 2
 

 voln*          Σ^   voln*             |
29 | 21, 12 | ovnxrcl 38391 |
. . . 4
  voln*            |
30 | 29 | adantr 467 |
. . 3
 
  voln*            |
31 | 20, 25 | sge0xrcl 38227 |
. . . 4
 Σ^   voln*             |
32 | 31 | adantr 467 |
. . 3
 
 Σ^   voln*             |
33 | 21 | ad2antrr 732 |
. . . 4
  


  |
34 | | neqne 37374 |
. . . . 5
   |
35 | 34 | ad2antlr 733 |
. . . 4
  

   |
36 | 4 | ad2antrr 732 |
. . . 4
  

          |
37 | | simpr 463 |
. . . 4
  

   |
38 | | eqid 2451 |
. . . 4
     
         
 
       
Σ^                           
         
 
       
Σ^                       |
39 | | sseq1 3453 |
. . . . . 6
 
                           |
40 | 39 | rabbidv 3036 |
. . . . 5
       
            
      
 
 
           |
41 | 40 | cbvmptv 4495 |
. . . 4
          
                        
               |
42 | | eqid 2451 |
. . . 4
     
                             |
43 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . . . 22
           |
44 | 43 | coeq2d 4997 |
. . . . . . . . . . . . . . . . . . . . 21
               |
45 | 44 | fveq1d 5867 |
. . . . . . . . . . . . . . . . . . . 20
  
                    |
46 | 45 | ixpeq2dv 7538 |
. . . . . . . . . . . . . . . . . . 19
 
          
 
          |
47 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . . 20
  
                    |
48 | 47 | cbvixpv 7540 |
. . . . . . . . . . . . . . . . . . 19

          
 
         |
49 | 46, 48 | syl6eq 2501 |
. . . . . . . . . . . . . . . . . 18
 
          
 
          |
50 | 49 | cbviunv 4317 |
. . . . . . . . . . . . . . . . 17
                         |
51 | 50 | sseq2i 3457 |
. . . . . . . . . . . . . . . 16
                           |
52 | 51 | a1i 11 |
. . . . . . . . . . . . . . 15
      
                            |
53 | 52 | rabbiia 3033 |
. . . . . . . . . . . . . 14
      
            
      
 
 
          |
54 | 53 | mpteq2i 4486 |
. . . . . . . . . . . . 13
          
                        
               |
55 | 54 | fveq1i 5866 |
. . . . . . . . . . . 12
           
                            
                  |
56 | | fveq2 5865 |
. . . . . . . . . . . 12
    
     
 
                    
     
 
                   |
57 | 55, 56 | syl5eq 2497 |
. . . . . . . . . . 11
    
     
 
                    
     
 
                   |
58 | 57 | eleq2d 2514 |
. . . . . . . . . 10
             
                
   
     
 
                    |
59 | | fveq2 5865 |
. . . . . . . . . . . . . . . . . . 19
  
            |
60 | 59 | fveq2d 5869 |
. . . . . . . . . . . . . . . . . 18
               
       |
61 | 60 | cbvprodv 13970 |
. . . . . . . . . . . . . . . . 17

                      |
62 | 61 | mpteq2i 4486 |
. . . . . . . . . . . . . . . 16
     
                             |
63 | 62 | a1i 11 |
. . . . . . . . . . . . . . 15
                       
             |
64 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
           |
65 | 63, 64 | fveq12d 5871 |
. . . . . . . . . . . . . 14
                                
                    |
66 | 65 | cbvmptv 4495 |
. . . . . . . . . . . . 13
                                                       |
67 | 66 | fveq2i 5868 |
. . . . . . . . . . . 12
Σ^      
                      Σ^                              |
68 | 67 | a1i 11 |
. . . . . . . . . . 11
 Σ^                             Σ^                               |
69 | | fveq2 5865 |
. . . . . . . . . . . 12
  voln*      voln*       |
70 | 69 | oveq1d 6305 |
. . . . . . . . . . 11
   voln*           voln*           |
71 | 68, 70 | breq12d 4415 |
. . . . . . . . . 10
  Σ^      
                        voln*         Σ^      
                        voln*            |
72 | 58, 71 | anbi12d 717 |
. . . . . . . . 9
      
     
 
                 Σ^                               voln*         
            
                
Σ^      
                        voln*             |
73 | 72 | rabbidva2 3034 |
. . . . . . . 8
             
                 Σ^      
                        voln*                      
                 Σ^      
                        voln*            |
74 | | fveq1 5864 |
. . . . . . . . . . . . 13
           |
75 | 74 | fveq2d 5869 |
. . . . . . . . . . . 12
                                
                    |
76 | 75 | mpteq2dv 4490 |
. . . . . . . . . . 11
                                                         |
77 | 76 | fveq2d 5869 |
. . . . . . . . . 10
 Σ^                             Σ^                               |
78 | 77 | breq1d 4412 |
. . . . . . . . 9
  Σ^      
                        voln*         Σ^      
                        voln*            |
79 | 78 | cbvrabv 3044 |
. . . . . . . 8
            
                 Σ^      
                        voln*                      
                 Σ^      
                        voln*           |
80 | 73, 79 | syl6eq 2501 |
. . . . . . 7
             
                 Σ^      
                        voln*                      
                 Σ^      
                        voln*            |
81 | 80 | mpteq2dv 4490 |
. . . . . 6
              
                 Σ^      
                        voln*                
     
 
                 Σ^                               voln*             |
82 | | oveq2 6298 |
. . . . . . . . 9
   voln*           voln*           |
83 | 82 | breq2d 4414 |
. . . . . . . 8
  Σ^      
                        voln*         Σ^      
                        voln*            |
84 | 83 | rabbidv 3036 |
. . . . . . 7
             
                 Σ^      
                        voln*                      
                 Σ^      
                        voln*            |
85 | 84 | cbvmptv 4495 |
. . . . . 6

            
                 Σ^      
                        voln*                
     
 
                 Σ^                               voln*            |
86 | 81, 85 | syl6eq 2501 |
. . . . 5
              
                 Σ^      
                        voln*                
     
 
                 Σ^                               voln*             |
87 | 86 | cbvmptv 4495 |
. . . 4
                 
                 Σ^      
                        voln*                
            
                 Σ^      
                        voln*             |
88 | 33, 35, 36, 37, 38, 41, 42, 87 | ovnsubaddlem2 38393 |
. . 3
  

  voln*           Σ^   voln*                 |
89 | 30, 32, 88 | xrlexaddrp 37575 |
. 2
 
  voln*          Σ^   voln*             |
90 | 28, 89 | pm2.61dan 800 |
1
  voln*          Σ^   voln*             |