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 \in ℂ \land N \in ℕ_{0}) \to {(1 + A)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{k}$

Proof

Step	Hyp	Ref	Expression
1		ax-1cn	$⊢ 1 \in ℂ$
2		binom	$⊢ (1 \in ℂ \land A \in ℂ \land N \in ℕ_{0}) \to {(1 + A)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{N - k} A^{k}$
3	1 2	mp3an1	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(1 + A)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) 1^{N - k} A^{k}$
4		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
5	4	adantl	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to N - k \in ℕ_{0}$
6	5	nn0zd	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to N - k \in ℤ$
7		1exp	$⊢ N - k \in ℤ \to 1^{N - k} = 1$
8	6 7	syl	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to 1^{N - k} = 1$
9	8	oveq1d	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to 1^{N - k} A^{k} = 1 A^{k}$
10		simpl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A \in ℂ$
11		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
12		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
13	10 11 12	syl2an	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A^{k} \in ℂ$
14	13	mullidd	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to 1 A^{k} = A^{k}$
15	9 14	eqtrd	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to 1^{N - k} A^{k} = A^{k}$
16	15	oveq2d	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to (\binom{N}{k}) 1^{N - k} A^{k} = (\binom{N}{k}) A^{k}$
17	16	sumeq2dv	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \sum_{k = 0}^{N} (\binom{N}{k}) 1^{N - k} A^{k} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{k}$
18	3 17	eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(1 + A)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{k}$