Step | Hyp | Ref
| Expression |
1 | | ovolsca.3 |
. . . 4
       |
2 | | ssrab2 3500 |
. . . 4
     |
3 | 1, 2 | syl6eqss 3468 |
. . 3

  |
4 | | ovolcl 22509 |
. . 3

       |
5 | 3, 4 | syl 17 |
. 2
        |
6 | | ovolsca.7 |
. . . . . . . . . . . 12
          |
7 | | ovolfcl 22497 |
. . . . . . . . . . . 12
                                              |
8 | 6, 7 | sylan 479 |
. . . . . . . . . . 11
 

                                    |
9 | 8 | simp3d 1044 |
. . . . . . . . . 10
 

                  |
10 | 8 | simp1d 1042 |
. . . . . . . . . . 11
 

          |
11 | 8 | simp2d 1043 |
. . . . . . . . . . 11
 

          |
12 | | ovolsca.2 |
. . . . . . . . . . . . 13
   |
13 | 12 | rpregt0d 11370 |
. . . . . . . . . . . 12
     |
14 | 13 | adantr 472 |
. . . . . . . . . . 11
 

    |
15 | | lediv1 10492 |
. . . . . . . . . . 11
                  
          
       
                       |
16 | 10, 11, 14, 15 | syl3anc 1292 |
. . . . . . . . . 10
 

                          
             |
17 | 9, 16 | mpbid 215 |
. . . . . . . . 9
 

                      |
18 | | df-br 4396 |
. . . . . . . . 9
                                             |
19 | 17, 18 | sylib 201 |
. . . . . . . 8
 

                        |
20 | 12 | adantr 472 |
. . . . . . . . . 10
 

  |
21 | 10, 20 | rerpdivcld 11392 |
. . . . . . . . 9
 

            |
22 | 11, 20 | rerpdivcld 11392 |
. . . . . . . . 9
 

            |
23 | | opelxpi 4871 |
. . . . . . . . 9
                                                  |
24 | 21, 22, 23 | syl2anc 673 |
. . . . . . . 8
 

                           |
25 | 19, 24 | elind 3609 |
. . . . . . 7
 

                            |
26 | | ovolsca.6 |
. . . . . . 7
                          |
27 | 25, 26 | fmptd 6061 |
. . . . . 6
          |
28 | | eqid 2471 |
. . . . . . 7
    
  |
29 | | eqid 2471 |
. . . . . . 7
   
     
   |
30 | 28, 29 | ovolsf 22503 |
. . . . . 6
           
           |
31 | 27, 30 | syl 17 |
. . . . 5
    
           |
32 | | frn 5747 |
. . . . 5
   
        
   
 
     |
33 | 31, 32 | syl 17 |
. . . 4
            |
34 | | icossxr 11744 |
. . . 4
    |
35 | 33, 34 | syl6ss 3430 |
. . 3
         |
36 | | supxrcl 11625 |
. . 3
    
       
      |
37 | 35, 36 | syl 17 |
. 2
      
      |
38 | | ovolsca.4 |
. . . . 5
        |
39 | 38, 12 | rerpdivcld 11392 |
. . . 4
          |
40 | | ovolsca.9 |
. . . . 5
   |
41 | 40 | rpred 11364 |
. . . 4
   |
42 | 39, 41 | readdcld 9688 |
. . 3
            |
43 | 42 | rexrd 9708 |
. 2
            |
44 | 1 | eleq2d 2534 |
. . . . . . 7
         |
45 | | oveq2 6316 |
. . . . . . . . 9
 
     |
46 | 45 | eleq1d 2533 |
. . . . . . . 8
   
     |
47 | 46 | elrab 3184 |
. . . . . . 7
    
      |
48 | 44, 47 | syl6bb 269 |
. . . . . 6
   
     |
49 | | simprr 774 |
. . . . . . . . 9
 
         |
50 | | ovolsca.8 |
. . . . . . . . . . 11

     |
51 | | ovolsca.1 |
. . . . . . . . . . . 12

  |
52 | | ovolfioo 22498 |
. . . . . . . . . . . 12
 
    
       

        
            |
53 | 51, 6, 52 | syl2anc 673 |
. . . . . . . . . . 11
     

        
            |
54 | 50, 53 | mpbid 215 |
. . . . . . . . . 10
  
        
           |
55 | 54 | adantr 472 |
. . . . . . . . 9
 
     

        
           |
56 | | breq2 4399 |
. . . . . . . . . . . 12
           
        
    |
57 | | breq1 4398 |
. . . . . . . . . . . 12
   
       
             |
58 | 56, 57 | anbi12d 725 |
. . . . . . . . . . 11
            
        
          
              |
59 | 58 | rexbidv 2892 |
. . . . . . . . . 10
    
        
        
          
  
            |
60 | 59 | rspcv 3132 |
. . . . . . . . 9
    

        
                   
  
            |
61 | 49, 55, 60 | sylc 61 |
. . . . . . . 8
 
     
        
  
            |
62 | | opex 4664 |
. . . . . . . . . . . . . . . 16
                        |
63 | 26 | fvmpt2 5972 |
. . . . . . . . . . . . . . . 16
                                                       |
64 | 62, 63 | mpan2 685 |
. . . . . . . . . . . . . . 15
                              |
65 | 64 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                                      |
66 | | ovex 6336 |
. . . . . . . . . . . . . . 15
           |
67 | | ovex 6336 |
. . . . . . . . . . . . . . 15
           |
68 | 66, 67 | op1st 6820 |
. . . . . . . . . . . . . 14
                                      |
69 | 65, 68 | syl6eq 2521 |
. . . . . . . . . . . . 13
                     |
70 | 69 | adantl 473 |
. . . . . . . . . . . 12
    
                        |
71 | 70 | breq1d 4405 |
. . . . . . . . . . 11
    
            
             |
72 | 10 | adantlr 729 |
. . . . . . . . . . . 12
    
              |
73 | | simplrl 778 |
. . . . . . . . . . . 12
    
      |
74 | 14 | adantlr 729 |
. . . . . . . . . . . 12
    
    
   |
75 | | ltdivmul 10502 |
. . . . . . . . . . . 12
         

            
        
    |
76 | 72, 73, 74, 75 | syl3anc 1292 |
. . . . . . . . . . 11
    
              
        
    |
77 | 71, 76 | bitr2d 262 |
. . . . . . . . . 10
    
            
 
           |
78 | 11 | adantlr 729 |
. . . . . . . . . . . 12
    
              |
79 | | ltmuldiv2 10501 |
. . . . . . . . . . . 12
          
            
             |
80 | 73, 78, 74, 79 | syl3anc 1292 |
. . . . . . . . . . 11
    
      
       
             |
81 | 64 | fveq2d 5883 |
. . . . . . . . . . . . . 14
                                      |
82 | 66, 67 | op2nd 6821 |
. . . . . . . . . . . . . 14
                                      |
83 | 81, 82 | syl6eq 2521 |
. . . . . . . . . . . . 13
                     |
84 | 83 | adantl 473 |
. . . . . . . . . . . 12
    
                        |
85 | 84 | breq2d 4407 |
. . . . . . . . . . 11
    
    
       
             |
86 | 80, 85 | bitr4d 264 |
. . . . . . . . . 10
    
      
       
           |
87 | 77, 86 | anbi12d 725 |
. . . . . . . . 9
    
             
  
         
        
            |
88 | 87 | rexbidva 2889 |
. . . . . . . 8
 
                
  
        
         
            |
89 | 61, 88 | mpbid 215 |
. . . . . . 7
 
     
        
           |
90 | 89 | ex 441 |
. . . . . 6
               
            |
91 | 48, 90 | sylbid 223 |
. . . . 5
           
            |
92 | 91 | ralrimiv 2808 |
. . . 4
  
        
           |
93 | | ovolfioo 22498 |
. . . . 5
 
    
       

        
            |
94 | 3, 27, 93 | syl2anc 673 |
. . . 4
     

        
            |
95 | 92, 94 | mpbird 240 |
. . 3

     |
96 | 29 | ovollb 22510 |
. . 3
         
                 
  |
97 | 27, 95, 96 | syl2anc 673 |
. 2
               
  |
98 | | fzfid 12224 |
. . . . . . . 8
 

      |
99 | 12 | rpcnd 11366 |
. . . . . . . . 9
   |
100 | 99 | adantr 472 |
. . . . . . . 8
 

  |
101 | | simpl 464 |
. . . . . . . . . 10
 

  |
102 | | elfznn 11854 |
. . . . . . . . . 10
       |
103 | 11, 10 | resubcld 10068 |
. . . . . . . . . 10
 

                    |
104 | 101, 102,
103 | syl2an 485 |
. . . . . . . . 9
                             |
105 | 104 | recnd 9687 |
. . . . . . . 8
                             |
106 | 12 | rpne0d 11369 |
. . . . . . . . 9
   |
107 | 106 | adantr 472 |
. . . . . . . 8
 

  |
108 | 98, 100, 105, 107 | fsumdivc 13924 |
. . . . . . 7
 

                                                      |
109 | 83, 69 | oveq12d 6326 |
. . . . . . . . . . 11
                                           |
110 | 109 | adantl 473 |
. . . . . . . . . 10
 

                                          |
111 | 28 | ovolfsval 22501 |
. . . . . . . . . . 11
            
                        |
112 | 27, 111 | sylan 479 |
. . . . . . . . . 10
 

  
                        |
113 | 11 | recnd 9687 |
. . . . . . . . . . 11
 

          |
114 | 10 | recnd 9687 |
. . . . . . . . . . 11
 

          |
115 | 12 | rpcnne0d 11373 |
. . . . . . . . . . . 12
     |
116 | 115 | adantr 472 |
. . . . . . . . . . 11
 

    |
117 | | divsubdir 10325 |
. . . . . . . . . . 11
                  
                                              |
118 | 113, 114,
116, 117 | syl3anc 1292 |
. . . . . . . . . 10
 

                                            |
119 | 110, 112,
118 | 3eqtr4d 2515 |
. . . . . . . . 9
 

  
                          |
120 | 101, 102,
119 | syl2an 485 |
. . . . . . . 8
           
                          |
121 | | simpr 468 |
. . . . . . . . 9
 

  |
122 | | nnuz 11218 |
. . . . . . . . 9
     |
123 | 121, 122 | syl6eleq 2559 |
. . . . . . . 8
 

      |
124 | 103, 20 | rerpdivcld 11392 |
. . . . . . . . . 10
 

                      |
125 | 124 | recnd 9687 |
. . . . . . . . 9
 

                      |
126 | 101, 102,
125 | syl2an 485 |
. . . . . . . 8
                               |
127 | 120, 123,
126 | fsumser 13873 |
. . . . . . 7
 

                             
       |
128 | 108, 127 | eqtrd 2505 |
. . . . . 6
 

                             
       |
129 | | ovolsca.10 |
. . . . . . . . . . 11
                |
130 | | eqid 2471 |
. . . . . . . . . . . . . . . 16
    
  |
131 | | ovolsca.5 |
. . . . . . . . . . . . . . . 16
   
   |
132 | 130, 131 | ovolsf 22503 |
. . . . . . . . . . . . . . 15
                 |
133 | 6, 132 | syl 17 |
. . . . . . . . . . . . . 14
          |
134 | | frn 5747 |
. . . . . . . . . . . . . 14
       
     |
135 | 133, 134 | syl 17 |
. . . . . . . . . . . . 13
  
   |
136 | 135, 34 | syl6ss 3430 |
. . . . . . . . . . . 12
   |
137 | 12, 40 | rpmulcld 11380 |
. . . . . . . . . . . . . . 15
     |
138 | 137 | rpred 11364 |
. . . . . . . . . . . . . 14
     |
139 | 38, 138 | readdcld 9688 |
. . . . . . . . . . . . 13
            |
140 | 139 | rexrd 9708 |
. . . . . . . . . . . 12
            |
141 | | supxrleub 11637 |
. . . . . . . . . . . 12
                         
             |
142 | 136, 140,
141 | syl2anc 673 |
. . . . . . . . . . 11
              
             |
143 | 129, 142 | mpbid 215 |
. . . . . . . . . 10
 
           |
144 | | ffn 5739 |
. . . . . . . . . . . 12
       
  |
145 | 133, 144 | syl 17 |
. . . . . . . . . . 11
   |
146 | | breq1 4398 |
. . . . . . . . . . . 12
     
        
                |
147 | 146 | ralrn 6040 |
. . . . . . . . . . 11
  
        
                 |
148 | 145, 147 | syl 17 |
. . . . . . . . . 10
  
                          |
149 | 143, 148 | mpbid 215 |
. . . . . . . . 9
                 |
150 | 149 | r19.21bi 2776 |
. . . . . . . 8
 

               |
151 | 6 | adantr 472 |
. . . . . . . . . . 11
 

   
     |
152 | 130 | ovolfsval 22501 |
. . . . . . . . . . 11
            
                        |
153 | 151, 102,
152 | syl2an 485 |
. . . . . . . . . 10
           
                        |
154 | 153, 123,
105 | fsumser 13873 |
. . . . . . . . 9
 

                           
       |
155 | 131 | fveq1i 5880 |
. . . . . . . . 9
              |
156 | 154, 155 | syl6eqr 2523 |
. . . . . . . 8
 

                              |
157 | 39 | recnd 9687 |
. . . . . . . . . . 11
          |
158 | 40 | rpcnd 11366 |
. . . . . . . . . . 11
   |
159 | 99, 157, 158 | adddid 9685 |
. . . . . . . . . 10
                           |
160 | 38 | recnd 9687 |
. . . . . . . . . . . 12
        |
161 | 160, 99, 106 | divcan2d 10407 |
. . . . . . . . . . 11
                 |
162 | 161 | oveq1d 6323 |
. . . . . . . . . 10
                         |
163 | 159, 162 | eqtrd 2505 |
. . . . . . . . 9
                       |
164 | 163 | adantr 472 |
. . . . . . . 8
 

                      |
165 | 150, 156,
164 | 3brtr4d 4426 |
. . . . . . 7
 

                                     |
166 | 98, 104 | fsumrecl 13877 |
. . . . . . . 8
 

                          |
167 | 42 | adantr 472 |
. . . . . . . 8
 

           |
168 | 13 | adantr 472 |
. . . . . . . 8
 

    |
169 | | ledivmul 10503 |
. . . . . . . 8
  
                                
                                                                            |
170 | 166, 167,
168, 169 | syl3anc 1292 |
. . . . . . 7
 

  
                                                                       |
171 | 165, 170 | mpbird 240 |
. . . . . 6
 

                         
           |
172 | 128, 171 | eqbrtrrd 4418 |
. . . . 5
 

   
    
           |
173 | 172 | ralrimiva 2809 |
. . . 4
     
                |
174 | | ffn 5739 |
. . . . . 6
   
            
    |
175 | 31, 174 | syl 17 |
. . . . 5
    
    |
176 | | breq1 4398 |
. . . . . 6
    
                  
                 |
177 | 176 | ralrn 6040 |
. . . . 5
   
       
           
    
                 |
178 | 175, 177 | syl 17 |
. . . 4
      
           
    
                 |
179 | 173, 178 | mpbird 240 |
. . 3
     
              |
180 | | supxrleub 11637 |
. . . 4
                        
            
                    |
181 | 35, 43, 180 | syl2anc 673 |
. . 3
       
   
             
               |
182 | 179, 181 | mpbird 240 |
. 2
      
               |
183 | 5, 37, 43, 97, 182 | xrletrd 11482 |
1
                 |