Metamath Proof Explorer

Theorem altgsumbc

Description: The sum of binomial coefficients for a fixed positive N with alternating signs is zero. Notice that this is not valid for N = 0 (since ( ( -u 1 ^ 0 ) x. ( 0 _C 0 ) ) = ( 1 x. 1 ) = 1 ). For a proof using Pascal's rule ( bcpascm1 ) instead of the binomial theorem ( binom ), see altgsumbcALT . (Contributed by AV, 13-Sep-2019)

Ref Expression
Assertion altgsumbc 
|- ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = 0 )

Proof

Step Hyp Ref Expression
1 1cnd 
 |-  ( N e. NN -> 1 e. CC )
2 negid 
 |-  ( 1 e. CC -> ( 1 + -u 1 ) = 0 )
3 2 eqcomd 
 |-  ( 1 e. CC -> 0 = ( 1 + -u 1 ) )
4 1 3 syl 
 |-  ( N e. NN -> 0 = ( 1 + -u 1 ) )
5 4 oveq1d 
 |-  ( N e. NN -> ( 0 ^ N ) = ( ( 1 + -u 1 ) ^ N ) )
6 0exp 
 |-  ( N e. NN -> ( 0 ^ N ) = 0 )
7 1 negcld 
 |-  ( N e. NN -> -u 1 e. CC )
8 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
9 binom 
 |-  ( ( 1 e. CC /\ -u 1 e. CC /\ N e. NN0 ) -> ( ( 1 + -u 1 ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) ) )
10 1 7 8 9 syl3anc 
 |-  ( N e. NN -> ( ( 1 + -u 1 ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) ) )
11 nnz 
 |-  ( N e. NN -> N e. ZZ )
12 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
13 zsubcl 
 |-  ( ( N e. ZZ /\ k e. ZZ ) -> ( N - k ) e. ZZ )
14 11 12 13 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( N - k ) e. ZZ )
15 1exp 
 |-  ( ( N - k ) e. ZZ -> ( 1 ^ ( N - k ) ) = 1 )
16 14 15 syl 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( 1 ^ ( N - k ) ) = 1 )
17 16 oveq1d 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) = ( 1 x. ( -u 1 ^ k ) ) )
18 neg1cn 
 |-  -u 1 e. CC
19 18 a1i 
 |-  ( N e. NN -> -u 1 e. CC )
20 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
21 expcl 
 |-  ( ( -u 1 e. CC /\ k e. NN0 ) -> ( -u 1 ^ k ) e. CC )
22 19 20 21 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( -u 1 ^ k ) e. CC )
23 22 mullidd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( 1 x. ( -u 1 ^ k ) ) = ( -u 1 ^ k ) )
24 17 23 eqtrd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) = ( -u 1 ^ k ) )
25 24 oveq2d 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) ) = ( ( N _C k ) x. ( -u 1 ^ k ) ) )
26 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
27 8 12 26 syl2an 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN0 )
28 27 nn0cnd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. CC )
29 28 22 mulcomd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( -u 1 ^ k ) ) = ( ( -u 1 ^ k ) x. ( N _C k ) ) )
30 25 29 eqtrd 
 |-  ( ( N e. NN /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) ) = ( ( -u 1 ^ k ) x. ( N _C k ) ) )
31 30 sumeq2dv 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( -u 1 ^ k ) ) ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) )
32 10 31 eqtrd 
 |-  ( N e. NN -> ( ( 1 + -u 1 ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) )
33 5 6 32 3eqtr3rd 
 |-  ( N e. NN -> sum_ k e. ( 0 ... N ) ( ( -u 1 ^ k ) x. ( N _C k ) ) = 0 )