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	eqtrid	⊢ ( 𝑁 ∈ ℕ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 𝑘 ) )