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 ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑁 C 𝑘 ) )

Proof

Step Hyp Ref Expression
1 df-2 ⊢ 2 = ( 1 + 1 )
2 1 oveq1i ⊢ ( 2 ↑ 𝑁 ) = ( ( 1 + 1 ) ↑ 𝑁 )
3 ax-1cn ⊢ 1 ∈ ℂ
4 binom1p ⊢ ( ( 1 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( ( 1 + 1 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 1 ↑ 𝑘 ) ) )
5 3 4 mpan ⊢ ( 𝑁 ∈ ℕ0 → ( ( 1 + 1 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 1 ↑ 𝑘 ) ) )
6 2 5 syl5eq ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 1 ↑ 𝑘 ) ) )
7 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
8 1exp ⊢ ( 𝑘 ∈ ℤ → ( 1 ↑ 𝑘 ) = 1 )
9 7 8 syl ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 1 ↑ 𝑘 ) = 1 )
10 9 oveq2d ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 C 𝑘 ) · ( 1 ↑ 𝑘 ) ) = ( ( 𝑁 C 𝑘 ) · 1 ) )
11 bccl2 ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) ∈ ℕ )
12 11 nncnd ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
13 12 mulid1d ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 C 𝑘 ) · 1 ) = ( 𝑁 C 𝑘 ) )
14 10 13 eqtrd ⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( ( 𝑁 C 𝑘 ) · ( 1 ↑ 𝑘 ) ) = ( 𝑁 C 𝑘 ) )
15 14 sumeq2i ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( 1 ↑ 𝑘 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑁 C 𝑘 )
16 6 15 eqtrdi ⊢ ( 𝑁 ∈ ℕ0 → ( 2 ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑁 C 𝑘 ) )