Step | Hyp | Ref
| Expression |
1 | | binomlem.4 |
. . . . . 6
                               |
2 | 1 | adantl 473 |
. . . . 5
 
                               |
3 | 2 | oveq1d 6323 |
. . . 4
 
          
                        |
4 | | fzfid 12224 |
. . . . . . 7
       |
5 | | binomlem.1 |
. . . . . . 7
   |
6 | | fzelp1 11874 |
. . . . . . . . 9
        
    |
7 | | binomlem.3 |
. . . . . . . . . . 11
   |
8 | | elfzelz 11826 |
. . . . . . . . . . 11
         |
9 | | bccl 12545 |
. . . . . . . . . . 11
 
     |
10 | 7, 8, 9 | syl2an 485 |
. . . . . . . . . 10
 
   
       |
11 | 10 | nn0cnd 10951 |
. . . . . . . . 9
 
   
       |
12 | 6, 11 | sylan2 482 |
. . . . . . . 8
 
         |
13 | | fznn0sub 11857 |
. . . . . . . . . 10
     
   |
14 | | expcl 12328 |
. . . . . . . . . 10
  
     
    |
15 | 5, 13, 14 | syl2an 485 |
. . . . . . . . 9
 
             |
16 | | binomlem.2 |
. . . . . . . . . . 11
   |
17 | | elfznn0 11913 |
. . . . . . . . . . 11
         |
18 | | expcl 12328 |
. . . . . . . . . . 11
 
       |
19 | 16, 17, 18 | syl2an 485 |
. . . . . . . . . 10
 
   
         |
20 | 6, 19 | sylan2 482 |
. . . . . . . . 9
 
           |
21 | 15, 20 | mulcld 9681 |
. . . . . . . 8
 
         
         |
22 | 12, 21 | mulcld 9681 |
. . . . . . 7
 
                       |
23 | 4, 5, 22 | fsummulc1 13923 |
. . . . . 6
               
                                   |
24 | 5 | adantr 472 |
. . . . . . . . 9
 
       |
25 | 12, 21, 24 | mulassd 9684 |
. . . . . . . 8
 
             
                             |
26 | 7 | nn0cnd 10951 |
. . . . . . . . . . . . . . 15
   |
27 | 26 | adantr 472 |
. . . . . . . . . . . . . 14
 
       |
28 | | 1cnd 9677 |
. . . . . . . . . . . . . 14
 
       |
29 | | elfzelz 11826 |
. . . . . . . . . . . . . . . 16
       |
30 | 29 | adantl 473 |
. . . . . . . . . . . . . . 15
 
       |
31 | 30 | zcnd 11064 |
. . . . . . . . . . . . . 14
 
       |
32 | 27, 28, 31 | addsubd 10026 |
. . . . . . . . . . . . 13
 
               |
33 | 32 | oveq2d 6324 |
. . . . . . . . . . . 12
 
                       |
34 | | expp1 12317 |
. . . . . . . . . . . . 13
  
                    |
35 | 5, 13, 34 | syl2an 485 |
. . . . . . . . . . . 12
 
                       |
36 | 33, 35 | eqtrd 2505 |
. . . . . . . . . . 11
 
                       |
37 | 36 | oveq1d 6323 |
. . . . . . . . . 10
 
                                   |
38 | 15, 24, 20 | mul32d 9861 |
. . . . . . . . . 10
 
                                   |
39 | 37, 38 | eqtrd 2505 |
. . . . . . . . 9
 
                                   |
40 | 39 | oveq2d 6324 |
. . . . . . . 8
 
                                           |
41 | 25, 40 | eqtr4d 2508 |
. . . . . . 7
 
             
                             |
42 | 41 | sumeq2dv 13846 |
. . . . . 6
                                                   |
43 | | fzssp1 11867 |
. . . . . . . 8
       
   |
44 | 43 | a1i 11 |
. . . . . . 7
    
        |
45 | | fznn0sub 11857 |
. . . . . . . . . . 11
             |
46 | | expcl 12328 |
. . . . . . . . . . 11
                 |
47 | 5, 45, 46 | syl2an 485 |
. . . . . . . . . 10
 
   
             |
48 | 47, 19 | mulcld 9681 |
. . . . . . . . 9
 
   
                   |
49 | 11, 48 | mulcld 9681 |
. . . . . . . 8
 
   
                       |
50 | 6, 49 | sylan2 482 |
. . . . . . 7
 
                         |
51 | 7 | adantr 472 |
. . . . . . . . . 10
 
            
  |
52 | | eldifi 3544 |
. . . . . . . . . . . 12
                
    |
53 | 52, 8 | syl 17 |
. . . . . . . . . . 11
               |
54 | 53 | adantl 473 |
. . . . . . . . . 10
 
            
  |
55 | | eldifn 3545 |
. . . . . . . . . . 11
            
      |
56 | 55 | adantl 473 |
. . . . . . . . . 10
 
            
      |
57 | | bcval3 12529 |
. . . . . . . . . 10
 
         |
58 | 51, 54, 56, 57 | syl3anc 1292 |
. . . . . . . . 9
 
            
    |
59 | 58 | oveq1d 6323 |
. . . . . . . 8
 
            
                                    |
60 | 48 | mul02d 9849 |
. . . . . . . . 9
 
   
                     |
61 | 52, 60 | sylan2 482 |
. . . . . . . 8
 
            
                  |
62 | 59, 61 | eqtrd 2505 |
. . . . . . 7
 
            
                    |
63 | | fzssuz 11865 |
. . . . . . . 8
           |
64 | 63 | a1i 11 |
. . . . . . 7
    
 
      |
65 | 44, 50, 62, 64 | sumss 13867 |
. . . . . 6
                             
                       |
66 | 23, 42, 65 | 3eqtrd 2509 |
. . . . 5
               
                                     |
67 | 66 | adantr 472 |
. . . 4
 
               
                                     |
68 | 3, 67 | eqtrd 2505 |
. . 3
 
             
                       |
69 | 1 | oveq1d 6323 |
. . . 4
          
                        |
70 | 4, 16, 22 | fsummulc1 13923 |
. . . . 5
               
                                   |
71 | | 1zzd 10992 |
. . . . . . . 8
   |
72 | | 0z 10972 |
. . . . . . . . 9
 |
73 | 72 | a1i 11 |
. . . . . . . 8
   |
74 | 7 | nn0zd 11061 |
. . . . . . . 8
   |
75 | 16 | adantr 472 |
. . . . . . . . 9
 
       |
76 | 22, 75 | mulcld 9681 |
. . . . . . . 8
 
             
           |
77 | | oveq2 6316 |
. . . . . . . . . 10
           |
78 | | oveq2 6316 |
. . . . . . . . . . . 12
   
       |
79 | 78 | oveq2d 6324 |
. . . . . . . . . . 11
            
      |
80 | | oveq2 6316 |
. . . . . . . . . . 11
               |
81 | 79, 80 | oveq12d 6326 |
. . . . . . . . . 10
       
                         |
82 | 77, 81 | oveq12d 6326 |
. . . . . . . . 9
                                           |
83 | 82 | oveq1d 6323 |
. . . . . . . 8
           
                                   |
84 | 71, 73, 74, 76, 83 | fsumshft 13918 |
. . . . . . 7
                                                             |
85 | | oveq1 6315 |
. . . . . . . . . . 11
       |
86 | 85 | oveq2d 6324 |
. . . . . . . . . 10
           |
87 | 85 | oveq2d 6324 |
. . . . . . . . . . . 12
 
         |
88 | 87 | oveq2d 6324 |
. . . . . . . . . . 11
            
      |
89 | 85 | oveq2d 6324 |
. . . . . . . . . . 11
               |
90 | 88, 89 | oveq12d 6326 |
. . . . . . . . . 10
     
                             |
91 | 86, 90 | oveq12d 6326 |
. . . . . . . . 9
                                               |
92 | 91 | oveq1d 6323 |
. . . . . . . 8
           
                                       |
93 | 92 | cbvsumv 13839 |
. . . . . . 7
      
                           
                   
              |
94 | 84, 93 | syl6eq 2521 |
. . . . . 6
                                                             |
95 | 26 | adantr 472 |
. . . . . . . . . . . . 13
 
     
     |
96 | | elfzelz 11826 |
. . . . . . . . . . . . . . 15
           |
97 | 96 | adantl 473 |
. . . . . . . . . . . . . 14
 
     
     |
98 | 97 | zcnd 11064 |
. . . . . . . . . . . . 13
 
     
     |
99 | | 1cnd 9677 |
. . . . . . . . . . . . 13
 
     
     |
100 | 95, 98, 99 | subsub3d 10035 |
. . . . . . . . . . . 12
 
     
   
         |
101 | 100 | oveq2d 6324 |
. . . . . . . . . . 11
 
     
                     |
102 | 101 | oveq1d 6323 |
. . . . . . . . . 10
 
     
       
                             |
103 | 102 | oveq2d 6324 |
. . . . . . . . 9
 
     
                                                 |
104 | 103 | oveq1d 6323 |
. . . . . . . 8
 
     
             
                                       |
105 | | fzp1ss 11873 |
. . . . . . . . . . . 12
                 |
106 | 72, 105 | ax-mp 5 |
. . . . . . . . . . 11
           
   |
107 | 106 | sseli 3414 |
. . . . . . . . . 10
            
    |
108 | 7 | adantr 472 |
. . . . . . . . . . . 12
 
   
     |
109 | 8 | adantl 473 |
. . . . . . . . . . . . 13
 
   
     |
110 | | peano2zm 11004 |
. . . . . . . . . . . . 13
     |
111 | 109, 110 | syl 17 |
. . . . . . . . . . . 12
 
   
       |
112 | | bccl 12545 |
. . . . . . . . . . . 12
           |
113 | 108, 111,
112 | syl2anc 673 |
. . . . . . . . . . 11
 
   
         |
114 | 113 | nn0cnd 10951 |
. . . . . . . . . 10
 
   
         |
115 | 107, 114 | sylan2 482 |
. . . . . . . . 9
 
     
         |
116 | 107, 47 | sylan2 482 |
. . . . . . . . . 10
 
     
             |
117 | 16 | adantr 472 |
. . . . . . . . . . 11
 
     
     |
118 | | elfznn 11854 |
. . . . . . . . . . . . . 14
         |
119 | | 0p1e1 10743 |
. . . . . . . . . . . . . . 15
   |
120 | 119 | oveq1i 6318 |
. . . . . . . . . . . . . 14
           
   |
121 | 118, 120 | eleq2s 2567 |
. . . . . . . . . . . . 13
           |
122 | 121 | adantl 473 |
. . . . . . . . . . . 12
 
     
     |
123 | | nnm1nn0 10935 |
. . . . . . . . . . . 12
     |
124 | 122, 123 | syl 17 |
. . . . . . . . . . 11
 
     
       |
125 | 117, 124 | expcld 12454 |
. . . . . . . . . 10
 
     
           |
126 | 116, 125 | mulcld 9681 |
. . . . . . . . 9
 
     
                     |
127 | 115, 126,
117 | mulassd 9684 |
. . . . . . . 8
 
     
                                                     |
128 | 116, 125,
117 | mulassd 9684 |
. . . . . . . . . 10
 
     
                                         |
129 | | expm1t 12338 |
. . . . . . . . . . . 12
 
               |
130 | 16, 121, 129 | syl2an 485 |
. . . . . . . . . . 11
 
     
                 |
131 | 130 | oveq2d 6324 |
. . . . . . . . . 10
 
     
                                     |
132 | 128, 131 | eqtr4d 2508 |
. . . . . . . . 9
 
     
                                     |
133 | 132 | oveq2d 6324 |
. . . . . . . 8
 
     
                                                 |
134 | 104, 127,
133 | 3eqtrd 2509 |
. . . . . . 7
 
     
             
                                   |
135 | 134 | sumeq2dv 13846 |
. . . . . 6
                                                                   |
136 | 106 | a1i 11 |
. . . . . . 7
      
 
        |
137 | 114, 48 | mulcld 9681 |
. . . . . . . 8
 
   
                         |
138 | 107, 137 | sylan2 482 |
. . . . . . 7
 
     
                         |
139 | 7 | adantr 472 |
. . . . . . . . . 10
 
                   |
140 | | eldifi 3544 |
. . . . . . . . . . . . 13
             
      
    |
141 | 140 | adantl 473 |
. . . . . . . . . . . 12
 
                    
    |
142 | 141, 8 | syl 17 |
. . . . . . . . . . 11
 
                   |
143 | 142, 110 | syl 17 |
. . . . . . . . . 10
 
                     |
144 | | eldifn 3545 |
. . . . . . . . . . . 12
             
  
          |
145 | 144 | adantl 473 |
. . . . . . . . . . 11
 
                
          |
146 | 72 | a1i 11 |
. . . . . . . . . . . . 13
 
                   |
147 | 139 | nn0zd 11061 |
. . . . . . . . . . . . 13
 
                   |
148 | | 1zzd 10992 |
. . . . . . . . . . . . 13
 
                   |
149 | | fzaddel 11859 |
. . . . . . . . . . . . 13
                               |
150 | 146, 147,
143, 148, 149 | syl22anc 1293 |
. . . . . . . . . . . 12
 
                       
         
     |
151 | 142 | zcnd 11064 |
. . . . . . . . . . . . . 14
 
                   |
152 | | ax-1cn 9615 |
. . . . . . . . . . . . . 14
 |
153 | | npcan 9904 |
. . . . . . . . . . . . . 14
 
       |
154 | 151, 152,
153 | sylancl 675 |
. . . . . . . . . . . . 13
 
                       |
155 | 154 | eleq1d 2533 |
. . . . . . . . . . . 12
 
                             
     
     |
156 | 150, 155 | bitrd 261 |
. . . . . . . . . . 11
 
                       
     
     |
157 | 145, 156 | mtbird 308 |
. . . . . . . . . 10
 
                         |
158 | | bcval3 12529 |
. . . . . . . . . 10
                 |
159 | 139, 143,
157, 158 | syl3anc 1292 |
. . . . . . . . 9
 
                       |
160 | 159 | oveq1d 6323 |
. . . . . . . 8
 
                                                       |
161 | 140, 60 | sylan2 482 |
. . . . . . . 8
 
                                   |
162 | 160, 161 | eqtrd 2505 |
. . . . . . 7
 
                                       |
163 | 136, 138,
162, 64 | sumss 13867 |
. . . . . 6
                                   
                         |
164 | 94, 135, 163 | 3eqtrd 2509 |
. . . . 5
                                                       |
165 | 70, 164 | eqtrd 2505 |
. . . 4
               
                                       |
166 | 69, 165 | sylan9eqr 2527 |
. . 3
 
             
                         |
167 | 68, 166 | oveq12d 6326 |
. 2
 
                    
                                                        |
168 | 5, 16 | addcld 9680 |
. . . . 5
     |
169 | 168, 7 | expp1d 12455 |
. . . 4
      
              |
170 | 168, 7 | expcld 12454 |
. . . . 5
         |
171 | 170, 5, 16 | adddid 9685 |
. . . 4
        
                      |
172 | 169, 171 | eqtrd 2505 |
. . 3
      
                      |
173 | 172 | adantr 472 |
. 2
 
      
                      |
174 | | bcpasc 12544 |
. . . . . . . 8
 
               |
175 | 7, 8, 174 | syl2an 485 |
. . . . . . 7
 
   
                 |
176 | 175 | oveq1d 6323 |
. . . . . 6
 
   
                                                 |
177 | 11, 114, 48 | adddird 9686 |
. . . . . 6
 
   
                                                                     |
178 | 176, 177 | eqtr3d 2507 |
. . . . 5
 
   
                                                                 |
179 | 178 | sumeq2dv 13846 |
. . . 4
                                 
                                             |
180 | | fzfid 12224 |
. . . . 5
    
    |
181 | 180, 49, 137 | fsumadd 13882 |
. . . 4
                                                      
                         
                          |
182 | 179, 181 | eqtrd 2505 |
. . 3
                              
                                                        |
183 | 182 | adantr 472 |
. 2
 
                              
                                                        |
184 | 167, 173,
183 | 3eqtr4d 2515 |
1
 
      
      
                         |