Metamath Proof Explorer

Theorem binom1p

Description: Special case of the binomial theorem for ( 1 + A ) ^ N . (Contributed by Paul Chapman, 10-May-2007)

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

Proof

Step Hyp Ref Expression
1 ax-1cn 
 |-  1 e. CC
2 binom 
 |-  ( ( 1 e. CC /\ A e. CC /\ N e. NN0 ) -> ( ( 1 + A ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( A ^ k ) ) ) )
3 1 2 mp3an1 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( 1 + A ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( A ^ k ) ) ) )
4 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
5 4 adantl 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N - k ) e. NN0 )
6 5 nn0zd 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( N - k ) e. ZZ )
7 1exp 
 |-  ( ( N - k ) e. ZZ -> ( 1 ^ ( N - k ) ) = 1 )
8 6 7 syl 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( 1 ^ ( N - k ) ) = 1 )
9 8 oveq1d 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( 1 ^ ( N - k ) ) x. ( A ^ k ) ) = ( 1 x. ( A ^ k ) ) )
10 simpl 
 |-  ( ( A e. CC /\ N e. NN0 ) -> A e. CC )
11 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
12 expcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( A ^ k ) e. CC )
13 10 11 12 syl2an 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( A ^ k ) e. CC )
14 13 mulid2d 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( 1 x. ( A ^ k ) ) = ( A ^ k ) )
15 9 14 eqtrd 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( 1 ^ ( N - k ) ) x. ( A ^ k ) ) = ( A ^ k ) )
16 15 oveq2d 
 |-  ( ( ( A e. CC /\ N e. NN0 ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( A ^ k ) ) ) = ( ( N _C k ) x. ( A ^ k ) ) )
17 16 sumeq2dv 
 |-  ( ( A e. CC /\ N e. NN0 ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( 1 ^ ( N - k ) ) x. ( A ^ k ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) )
18 3 17 eqtrd 
 |-  ( ( A e. CC /\ N e. NN0 ) -> ( ( 1 + A ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( A ^ k ) ) )