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 N 0 1 + A N = k = 0 N ( N k) A k

Proof

Step Hyp Ref Expression
1 ax-1cn 1
2 binom 1 A N 0 1 + A N = k = 0 N ( N k) 1 N k A k
3 1 2 mp3an1 A N 0 1 + A N = k = 0 N ( N k) 1 N k A k
4 fznn0sub k 0 N N k 0
5 4 adantl A N 0 k 0 N N k 0
6 5 nn0zd A N 0 k 0 N N k
7 1exp N k 1 N k = 1
8 6 7 syl A N 0 k 0 N 1 N k = 1
9 8 oveq1d A N 0 k 0 N 1 N k A k = 1 A k
10 simpl A N 0 A
11 elfznn0 k 0 N k 0
12 expcl A k 0 A k
13 10 11 12 syl2an A N 0 k 0 N A k
14 13 mulid2d A N 0 k 0 N 1 A k = A k
15 9 14 eqtrd A N 0 k 0 N 1 N k A k = A k
16 15 oveq2d A N 0 k 0 N ( N k) 1 N k A k = ( N k) A k
17 16 sumeq2dv A N 0 k = 0 N ( N k) 1 N k A k = k = 0 N ( N k) A k
18 3 17 eqtrd A N 0 1 + A N = k = 0 N ( N k) A k