Metamath Proof Explorer

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 ) ) )