binom1dif

Description: A summation for the difference between ( ( A + 1 ) ^ N ) and ( A ^ N ) . (Contributed by Scott Fenton, 9-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

		Ref	Expression
	Assertion	binom1dif	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(A + 1)}^{N} - A^{N} = \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k}$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (0 \dots N - 1) \in Fin$
2		fzssp1	$⊢ (0 \dots N - 1) \subseteq (0 \dots N - 1 + 1)$
3		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
4	3	adantl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℂ$
5		ax-1cn	$⊢ 1 \in ℂ$
6		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
7	4 5 6	sylancl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N - 1 + 1 = N$
8	7	oveq2d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (0 \dots N - 1 + 1) = (0 \dots N)$
9	2 8	sseqtrid	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (0 \dots N - 1) \subseteq (0 \dots N)$
10	9	sselda	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N - 1)) \to k \in (0 \dots N)$
11		bccl2	$⊢ k \in (0 \dots N) \to (\binom{N}{k}) \in ℕ$
12	11	adantl	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℕ$
13	12	nncnd	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℂ$
14		simpl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A \in ℂ$
15		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
16		expcl	$⊢ (A \in ℂ \land k \in ℕ_{0}) \to A^{k} \in ℂ$
17	14 15 16	syl2an	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to A^{k} \in ℂ$
18	13 17	mulcld	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{k} \in ℂ$
19	10 18	syldan	$⊢ ((A \in ℂ \land N \in ℕ_{0}) \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) A^{k} \in ℂ$
20	1 19	fsumcl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k} \in ℂ$
21		expcl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A^{N} \in ℂ$
22		addcom	$⊢ (A \in ℂ \land 1 \in ℂ) \to A + 1 = 1 + A$
23	14 5 22	sylancl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to A + 1 = 1 + A$
24	23	oveq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(A + 1)}^{N} = {(1 + A)}^{N}$
25		binom1p	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(1 + A)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{k}$
26		simpr	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℕ_{0}$
27		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
28	26 27	eleqtrdi	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to N \in ℤ_{\geq 0}$
29		oveq2	$⊢ k = N \to (\binom{N}{k}) = (\binom{N}{N})$
30		oveq2	$⊢ k = N \to A^{k} = A^{N}$
31	29 30	oveq12d	$⊢ k = N \to (\binom{N}{k}) A^{k} = (\binom{N}{N}) A^{N}$
32	28 18 31	fsumm1	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{k} = \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k} + (\binom{N}{N}) A^{N}$
33		bcnn	$⊢ N \in ℕ_{0} \to (\binom{N}{N}) = 1$
34	33	adantl	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (\binom{N}{N}) = 1$
35	34	oveq1d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (\binom{N}{N}) A^{N} = 1 A^{N}$
36	21	mulid2d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to 1 A^{N} = A^{N}$
37	35 36	eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to (\binom{N}{N}) A^{N} = A^{N}$
38	37	oveq2d	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k} + (\binom{N}{N}) A^{N} = \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k} + A^{N}$
39	32 38	eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{k} = \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k} + A^{N}$
40	24 25 39	3eqtrd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(A + 1)}^{N} = \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k} + A^{N}$
41	20 21 40	mvrraddd	$⊢ (A \in ℂ \land N \in ℕ_{0}) \to {(A + 1)}^{N} - A^{N} = \sum_{k = 0}^{N - 1} (\binom{N}{k}) A^{k}$

Metamath Proof Explorer

Theorem binom1dif

Proof