Step | Hyp | Ref
| Expression |
1 | | esumcst.1 |
. . . . 5
   |
2 | 1 | nfel1 2606 |
. . . 4
  |
3 | | esumcst.2 |
. . . . 5
   |
4 | 3 | nfel1 2606 |
. . . 4
     |
5 | 2, 4 | nfan 2011 |
. . 3
  
 
   |
6 | | simpl 459 |
. . 3
 
      |
7 | | simplr 762 |
. . 3
  
 
 
      |
8 | | xrge0tmd 28752 |
. . . . . . 7
  ↾s     TopMnd |
9 | | tmdmnd 21090 |
. . . . . . 7
  
↾s     TopMnd  
↾s       |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
  ↾s      |
11 | 10 | a1i 11 |
. . . . 5
  
 
 
     
↾s       |
12 | | inss2 3653 |
. . . . . 6
    |
13 | | simpr 463 |
. . . . . 6
  
 
 
         |
14 | 12, 13 | sseldi 3430 |
. . . . 5
  
 
 
      |
15 | | simplr 762 |
. . . . 5
  
 
 
         |
16 | | xrge0base 28447 |
. . . . . 6
       
↾s       |
17 | | eqid 2451 |
. . . . . 6
.g  
↾s      .g   ↾s  
    |
18 | 3, 16, 17 | gsumconstf 17568 |
. . . . 5
    ↾s           
↾s     g          .g   ↾s  
       |
19 | 11, 14, 15, 18 | syl3anc 1268 |
. . . 4
  
 
 
      
↾s     g          .g   ↾s  
       |
20 | | hashcl 12538 |
. . . . . 6
       |
21 | 14, 20 | syl 17 |
. . . . 5
  
 
 
          |
22 | | xrge0mulgnn0 28451 |
. . . . 5
     
          .g  
↾s                   |
23 | 21, 15, 22 | syl2anc 667 |
. . . 4
  
 
 
          .g   ↾s  
                |
24 | 19, 23 | eqtrd 2485 |
. . 3
  
 
 
      
↾s     g               |
25 | 5, 1, 6, 7, 24 | esumval 28867 |
. 2
 
    Σ*                   
  |
26 | | nn0ssre 10873 |
. . . . . . . . . 10
 |
27 | | ressxr 9684 |
. . . . . . . . . 10
 |
28 | 26, 27 | sstri 3441 |
. . . . . . . . 9
 |
29 | | pnfxr 11412 |
. . . . . . . . . 10
 |
30 | | snssi 4116 |
. . . . . . . . . 10
   |
31 | 29, 30 | ax-mp 5 |
. . . . . . . . 9
  |
32 | 28, 31 | unssi 3609 |
. . . . . . . 8

   |
33 | | hashf 12522 |
. . . . . . . . 9
        |
34 | | vex 3048 |
. . . . . . . . 9
 |
35 | | ffvelrn 6020 |
. . . . . . . . 9
      
       
    |
36 | 33, 34, 35 | mp2an 678 |
. . . . . . . 8
        |
37 | 32, 36 | sselii 3429 |
. . . . . . 7
     |
38 | 37 | a1i 11 |
. . . . . 6
  
 
 
          |
39 | | iccssxr 11717 |
. . . . . . . 8
    |
40 | | simpr 463 |
. . . . . . . 8
 
         |
41 | 39, 40 | sseldi 3430 |
. . . . . . 7
 
      |
42 | 41 | adantr 467 |
. . . . . 6
  
 
 
      |
43 | 38, 42 | xmulcld 11588 |
. . . . 5
  
 
 
               |
44 | | eqid 2451 |
. . . . 5
                             |
45 | 43, 44 | fmptd 6046 |
. . . 4
 
                           |
46 | | frn 5735 |
. . . 4
                     
             
  |
47 | 45, 46 | syl 17 |
. . 3
 
   
                |
48 | | hashxrcl 12539 |
. . . . 5
       |
49 | 48 | adantr 467 |
. . . 4
 
          |
50 | 49, 41 | xmulcld 11588 |
. . 3
 
               |
51 | | vex 3048 |
. . . . . . . 8
 |
52 | 44 | elrnmpt 5081 |
. . . . . . . 8
               
                 |
53 | 51, 52 | ax-mp 5 |
. . . . . . 7
                               |
54 | 53 | biimpi 198 |
. . . . . 6
              
                |
55 | 49 | adantr 467 |
. . . . . . . 8
  
 
 
          |
56 | | 0xr 9687 |
. . . . . . . . . . 11
 |
57 | 56 | a1i 11 |
. . . . . . . . . 10
  
 
 
      |
58 | 29 | a1i 11 |
. . . . . . . . . 10
  
 
 
      |
59 | | iccgelb 11691 |
. . . . . . . . . 10
        |
60 | 57, 58, 15, 59 | syl3anc 1268 |
. . . . . . . . 9
  
 
 
      |
61 | 42, 60 | jca 535 |
. . . . . . . 8
  
 
 
    
   |
62 | 6 | adantr 467 |
. . . . . . . . . 10
  
 
 
      |
63 | | inss1 3652 |
. . . . . . . . . . . 12
     |
64 | 63 | sseli 3428 |
. . . . . . . . . . 11
       |
65 | | elpwi 3960 |
. . . . . . . . . . 11
    |
66 | 13, 64, 65 | 3syl 18 |
. . . . . . . . . 10
  
 
 
      |
67 | | ssdomg 7615 |
. . . . . . . . . 10
 
   |
68 | 62, 66, 67 | sylc 62 |
. . . . . . . . 9
  
 
 
      |
69 | | hashdomi 12559 |
. . . . . . . . 9

   
      |
70 | 68, 69 | syl 17 |
. . . . . . . 8
  
 
 
              |
71 | | xlemul1a 11574 |
. . . . . . . 8
          
                                |
72 | 38, 55, 61, 70, 71 | syl31anc 1271 |
. . . . . . 7
  
 
 
                        |
73 | 72 | ralrimiva 2802 |
. . . . . 6
 
                             |
74 | | r19.29r 2926 |
. . . . . 6
                                       
                                    |
75 | 54, 73, 74 | syl2anr 481 |
. . . . 5
  
 
 
                                                   |
76 | | simpl 459 |
. . . . . . 7
                             
           |
77 | | simpr 463 |
. . . . . . 7
                             
                    |
78 | 76, 77 | eqbrtrd 4423 |
. . . . . 6
                             
           |
79 | 78 | rexlimivw 2876 |
. . . . 5
                                  
           |
80 | 75, 79 | syl 17 |
. . . 4
  
 
 
                          |
81 | 80 | ralrimiva 2802 |
. . 3
 
     
 
                       |
82 | | pwidg 3964 |
. . . . . . . . . . 11
    |
83 | 82 | ancri 555 |
. . . . . . . . . 10
 

   |
84 | | elin 3617 |
. . . . . . . . . 10
   
     |
85 | 83, 84 | sylibr 216 |
. . . . . . . . 9
      |
86 | | eqid 2451 |
. . . . . . . . . . 11
                   |
87 | | fveq2 5865 |
. . . . . . . . . . . . . 14
           |
88 | 87 | oveq1d 6305 |
. . . . . . . . . . . . 13
                     |
89 | 88 | eqeq2d 2461 |
. . . . . . . . . . . 12
                                         |
90 | 89 | rspcev 3150 |
. . . . . . . . . . 11
                       
                         |
91 | 86, 90 | mpan2 677 |
. . . . . . . . . 10
                             |
92 | | ovex 6318 |
. . . . . . . . . . 11
          |
93 | 44 | elrnmpt 5081 |
. . . . . . . . . . 11
                                 
                          |
94 | 92, 93 | ax-mp 5 |
. . . . . . . . . 10
                       
                         |
95 | 91, 94 | sylibr 216 |
. . . . . . . . 9
                             |
96 | 85, 95 | syl 17 |
. . . . . . . 8
                          |
97 | 96 | adantl 468 |
. . . . . . 7
                                              |
98 | | simplr 762 |
. . . . . . 7
                                |
99 | | breq2 4406 |
. . . . . . . 8
          
            |
100 | 99 | rspcev 3150 |
. . . . . . 7
                                                     |
101 | 97, 98, 100 | syl2anc 667 |
. . . . . 6
                                       |
102 | | 0elpw 4572 |
. . . . . . . . . . . 12
  |
103 | | 0fin 7799 |
. . . . . . . . . . . 12
 |
104 | | elin 3617 |
. . . . . . . . . . . 12
         |
105 | 102, 103,
104 | mpbir2an 931 |
. . . . . . . . . . 11
    |
106 | 105 | a1i 11 |
. . . . . . . . . 10
     
                      |
107 | | simpr 463 |
. . . . . . . . . . . 12
     
                
  |
108 | 107 | oveq2d 6306 |
. . . . . . . . . . 11
     
                                     |
109 | | hash0 12548 |
. . . . . . . . . . . . 13
     |
110 | 109, 56 | eqeltri 2525 |
. . . . . . . . . . . 12
     |
111 | | xmul01 11553 |
. . . . . . . . . . . 12
                |
112 | 110, 111 | ax-mp 5 |
. . . . . . . . . . 11
          |
113 | 108, 112 | syl6req 2502 |
. . . . . . . . . 10
     
                            |
114 | | fveq2 5865 |
. . . . . . . . . . . . 13

          |
115 | 114 | oveq1d 6305 |
. . . . . . . . . . . 12

                    |
116 | 115 | eqeq2d 2461 |
. . . . . . . . . . 11

         
            |
117 | 116 | rspcev 3150 |
. . . . . . . . . 10
 
  
          
 
             |
118 | 106, 113,
117 | syl2anc 667 |
. . . . . . . . 9
     
                 
 
             |
119 | | ovex 6318 |
. . . . . . . . . 10
          |
120 | 44, 119 | elrnmpti 5085 |
. . . . . . . . 9
                               |
121 | 118, 120 | sylibr 216 |
. . . . . . . 8
     
                                 |
122 | | simpllr 769 |
. . . . . . . . 9
     
                
           |
123 | 107 | oveq2d 6306 |
. . . . . . . . . 10
     
                                     |
124 | 49 | ad4antr 738 |
. . . . . . . . . . 11
     
                       |
125 | | xmul01 11553 |
. . . . . . . . . . 11
    
           |
126 | 124, 125 | syl 17 |
. . . . . . . . . 10
     
                            |
127 | 123, 126 | eqtrd 2485 |
. . . . . . . . 9
     
                            |
128 | 122, 127 | breqtrd 4427 |
. . . . . . . 8
     
                
  |
129 | | breq2 4406 |
. . . . . . . . 9
 
   |
130 | 129 | rspcev 3150 |
. . . . . . . 8
                                   |
131 | 121, 128,
130 | syl2anc 667 |
. . . . . . 7
     
                 

 
              |
132 | | simplr 762 |
. . . . . . . . . . . . . . 15
         
                    
 
        |
133 | | simpr 463 |
. . . . . . . . . . . . . . . . 17
         
                    
 
           |
134 | | simp-4r 777 |
. . . . . . . . . . . . . . . . 17
         
                    
 
       |
135 | 133, 134 | eqeltrd 2529 |
. . . . . . . . . . . . . . . 16
         
                    
 
           |
136 | | nnnn0 10876 |
. . . . . . . . . . . . . . . . 17
    
      |
137 | | vex 3048 |
. . . . . . . . . . . . . . . . . 18
 |
138 | | hashclb 12540 |
. . . . . . . . . . . . . . . . . 18
 
       |
139 | 137, 138 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17

      |
140 | 136, 139 | sylibr 216 |
. . . . . . . . . . . . . . . 16
    
  |
141 | 135, 140 | syl 17 |
. . . . . . . . . . . . . . 15
         
                    
 
       |
142 | 132, 141 | elind 3618 |
. . . . . . . . . . . . . 14
         
                    
 
          |
143 | | eqidd 2452 |
. . . . . . . . . . . . . 14
         
                    
 
                         |
144 | | fveq2 5865 |
. . . . . . . . . . . . . . . . 17
           |
145 | 144 | oveq1d 6305 |
. . . . . . . . . . . . . . . 16
                     |
146 | 145 | eqeq2d 2461 |
. . . . . . . . . . . . . . 15
                                         |
147 | 146 | rspcev 3150 |
. . . . . . . . . . . . . 14
                       
                         |
148 | 142, 143,
147 | syl2anc 667 |
. . . . . . . . . . . . 13
         
                    
 
                              |
149 | 44, 119 | elrnmpti 5085 |
. . . . . . . . . . . . 13
                       
                         |
150 | 148, 149 | sylibr 216 |
. . . . . . . . . . . 12
         
                    
 
              
 
             |
151 | | simpllr 769 |
. . . . . . . . . . . . . 14
         
                    
 
         |
152 | | simp-8r 785 |
. . . . . . . . . . . . . . 15
         
                    
 
       |
153 | 134 | nnred 10624 |
. . . . . . . . . . . . . . 15
         
                    
 
       |
154 | | simp-5r 779 |
. . . . . . . . . . . . . . 15
         
                    
 
       |
155 | 152, 153,
154 | ltdivmul2d 11390 |
. . . . . . . . . . . . . 14
         
                    
 
             |
156 | 151, 155 | mpbid 214 |
. . . . . . . . . . . . 13
         
                    
 
         |
157 | 133 | oveq1d 6305 |
. . . . . . . . . . . . . 14
         
                    
 
                     |
158 | 154 | rpred 11341 |
. . . . . . . . . . . . . . 15
         
                    
 
       |
159 | | rexmul 11557 |
. . . . . . . . . . . . . . 15
 
          |
160 | 153, 158,
159 | syl2anc 667 |
. . . . . . . . . . . . . 14
         
                    
 
              |
161 | 157, 160 | eqtrd 2485 |
. . . . . . . . . . . . 13
         
                    
 
                  |
162 | 156, 161 | breqtrrd 4429 |
. . . . . . . . . . . 12
         
                    
 
                |
163 | | breq2 4406 |
. . . . . . . . . . . . 13
          
            |
164 | 163 | rspcev 3150 |
. . . . . . . . . . . 12
                                                     |
165 | 150, 162,
164 | syl2anc 667 |
. . . . . . . . . . 11
         
                    
 
      
 
              |
166 | 165 | ex 436 |
. . . . . . . . . 10
                       


   
                          |
167 | 166 | rexlimdva 2879 |
. . . . . . . . 9
                      


   
 
                        |
168 | 167 | impr 625 |
. . . . . . . 8
                      


   
                          |
169 | | simp-4r 777 |
. . . . . . . . . . 11
     
                   |
170 | | simpr 463 |
. . . . . . . . . . 11
     
                   |
171 | 169, 170 | rerpdivcld 11369 |
. . . . . . . . . 10
     
                     |
172 | | arch 10866 |
. . . . . . . . . 10
        |
173 | 171, 172 | syl 17 |
. . . . . . . . 9
     
                      |
174 | | ishashinf 12626 |
. . . . . . . . . 10
  
       |
175 | 174 | ad2antlr 733 |
. . . . . . . . 9
     
                          |
176 | | r19.29r 2926 |
. . . . . . . . 9
    
 
      
            |
177 | 173, 175,
176 | syl2anc 667 |
. . . . . . . 8
     
                    
         |
178 | 168, 177 | r19.29a 2932 |
. . . . . . 7
     
                                   |
179 | | nfielex 7800 |
. . . . . . . . . . . 12
    |
180 | 179 | adantr 467 |
. . . . . . . . . . 11
      |
181 | | snelpwi 4645 |
. . . . . . . . . . . . . . 15
      |
182 | | snfi 7650 |
. . . . . . . . . . . . . . 15
   |
183 | 181, 182 | jctir 541 |
. . . . . . . . . . . . . 14
    
     |
184 | | elin 3617 |
. . . . . . . . . . . . . 14
               |
185 | 183, 184 | sylibr 216 |
. . . . . . . . . . . . 13
        |
186 | 185 | adantl 468 |
. . . . . . . . . . . 12
  

        |
187 | | simplr 762 |
. . . . . . . . . . . . . 14
  

   |
188 | 187 | oveq2d 6306 |
. . . . . . . . . . . . 13
  

                        |
189 | | hashsng 12549 |
. . . . . . . . . . . . . . . 16
         |
190 | | 1re 9642 |
. . . . . . . . . . . . . . . . 17
 |
191 | 27, 190 | sselii 3429 |
. . . . . . . . . . . . . . . 16
 |
192 | 189, 191 | syl6eqel 2537 |
. . . . . . . . . . . . . . 15
         |
193 | | 0lt1 10136 |
. . . . . . . . . . . . . . . 16
 |
194 | 193, 189 | syl5breqr 4439 |
. . . . . . . . . . . . . . 15
         |
195 | | xmulpnf1 11560 |
. . . . . . . . . . . . . . 15
       
                   |
196 | 192, 194,
195 | syl2anc 667 |
. . . . . . . . . . . . . 14
             |
197 | 196 | adantl 468 |
. . . . . . . . . . . . 13
  

             |
198 | 188, 197 | eqtr2d 2486 |
. . . . . . . . . . . 12
  

              |
199 | | fveq2 5865 |
. . . . . . . . . . . . . . 15
               |
200 | 199 | oveq1d 6305 |
. . . . . . . . . . . . . 14
                         |
201 | 200 | eqeq2d 2461 |
. . . . . . . . . . . . 13
                          |
202 | 201 | rspcev 3150 |
. . . . . . . . . . . 12
                                  |
203 | 186, 198,
202 | syl2anc 667 |
. . . . . . . . . . 11
  

                |
204 | 180, 203 | exlimddv 1781 |
. . . . . . . . . 10
                  |
205 | 204 | adantll 720 |
. . . . . . . . 9
     
                                |
206 | 44, 119 | elrnmpti 5085 |
. . . . . . . . 9
             
               |
207 | 205, 206 | sylibr 216 |
. . . . . . . 8
     
                                 |
208 | | simp-4r 777 |
. . . . . . . . 9
     
                   |
209 | | ltpnf 11422 |
. . . . . . . . 9
   |
210 | 208, 209 | syl 17 |
. . . . . . . 8
     
                   |
211 | | breq2 4406 |
. . . . . . . . 9
 
   |
212 | 211 | rspcev 3150 |
. . . . . . . 8
                                  |
213 | 207, 210,
212 | syl2anc 667 |
. . . . . . 7
     
                                   |
214 | | simp-4r 777 |
. . . . . . . 8
                   
      |
215 | | elxrge02 28401 |
. . . . . . . 8
   
    |
216 | 214, 215 | sylib 200 |
. . . . . . 7
                   
     |
217 | 131, 178,
213, 216 | mpjao3dan 1335 |
. . . . . 6
                   
  
 
              |
218 | 101, 217 | pm2.61dan 800 |
. . . . 5
                                     |
219 | 218 | ex 436 |
. . . 4
  
 
 

                             |
220 | 219 | ralrimiva 2802 |
. . 3
 
                
 
               |
221 | | supxr2 11599 |
. . 3
                
           

 
                               
                  
                 
           |
222 | 47, 50, 81, 220, 221 | syl22anc 1269 |
. 2
 
                                 |
223 | 25, 222 | eqtrd 2485 |
1
 
    Σ*             |