Metamath Proof Explorer

Theorem binom1dif

Description: A summation for the difference between ( ( A + 1 ) ^ N ) and ( A ^ N ) . (Contributed by Scott Fenton, 9-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion binom1dif 
|- ( ( A e. CC /\ N e. NN0 ) -> ( ( ( A + 1 ) ^ N ) - ( A ^ N ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) )

Proof

Step Hyp Ref Expression
1 fzfid 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( 0 ... ( N - 1 ) ) e. Fin )
2 fzssp1 
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
3 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
4 3 adantl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> N e. CC )
5 ax-1cn 
 |-  1 e. CC
6 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
7 4 5 6 sylancl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( N - 1 ) + 1 ) = N )
8 7 oveq2d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
9 2 8 sseqtrid 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
10 9 sselda 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. ( 0 ... N ) )
11 bccl2 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) e. NN )
12 11 adantl 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN )
13 12 nncnd 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. CC )
14 simpl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> A e. CC )
15 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
16 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
17 14 15 16 syl2an 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( A ^ k ) e. CC )
18 13 17 mulcld 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( A ^ k ) ) e. CC )
19 10 18 syldan 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( A ^ k ) ) e. CC )
20 1 19 fsumcl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) e. CC )
21 expcl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A ^ N ) e. CC )
22 addcom 
 |-  ( ( A e. CC /\ 1 e. CC ) -> ( A + 1 ) = ( 1 + A ) )
23 14 5 22 sylancl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( A + 1 ) = ( 1 + A ) )
24 23 oveq1d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( A + 1 ) ^ N ) = ( ( 1 + A ) ^ N ) )
25 binom1p 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( 1 + A ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) )
26 simpr 
 |-  ( ( A e. CC /\ N e. NN0 ) -> N e. NN0 )
27 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
28 26 27 eleqtrdi 
 |-  ( ( A e. CC /\ N e. NN0 ) -> N e. ( ZZ>= ` 0 ) )
29 oveq2 
 |-  ( k = N -> ( N _C k ) = ( N _C N ) )
30 oveq2 
 |-  ( k = N -> ( A ^ k ) = ( A ^ N ) )
31 29 30 oveq12d 
 |-  ( k = N -> ( ( N _C k ) x. ( A ^ k ) ) = ( ( N _C N ) x. ( A ^ N ) ) )
32 28 18 31 fsumm1 
 |-  ( ( A e. CC /\ N e. NN0 ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) + ( ( N _C N ) x. ( A ^ N ) ) ) )
33 bcnn 
 |-  ( N e. NN0 -> ( N _C N ) = 1 )
34 33 adantl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( N _C N ) = 1 )
35 34 oveq1d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( N _C N ) x. ( A ^ N ) ) = ( 1 x. ( A ^ N ) ) )
36 21 mullidd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( 1 x. ( A ^ N ) ) = ( A ^ N ) )
37 35 36 eqtrd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( N _C N ) x. ( A ^ N ) ) = ( A ^ N ) )
38 37 oveq2d 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) + ( ( N _C N ) x. ( A ^ N ) ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) + ( A ^ N ) ) )
39 32 38 eqtrd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) + ( A ^ N ) ) )
40 24 25 39 3eqtrd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( A + 1 ) ^ N ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) + ( A ^ N ) ) )
41 20 21 40 mvrraddd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( ( A + 1 ) ^ N ) - ( A ^ N ) ) = sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( A ^ k ) ) )