Metamath Proof Explorer

Theorem binom11

Description: Special case of the binomial theorem for 2 ^ N . (Contributed by Mario Carneiro, 13-Mar-2014)

Ref Expression
Assertion binom11 
|- ( N e. NN0 -> ( 2 ^ N ) = sum_ k e. ( 0 ... N ) ( N _C k ) )

Proof

Step Hyp Ref Expression
1 df-2 
 |-  2 = ( 1 + 1 )
2 1 oveq1i 
 |-  ( 2 ^ N ) = ( ( 1 + 1 ) ^ N )
3 ax-1cn 
 |-  1 e. CC
4 binom1p 
 |-  ( ( 1 e. CC /\ N e. NN0 ) -> ( ( 1 + 1 ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( 1 ^ k ) ) )
5 3 4 mpan 
 |-  ( N e. NN0 -> ( ( 1 + 1 ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( 1 ^ k ) ) )
6 2 5 syl5eq 
 |-  ( N e. NN0 -> ( 2 ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( 1 ^ k ) ) )
7 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
8 1exp 
 |-  ( k e. ZZ -> ( 1 ^ k ) = 1 )
9 7 8 syl 
 |-  ( k e. ( 0 ... N ) -> ( 1 ^ k ) = 1 )
10 9 oveq2d 
 |-  ( k e. ( 0 ... N ) -> ( ( N _C k ) x. ( 1 ^ k ) ) = ( ( N _C k ) x. 1 ) )
11 bccl2 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) e. NN )
12 11 nncnd 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) e. CC )
13 12 mulid1d 
 |-  ( k e. ( 0 ... N ) -> ( ( N _C k ) x. 1 ) = ( N _C k ) )
14 10 13 eqtrd 
 |-  ( k e. ( 0 ... N ) -> ( ( N _C k ) x. ( 1 ^ k ) ) = ( N _C k ) )
15 14 sumeq2i 
 |-  sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( 1 ^ k ) ) = sum_ k e. ( 0 ... N ) ( N _C k )
16 6 15 eqtrdi 
 |-  ( N e. NN0 -> ( 2 ^ N ) = sum_ k e. ( 0 ... N ) ( N _C k ) )