Step | Hyp | Ref
| Expression |
1 | | unieq 4206 |
. . . . . . . . . . 11

    |
2 | | uni0 4225 |
. . . . . . . . . . 11
  |
3 | 1, 2 | syl6eq 2501 |
. . . . . . . . . 10

   |
4 | 3 | ineq2d 3634 |
. . . . . . . . 9

       |
5 | | in0 3760 |
. . . . . . . . 9
   |
6 | 4, 5 | syl6eq 2501 |
. . . . . . . 8

     |
7 | 6 | fveq2d 5869 |
. . . . . . 7

             |
8 | | hash0 12548 |
. . . . . . 7
     |
9 | 7, 8 | syl6eq 2501 |
. . . . . 6

         |
10 | 9 | oveq2d 6306 |
. . . . 5

        
            |
11 | | pweq 3954 |
. . . . . . 7

    |
12 | | pw0 4119 |
. . . . . . 7
    |
13 | 11, 12 | syl6eq 2501 |
. . . . . 6

     |
14 | 13 | sumeq1d 13767 |
. . . . 5

               
    
               
      |
15 | 10, 14 | eqeq12d 2466 |
. . . 4

                             
   
      
               
       |
16 | 15 | ralbidv 2827 |
. . 3

 
        
                   
   
                       
       |
17 | | unieq 4206 |
. . . . . . . 8
     |
18 | 17 | ineq2d 3634 |
. . . . . . 7
 
       |
19 | 18 | fveq2d 5869 |
. . . . . 6
           
     |
20 | 19 | oveq2d 6306 |
. . . . 5
         
                   |
21 | | pweq 3954 |
. . . . . 6
 
   |
22 | 21 | sumeq1d 13767 |
. . . . 5
                
    
                     |
23 | 20, 22 | eqeq12d 2466 |
. . . 4
                              
   
             
                      |
24 | 23 | ralbidv 2827 |
. . 3
  
                            
   
                             
       |
25 | | unieq 4206 |
. . . . . . . . 9
             |
26 | | uniun 4217 |
. . . . . . . . . 10
            |
27 | | vex 3048 |
. . . . . . . . . . . 12
 |
28 | 27 | unisn 4213 |
. . . . . . . . . . 11
    |
29 | 28 | uneq2i 3585 |
. . . . . . . . . 10
 
        |
30 | 26, 29 | eqtri 2473 |
. . . . . . . . 9
         |
31 | 25, 30 | syl6eq 2501 |
. . . . . . . 8
           |
32 | 31 | ineq2d 3634 |
. . . . . . 7
          
    |
33 | 32 | fveq2d 5869 |
. . . . . 6
        
              |
34 | 33 | oveq2d 6306 |
. . . . 5
                                   |
35 | | pweq 3954 |
. . . . . 6
             |
36 | 35 | sumeq1d 13767 |
. . . . 5
                    
    
                  
      |
37 | 34, 36 | eqeq12d 2466 |
. . . 4
              
                   
   
                                          |
38 | 37 | ralbidv 2827 |
. . 3
                                   
   
                                           |
39 | | unieq 4206 |
. . . . . . . 8
     |
40 | 39 | ineq2d 3634 |
. . . . . . 7
 
       |
41 | 40 | fveq2d 5869 |
. . . . . 6
           
     |
42 | 41 | oveq2d 6306 |
. . . . 5
         
                   |
43 | | pweq 3954 |
. . . . . 6
 
   |
44 | 43 | sumeq1d 13767 |
. . . . 5
                
    
                     |
45 | 42, 44 | eqeq12d 2466 |
. . . 4
                              
   
             
                      |
46 | 45 | ralbidv 2827 |
. . 3
  
                            
   
                             
       |
47 | | hashcl 12538 |
. . . . . . 7
       |
48 | 47 | nn0cnd 10927 |
. . . . . 6
       |
49 | 48 | mulid2d 9661 |
. . . . 5
             |
50 | | 0ex 4535 |
. . . . . 6
 |
51 | 49, 48 | eqeltrd 2529 |
. . . . . 6
         |
52 | | fveq2 5865 |
. . . . . . . . . . 11

          |
53 | 52, 8 | syl6eq 2501 |
. . . . . . . . . 10

      |
54 | 53 | oveq2d 6306 |
. . . . . . . . 9

                |
55 | | neg1cn 10713 |
. . . . . . . . . 10
  |
56 | | exp0 12276 |
. . . . . . . . . 10
         |
57 | 55, 56 | ax-mp 5 |
. . . . . . . . 9
      |
58 | 54, 57 | syl6eq 2501 |
. . . . . . . 8

           |
59 | | rint0 4275 |
. . . . . . . . 9

     |
60 | 59 | fveq2d 5869 |
. . . . . . . 8

             |
61 | 58, 60 | oveq12d 6308 |
. . . . . . 7

             
            |
62 | 61 | sumsn 13807 |
. . . . . 6
 
                       
            |
63 | 50, 51, 62 | sylancr 669 |
. . . . 5
                 
            |
64 | 48 | subid1d 9975 |
. . . . 5
             |
65 | 49, 63, 64 | 3eqtr4rd 2496 |
. . . 4
                       
      |
66 | 65 | rgen 2747 |
. . 3
                       
     |
67 | | fveq2 5865 |
. . . . . . . . . . . 12
           |
68 | | ineq1 3627 |
. . . . . . . . . . . . 13
 
       |
69 | 68 | fveq2d 5869 |
. . . . . . . . . . . 12
           
     |
70 | 67, 69 | oveq12d 6308 |
. . . . . . . . . . 11
         
                   |
71 | | simpl 459 |
. . . . . . . . . . . . . . 15
 
 
  |
72 | 71 | ineq1d 3633 |
. . . . . . . . . . . . . 14
 
 
        |
73 | 72 | fveq2d 5869 |
. . . . . . . . . . . . 13
 
 
   
            |
74 | 73 | oveq2d 6306 |
. . . . . . . . . . . 12
 
 
             
                        |
75 | 74 | sumeq2dv 13769 |
. . . . . . . . . . 11
                
    
                     |
76 | 70, 75 | eqeq12d 2466 |
. . . . . . . . . 10
                              
   
             
                      |
77 | 76 | rspcva 3148 |
. . . . . . . . 9
           
                   
                                 
      |
78 | 77 | adantll 720 |
. . . . . . . 8
   
  
        
                   
                                 
      |
79 | | simpr 463 |
. . . . . . . . . 10
       |
80 | | inss1 3652 |
. . . . . . . . . 10
   |
81 | | ssfi 7792 |
. . . . . . . . . 10
  

     |
82 | 79, 80, 81 | sylancl 668 |
. . . . . . . . 9
     
   |
83 | | fveq2 5865 |
. . . . . . . . . . . 12
          
    |
84 | | ineq1 3627 |
. . . . . . . . . . . . . 14
   
         |
85 | | in32 3644 |
. . . . . . . . . . . . . . 15
           |
86 | | inass 3642 |
. . . . . . . . . . . . . . 15
   
       |
87 | 85, 86 | eqtri 2473 |
. . . . . . . . . . . . . 14
           |
88 | 84, 87 | syl6eq 2501 |
. . . . . . . . . . . . 13
   
         |
89 | 88 | fveq2d 5869 |
. . . . . . . . . . . 12
             
       |
90 | 83, 89 | oveq12d 6308 |
. . . . . . . . . . 11
           
        
       
      |
91 | | ineq1 3627 |
. . . . . . . . . . . . . . 15
   
         |
92 | | in32 3644 |
. . . . . . . . . . . . . . . 16
           |
93 | | inass 3642 |
. . . . . . . . . . . . . . . 16
   
       |
94 | 92, 93 | eqtri 2473 |
. . . . . . . . . . . . . . 15
       
   |
95 | 91, 94 | syl6eq 2501 |
. . . . . . . . . . . . . 14
   
         |
96 | 95 | fveq2d 5869 |
. . . . . . . . . . . . 13
             
       |
97 | 96 | oveq2d 6306 |
. . . . . . . . . . . 12
                
                          |
98 | 97 | sumeq2sdv 13770 |
. . . . . . . . . . 11
                  
    
                       |
99 | 90, 98 | eqeq12d 2466 |
. . . . . . . . . 10
                                
   
                                
         |
100 | 99 | rspcva 3148 |
. . . . . . . . 9
             
                   
         
       
                   
        |
101 | 82, 100 | sylan 474 |
. . . . . . . 8
   
  
        
                   
         
       
                   
        |
102 | 78, 101 | oveq12d 6308 |
. . . . . . 7
   
  
        
                   
                                                     
    
                        |
103 | | inss1 3652 |
. . . . . . . . . . . . . 14
    |
104 | | ssfi 7792 |
. . . . . . . . . . . . . 14
  
 
      |
105 | 79, 103, 104 | sylancl 668 |
. . . . . . . . . . . . 13
     
    |
106 | | hashun3 12563 |
. . . . . . . . . . . . 13
               
        
                 
      |
107 | 105, 82, 106 | syl2anc 667 |
. . . . . . . . . . . 12
                            
                 |
108 | | indi 3689 |
. . . . . . . . . . . . 13
         
   |
109 | 108 | fveq2i 5868 |
. . . . . . . . . . . 12
     
          
    |
110 | | inindi 3649 |
. . . . . . . . . . . . . 14
         
   |
111 | 110 | fveq2i 5868 |
. . . . . . . . . . . . 13
     
          
    |
112 | 111 | oveq2i 6301 |
. . . . . . . . . . . 12
     
             
           
                 
     |
113 | 107, 109,
112 | 3eqtr4g 2510 |
. . . . . . . . . . 11
                          
               |
114 | | hashcl 12538 |
. . . . . . . . . . . . . 14
             |
115 | 105, 114 | syl 17 |
. . . . . . . . . . . . 13
              |
116 | 115 | nn0cnd 10927 |
. . . . . . . . . . . 12
              |
117 | | hashcl 12538 |
. . . . . . . . . . . . . 14
           |
118 | 82, 117 | syl 17 |
. . . . . . . . . . . . 13
             |
119 | 118 | nn0cnd 10927 |
. . . . . . . . . . . 12
             |
120 | | inss1 3652 |
. . . . . . . . . . . . . . 15
      |
121 | | ssfi 7792 |
. . . . . . . . . . . . . . 15
  
 
  
       |
122 | 79, 120, 121 | sylancl 668 |
. . . . . . . . . . . . . 14
     
      |
123 | | hashcl 12538 |
. . . . . . . . . . . . . 14
                 |
124 | 122, 123 | syl 17 |
. . . . . . . . . . . . 13
                |
125 | 124 | nn0cnd 10927 |
. . . . . . . . . . . 12
                |
126 | 116, 119,
125 | addsubassd 10006 |
. . . . . . . . . . 11
          
             
          
       
       
       |
127 | 113, 126 | eqtrd 2485 |
. . . . . . . . . 10
                          
       
       |
128 | 127 | oveq2d 6306 |
. . . . . . . . 9
             
 
                                      |
129 | | hashcl 12538 |
. . . . . . . . . . . 12
       |
130 | 129 | adantl 468 |
. . . . . . . . . . 11
           |
131 | 130 | nn0cnd 10927 |
. . . . . . . . . 10
           |
132 | 119, 125 | subcld 9986 |
. . . . . . . . . 10
               
        |
133 | 131, 116,
132 | subsub4d 10017 |
. . . . . . . . 9
                                                                       |
134 | 128, 133 | eqtr4d 2488 |
. . . . . . . 8
             
 
                                      |
135 | 134 | adantr 467 |
. . . . . . 7
   
  
        
                   
               
             
        
       
       |
136 | | disjdif 3839 |
. . . . . . . . . . 11
            |
137 | 136 | a1i 11 |
. . . . . . . . . 10
      
           |
138 | | ssun1 3597 |
. . . . . . . . . . . . . 14
     |
139 | | sspwb 4649 |
. . . . . . . . . . . . . 14
     
       |
140 | 138, 139 | mpbi 212 |
. . . . . . . . . . . . 13
       |
141 | | undif 3848 |
. . . . . . . . . . . . 13
 
    
 
                |
142 | 140, 141 | mpbi 212 |
. . . . . . . . . . . 12
                 |
143 | 142 | eqcomi 2460 |
. . . . . . . . . . 11
                 |
144 | 143 | a1i 11 |
. . . . . . . . . 10
                       |
145 | | simpll 760 |
. . . . . . . . . . . 12
       |
146 | | snfi 7650 |
. . . . . . . . . . . 12
   |
147 | | unfi 7838 |
. . . . . . . . . . . 12
           |
148 | 145, 146,
147 | sylancl 668 |
. . . . . . . . . . 11
           |
149 | | pwfi 7869 |
. . . . . . . . . . 11
            |
150 | 148, 149 | sylib 200 |
. . . . . . . . . 10
            |
151 | 55 | a1i 11 |
. . . . . . . . . . . 12
   
       
   |
152 | | elpwi 3960 |
. . . . . . . . . . . . . 14
     
      |
153 | | ssfi 7792 |
. . . . . . . . . . . . . 14
     
       |
154 | 148, 152,
153 | syl2an 480 |
. . . . . . . . . . . . 13
   
       
  |
155 | | hashcl 12538 |
. . . . . . . . . . . . 13
       |
156 | 154, 155 | syl 17 |
. . . . . . . . . . . 12
   
       
      |
157 | 151, 156 | expcld 12416 |
. . . . . . . . . . 11
   
       
           |
158 | | simplr 762 |
. . . . . . . . . . . . . 14
   
       
  |
159 | | inss1 3652 |
. . . . . . . . . . . . . 14
    |
160 | | ssfi 7792 |
. . . . . . . . . . . . . 14
  
 
      |
161 | 158, 159,
160 | sylancl 668 |
. . . . . . . . . . . . 13
   
       
     |
162 | | hashcl 12538 |
. . . . . . . . . . . . 13
             |
163 | 161, 162 | syl 17 |
. . . . . . . . . . . 12
   
       
   
     |
164 | 163 | nn0cnd 10927 |
. . . . . . . . . . 11
   
       
   
     |
165 | 157, 164 | mulcld 9663 |
. . . . . . . . . 10
   
       
             
      |
166 | 137, 144,
150, 165 | fsumsplit 13806 |
. . . . . . . . 9
                                             
    
                      
       |
167 | | fveq2 5865 |
. . . . . . . . . . . . . 14
                   |
168 | 167 | oveq2d 6306 |
. . . . . . . . . . . . 13
                             |
169 | | inteq 4237 |
. . . . . . . . . . . . . . . 16
             |
170 | 27 | intunsn 4274 |
. . . . . . . . . . . . . . . 16
         |
171 | 169, 170 | syl6eq 2501 |
. . . . . . . . . . . . . . 15
           |
172 | 171 | ineq2d 3634 |
. . . . . . . . . . . . . 14
               |
173 | 172 | fveq2d 5869 |
. . . . . . . . . . . . 13
        
        
     |
174 | 168, 173 | oveq12d 6308 |
. . . . . . . . . . . 12
                  
                     
        |
175 | | pwfi 7869 |
. . . . . . . . . . . . 13

   |
176 | 145, 175 | sylib 200 |
. . . . . . . . . . . 12
     
  |
177 | | eqid 2451 |
. . . . . . . . . . . . 13
               |
178 | | elpwi 3960 |
. . . . . . . . . . . . . . . . 17
    |
179 | 178 | adantl 468 |
. . . . . . . . . . . . . . . 16
   
      |
180 | | unss1 3603 |
. . . . . . . . . . . . . . . 16
           |
181 | 179, 180 | syl 17 |
. . . . . . . . . . . . . . 15
   
              |
182 | | vex 3048 |
. . . . . . . . . . . . . . . . 17
 |
183 | | snex 4641 |
. . . . . . . . . . . . . . . . 17
   |
184 | 182, 183 | unex 6589 |
. . . . . . . . . . . . . . . 16
     |
185 | 184 | elpw 3957 |
. . . . . . . . . . . . . . 15
         
          |
186 | 181, 185 | sylibr 216 |
. . . . . . . . . . . . . 14
   
               |
187 | | simpllr 769 |
. . . . . . . . . . . . . . 15
   
   
  |
188 | | elpwi 3960 |
. . . . . . . . . . . . . . . 16
            |
189 | | ssun2 3598 |
. . . . . . . . . . . . . . . . . . 19
 
     |
190 | 27 | snss 4096 |
. . . . . . . . . . . . . . . . . . 19
       
     |
191 | 189, 190 | mpbir 213 |
. . . . . . . . . . . . . . . . . 18
     |
192 | 191 | a1i 11 |
. . . . . . . . . . . . . . . . 17
   
          |
193 | | ssel 3426 |
. . . . . . . . . . . . . . . . 17
             |
194 | 192, 193 | syl5com 31 |
. . . . . . . . . . . . . . . 16
   
            |
195 | 188, 194 | syl5 33 |
. . . . . . . . . . . . . . 15
   
             |
196 | 187, 195 | mtod 181 |
. . . . . . . . . . . . . 14
   
           |
197 | 186, 196 | eldifd 3415 |
. . . . . . . . . . . . 13
   
                  |
198 | | eldifi 3555 |
. . . . . . . . . . . . . . . . . 18
                |
199 | 198 | adantl 468 |
. . . . . . . . . . . . . . . . 17
   
                  |
200 | 199 | elpwid 3961 |
. . . . . . . . . . . . . . . 16
   
                 |
201 | | uncom 3578 |
. . . . . . . . . . . . . . . 16
         |
202 | 200, 201 | syl6sseq 3478 |
. . . . . . . . . . . . . . 15
   
                 |
203 | | ssundif 3851 |
. . . . . . . . . . . . . . 15
           |
204 | 202, 203 | sylib 200 |
. . . . . . . . . . . . . 14
   
           
     |
205 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
206 | 205 | elpw2 4567 |
. . . . . . . . . . . . . 14
            |
207 | 204, 206 | sylibr 216 |
. . . . . . . . . . . . 13
   
           
      |
208 | | elpwunsn 4012 |
. . . . . . . . . . . . . . . . . . 19
           |
209 | 208 | ad2antll 735 |
. . . . . . . . . . . . . . . . . 18
   
   
            |
210 | 209 | snssd 4117 |
. . . . . . . . . . . . . . . . 17
   
   
              |
211 | | ssequn2 3607 |
. . . . . . . . . . . . . . . . 17
         |
212 | 210, 211 | sylib 200 |
. . . . . . . . . . . . . . . 16
   
   
                |
213 | 212 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
   
   
                |
214 | | uneq1 3581 |
. . . . . . . . . . . . . . . . 17
                   |
215 | | undif1 3842 |
. . . . . . . . . . . . . . . . 17
             |
216 | 214, 215 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
               |
217 | 216 | eqeq2d 2461 |
. . . . . . . . . . . . . . 15
         
       |
218 | 213, 217 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
   
   
                      |
219 | 178 | ad2antrl 734 |
. . . . . . . . . . . . . . . . . 18
   
   
            |
220 | | simpllr 769 |
. . . . . . . . . . . . . . . . . 18
   
   
         
  |
221 | 219, 220 | ssneldd 3435 |
. . . . . . . . . . . . . . . . 17
   
   
         
  |
222 | | difsnb 4114 |
. . . . . . . . . . . . . . . . 17

      |
223 | 221, 222 | sylib 200 |
. . . . . . . . . . . . . . . 16
   
   
                |
224 | 223 | eqcomd 2457 |
. . . . . . . . . . . . . . 15
   
   
                |
225 | | difeq1 3544 |
. . . . . . . . . . . . . . . . 17
                   |
226 | | difun2 3847 |
. . . . . . . . . . . . . . . . 17
             |
227 | 225, 226 | syl6eq 2501 |
. . . . . . . . . . . . . . . 16
               |
228 | 227 | eqeq2d 2461 |
. . . . . . . . . . . . . . 15
         

      |
229 | 224, 228 | syl5ibrcom 226 |
. . . . . . . . . . . . . 14
   
   
              
       |
230 | 218, 229 | impbid 194 |
. . . . . . . . . . . . 13
   
   
              

      |
231 | 177, 197,
207, 230 | f1o2d 6521 |
. . . . . . . . . . . 12
                           |
232 | | uneq1 3581 |
. . . . . . . . . . . . . 14
           |
233 | | vex 3048 |
. . . . . . . . . . . . . . 15
 |
234 | 233, 183 | unex 6589 |
. . . . . . . . . . . . . 14
     |
235 | 232, 177,
234 | fvmpt 5948 |
. . . . . . . . . . . . 13
                   |
236 | 235 | adantl 468 |
. . . . . . . . . . . 12
   
                     |
237 | 198, 165 | sylan2 477 |
. . . . . . . . . . . 12
   
                        
      |
238 | 174, 176,
231, 236, 237 | fsumf1o 13789 |
. . . . . . . . . . 11
                            
    
                  
        |
239 | | uneq1 3581 |
. . . . . . . . . . . . . . . 16
           |
240 | 239 | fveq2d 5869 |
. . . . . . . . . . . . . . 15
                   |
241 | 240 | oveq2d 6306 |
. . . . . . . . . . . . . 14
                             |
242 | | inteq 4237 |
. . . . . . . . . . . . . . . . 17
     |
243 | 242 | ineq1d 3633 |
. . . . . . . . . . . . . . . 16
  
      |
244 | 243 | ineq2d 3634 |
. . . . . . . . . . . . . . 15
 
           |
245 | 244 | fveq2d 5869 |
. . . . . . . . . . . . . 14
             
       |
246 | 241, 245 | oveq12d 6308 |
. . . . . . . . . . . . 13
                                                   |
247 | 246 | cbvsumv 13762 |
. . . . . . . . . . . 12
                                                     |
248 | | elpwi 3960 |
. . . . . . . . . . . . . . . . . . . 20
 
  |
249 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . . . 20
     |
250 | 145, 248,
249 | syl2an 480 |
. . . . . . . . . . . . . . . . . . 19
   
      |
251 | 248 | adantl 468 |
. . . . . . . . . . . . . . . . . . . 20
   
   
  |
252 | | simpllr 769 |
. . . . . . . . . . . . . . . . . . . 20
   
   
  |
253 | 251, 252 | ssneldd 3435 |
. . . . . . . . . . . . . . . . . . 19
   
   
  |
254 | | hashunsng 12571 |
. . . . . . . . . . . . . . . . . . . 20
   
                 |
255 | 27, 254 | ax-mp 5 |
. . . . . . . . . . . . . . . . . . 19
 

                |
256 | 250, 253,
255 | syl2anc 667 |
. . . . . . . . . . . . . . . . . 18
   
                    |
257 | 256 | oveq2d 6306 |
. . . . . . . . . . . . . . . . 17
   
                              |
258 | 55 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
   
       |
259 | 250, 155 | syl 17 |
. . . . . . . . . . . . . . . . . 18
   
          |
260 | 258, 259 | expp1d 12417 |
. . . . . . . . . . . . . . . . 17
   
                             |
261 | 257, 260 | eqtrd 2485 |
. . . . . . . . . . . . . . . 16
   
                               |
262 | 140 | sseli 3428 |
. . . . . . . . . . . . . . . . . 18
         |
263 | 262, 157 | sylan2 477 |
. . . . . . . . . . . . . . . . 17
   
               |
264 | 258, 263 | mulcomd 9664 |
. . . . . . . . . . . . . . . 16
   
                              |
265 | 263 | mulm1d 10070 |
. . . . . . . . . . . . . . . 16
   
                            |
266 | 261, 264,
265 | 3eqtr2d 2491 |
. . . . . . . . . . . . . . 15
   
                             |
267 | 266 | oveq1d 6305 |
. . . . . . . . . . . . . 14
   
                     
                             |
268 | | inss1 3652 |
. . . . . . . . . . . . . . . . . . 19
      |
269 | | ssfi 7792 |
. . . . . . . . . . . . . . . . . . 19
  
 
  
       |
270 | 158, 268,
269 | sylancl 668 |
. . . . . . . . . . . . . . . . . 18
   
       
       |
271 | | hashcl 12538 |
. . . . . . . . . . . . . . . . . 18
                 |
272 | 270, 271 | syl 17 |
. . . . . . . . . . . . . . . . 17
   
       
   
       |
273 | 272 | nn0cnd 10927 |
. . . . . . . . . . . . . . . 16
   
       
   
       |
274 | 262, 273 | sylan2 477 |
. . . . . . . . . . . . . . 15
   
               |
275 | 263, 274 | mulneg1d 10071 |
. . . . . . . . . . . . . 14
   
                                       
        |
276 | 267, 275 | eqtrd 2485 |
. . . . . . . . . . . . 13
   
                     
                             |
277 | 276 | sumeq2dv 13769 |
. . . . . . . . . . . 12
                                               
        |
278 | 247, 277 | syl5eq 2497 |
. . . . . . . . . . 11
                                               
        |
279 | 157, 273 | mulcld 9663 |
. . . . . . . . . . . . 13
   
       
             
        |
280 | 262, 279 | sylan2 477 |
. . . . . . . . . . . 12
   
                          |
281 | 176, 280 | fsumneg 13848 |
. . . . . . . . . . 11
                     
                               |
282 | 238, 278,
281 | 3eqtrd 2489 |
. . . . . . . . . 10
                            
                             |
283 | 282 | oveq2d 6306 |
. . . . . . . . 9
                                                        
                                   
         |
284 | 140 | a1i 11 |
. . . . . . . . . . . . 13
             |
285 | 284 | sselda 3432 |
. . . . . . . . . . . 12
   
           |
286 | 285, 165 | syldan 473 |
. . . . . . . . . . 11
   
                        |
287 | 176, 286 | fsumcl 13799 |
. . . . . . . . . 10
                    
      |
288 | 285, 279 | syldan 473 |
. . . . . . . . . . 11
   
                          |
289 | 176, 288 | fsumcl 13799 |
. . . . . . . . . 10
                    
        |
290 | 287, 289 | negsubd 9992 |
. . . . . . . . 9
                                          
                       
    
                        |
291 | 166, 283,
290 | 3eqtrd 2489 |
. . . . . . . 8
                                             
    
                        |
292 | 291 | adantr 467 |
. . . . . . 7
   
  
        
                   
                        
                    
    
                        |
293 | 102, 135,
292 | 3eqtr4d 2495 |
. . . . . 6
   
  
        
                   
               
                              |
294 | 293 | ex 436 |
. . . . 5
      
                            
            
 
                               |
295 | 294 | ralrimdva 2806 |
. . . 4
 

 
        
                   
                                               |
296 | | ineq1 3627 |
. . . . . . . 8
 
 
         |
297 | 296 | fveq2d 5869 |
. . . . . . 7
             
 
     |
298 | 67, 297 | oveq12d 6308 |
. . . . . 6
         
 
              
      |
299 | | ineq1 3627 |
. . . . . . . . 9
 
       |
300 | 299 | fveq2d 5869 |
. . . . . . . 8
           
     |
301 | 300 | oveq2d 6306 |
. . . . . . 7
              
                        |
302 | 301 | sumeq2sdv 13770 |
. . . . . 6
                                                   |
303 | 298, 302 | eqeq12d 2466 |
. . . . 5
            
                                      
                               |
304 | 303 | cbvralv 3019 |
. . . 4
 
        
 
                            
          
                              |
305 | 295, 304 | syl6ibr 231 |
. . 3
 

 
        
                   
                                               |
306 | 16, 24, 38, 46, 66, 305 | findcard2s 7812 |
. 2
                              
      |
307 | | fveq2 5865 |
. . . . 5
           |
308 | | ineq1 3627 |
. . . . . 6
 
       |
309 | 308 | fveq2d 5869 |
. . . . 5
                 |
310 | 307, 309 | oveq12d 6308 |
. . . 4
         
                   |
311 | | simpl 459 |
. . . . . . . 8
 
 
  |
312 | 311 | ineq1d 3633 |
. . . . . . 7
 
 
        |
313 | 312 | fveq2d 5869 |
. . . . . 6
 
 
   
            |
314 | 313 | oveq2d 6306 |
. . . . 5
 
 
             
                        |
315 | 314 | sumeq2dv 13769 |
. . . 4
                
    
                     |
316 | 310, 315 | eqeq12d 2466 |
. . 3
                              
   
             
                      |
317 | 316 | rspccva 3149 |
. 2
                               
                  
                     |
318 | 306, 317 | sylan 474 |
1
 
                                    |