bpolydiflem

	Ref	Expression
Hypotheses	bpolydiflem.1	$⊢ φ \to N \in ℕ$
	bpolydiflem.2	$⊢ φ \to X \in ℂ$
	bpolydiflem.3	$⊢ (φ \land k \in (1 \dots N - 1)) \to (k BernPoly (X + 1)) - (k BernPoly X) = k X^{k - 1}$
Assertion	bpolydiflem	$⊢ φ \to (N BernPoly (X + 1)) - (N BernPoly X) = N X^{N - 1}$

Proof

Step	Hyp	Ref	Expression
1		bpolydiflem.1	$⊢ φ \to N \in ℕ$
2		bpolydiflem.2	$⊢ φ \to X \in ℂ$
3		bpolydiflem.3	$⊢ (φ \land k \in (1 \dots N - 1)) \to (k BernPoly (X + 1)) - (k BernPoly X) = k X^{k - 1}$
4	1	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
5		peano2cn	$⊢ X \in ℂ \to X + 1 \in ℂ$
6	2 5	syl	$⊢ φ \to X + 1 \in ℂ$
7		bpolyval	$⊢ (N \in ℕ_{0} \land X + 1 \in ℂ) \to N BernPoly (X + 1) = {(X + 1)}^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1})$
8	4 6 7	syl2anc	$⊢ φ \to N BernPoly (X + 1) = {(X + 1)}^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1})$
9		bpolyval	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
10	4 2 9	syl2anc	$⊢ φ \to N BernPoly X = X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
11	8 10	oveq12d	$⊢ φ \to (N BernPoly (X + 1)) - (N BernPoly X) = {(X + 1)}^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}))$
12	6 4	expcld	$⊢ φ \to {(X + 1)}^{N} \in ℂ$
13		fzfid	$⊢ φ \to (0 \dots N - 1) \in Fin$
14		elfzelz	$⊢ k \in (0 \dots N - 1) \to k \in ℤ$
15		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
16	4 14 15	syl2an	$⊢ (φ \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) \in ℕ_{0}$
17	16	nn0cnd	$⊢ (φ \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) \in ℂ$
18		elfznn0	$⊢ k \in (0 \dots N - 1) \to k \in ℕ_{0}$
19		bpolycl	$⊢ (k \in ℕ_{0} \land X + 1 \in ℂ) \to k BernPoly (X + 1) \in ℂ$
20	18 6 19	syl2anr	$⊢ (φ \land k \in (0 \dots N - 1)) \to k BernPoly (X + 1) \in ℂ$
21		fzssp1	$⊢ (0 \dots N - 1) \subseteq (0 \dots N - 1 + 1)$
22	1	nncnd	$⊢ φ \to N \in ℂ$
23		ax-1cn	$⊢ 1 \in ℂ$
24		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
25	22 23 24	sylancl	$⊢ φ \to N - 1 + 1 = N$
26	25	oveq2d	$⊢ φ \to (0 \dots N - 1 + 1) = (0 \dots N)$
27	21 26	sseqtrid	$⊢ φ \to (0 \dots N - 1) \subseteq (0 \dots N)$
28	27	sselda	$⊢ (φ \land k \in (0 \dots N - 1)) \to k \in (0 \dots N)$
29		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
30	28 29	syl	$⊢ (φ \land k \in (0 \dots N - 1)) \to N - k \in ℕ_{0}$
31		nn0p1nn	$⊢ N - k \in ℕ_{0} \to N - k + 1 \in ℕ$
32	30 31	syl	$⊢ (φ \land k \in (0 \dots N - 1)) \to N - k + 1 \in ℕ$
33	32	nncnd	$⊢ (φ \land k \in (0 \dots N - 1)) \to N - k + 1 \in ℂ$
34	32	nnne0d	$⊢ (φ \land k \in (0 \dots N - 1)) \to N - k + 1 \neq 0$
35	20 33 34	divcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to \frac{k BernPoly (X + 1)}{N - k + 1} \in ℂ$
36	17 35	mulcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) \in ℂ$
37	13 36	fsumcl	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) \in ℂ$
38	2 4	expcld	$⊢ φ \to X^{N} \in ℂ$
39		bpolycl	$⊢ (k \in ℕ_{0} \land X \in ℂ) \to k BernPoly X \in ℂ$
40	18 2 39	syl2anr	$⊢ (φ \land k \in (0 \dots N - 1)) \to k BernPoly X \in ℂ$
41	40 33 34	divcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to \frac{k BernPoly X}{N - k + 1} \in ℂ$
42	17 41	mulcld	$⊢ (φ \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
43	13 42	fsumcl	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
44	12 37 38 43	sub4d	$⊢ φ \to {(X + 1)}^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})) = {(X + 1)}^{N} - X^{N} - (\sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}))$
45	27	sselda	$⊢ (φ \land m \in (0 \dots N - 1)) \to m \in (0 \dots N)$
46		bccl2	$⊢ m \in (0 \dots N) \to (\binom{N}{m}) \in ℕ$
47	46	adantl	$⊢ (φ \land m \in (0 \dots N)) \to (\binom{N}{m}) \in ℕ$
48	47	nncnd	$⊢ (φ \land m \in (0 \dots N)) \to (\binom{N}{m}) \in ℂ$
49		elfznn0	$⊢ m \in (0 \dots N) \to m \in ℕ_{0}$
50		expcl	$⊢ (X \in ℂ \land m \in ℕ_{0}) \to X^{m} \in ℂ$
51	2 49 50	syl2an	$⊢ (φ \land m \in (0 \dots N)) \to X^{m} \in ℂ$
52	48 51	mulcld	$⊢ (φ \land m \in (0 \dots N)) \to (\binom{N}{m}) X^{m} \in ℂ$
53	45 52	syldan	$⊢ (φ \land m \in (0 \dots N - 1)) \to (\binom{N}{m}) X^{m} \in ℂ$
54	13 53	fsumcl	$⊢ φ \to \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m} \in ℂ$
55		addcom	$⊢ (X \in ℂ \land 1 \in ℂ) \to X + 1 = 1 + X$
56	2 23 55	sylancl	$⊢ φ \to X + 1 = 1 + X$
57	56	oveq1d	$⊢ φ \to {(X + 1)}^{N} = {(1 + X)}^{N}$
58		binom1p	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to {(1 + X)}^{N} = \sum_{m = 0}^{N} (\binom{N}{m}) X^{m}$
59	2 4 58	syl2anc	$⊢ φ \to {(1 + X)}^{N} = \sum_{m = 0}^{N} (\binom{N}{m}) X^{m}$
60	57 59	eqtrd	$⊢ φ \to {(X + 1)}^{N} = \sum_{m = 0}^{N} (\binom{N}{m}) X^{m}$
61		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
62	4 61	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
63		oveq2	$⊢ m = N \to (\binom{N}{m}) = (\binom{N}{N})$
64		oveq2	$⊢ m = N \to X^{m} = X^{N}$
65	63 64	oveq12d	$⊢ m = N \to (\binom{N}{m}) X^{m} = (\binom{N}{N}) X^{N}$
66	62 52 65	fsumm1	$⊢ φ \to \sum_{m = 0}^{N} (\binom{N}{m}) X^{m} = \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m} + (\binom{N}{N}) X^{N}$
67		bcnn	$⊢ N \in ℕ_{0} \to (\binom{N}{N}) = 1$
68	4 67	syl	$⊢ φ \to (\binom{N}{N}) = 1$
69	68	oveq1d	$⊢ φ \to (\binom{N}{N}) X^{N} = 1 X^{N}$
70	38	mulid2d	$⊢ φ \to 1 X^{N} = X^{N}$
71	69 70	eqtrd	$⊢ φ \to (\binom{N}{N}) X^{N} = X^{N}$
72	71	oveq2d	$⊢ φ \to \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m} + (\binom{N}{N}) X^{N} = \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m} + X^{N}$
73	60 66 72	3eqtrd	$⊢ φ \to {(X + 1)}^{N} = \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m} + X^{N}$
74	54 38 73	mvrraddd	$⊢ φ \to {(X + 1)}^{N} - X^{N} = \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m}$
75		nnm1nn0	$⊢ N \in ℕ \to N - 1 \in ℕ_{0}$
76	1 75	syl	$⊢ φ \to N - 1 \in ℕ_{0}$
77	76 61	eleqtrdi	$⊢ φ \to N - 1 \in ℤ_{\geq 0}$
78		oveq2	$⊢ m = N - 1 \to (\binom{N}{m}) = (\binom{N}{N - 1})$
79		oveq2	$⊢ m = N - 1 \to X^{m} = X^{N - 1}$
80	78 79	oveq12d	$⊢ m = N - 1 \to (\binom{N}{m}) X^{m} = (\binom{N}{N - 1}) X^{N - 1}$
81	77 53 80	fsumm1	$⊢ φ \to \sum_{m = 0}^{N - 1} (\binom{N}{m}) X^{m} = \sum_{m = 0}^{N - 1 - 1} (\binom{N}{m}) X^{m} + (\binom{N}{N - 1}) X^{N - 1}$
82		1cnd	$⊢ φ \to 1 \in ℂ$
83	22 82 82	subsub4d	$⊢ φ \to N - 1 - 1 = N - (1 + 1)$
84		df-2	$⊢ 2 = 1 + 1$
85	84	oveq2i	$⊢ N - 2 = N - (1 + 1)$
86	83 85	eqtr4di	$⊢ φ \to N - 1 - 1 = N - 2$
87	86	oveq2d	$⊢ φ \to (0 \dots N - 1 - 1) = (0 \dots N - 2)$
88	87	sumeq1d	$⊢ φ \to \sum_{m = 0}^{N - 1 - 1} (\binom{N}{m}) X^{m} = \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m}$
89		bcnm1	$⊢ N \in ℕ_{0} \to (\binom{N}{N - 1}) = N$
90	4 89	syl	$⊢ φ \to (\binom{N}{N - 1}) = N$
91	90	oveq1d	$⊢ φ \to (\binom{N}{N - 1}) X^{N - 1} = N X^{N - 1}$
92	88 91	oveq12d	$⊢ φ \to \sum_{m = 0}^{N - 1 - 1} (\binom{N}{m}) X^{m} + (\binom{N}{N - 1}) X^{N - 1} = \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} + N X^{N - 1}$
93	74 81 92	3eqtrd	$⊢ φ \to {(X + 1)}^{N} - X^{N} = \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} + N X^{N - 1}$
94		oveq2	$⊢ k = 0 \to (\binom{N}{k}) = (\binom{N}{0})$
95		oveq1	$⊢ k = 0 \to k BernPoly (X + 1) = 0 BernPoly (X + 1)$
96		oveq2	$⊢ k = 0 \to N - k = N - 0$
97	96	oveq1d	$⊢ k = 0 \to N - k + 1 = N - 0 + 1$
98	95 97	oveq12d	$⊢ k = 0 \to \frac{k BernPoly (X + 1)}{N - k + 1} = \frac{0 BernPoly (X + 1)}{N - 0 + 1}$
99	94 98	oveq12d	$⊢ k = 0 \to (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) = (\binom{N}{0}) (\frac{0 BernPoly (X + 1)}{N - 0 + 1})$
100	77 36 99	fsum1p	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) = (\binom{N}{0}) (\frac{0 BernPoly (X + 1)}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1})$
101		bpoly0	$⊢ X + 1 \in ℂ \to 0 BernPoly (X + 1) = 1$
102	6 101	syl	$⊢ φ \to 0 BernPoly (X + 1) = 1$
103	102	oveq1d	$⊢ φ \to \frac{0 BernPoly (X + 1)}{N - 0 + 1} = \frac{1}{N - 0 + 1}$
104	103	oveq2d	$⊢ φ \to (\binom{N}{0}) (\frac{0 BernPoly (X + 1)}{N - 0 + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1})$
105	104	oveq1d	$⊢ φ \to (\binom{N}{0}) (\frac{0 BernPoly (X + 1)}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1})$
106	100 105	eqtrd	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1})$
107		oveq1	$⊢ k = 0 \to k BernPoly X = 0 BernPoly X$
108	107 97	oveq12d	$⊢ k = 0 \to \frac{k BernPoly X}{N - k + 1} = \frac{0 BernPoly X}{N - 0 + 1}$
109	94 108	oveq12d	$⊢ k = 0 \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{0}) (\frac{0 BernPoly X}{N - 0 + 1})$
110	77 42 109	fsum1p	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{0}) (\frac{0 BernPoly X}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
111		bpoly0	$⊢ X \in ℂ \to 0 BernPoly X = 1$
112	2 111	syl	$⊢ φ \to 0 BernPoly X = 1$
113	112	oveq1d	$⊢ φ \to \frac{0 BernPoly X}{N - 0 + 1} = \frac{1}{N - 0 + 1}$
114	113	oveq2d	$⊢ φ \to (\binom{N}{0}) (\frac{0 BernPoly X}{N - 0 + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1})$
115	114	oveq1d	$⊢ φ \to (\binom{N}{0}) (\frac{0 BernPoly X}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
116	110 115	eqtrd	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
117	106 116	oveq12d	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - ((\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}))$
118		0z	$⊢ 0 \in ℤ$
119		bccl	$⊢ (N \in ℕ_{0} \land 0 \in ℤ) \to (\binom{N}{0}) \in ℕ_{0}$
120	4 118 119	sylancl	$⊢ φ \to (\binom{N}{0}) \in ℕ_{0}$
121	120	nn0cnd	$⊢ φ \to (\binom{N}{0}) \in ℂ$
122	22	subid1d	$⊢ φ \to N - 0 = N$
123	122 1	eqeltrd	$⊢ φ \to N - 0 \in ℕ$
124	123	peano2nnd	$⊢ φ \to N - 0 + 1 \in ℕ$
125	124	nnrecred	$⊢ φ \to \frac{1}{N - 0 + 1} \in ℝ$
126	125	recnd	$⊢ φ \to \frac{1}{N - 0 + 1} \in ℂ$
127	121 126	mulcld	$⊢ φ \to (\binom{N}{0}) (\frac{1}{N - 0 + 1}) \in ℂ$
128		fzfid	$⊢ φ \to (0 + 1 \dots N - 1) \in Fin$
129		fzp1ss	$⊢ 0 \in ℤ \to (0 + 1 \dots N - 1) \subseteq (0 \dots N - 1)$
130	118 129	ax-mp	$⊢ (0 + 1 \dots N - 1) \subseteq (0 \dots N - 1)$
131	130	sseli	$⊢ k \in (0 + 1 \dots N - 1) \to k \in (0 \dots N - 1)$
132	131 36	sylan2	$⊢ (φ \land k \in (0 + 1 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) \in ℂ$
133	128 132	fsumcl	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) \in ℂ$
134	131 42	sylan2	$⊢ (φ \land k \in (0 + 1 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
135	128 134	fsumcl	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
136	127 133 135	pnpcand	$⊢ φ \to (\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - ((\binom{N}{0}) (\frac{1}{N - 0 + 1}) + \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})) = \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
137		1zzd	$⊢ φ \to 1 \in ℤ$
138		0zd	$⊢ φ \to 0 \in ℤ$
139	1	nnzd	$⊢ φ \to N \in ℤ$
140		2z	$⊢ 2 \in ℤ$
141		zsubcl	$⊢ (N \in ℤ \land 2 \in ℤ) \to N - 2 \in ℤ$
142	139 140 141	sylancl	$⊢ φ \to N - 2 \in ℤ$
143		fzssp1	$⊢ (0 \dots N - 2) \subseteq (0 \dots N - 2 + 1)$
144		2cnd	$⊢ φ \to 2 \in ℂ$
145	22 144 82	subsubd	$⊢ φ \to N - (2 - 1) = N - 2 + 1$
146		2m1e1	$⊢ 2 - 1 = 1$
147	146	oveq2i	$⊢ N - (2 - 1) = N - 1$
148	145 147	eqtr3di	$⊢ φ \to N - 2 + 1 = N - 1$
149	148	oveq2d	$⊢ φ \to (0 \dots N - 2 + 1) = (0 \dots N - 1)$
150	143 149	sseqtrid	$⊢ φ \to (0 \dots N - 2) \subseteq (0 \dots N - 1)$
151	150	sselda	$⊢ (φ \land m \in (0 \dots N - 2)) \to m \in (0 \dots N - 1)$
152	151 53	syldan	$⊢ (φ \land m \in (0 \dots N - 2)) \to (\binom{N}{m}) X^{m} \in ℂ$
153		oveq2	$⊢ m = k - 1 \to (\binom{N}{m}) = (\binom{N}{k - 1})$
154		oveq2	$⊢ m = k - 1 \to X^{m} = X^{k - 1}$
155	153 154	oveq12d	$⊢ m = k - 1 \to (\binom{N}{m}) X^{m} = (\binom{N}{k - 1}) X^{k - 1}$
156	137 138 142 152 155	fsumshft	$⊢ φ \to \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} = \sum_{k = 0 + 1}^{N - 2 + 1} (\binom{N}{k - 1}) X^{k - 1}$
157	148	oveq2d	$⊢ φ \to (0 + 1 \dots N - 2 + 1) = (0 + 1 \dots N - 1)$
158	157	sumeq1d	$⊢ φ \to \sum_{k = 0 + 1}^{N - 2 + 1} (\binom{N}{k - 1}) X^{k - 1} = \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k - 1}) X^{k - 1}$
159	156 158	eqtrd	$⊢ φ \to \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} = \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k - 1}) X^{k - 1}$
160		0p1e1	$⊢ 0 + 1 = 1$
161	160	oveq1i	$⊢ (0 + 1 \dots N - 1) = (1 \dots N - 1)$
162	161	eleq2i	$⊢ k \in (0 + 1 \dots N - 1) \leftrightarrow k \in (1 \dots N - 1)$
163		fzssp1	$⊢ (1 \dots N - 1) \subseteq (1 \dots N - 1 + 1)$
164	25	oveq2d	$⊢ φ \to (1 \dots N - 1 + 1) = (1 \dots N)$
165	163 164	sseqtrid	$⊢ φ \to (1 \dots N - 1) \subseteq (1 \dots N)$
166	165	sselda	$⊢ (φ \land k \in (1 \dots N - 1)) \to k \in (1 \dots N)$
167		bcm1k	$⊢ k \in (1 \dots N) \to (\binom{N}{k}) = (\binom{N}{k - 1}) (\frac{N - (k - 1)}{k})$
168	166 167	syl	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k}) = (\binom{N}{k - 1}) (\frac{N - (k - 1)}{k})$
169	1	adantr	$⊢ (φ \land k \in (1 \dots N - 1)) \to N \in ℕ$
170	169	nncnd	$⊢ (φ \land k \in (1 \dots N - 1)) \to N \in ℂ$
171		elfznn	$⊢ k \in (1 \dots N - 1) \to k \in ℕ$
172	171	adantl	$⊢ (φ \land k \in (1 \dots N - 1)) \to k \in ℕ$
173	172	nncnd	$⊢ (φ \land k \in (1 \dots N - 1)) \to k \in ℂ$
174		1cnd	$⊢ (φ \land k \in (1 \dots N - 1)) \to 1 \in ℂ$
175	170 173 174	subsubd	$⊢ (φ \land k \in (1 \dots N - 1)) \to N - (k - 1) = N - k + 1$
176	175	oveq1d	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{N - (k - 1)}{k} = \frac{N - k + 1}{k}$
177	176	oveq2d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k - 1}) (\frac{N - (k - 1)}{k}) = (\binom{N}{k - 1}) (\frac{N - k + 1}{k})$
178	168 177	eqtrd	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k}) = (\binom{N}{k - 1}) (\frac{N - k + 1}{k})$
179	3	oveq1d	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{(k BernPoly (X + 1)) - (k BernPoly X)}{N - k + 1} = \frac{k X^{k - 1}}{N - k + 1}$
180	162 131	sylbir	$⊢ k \in (1 \dots N - 1) \to k \in (0 \dots N - 1)$
181	180 20	sylan2	$⊢ (φ \land k \in (1 \dots N - 1)) \to k BernPoly (X + 1) \in ℂ$
182	180 40	sylan2	$⊢ (φ \land k \in (1 \dots N - 1)) \to k BernPoly X \in ℂ$
183	180 33	sylan2	$⊢ (φ \land k \in (1 \dots N - 1)) \to N - k + 1 \in ℂ$
184	180 34	sylan2	$⊢ (φ \land k \in (1 \dots N - 1)) \to N - k + 1 \neq 0$
185	181 182 183 184	divsubdird	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{(k BernPoly (X + 1)) - (k BernPoly X)}{N - k + 1} = (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\frac{k BernPoly X}{N - k + 1})$
186	2	adantr	$⊢ (φ \land k \in (1 \dots N - 1)) \to X \in ℂ$
187		nnm1nn0	$⊢ k \in ℕ \to k - 1 \in ℕ_{0}$
188	172 187	syl	$⊢ (φ \land k \in (1 \dots N - 1)) \to k - 1 \in ℕ_{0}$
189	186 188	expcld	$⊢ (φ \land k \in (1 \dots N - 1)) \to X^{k - 1} \in ℂ$
190	173 189 183 184	div23d	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{k X^{k - 1}}{N - k + 1} = (\frac{k}{N - k + 1}) X^{k - 1}$
191	179 185 190	3eqtr3d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\frac{k BernPoly X}{N - k + 1}) = (\frac{k}{N - k + 1}) X^{k - 1}$
192	178 191	oveq12d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k}) ((\frac{k BernPoly (X + 1)}{N - k + 1}) - (\frac{k BernPoly X}{N - k + 1})) = (\binom{N}{k - 1}) (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1}$
193	180 17	sylan2	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k}) \in ℂ$
194	181 183 184	divcld	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{k BernPoly (X + 1)}{N - k + 1} \in ℂ$
195	182 183 184	divcld	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{k BernPoly X}{N - k + 1} \in ℂ$
196	193 194 195	subdid	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k}) ((\frac{k BernPoly (X + 1)}{N - k + 1}) - (\frac{k BernPoly X}{N - k + 1})) = (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
197	169	nnnn0d	$⊢ (φ \land k \in (1 \dots N - 1)) \to N \in ℕ_{0}$
198	188	nn0zd	$⊢ (φ \land k \in (1 \dots N - 1)) \to k - 1 \in ℤ$
199		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
200	197 198 199	syl2anc	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
201	200	nn0cnd	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k - 1}) \in ℂ$
202	172	nnne0d	$⊢ (φ \land k \in (1 \dots N - 1)) \to k \neq 0$
203	183 173 202	divcld	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{N - k + 1}{k} \in ℂ$
204	173 183 184	divcld	$⊢ (φ \land k \in (1 \dots N - 1)) \to \frac{k}{N - k + 1} \in ℂ$
205	204 189	mulcld	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\frac{k}{N - k + 1}) X^{k - 1} \in ℂ$
206	201 203 205	mulassd	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k - 1}) (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1} = (\binom{N}{k - 1}) (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1}$
207	183 173 184 202	divcan6d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) = 1$
208	207	oveq1d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1} = 1 X^{k - 1}$
209	203 204 189	mulassd	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1} = (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1}$
210	189	mulid2d	$⊢ (φ \land k \in (1 \dots N - 1)) \to 1 X^{k - 1} = X^{k - 1}$
211	208 209 210	3eqtr3d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1} = X^{k - 1}$
212	211	oveq2d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k - 1}) (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1} = (\binom{N}{k - 1}) X^{k - 1}$
213	206 212	eqtrd	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k - 1}) (\frac{N - k + 1}{k}) (\frac{k}{N - k + 1}) X^{k - 1} = (\binom{N}{k - 1}) X^{k - 1}$
214	192 196 213	3eqtr3d	$⊢ (φ \land k \in (1 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{k - 1}) X^{k - 1}$
215	162 214	sylan2b	$⊢ (φ \land k \in (0 + 1 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{k - 1}) X^{k - 1}$
216	215	sumeq2dv	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} ((\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})) = \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k - 1}) X^{k - 1}$
217	128 132 134	fsumsub	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} ((\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})) = \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})$
218	159 216 217	3eqtr2rd	$⊢ φ \to \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0 + 1}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m}$
219	117 136 218	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m}$
220	93 219	oveq12d	$⊢ φ \to {(X + 1)}^{N} - X^{N} - (\sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})) = \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} + N X^{N - 1} - \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m}$
221		fzfid	$⊢ φ \to (0 \dots N - 2) \in Fin$
222	221 152	fsumcl	$⊢ φ \to \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} \in ℂ$
223	2 76	expcld	$⊢ φ \to X^{N - 1} \in ℂ$
224	22 223	mulcld	$⊢ φ \to N X^{N - 1} \in ℂ$
225	222 224	pncan2d	$⊢ φ \to \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} + N X^{N - 1} - \sum_{m = 0}^{N - 2} (\binom{N}{m}) X^{m} = N X^{N - 1}$
226	220 225	eqtrd	$⊢ φ \to {(X + 1)}^{N} - X^{N} - (\sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly (X + 1)}{N - k + 1}) - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1})) = N X^{N - 1}$
227	11 44 226	3eqtrd	$⊢ φ \to (N BernPoly (X + 1)) - (N BernPoly X) = N X^{N - 1}$

Metamath Proof Explorer

Theorem bpolydiflem

Proof