Theorem 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	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( 𝑛 ↑ 𝐾 ) = ( ( ( ( 𝐾 + 1 ) BernPoly ( 𝑀 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 0 ) ) / ( 𝐾 + 1 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nn0p1nn	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ )
2	1	adantr	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 + 1 ) ∈ ℕ )
3	2	nncnd	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 + 1 ) ∈ ℂ )
4		fzfid	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 0 ... 𝑀 ) ∈ Fin )
5		elfzelz	⊢ ( 𝑛 ∈ ( 0 ... 𝑀 ) → 𝑛 ∈ ℤ )
6	5	zcnd	⊢ ( 𝑛 ∈ ( 0 ... 𝑀 ) → 𝑛 ∈ ℂ )
7		simpl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → 𝐾 ∈ ℕ0 )
8		expcl	⊢ ( ( 𝑛 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝑛 ↑ 𝐾 ) ∈ ℂ )
9	6 7 8	syl2anr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( 𝑛 ↑ 𝐾 ) ∈ ℂ )
10	4 9	fsumcl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( 𝑛 ↑ 𝐾 ) ∈ ℂ )
11	2	nnne0d	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝐾 + 1 ) ≠ 0 )
12	4 3 9	fsummulc2	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 + 1 ) · Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( 𝑛 ↑ 𝐾 ) ) = Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( ( 𝐾 + 1 ) · ( 𝑛 ↑ 𝐾 ) ) )
13		bpolydif	⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ ∧ 𝑛 ∈ ℂ ) → ( ( ( 𝐾 + 1 ) BernPoly ( 𝑛 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 𝑛 ) ) = ( ( 𝐾 + 1 ) · ( 𝑛 ↑ ( ( 𝐾 + 1 ) − 1 ) ) ) )
14	2 6 13	syl2an	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝐾 + 1 ) BernPoly ( 𝑛 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 𝑛 ) ) = ( ( 𝐾 + 1 ) · ( 𝑛 ↑ ( ( 𝐾 + 1 ) − 1 ) ) ) )
15		nn0cn	⊢ ( 𝐾 ∈ ℕ0 → 𝐾 ∈ ℂ )
16	15	ad2antrr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → 𝐾 ∈ ℂ )
17		ax-1cn	⊢ 1 ∈ ℂ
18		pncan	⊢ ( ( 𝐾 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
19	16 17 18	sylancl	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐾 + 1 ) − 1 ) = 𝐾 )
20	19	oveq2d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( 𝑛 ↑ ( ( 𝐾 + 1 ) − 1 ) ) = ( 𝑛 ↑ 𝐾 ) )
21	20	oveq2d	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( 𝐾 + 1 ) · ( 𝑛 ↑ ( ( 𝐾 + 1 ) − 1 ) ) ) = ( ( 𝐾 + 1 ) · ( 𝑛 ↑ 𝐾 ) ) )
22	14 21	eqtrd	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑛 ∈ ( 0 ... 𝑀 ) ) → ( ( ( 𝐾 + 1 ) BernPoly ( 𝑛 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 𝑛 ) ) = ( ( 𝐾 + 1 ) · ( 𝑛 ↑ 𝐾 ) ) )
23	22	sumeq2dv	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐾 + 1 ) BernPoly ( 𝑛 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 𝑛 ) ) = Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( ( 𝐾 + 1 ) · ( 𝑛 ↑ 𝐾 ) ) )
24		oveq2	⊢ ( 𝑘 = 𝑛 → ( ( 𝐾 + 1 ) BernPoly 𝑘 ) = ( ( 𝐾 + 1 ) BernPoly 𝑛 ) )
25		oveq2	⊢ ( 𝑘 = ( 𝑛 + 1 ) → ( ( 𝐾 + 1 ) BernPoly 𝑘 ) = ( ( 𝐾 + 1 ) BernPoly ( 𝑛 + 1 ) ) )
26		oveq2	⊢ ( 𝑘 = 0 → ( ( 𝐾 + 1 ) BernPoly 𝑘 ) = ( ( 𝐾 + 1 ) BernPoly 0 ) )
27		oveq2	⊢ ( 𝑘 = ( 𝑀 + 1 ) → ( ( 𝐾 + 1 ) BernPoly 𝑘 ) = ( ( 𝐾 + 1 ) BernPoly ( 𝑀 + 1 ) ) )
28		nn0z	⊢ ( 𝑀 ∈ ℕ0 → 𝑀 ∈ ℤ )
29	28	adantl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → 𝑀 ∈ ℤ )
30		peano2nn0	⊢ ( 𝑀 ∈ ℕ0 → ( 𝑀 + 1 ) ∈ ℕ0 )
31	30	adantl	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ℕ0 )
32		nn0uz	⊢ ℕ0 = ( ℤ≥ ‘ 0 )
33	31 32	eleqtrdi	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( 𝑀 + 1 ) ∈ ( ℤ≥ ‘ 0 ) )
34		peano2nn0	⊢ ( 𝐾 ∈ ℕ0 → ( 𝐾 + 1 ) ∈ ℕ0 )
35	34	ad2antrr	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 1 ) ) ) → ( 𝐾 + 1 ) ∈ ℕ0 )
36		elfznn0	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑀 + 1 ) ) → 𝑘 ∈ ℕ0 )
37	36	adantl	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 1 ) ) ) → 𝑘 ∈ ℕ0 )
38	37	nn0cnd	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 1 ) ) ) → 𝑘 ∈ ℂ )
39		bpolycl	⊢ ( ( ( 𝐾 + 1 ) ∈ ℕ0 ∧ 𝑘 ∈ ℂ ) → ( ( 𝐾 + 1 ) BernPoly 𝑘 ) ∈ ℂ )
40	35 38 39	syl2anc	⊢ ( ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) ∧ 𝑘 ∈ ( 0 ... ( 𝑀 + 1 ) ) ) → ( ( 𝐾 + 1 ) BernPoly 𝑘 ) ∈ ℂ )
41	24 25 26 27 29 33 40	telfsum2	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( ( ( 𝐾 + 1 ) BernPoly ( 𝑛 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 𝑛 ) ) = ( ( ( 𝐾 + 1 ) BernPoly ( 𝑀 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 0 ) ) )
42	12 23 41	3eqtr2d	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝐾 + 1 ) · Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( 𝑛 ↑ 𝐾 ) ) = ( ( ( 𝐾 + 1 ) BernPoly ( 𝑀 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 0 ) ) )
43	3 10 11 42	mvllmuld	⊢ ( ( 𝐾 ∈ ℕ0 ∧ 𝑀 ∈ ℕ0 ) → Σ 𝑛 ∈ ( 0 ... 𝑀 ) ( 𝑛 ↑ 𝐾 ) = ( ( ( ( 𝐾 + 1 ) BernPoly ( 𝑀 + 1 ) ) − ( ( 𝐾 + 1 ) BernPoly 0 ) ) / ( 𝐾 + 1 ) ) )