binom11

Description: Special case of the binomial theorem for 2 ^ N . (Contributed by Mario Carneiro, 13-Mar-2014)

		Ref	Expression
	Assertion	binom11	$⊢ N \in ℕ_{0} \to 2^{N} = \sum_{k = 0}^{N} (\binom{N}{k})$

Step	Hyp	Ref	Expression
1		df-2	$⊢ 2 = 1 + 1$
2	1	oveq1i	$⊢ 2^{N} = {(1 + 1)}^{N}$
3		ax-1cn	$⊢ 1 \in ℂ$
4		binom1p	$⊢ (1 \in ℂ \land N \in ℕ_{0}) \to {(1 + 1)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{k}$
5	3 4	mpan	$⊢ N \in ℕ_{0} \to {(1 + 1)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{k}$
6	2 5	syl5eq	$⊢ N \in ℕ_{0} \to 2^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{k}$
7		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
8		1exp	$⊢ k \in ℤ \to 1^{k} = 1$
9	7 8	syl	$⊢ k \in (0 \dots N) \to 1^{k} = 1$
10	9	oveq2d	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) 1^{k} = (\binom{N}{k}) \cdot 1$
11		bccl2	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) \in ℕ$
12	11	nncnd	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) \in ℂ$
13	12	mulid1d	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) \cdot 1 = (\binom{N}{k})$
14	10 13	eqtrd	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) 1^{k} = (\binom{N}{k})$
15	14	sumeq2i	$⊢ \sum_{k = 0}^{N} (\binom{N}{k}) 1^{k} = \sum_{k = 0}^{N} (\binom{N}{k})$
16	6 15	eqtrdi	$⊢ N \in ℕ_{0} \to 2^{N} = \sum_{k = 0}^{N} (\binom{N}{k})$

Metamath Proof Explorer