bpolysum

Description: A sum for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014) (Proof shortened by Mario Carneiro, 22-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N \in ℕ_{0}$
2		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
3	1 2	eleqtrdi	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N \in ℤ_{\geq 0}$
4		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
5		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
6	1 4 5	syl2an	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℕ_{0}$
7	6	nn0cnd	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to (\binom{N}{k}) \in ℂ$
8		elfznn0	$⊢ k \in (0 \dots N) \to k \in ℕ_{0}$
9		simpr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to X \in ℂ$
10		bpolycl	$⊢ (k \in ℕ_{0} \land X \in ℂ) \to k BernPoly X \in ℂ$
11	8 9 10	syl2anr	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to k BernPoly X \in ℂ$
12		fznn0sub	$⊢ k \in (0 \dots N) \to N - k \in ℕ_{0}$
13	12	adantl	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to N - k \in ℕ_{0}$
14		nn0p1nn	$⊢ N - k \in ℕ_{0} \to N - k + 1 \in ℕ$
15	13 14	syl	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to N - k + 1 \in ℕ$
16	15	nncnd	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to N - k + 1 \in ℂ$
17	15	nnne0d	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to N - k + 1 \neq 0$
18	11 16 17	divcld	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to \frac{k BernPoly X}{N - k + 1} \in ℂ$
19	7 18	mulcld	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N)) \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
20		oveq2	$⊢ k = N \to (\binom{N}{k}) = (\binom{N}{N})$
21		oveq1	$⊢ k = N \to k BernPoly X = N BernPoly X$
22		oveq2	$⊢ k = N \to N - k = N - N$
23	22	oveq1d	$⊢ k = N \to N - k + 1 = N - N + 1$
24	21 23	oveq12d	$⊢ k = N \to \frac{k BernPoly X}{N - k + 1} = \frac{N BernPoly X}{N - N + 1}$
25	20 24	oveq12d	$⊢ k = N \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = (\binom{N}{N}) (\frac{N BernPoly X}{N - N + 1})$
26	3 19 25	fsumm1	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \sum_{k = 0}^{N} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) + (\binom{N}{N}) (\frac{N BernPoly X}{N - N + 1})$
27		bcnn	$⊢ N \in ℕ_{0} \to (\binom{N}{N}) = 1$
28	27	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (\binom{N}{N}) = 1$
29		nn0cn	$⊢ N \in ℕ_{0} \to N \in ℂ$
30	29	adantr	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N \in ℂ$
31	30	subidd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N - N = 0$
32	31	oveq1d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N - N + 1 = 0 + 1$
33		0p1e1	$⊢ 0 + 1 = 1$
34	32 33	eqtrdi	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N - N + 1 = 1$
35	34	oveq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \frac{N BernPoly X}{N - N + 1} = \frac{N BernPoly X}{1}$
36		bpolycl	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N BernPoly X \in ℂ$
37	36	div1d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \frac{N BernPoly X}{1} = N BernPoly X$
38	35 37	eqtrd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \frac{N BernPoly X}{N - N + 1} = N BernPoly X$
39	28 38	oveq12d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (\binom{N}{N}) (\frac{N BernPoly X}{N - N + 1}) = 1 (N BernPoly X)$
40	36	mullidd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to 1 (N BernPoly X) = N BernPoly X$
41	39 40	eqtrd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (\binom{N}{N}) (\frac{N BernPoly X}{N - N + 1}) = N BernPoly X$
42	41	oveq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) + (\binom{N}{N}) (\frac{N BernPoly X}{N - N + 1}) = \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) + (N BernPoly X)$
43		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})$
44	43	eqcomd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = N BernPoly X$
45		expcl	$⊢ (X \in ℂ \land N \in ℕ_{0}) \to X^{N} \in ℂ$
46	45	ancoms	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to X^{N} \in ℂ$
47		fzfid	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (0 \dots N - 1) \in Fin$
48		fzssp1	$⊢ (0 \dots N - 1) \subseteq (0 \dots N - 1 + 1)$
49		ax-1cn	$⊢ 1 \in ℂ$
50		npcan	$⊢ (N \in ℂ \land 1 \in ℂ) \to N - 1 + 1 = N$
51	30 49 50	sylancl	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to N - 1 + 1 = N$
52	51	oveq2d	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (0 \dots N - 1 + 1) = (0 \dots N)$
53	48 52	sseqtrid	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (0 \dots N - 1) \subseteq (0 \dots N)$
54	53	sselda	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N - 1)) \to k \in (0 \dots N)$
55	54 19	syldan	$⊢ ((N \in ℕ_{0} \land X \in ℂ) \land k \in (0 \dots N - 1)) \to (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
56	47 55	fsumcl	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) \in ℂ$
57	46 56 36	subaddd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to (X^{N} - \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = N BernPoly X \leftrightarrow \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) + (N BernPoly X) = X^{N})$
58	44 57	mpbid	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \sum_{k = 0}^{N - 1} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) + (N BernPoly X) = X^{N}$
59	26 42 58	3eqtrd	$⊢ (N \in ℕ_{0} \land X \in ℂ) \to \sum_{k = 0}^{N} (\binom{N}{k}) (\frac{k BernPoly X}{N - k + 1}) = X^{N}$

Metamath Proof Explorer

Theorem bpolysum

Proof