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