fsumkthpow

Description: A closed-form expression for the sum of K -th powers. (Contributed by Scott Fenton, 16-May-2014) This is Metamath 100 proof #77. (Revised by Mario Carneiro, 16-Jun-2014)

		Ref	Expression
	Assertion	fsumkthpow	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to \sum_{n = 0}^{M} n^{K} = \frac{((K + 1) BernPoly (M + 1)) - ((K + 1) BernPoly 0)}{K + 1}$

Proof

Step	Hyp	Ref	Expression
1		nn0p1nn	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ$
2	1	adantr	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K + 1 \in ℕ$
3	2	nncnd	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K + 1 \in ℂ$
4		fzfid	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (0 \dots M) \in Fin$
5		elfzelz	$⊢ n \in (0 \dots M) \to n \in ℤ$
6	5	zcnd	$⊢ n \in (0 \dots M) \to n \in ℂ$
7		simpl	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K \in ℕ_{0}$
8		expcl	$⊢ (n \in ℂ \land K \in ℕ_{0}) \to n^{K} \in ℂ$
9	6 7 8	syl2anr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to n^{K} \in ℂ$
10	4 9	fsumcl	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to \sum_{n = 0}^{M} n^{K} \in ℂ$
11	2	nnne0d	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to K + 1 \neq 0$
12	4 3 9	fsummulc2	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (K + 1) \sum_{n = 0}^{M} n^{K} = \sum_{n = 0}^{M} (K + 1) n^{K}$
13		bpolydif	$⊢ (K + 1 \in ℕ \land n \in ℂ) \to ((K + 1) BernPoly (n + 1)) - ((K + 1) BernPoly n) = (K + 1) n^{K + 1 - 1}$
14	2 6 13	syl2an	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to ((K + 1) BernPoly (n + 1)) - ((K + 1) BernPoly n) = (K + 1) n^{K + 1 - 1}$
15		nn0cn	$⊢ K \in ℕ_{0} \to K \in ℂ$
16	15	ad2antrr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to K \in ℂ$
17		ax-1cn	$⊢ 1 \in ℂ$
18		pncan	$⊢ (K \in ℂ \land 1 \in ℂ) \to K + 1 - 1 = K$
19	16 17 18	sylancl	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to K + 1 - 1 = K$
20	19	oveq2d	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to n^{K + 1 - 1} = n^{K}$
21	20	oveq2d	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to (K + 1) n^{K + 1 - 1} = (K + 1) n^{K}$
22	14 21	eqtrd	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land n \in (0 \dots M)) \to ((K + 1) BernPoly (n + 1)) - ((K + 1) BernPoly n) = (K + 1) n^{K}$
23	22	sumeq2dv	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to \sum_{n = 0}^{M} (((K + 1) BernPoly (n + 1)) - ((K + 1) BernPoly n)) = \sum_{n = 0}^{M} (K + 1) n^{K}$
24		oveq2	$⊢ k = n \to (K + 1) BernPoly k = (K + 1) BernPoly n$
25		oveq2	$⊢ k = n + 1 \to (K + 1) BernPoly k = (K + 1) BernPoly (n + 1)$
26		oveq2	$⊢ k = 0 \to (K + 1) BernPoly k = (K + 1) BernPoly 0$
27		oveq2	$⊢ k = M + 1 \to (K + 1) BernPoly k = (K + 1) BernPoly (M + 1)$
28		nn0z	$⊢ M \in ℕ_{0} \to M \in ℤ$
29	28	adantl	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to M \in ℤ$
30		peano2nn0	$⊢ M \in ℕ_{0} \to M + 1 \in ℕ_{0}$
31	30	adantl	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to M + 1 \in ℕ_{0}$
32		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
33	31 32	eleqtrdi	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to M + 1 \in ℤ_{\geq 0}$
34		peano2nn0	$⊢ K \in ℕ_{0} \to K + 1 \in ℕ_{0}$
35	34	ad2antrr	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land k \in (0 \dots M + 1)) \to K + 1 \in ℕ_{0}$
36		elfznn0	$⊢ k \in (0 \dots M + 1) \to k \in ℕ_{0}$
37	36	adantl	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land k \in (0 \dots M + 1)) \to k \in ℕ_{0}$
38	37	nn0cnd	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land k \in (0 \dots M + 1)) \to k \in ℂ$
39		bpolycl	$⊢ (K + 1 \in ℕ_{0} \land k \in ℂ) \to (K + 1) BernPoly k \in ℂ$
40	35 38 39	syl2anc	$⊢ ((K \in ℕ_{0} \land M \in ℕ_{0}) \land k \in (0 \dots M + 1)) \to (K + 1) BernPoly k \in ℂ$
41	24 25 26 27 29 33 40	telfsum2	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to \sum_{n = 0}^{M} (((K + 1) BernPoly (n + 1)) - ((K + 1) BernPoly n)) = ((K + 1) BernPoly (M + 1)) - ((K + 1) BernPoly 0)$
42	12 23 41	3eqtr2d	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to (K + 1) \sum_{n = 0}^{M} n^{K} = ((K + 1) BernPoly (M + 1)) - ((K + 1) BernPoly 0)$
43	3 10 11 42	mvllmuld	$⊢ (K \in ℕ_{0} \land M \in ℕ_{0}) \to \sum_{n = 0}^{M} n^{K} = \frac{((K + 1) BernPoly (M + 1)) - ((K + 1) BernPoly 0)}{K + 1}$

Metamath Proof Explorer

Theorem fsumkthpow

Proof