Step | Hyp | Ref
| Expression |
1 | | stoweidlem17.2 |
. . 3
   |
2 | 1 | nnnn0d 10949 |
. 2
   |
3 | | nn0uz 11217 |
. . . . 5
     |
4 | 2, 3 | syl6eleq 2559 |
. . . 4
       |
5 | | eluzfz2 11833 |
. . . 4
    
      |
6 | 4, 5 | syl 17 |
. . 3
       |
7 | 6 | ancli 560 |
. 2
         |
8 | | eleq1 2537 |
. . . . 5
     
       |
9 | 8 | anbi2d 718 |
. . . 4
  
    
         |
10 | | oveq2 6316 |
. . . . . . 7
           |
11 | 10 | sumeq1d 13844 |
. . . . . 6
                 
                 |
12 | 11 | mpteq2dv 4483 |
. . . . 5
                                       |
13 | 12 | eleq1d 2533 |
. . . 4
                                         |
14 | 9, 13 | imbi12d 327 |
. . 3
   
                                                     |
15 | | eleq1 2537 |
. . . . 5
     
       |
16 | 15 | anbi2d 718 |
. . . 4
  
    
         |
17 | | oveq2 6316 |
. . . . . . 7
           |
18 | 17 | sumeq1d 13844 |
. . . . . 6
                 
                 |
19 | 18 | mpteq2dv 4483 |
. . . . 5
                                       |
20 | 19 | eleq1d 2533 |
. . . 4
                                         |
21 | 16, 20 | imbi12d 327 |
. . 3
   
                                                     |
22 | | eleq1 2537 |
. . . . 5
       
         |
23 | 22 | anbi2d 718 |
. . . 4
    
    
           |
24 | | oveq2 6316 |
. . . . . . 7
               |
25 | 24 | sumeq1d 13844 |
. . . . . 6
                   
                   |
26 | 25 | mpteq2dv 4483 |
. . . . 5
                                           |
27 | 26 | eleq1d 2533 |
. . . 4
                                             |
28 | 23, 27 | imbi12d 327 |
. . 3
     
                                                         |
29 | | eleq1 2537 |
. . . . 5
     
       |
30 | 29 | anbi2d 718 |
. . . 4
  
    
         |
31 | | oveq2 6316 |
. . . . . . 7
           |
32 | 31 | sumeq1d 13844 |
. . . . . 6
                 
                 |
33 | 32 | mpteq2dv 4483 |
. . . . 5
                                       |
34 | 33 | eleq1d 2533 |
. . . 4
                                         |
35 | 30, 34 | imbi12d 327 |
. . 3
   
                                                     |
36 | | 0z 10972 |
. . . . . . . . 9
 |
37 | | fzsn 11866 |
. . . . . . . . 9
         |
38 | 36, 37 | ax-mp 5 |
. . . . . . . 8
       |
39 | 38 | sumeq1i 13841 |
. . . . . . 7
                
             |
40 | 39 | mpteq2i 4479 |
. . . . . 6
                                  |
41 | | stoweidlem17.1 |
. . . . . . 7
   |
42 | | stoweidlem17.7 |
. . . . . . . . . . 11
   |
43 | 42 | adantr 472 |
. . . . . . . . . 10
 
   |
44 | 43 | recnd 9687 |
. . . . . . . . 9
 
   |
45 | | stoweidlem17.3 |
. . . . . . . . . . . . 13
           |
46 | | nnz 10983 |
. . . . . . . . . . . . . . . . 17
   |
47 | | nngt0 10660 |
. . . . . . . . . . . . . . . . . 18
   |
48 | | 0re 9661 |
. . . . . . . . . . . . . . . . . . 19
 |
49 | | nnre 10638 |
. . . . . . . . . . . . . . . . . . 19
   |
50 | | ltle 9740 |
. . . . . . . . . . . . . . . . . . 19
 
 
   |
51 | 48, 49, 50 | sylancr 676 |
. . . . . . . . . . . . . . . . . 18
 
   |
52 | 47, 51 | mpd 15 |
. . . . . . . . . . . . . . . . 17
   |
53 | 46, 52 | jca 541 |
. . . . . . . . . . . . . . . 16
 
   |
54 | 1, 53 | syl 17 |
. . . . . . . . . . . . . . 15
 
   |
55 | 36 | eluz1i 11190 |
. . . . . . . . . . . . . . 15
         |
56 | 54, 55 | sylibr 217 |
. . . . . . . . . . . . . 14
       |
57 | | eluzfz1 11832 |
. . . . . . . . . . . . . 14
    
      |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
       |
59 | 45, 58 | ffvelrnd 6038 |
. . . . . . . . . . . 12
       |
60 | | feq1 5720 |
. . . . . . . . . . . . . 14
         
           |
61 | 60 | imbi2d 323 |
. . . . . . . . . . . . 13
      
    
             |
62 | | stoweidlem17.8 |
. . . . . . . . . . . . . 14
 
       |
63 | 62 | expcom 442 |
. . . . . . . . . . . . 13
         |
64 | 61, 63 | vtoclga 3099 |
. . . . . . . . . . . 12
                 |
65 | 59, 64 | mpcom 36 |
. . . . . . . . . . 11
           |
66 | 65 | fnvinran 37398 |
. . . . . . . . . 10
 
           |
67 | 66 | recnd 9687 |
. . . . . . . . 9
 
           |
68 | 44, 67 | mulcld 9681 |
. . . . . . . 8
 
 
           |
69 | | fveq2 5879 |
. . . . . . . . . . 11
           |
70 | 69 | fveq1d 5881 |
. . . . . . . . . 10
                   |
71 | 70 | oveq2d 6324 |
. . . . . . . . 9
 
                     |
72 | 71 | sumsn 13884 |
. . . . . . . 8
  
                                   |
73 | 36, 68, 72 | sylancr 676 |
. . . . . . 7
 
    
                     |
74 | 41, 73 | mpteq2da 4481 |
. . . . . 6
                              |
75 | 40, 74 | syl5eq 2517 |
. . . . 5
                                 |
76 | | stoweidlem17.5 |
. . . . . 6
 


             |
77 | | stoweidlem17.6 |
. . . . . 6
 

    |
78 | 41, 76, 77, 62, 42, 59 | stoweidlem2 37974 |
. . . . 5
               |
79 | 75, 78 | eqeltrd 2549 |
. . . 4
                     |
80 | 79 | adantr 472 |
. . 3
 
                         |
81 | | eqidd 2472 |
. . . . . . . . . . . . . . . 16
   |
82 | 81 | cbvmptv 4488 |
. . . . . . . . . . . . . . 15
     |
83 | 82 | eqcomi 2480 |
. . . . . . . . . . . . . 14
     |
84 | 83 | a1i 11 |
. . . . . . . . . . . . 13
 
       |
85 | | eqidd 2472 |
. . . . . . . . . . . . 13
    
  |
86 | | simpr 468 |
. . . . . . . . . . . . 13
 
   |
87 | 84, 85, 86, 43 | fvmptd 5969 |
. . . . . . . . . . . 12
 
         |
88 | 87 | oveq1d 6323 |
. . . . . . . . . . 11
 
                                 |
89 | 41, 88 | mpteq2da 4481 |
. . . . . . . . . 10
             
                       |
90 | 89 | adantr 472 |
. . . . . . . . 9
 
                                           |
91 | 45 | fnvinran 37398 |
. . . . . . . . . 10
 
               |
92 | | simpl 464 |
. . . . . . . . . 10
 
         |
93 | | id 22 |
. . . . . . . . . . . . . . . 16
   |
94 | 93 | mpteq2dv 4483 |
. . . . . . . . . . . . . . 15
       |
95 | 94 | eleq1d 2533 |
. . . . . . . . . . . . . 14
         |
96 | 95 | imbi2d 323 |
. . . . . . . . . . . . 13
  
  
       |
97 | 77 | expcom 442 |
. . . . . . . . . . . . 13
       |
98 | 96, 97 | vtoclga 3099 |
. . . . . . . . . . . 12
       |
99 | 42, 98 | mpcom 36 |
. . . . . . . . . . 11
     |
100 | 99 | adantr 472 |
. . . . . . . . . 10
 
           |
101 | | fveq1 5878 |
. . . . . . . . . . . . . . . 16
    
                  |
102 | 101 | oveq2d 6324 |
. . . . . . . . . . . . . . 15
    
                                  |
103 | 102 | mpteq2dv 4483 |
. . . . . . . . . . . . . 14
    
                                      |
104 | 103 | eleq1d 2533 |
. . . . . . . . . . . . 13
    
                                        |
105 | 104 | imbi2d 323 |
. . . . . . . . . . . 12
    
       

                  

                       |
106 | 82 | eleq1i 2540 |
. . . . . . . . . . . . . . . 16
  

   |
107 | | fveq1 5878 |
. . . . . . . . . . . . . . . . . . . . . 22
               |
108 | 82 | fveq1i 5880 |
. . . . . . . . . . . . . . . . . . . . . 22
             |
109 | 107, 108 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . . . 21
               |
110 | 109 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . . . 20
                           |
111 | 110 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . . . 19
                               |
112 | 111 | eleq1d 2533 |
. . . . . . . . . . . . . . . . . 18
                                 |
113 | 112 | imbi2d 323 |
. . . . . . . . . . . . . . . . 17
                   
  

                 |
114 | 76 | 3com12 1235 |
. . . . . . . . . . . . . . . . . 18
  

             |
115 | 114 | 3expib 1234 |
. . . . . . . . . . . . . . . . 17
  
                |
116 | 113, 115 | vtoclga 3099 |
. . . . . . . . . . . . . . . 16
    
                  |
117 | 106, 116 | sylbir 218 |
. . . . . . . . . . . . . . 15
    
                  |
118 | 117 | 3impib 1229 |
. . . . . . . . . . . . . 14
                     |
119 | 118 | 3com13 1236 |
. . . . . . . . . . . . 13
                     |
120 | 119 | 3expib 1234 |
. . . . . . . . . . . 12
  
                    |
121 | 105, 120 | vtoclga 3099 |
. . . . . . . . . . 11
        
                          |
122 | 121 | 3impib 1229 |
. . . . . . . . . 10
                                 |
123 | 91, 92, 100, 122 | syl3anc 1292 |
. . . . . . . . 9
 
                             |
124 | 90, 123 | eqeltrrd 2550 |
. . . . . . . 8
 
                       |
125 | 124 | ad2antll 743 |
. . . . . . 7
    
                                          
         |
126 | | simprrl 782 |
. . . . . . 7
    
                                      |
127 | | simpl 464 |
. . . . . . . . . 10
          
  |
128 | | simprl 772 |
. . . . . . . . . 10
             |
129 | 1 | ad2antrl 742 |
. . . . . . . . . . . 12
          
  |
130 | 129 | nnnn0d 10949 |
. . . . . . . . . . 11
          
  |
131 | | nn0re 10902 |
. . . . . . . . . . . . 13

  |
132 | 131 | adantr 472 |
. . . . . . . . . . . 12
          
  |
133 | | peano2nn0 10934 |
. . . . . . . . . . . . . 14

    |
134 | 133 | nn0red 10950 |
. . . . . . . . . . . . 13

    |
135 | 134 | adantr 472 |
. . . . . . . . . . . 12
               |
136 | 1 | nnred 10646 |
. . . . . . . . . . . . 13
   |
137 | 136 | ad2antrl 742 |
. . . . . . . . . . . 12
          
  |
138 | | lep1 10466 |
. . . . . . . . . . . . 13
     |
139 | 127, 131,
138 | 3syl 18 |
. . . . . . . . . . . 12
               |
140 | | elfzle2 11829 |
. . . . . . . . . . . . 13
           |
141 | 140 | ad2antll 743 |
. . . . . . . . . . . 12
            
  |
142 | 132, 135,
137, 139, 141 | letrd 9809 |
. . . . . . . . . . 11
             |
143 | | elfz2nn0 11911 |
. . . . . . . . . . 11
    

   |
144 | 127, 130,
142, 143 | syl3anbrc 1214 |
. . . . . . . . . 10
          
      |
145 | 127, 128,
144 | jca32 544 |
. . . . . . . . 9
                     |
146 | 145 | adantl 473 |
. . . . . . . 8
    
                                    
         |
147 | | pm3.31 452 |
. . . . . . . . 9
                            
                              |
148 | 147 | adantr 472 |
. . . . . . . 8
    
                                     
                            |
149 | 146, 148 | mpd 15 |
. . . . . . 7
    
                                                        |
150 | | fveq2 5879 |
. . . . . . . . . . . 12
                       |
151 | 150 | oveq2d 6324 |
. . . . . . . . . . 11
 
                
        |
152 | 151 | cbvmptv 4488 |
. . . . . . . . . 10
                    
        |
153 | 152 | eleq1i 2540 |
. . . . . . . . 9
              

               |
154 | | fveq1 5878 |
. . . . . . . . . . . . . . 15
       
                               |
155 | 152 | fveq1i 5880 |
. . . . . . . . . . . . . . 15
                                     |
156 | 154, 155 | syl6eq 2521 |
. . . . . . . . . . . . . 14
       
                               |
157 | 156 | oveq2d 6324 |
. . . . . . . . . . . . 13
       
                                                                               |
158 | 157 | mpteq2dv 4483 |
. . . . . . . . . . . 12
       
                                                                                   |
159 | 158 | eleq1d 2533 |
. . . . . . . . . . 11
       
                                     

                                              |
160 | 159 | imbi2d 323 |
. . . . . . . . . 10
       
                            

                                                  

                                               |
161 | | fveq2 5879 |
. . . . . . . . . . . . . . . . . 18
                   |
162 | 161 | oveq2d 6324 |
. . . . . . . . . . . . . . . . 17
 
                     |
163 | 162 | sumeq2sdv 13847 |
. . . . . . . . . . . . . . . 16
                 
                 |
164 | 163 | cbvmptv 4488 |
. . . . . . . . . . . . . . 15
                                     |
165 | 164 | eleq1i 2540 |
. . . . . . . . . . . . . 14
                  

                   |
166 | | fveq1 5878 |
. . . . . . . . . . . . . . . . . . . 20
                                               |
167 | 164 | fveq1i 5880 |
. . . . . . . . . . . . . . . . . . . 20
                                             |
168 | 166, 167 | syl6eq 2521 |
. . . . . . . . . . . . . . . . . . 19
                                               |
169 | 168 | oveq1d 6323 |
. . . . . . . . . . . . . . . . . 18
                                                           |
170 | 169 | mpteq2dv 4483 |
. . . . . . . . . . . . . . . . 17
                                                               |
171 | 170 | eleq1d 2533 |
. . . . . . . . . . . . . . . 16
                                                                 |
172 | 171 | imbi2d 323 |
. . . . . . . . . . . . . . 15
                     
                                                   |
173 | | stoweidlem17.4 |
. . . . . . . . . . . . . . . . 17
 


             |
174 | 173 | 3com12 1235 |
. . . . . . . . . . . . . . . 16
  

             |
175 | 174 | 3expib 1234 |
. . . . . . . . . . . . . . 15
  
                |
176 | 172, 175 | vtoclga 3099 |
. . . . . . . . . . . . . 14
                    
                                  |
177 | 165, 176 | sylbir 218 |
. . . . . . . . . . . . 13
                    
                                  |
178 | 177 | 3impib 1229 |
. . . . . . . . . . . 12
                                                     |
179 | 178 | 3com13 1236 |
. . . . . . . . . . 11
                    

                               |
180 | 179 | 3expib 1234 |
. . . . . . . . . 10
  
                                                    |
181 | 160, 180 | vtoclga 3099 |
. . . . . . . . 9
                                   

                                              |
182 | 153, 181 | sylbir 218 |
. . . . . . . 8
                                   

                                              |
183 | 182 | 3impib 1229 |
. . . . . . 7
                                                                                 |
184 | 125, 126,
149, 183 | syl3anc 1292 |
. . . . . 6
    
                                                                                  |
185 | | 3anass 1011 |
. . . . . . . . 9
         
           |
186 | 185 | biimpri 211 |
. . . . . . . 8
           
         |
187 | 186 | adantl 473 |
. . . . . . 7
    
                                    
         |
188 | | nfv 1769 |
. . . . . . . . . 10
  |
189 | | nfv 1769 |
. . . . . . . . . 10
         |
190 | 188, 41, 189 | nf3an 2033 |
. . . . . . . . 9
  
        |
191 | | simpr 468 |
. . . . . . . . . . . 12
  
          |
192 | | fzfid 12224 |
. . . . . . . . . . . . 13
  
              |
193 | 42 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . 16
        
  |
194 | 193 | adantr 472 |
. . . . . . . . . . . . . . 15
  
          |
195 | 194 | adantr 472 |
. . . . . . . . . . . . . 14
   
      

       |
196 | | fzelp1 11874 |
. . . . . . . . . . . . . . . . 17
             |
197 | 196 | anim2i 579 |
. . . . . . . . . . . . . . . 16
   
      

                         |
198 | | an32 815 |
. . . . . . . . . . . . . . . 16
   
      

         

                |
199 | 197, 198 | sylib 201 |
. . . . . . . . . . . . . . 15
   
      

                         |
200 | 45 | 3ad2ant2 1052 |
. . . . . . . . . . . . . . . . . . 19
        
          |
201 | 200 | adantr 472 |
. . . . . . . . . . . . . . . . . 18
  
                        |
202 | | elfzuz3 11823 |
. . . . . . . . . . . . . . . . . . . . 21
               |
203 | | fzss2 11864 |
. . . . . . . . . . . . . . . . . . . . 21
      
            |
204 | 202, 203 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
                   |
205 | 204 | sselda 3418 |
. . . . . . . . . . . . . . . . . . 19
       
             |
206 | 205 | 3ad2antl3 1194 |
. . . . . . . . . . . . . . . . . 18
  
                    |
207 | 201, 206 | ffvelrnd 6038 |
. . . . . . . . . . . . . . . . 17
  
                    |
208 | | simpl2 1034 |
. . . . . . . . . . . . . . . . 17
  
                |
209 | | feq1 5720 |
. . . . . . . . . . . . . . . . . . 19
         
           |
210 | 209 | imbi2d 323 |
. . . . . . . . . . . . . . . . . 18
      
    
             |
211 | 210, 63 | vtoclga 3099 |
. . . . . . . . . . . . . . . . 17
                 |
212 | 207, 208,
211 | sylc 61 |
. . . . . . . . . . . . . . . 16
  
                        |
213 | 212 | fnvinran 37398 |
. . . . . . . . . . . . . . 15
   
      
       
          |
214 | 199, 213 | syl 17 |
. . . . . . . . . . . . . 14
   
      

               |
215 | 195, 214 | remulcld 9689 |
. . . . . . . . . . . . 13
   
      

                 |
216 | 192, 215 | fsumrecl 13877 |
. . . . . . . . . . . 12
  
                          |
217 | | eqid 2471 |
. . . . . . . . . . . . 13
                                     |
218 | 217 | fvmpt2 5972 |
. . . . . . . . . . . 12
                                                           |
219 | 191, 216,
218 | syl2anc 673 |
. . . . . . . . . . 11
  
                                                |
220 | 219 | oveq1d 6323 |
. . . . . . . . . 10
  
                                                                            |
221 | | 3simpc 1029 |
. . . . . . . . . . . . . . . 16
        
          |
222 | 221 | adantr 472 |
. . . . . . . . . . . . . . 15
  
                  |
223 | | feq1 5720 |
. . . . . . . . . . . . . . . . . 18
    
      
             |
224 | 223 | imbi2d 323 |
. . . . . . . . . . . . . . . . 17
    
   
    
               |
225 | 224, 63 | vtoclga 3099 |
. . . . . . . . . . . . . . . 16
           
         |
226 | 91, 92, 225 | sylc 61 |
. . . . . . . . . . . . . . 15
 
                   |
227 | 222, 226 | syl 17 |
. . . . . . . . . . . . . 14
  
                    |
228 | 227, 191 | ffvelrnd 6038 |
. . . . . . . . . . . . 13
  
                    |
229 | 194, 228 | remulcld 9689 |
. . . . . . . . . . . 12
  
        
             |
230 | | eqid 2471 |
. . . . . . . . . . . . 13
                    
        |
231 | 230 | fvmpt2 5972 |
. . . . . . . . . . . 12
  
                                            |
232 | 191, 229,
231 | syl2anc 673 |
. . . . . . . . . . 11
  
                                        |
233 | 232 | oveq2d 6324 |
. . . . . . . . . 10
  
                                                                                        |
234 | | elfzuz 11822 |
. . . . . . . . . . . . . 14
               |
235 | 234 | 3ad2ant3 1053 |
. . . . . . . . . . . . 13
        
        |
236 | 235 | adantr 472 |
. . . . . . . . . . . 12
  
                |
237 | 194 | adantr 472 |
. . . . . . . . . . . . 13
   
      

         |
238 | 213 | an32s 821 |
. . . . . . . . . . . . 13
   
      

                 |
239 | | remulcl 9642 |
. . . . . . . . . . . . . 14
                       |
240 | 239 | recnd 9687 |
. . . . . . . . . . . . 13
                       |
241 | 237, 238,
240 | syl2anc 673 |
. . . . . . . . . . . 12
   
      

                   |
242 | | fveq2 5879 |
. . . . . . . . . . . . . 14
          
    |
243 | 242 | fveq1d 5881 |
. . . . . . . . . . . . 13
                       |
244 | 243 | oveq2d 6324 |
. . . . . . . . . . . 12
   
                       |
245 | 236, 241,
244 | fsumm1 13889 |
. . . . . . . . . . 11
  
                                                              |
246 | | nn0cn 10903 |
. . . . . . . . . . . . . . . . 17

  |
247 | 246 | 3ad2ant1 1051 |
. . . . . . . . . . . . . . . 16
        
  |
248 | 247 | adantr 472 |
. . . . . . . . . . . . . . 15
  
          |
249 | | 1cnd 9677 |
. . . . . . . . . . . . . . 15
  
          |
250 | 248, 249 | pncand 10006 |
. . . . . . . . . . . . . 14
  
              |
251 | 250 | oveq2d 6324 |
. . . . . . . . . . . . 13
  
                      |
252 | 251 | sumeq1d 13844 |
. . . . . . . . . . . 12
  
                            
                 |
253 | 252 | oveq1d 6323 |
. . . . . . . . . . 11
  
                                  
                                       |
254 | 245, 253 | eqtrd 2505 |
. . . . . . . . . 10
  
                                                          |
255 | 220, 233,
254 | 3eqtr4rd 2516 |
. . . . . . . . 9
  
                                                                      |
256 | 190, 255 | mpteq2da 4481 |
. . . . . . . 8
        

                                                                 |
257 | 256 | eleq1d 2533 |
. . . . . . 7
        
                    

                                              |
258 | 187, 257 | syl 17 |
. . . . . 6
    
                                                                                                        |
259 | 184, 258 | mpbird 240 |
. . . . 5
    
                                                          |
260 | 259 | exp32 616 |
. . . 4
                            

        

                       |
261 | 260 | pm2.86i 103 |
. . 3

                                                            |
262 | 14, 21, 28, 35, 80, 261 | nn0ind 11053 |
. 2

 
                          |
263 | 2, 7, 262 | sylc 61 |
1
                     |