binomlem

Description: Lemma for binom (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	binomlem.1	$⊢ φ \to A \in ℂ$
	binomlem.2	$⊢ φ \to B \in ℂ$
	binomlem.3	$⊢ φ \to N \in ℕ_{0}$
	binomlem.4	$⊢ ψ \to {(A + B)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k}$
Assertion	binomlem	$⊢ (φ \land ψ) \to {(A + B)}^{N + 1} = \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) A^{N + 1 - k} B^{k}$

Proof

Step	Hyp	Ref	Expression
1		binomlem.1	$⊢ φ \to A \in ℂ$
2		binomlem.2	$⊢ φ \to B \in ℂ$
3		binomlem.3	$⊢ φ \to N \in ℕ_{0}$
4		binomlem.4	$⊢ ψ \to {(A + B)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k}$
5	4	adantl	$⊢ (φ \land ψ) \to {(A + B)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k}$
6	5	oveq1d	$⊢ (φ \land ψ) \to {(A + B)}^{N} A = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} A$
7		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
8		fzelp1	$⊢ k \in (0 \dots N) \to k \in (0 \dots N + 1)$
9		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
10		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
11	3 9 10	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℕ_{0}$
12	11	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℂ$
13	8 12	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℂ$
14		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
15		expcl	$⊢ (A \in ℂ \land N - k \in ℕ_{0}) \to A^{N - k} \in ℂ$
16	1 14 15	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A^{N - k} \in ℂ$
17		elfznn0	$⊢ k \in (0 \dots N + 1) \to k \in ℕ_{0}$
18		expcl	$⊢ (B \in ℂ \land k \in ℕ_{0}) \to B^{k} \in ℂ$
19	2 17 18	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to B^{k} \in ℂ$
20	8 19	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to B^{k} \in ℂ$
21	16 20	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to A^{N - k} B^{k} \in ℂ$
22	13 21	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{N - k} B^{k} \in ℂ$
23	7 1 22	fsummulc1	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} A = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} A$
24	1	adantr	$⊢ (φ \land k \in (0 \dots N)) \to A \in ℂ$
25	13 21 24	mulassd	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{N - k} B^{k} A = (\binom{N}{k}) A^{N - k} B^{k} A$
26	3	nn0cnd	$⊢ φ \to N \in ℂ$
27	26	adantr	$⊢ (φ \land k \in (0 \dots N)) \to N \in ℂ$
28		1cnd	$⊢ (φ \land k \in (0 \dots N)) \to 1 \in ℂ$
29		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
30	29	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℤ$
31	30	zcnd	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℂ$
32	27 28 31	addsubd	$⊢ (φ \land k \in (0 \dots N)) \to N + 1 - k = N - k + 1$
33	32	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to A^{N + 1 - k} = A^{N - k + 1}$
34		expp1	$⊢ (A \in ℂ \land N - k \in ℕ_{0}) \to A^{N - k + 1} = A^{N - k} A$
35	1 14 34	syl2an	$⊢ (φ \land k \in (0 \dots N)) \to A^{N - k + 1} = A^{N - k} A$
36	33 35	eqtrd	$⊢ (φ \land k \in (0 \dots N)) \to A^{N + 1 - k} = A^{N - k} A$
37	36	oveq1d	$⊢ (φ \land k \in (0 \dots N)) \to A^{N + 1 - k} B^{k} = A^{N - k} A B^{k}$
38	16 24 20	mul32d	$⊢ (φ \land k \in (0 \dots N)) \to A^{N - k} A B^{k} = A^{N - k} B^{k} A$
39	37 38	eqtrd	$⊢ (φ \land k \in (0 \dots N)) \to A^{N + 1 - k} B^{k} = A^{N - k} B^{k} A$
40	39	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{N + 1 - k} B^{k} = (\binom{N}{k}) A^{N - k} B^{k} A$
41	25 40	eqtr4d	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{N - k} B^{k} A = (\binom{N}{k}) A^{N + 1 - k} B^{k}$
42	41	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} A = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N + 1 - k} B^{k}$
43		fzssp1	$⊢ (0 \dots N) \subseteq (0 \dots N + 1)$
44	43	a1i	$⊢ φ \to (0 \dots N) \subseteq (0 \dots N + 1)$
45		fznn0sub	$⊢ k \in (0 \dots N + 1) \to N + 1 - k \in ℕ_{0}$
46		expcl	$⊢ (A \in ℂ \land N + 1 - k \in ℕ_{0}) \to A^{N + 1 - k} \in ℂ$
47	1 45 46	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to A^{N + 1 - k} \in ℂ$
48	47 19	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to A^{N + 1 - k} B^{k} \in ℂ$
49	12 48	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) A^{N + 1 - k} B^{k} \in ℂ$
50	8 49	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{N + 1 - k} B^{k} \in ℂ$
51	3	adantr	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to N \in ℕ_{0}$
52		eldifi	$⊢ k \in ((0 \dots N + 1) ∖ (0 \dots N)) \to k \in (0 \dots N + 1)$
53	52 9	syl	$⊢ k \in ((0 \dots N + 1) ∖ (0 \dots N)) \to k \in ℤ$
54	53	adantl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to k \in ℤ$
55		eldifn	$⊢ k \in ((0 \dots N + 1) ∖ (0 \dots N)) \to \neg k \in (0 \dots N)$
56	55	adantl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to \neg k \in (0 \dots N)$
57		bcval3	$⊢ (N \in ℕ_{0} \land k \in ℤ \land \neg k \in (0 \dots N)) \to (\binom{N}{k}) = 0$
58	51 54 56 57	syl3anc	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to (\binom{N}{k}) = 0$
59	58	oveq1d	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to (\binom{N}{k}) A^{N + 1 - k} B^{k} = 0 \cdot A^{N + 1 - k} B^{k}$
60	48	mul02d	$⊢ (φ \land k \in (0 \dots N + 1)) \to 0 \cdot A^{N + 1 - k} B^{k} = 0$
61	52 60	sylan2	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to 0 \cdot A^{N + 1 - k} B^{k} = 0$
62	59 61	eqtrd	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 \dots N))) \to (\binom{N}{k}) A^{N + 1 - k} B^{k} = 0$
63		fzssuz	$⊢ (0 \dots N + 1) \subseteq ℤ_{\geq 0}$
64	63	a1i	$⊢ φ \to (0 \dots N + 1) \subseteq ℤ_{\geq 0}$
65	44 50 62 64	sumss	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N + 1 - k} B^{k} = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k}$
66	23 42 65	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} A = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k}$
67	66	adantr	$⊢ (φ \land ψ) \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} A = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k}$
68	6 67	eqtrd	$⊢ (φ \land ψ) \to {(A + B)}^{N} A = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k}$
69	4	oveq1d	$⊢ ψ \to {(A + B)}^{N} B = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B$
70	7 2 22	fsummulc1	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B$
71		1zzd	$⊢ φ \to 1 \in ℤ$
72		0z	$⊢ 0 \in ℤ$
73	72	a1i	$⊢ φ \to 0 \in ℤ$
74	3	nn0zd	$⊢ φ \to N \in ℤ$
75	2	adantr	$⊢ (φ \land k \in (0 \dots N)) \to B \in ℂ$
76	22 75	mulcld	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) A^{N - k} B^{k} B \in ℂ$
77		oveq2	$⊢ k = j - 1 \to (\binom{N}{k}) = (\binom{N}{j - 1})$
78		oveq2	$⊢ k = j - 1 \to N - k = N - (j - 1)$
79	78	oveq2d	$⊢ k = j - 1 \to A^{N - k} = A^{N - (j - 1)}$
80		oveq2	$⊢ k = j - 1 \to B^{k} = B^{j - 1}$
81	79 80	oveq12d	$⊢ k = j - 1 \to A^{N - k} B^{k} = A^{N - (j - 1)} B^{j - 1}$
82	77 81	oveq12d	$⊢ k = j - 1 \to (\binom{N}{k}) A^{N - k} B^{k} = (\binom{N}{j - 1}) A^{N - (j - 1)} B^{j - 1}$
83	82	oveq1d	$⊢ k = j - 1 \to (\binom{N}{k}) A^{N - k} B^{k} B = (\binom{N}{j - 1}) A^{N - (j - 1)} B^{j - 1} B$
84	71 73 74 76 83	fsumshft	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B = \sum_{j = 0 + 1}^{N + 1} (\binom{N}{j - 1}) A^{N - (j - 1)} B^{j - 1} B$
85		oveq1	$⊢ j = k \to j - 1 = k - 1$
86	85	oveq2d	$⊢ j = k \to (\binom{N}{j - 1}) = (\binom{N}{k - 1})$
87	85	oveq2d	$⊢ j = k \to N - (j - 1) = N - (k - 1)$
88	87	oveq2d	$⊢ j = k \to A^{N - (j - 1)} = A^{N - (k - 1)}$
89	85	oveq2d	$⊢ j = k \to B^{j - 1} = B^{k - 1}$
90	88 89	oveq12d	$⊢ j = k \to A^{N - (j - 1)} B^{j - 1} = A^{N - (k - 1)} B^{k - 1}$
91	86 90	oveq12d	$⊢ j = k \to (\binom{N}{j - 1}) A^{N - (j - 1)} B^{j - 1} = (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1}$
92	91	oveq1d	$⊢ j = k \to (\binom{N}{j - 1}) A^{N - (j - 1)} B^{j - 1} B = (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} B$
93	92	cbvsumv	$⊢ \sum_{j = 0 + 1}^{N + 1} (\binom{N}{j - 1}) A^{N - (j - 1)} B^{j - 1} B = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} B$
94	84 93	eqtrdi	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} B$
95	26	adantr	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to N \in ℂ$
96		elfzelz	$⊢ k \in (0 + 1 \dots N + 1) \to k \in ℤ$
97	96	adantl	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in ℤ$
98	97	zcnd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in ℂ$
99		1cnd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to 1 \in ℂ$
100	95 98 99	subsub3d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to N - (k - 1) = N + 1 - k$
101	100	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N - (k - 1)} = A^{N + 1 - k}$
102	101	oveq1d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N - (k - 1)} B^{k - 1} = A^{N + 1 - k} B^{k - 1}$
103	102	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} = (\binom{N}{k - 1}) A^{N + 1 - k} B^{k - 1}$
104	103	oveq1d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} B = (\binom{N}{k - 1}) A^{N + 1 - k} B^{k - 1} B$
105		fzp1ss	$⊢ 0 \in ℤ \to (0 + 1 \dots N + 1) \subseteq (0 \dots N + 1)$
106	72 105	ax-mp	$⊢ (0 + 1 \dots N + 1) \subseteq (0 \dots N + 1)$
107	106	sseli	$⊢ k \in (0 + 1 \dots N + 1) \to k \in (0 \dots N + 1)$
108	9	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℤ$
109		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
110	108 109	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k - 1 \in ℤ$
111		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
112	3 110 111	syl2an2r	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
113	112	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℂ$
114	107 113	sylan2	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℂ$
115	107 47	sylan2	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N + 1 - k} \in ℂ$
116	2	adantr	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to B \in ℂ$
117		elfznn	$⊢ k \in (1 \dots N + 1) \to k \in ℕ$
118		0p1e1	$⊢ 0 + 1 = 1$
119	118	oveq1i	$⊢ (0 + 1 \dots N + 1) = (1 \dots N + 1)$
120	117 119	eleq2s	$⊢ k \in (0 + 1 \dots N + 1) \to k \in ℕ$
121	120	adantl	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in ℕ$
122		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
123	121 122	syl	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k - 1 \in ℕ_{0}$
124	116 123	expcld	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to B^{k - 1} \in ℂ$
125	115 124	mulcld	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N + 1 - k} B^{k - 1} \in ℂ$
126	114 125 116	mulassd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N + 1 - k} B^{k - 1} B = (\binom{N}{k - 1}) A^{N + 1 - k} B^{k - 1} B$
127	115 124 116	mulassd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N + 1 - k} B^{k - 1} B = A^{N + 1 - k} B^{k - 1} B$
128		expm1t	$⊢ (B \in ℂ \land k \in ℕ) \to B^{k} = B^{k - 1} B$
129	2 120 128	syl2an	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to B^{k} = B^{k - 1} B$
130	129	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N + 1 - k} B^{k} = A^{N + 1 - k} B^{k - 1} B$
131	127 130	eqtr4d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to A^{N + 1 - k} B^{k - 1} B = A^{N + 1 - k} B^{k}$
132	131	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N + 1 - k} B^{k - 1} B = (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
133	104 126 132	3eqtrd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} B = (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
134	133	sumeq2dv	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) A^{N - (k - 1)} B^{k - 1} B = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
135	106	a1i	$⊢ φ \to (0 + 1 \dots N + 1) \subseteq (0 \dots N + 1)$
136	113 48	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N + 1 - k} B^{k} \in ℂ$
137	107 136	sylan2	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) A^{N + 1 - k} B^{k} \in ℂ$
138	3	adantr	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to N \in ℕ_{0}$
139		eldifi	$⊢ k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1)) \to k \in (0 \dots N + 1)$
140	139	adantl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to k \in (0 \dots N + 1)$
141	140 9	syl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to k \in ℤ$
142	141 109	syl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to k - 1 \in ℤ$
143		eldifn	$⊢ k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1)) \to \neg k \in (0 + 1 \dots N + 1)$
144	143	adantl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to \neg k \in (0 + 1 \dots N + 1)$
145	72	a1i	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to 0 \in ℤ$
146	138	nn0zd	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to N \in ℤ$
147		1zzd	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to 1 \in ℤ$
148		fzaddel	$⊢ ((0 \in ℤ \land N \in ℤ) \land (k - 1 \in ℤ \land 1 \in ℤ)) \to (k - 1 \in (0 \dots N) \leftrightarrow k - 1 + 1 \in (0 + 1 \dots N + 1))$
149	145 146 142 147 148	syl22anc	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to (k - 1 \in (0 \dots N) \leftrightarrow k - 1 + 1 \in (0 + 1 \dots N + 1))$
150	141	zcnd	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to k \in ℂ$
151		ax-1cn	$⊢ 1 \in ℂ$
152		npcan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k - 1 + 1 = k$
153	150 151 152	sylancl	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to k - 1 + 1 = k$
154	153	eleq1d	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to (k - 1 + 1 \in (0 + 1 \dots N + 1) \leftrightarrow k \in (0 + 1 \dots N + 1))$
155	149 154	bitrd	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to (k - 1 \in (0 \dots N) \leftrightarrow k \in (0 + 1 \dots N + 1))$
156	144 155	mtbird	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to \neg k - 1 \in (0 \dots N)$
157		bcval3	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ \land \neg k - 1 \in (0 \dots N)) \to (\binom{N}{k - 1}) = 0$
158	138 142 156 157	syl3anc	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to (\binom{N}{k - 1}) = 0$
159	158	oveq1d	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to (\binom{N}{k - 1}) A^{N + 1 - k} B^{k} = 0 \cdot A^{N + 1 - k} B^{k}$
160	139 60	sylan2	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to 0 \cdot A^{N + 1 - k} B^{k} = 0$
161	159 160	eqtrd	$⊢ (φ \land k \in ((0 \dots N + 1) ∖ (0 + 1 \dots N + 1))) \to (\binom{N}{k - 1}) A^{N + 1 - k} B^{k} = 0$
162	135 137 161 64	sumss	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k} = \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
163	94 134 162	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B = \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
164	70 163	eqtrd	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k} B = \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
165	69 164	sylan9eqr	$⊢ (φ \land ψ) \to {(A + B)}^{N} B = \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
166	68 165	oveq12d	$⊢ (φ \land ψ) \to {(A + B)}^{N} A + {(A + B)}^{N} B = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k} + \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
167	1 2	addcld	$⊢ φ \to A + B \in ℂ$
168	167 3	expp1d	$⊢ φ \to {(A + B)}^{N + 1} = {(A + B)}^{N} (A + B)$
169	167 3	expcld	$⊢ φ \to {(A + B)}^{N} \in ℂ$
170	169 1 2	adddid	$⊢ φ \to {(A + B)}^{N} (A + B) = {(A + B)}^{N} A + {(A + B)}^{N} B$
171	168 170	eqtrd	$⊢ φ \to {(A + B)}^{N + 1} = {(A + B)}^{N} A + {(A + B)}^{N} B$
172	171	adantr	$⊢ (φ \land ψ) \to {(A + B)}^{N + 1} = {(A + B)}^{N} A + {(A + B)}^{N} B$
173		bcpasc	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
174	3 9 173	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
175	174	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) A^{N + 1 - k} B^{k} = (\binom{N + 1}{k}) A^{N + 1 - k} B^{k}$
176	12 113 48	adddird	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) A^{N + 1 - k} B^{k} = (\binom{N}{k}) A^{N + 1 - k} B^{k} + (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
177	175 176	eqtr3d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N + 1}{k}) A^{N + 1 - k} B^{k} = (\binom{N}{k}) A^{N + 1 - k} B^{k} + (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
178	177	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) A^{N + 1 - k} B^{k} = \sum_{k = 0}^{N + 1} ((\binom{N}{k}) A^{N + 1 - k} B^{k} + (\binom{N}{k - 1}) A^{N + 1 - k} B^{k})$
179		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
180	179 49 136	fsumadd	$⊢ φ \to \sum_{k = 0}^{N + 1} ((\binom{N}{k}) A^{N + 1 - k} B^{k} + (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}) = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k} + \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
181	178 180	eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) A^{N + 1 - k} B^{k} = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k} + \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
182	181	adantr	$⊢ (φ \land ψ) \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) A^{N + 1 - k} B^{k} = \sum_{k = 0}^{N + 1} (\binom{N}{k}) A^{N + 1 - k} B^{k} + \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) A^{N + 1 - k} B^{k}$
183	166 172 182	3eqtr4d	$⊢ (φ \land ψ) \to {(A + B)}^{N + 1} = \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) A^{N + 1 - k} B^{k}$

Metamath Proof Explorer

Theorem binomlem

Proof