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 
|- ( ( K e. NN0 /\ M e. NN0 ) -> sum_ n e. ( 0 ... M ) ( n ^ K ) = ( ( ( ( K + 1 ) BernPoly ( M + 1 ) ) - ( ( K + 1 ) BernPoly 0 ) ) / ( K + 1 ) ) )

Proof

Step Hyp Ref Expression
1 nn0p1nn 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN )
2 1 adantr 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K + 1 ) e. NN )
3 2 nncnd 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K + 1 ) e. CC )
4 fzfid 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( 0 ... M ) e. Fin )
5 elfzelz 
 |-  ( n e. ( 0 ... M ) -> n e. ZZ )
6 5 zcnd 
 |-  ( n e. ( 0 ... M ) -> n e. CC )
7 simpl 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> K e. NN0 )
8 expcl 
 |-  ( ( n e. CC /\ K e. NN0 ) -> ( n ^ K ) e. CC )
9 6 7 8 syl2anr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> ( n ^ K ) e. CC )
10 4 9 fsumcl 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> sum_ n e. ( 0 ... M ) ( n ^ K ) e. CC )
11 2 nnne0d 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( K + 1 ) =/= 0 )
12 4 3 9 fsummulc2 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( ( K + 1 ) x. sum_ n e. ( 0 ... M ) ( n ^ K ) ) = sum_ n e. ( 0 ... M ) ( ( K + 1 ) x. ( n ^ K ) ) )
13 bpolydif 
 |-  ( ( ( K + 1 ) e. NN /\ n e. CC ) -> ( ( ( K + 1 ) BernPoly ( n + 1 ) ) - ( ( K + 1 ) BernPoly n ) ) = ( ( K + 1 ) x. ( n ^ ( ( K + 1 ) - 1 ) ) ) )
14 2 6 13 syl2an 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> ( ( ( K + 1 ) BernPoly ( n + 1 ) ) - ( ( K + 1 ) BernPoly n ) ) = ( ( K + 1 ) x. ( n ^ ( ( K + 1 ) - 1 ) ) ) )
15 nn0cn 
 |-  ( K e. NN0 -> K e. CC )
16 15 ad2antrr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> K e. CC )
17 ax-1cn 
 |-  1 e. CC
18 pncan 
 |-  ( ( K e. CC /\ 1 e. CC ) -> ( ( K + 1 ) - 1 ) = K )
19 16 17 18 sylancl 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> ( ( K + 1 ) - 1 ) = K )
20 19 oveq2d 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> ( n ^ ( ( K + 1 ) - 1 ) ) = ( n ^ K ) )
21 20 oveq2d 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> ( ( K + 1 ) x. ( n ^ ( ( K + 1 ) - 1 ) ) ) = ( ( K + 1 ) x. ( n ^ K ) ) )
22 14 21 eqtrd 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ n e. ( 0 ... M ) ) -> ( ( ( K + 1 ) BernPoly ( n + 1 ) ) - ( ( K + 1 ) BernPoly n ) ) = ( ( K + 1 ) x. ( n ^ K ) ) )
23 22 sumeq2dv 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> sum_ n e. ( 0 ... M ) ( ( ( K + 1 ) BernPoly ( n + 1 ) ) - ( ( K + 1 ) BernPoly n ) ) = sum_ n e. ( 0 ... M ) ( ( K + 1 ) x. ( n ^ K ) ) )
24 oveq2 
 |-  ( k = n -> ( ( K + 1 ) BernPoly k ) = ( ( K + 1 ) BernPoly n ) )
25 oveq2 
 |-  ( k = ( n + 1 ) -> ( ( K + 1 ) BernPoly k ) = ( ( K + 1 ) BernPoly ( n + 1 ) ) )
26 oveq2 
 |-  ( k = 0 -> ( ( K + 1 ) BernPoly k ) = ( ( K + 1 ) BernPoly 0 ) )
27 oveq2 
 |-  ( k = ( M + 1 ) -> ( ( K + 1 ) BernPoly k ) = ( ( K + 1 ) BernPoly ( M + 1 ) ) )
28 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
29 28 adantl 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> M e. ZZ )
30 peano2nn0 
 |-  ( M e. NN0 -> ( M + 1 ) e. NN0 )
31 30 adantl 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( M + 1 ) e. NN0 )
32 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
33 31 32 eleqtrdi 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> ( M + 1 ) e. ( ZZ>= ` 0 ) )
34 peano2nn0 
 |-  ( K e. NN0 -> ( K + 1 ) e. NN0 )
35 34 ad2antrr 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ k e. ( 0 ... ( M + 1 ) ) ) -> ( K + 1 ) e. NN0 )
36 elfznn0 
 |-  ( k e. ( 0 ... ( M + 1 ) ) -> k e. NN0 )
37 36 adantl 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ k e. ( 0 ... ( M + 1 ) ) ) -> k e. NN0 )
38 37 nn0cnd 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ k e. ( 0 ... ( M + 1 ) ) ) -> k e. CC )
39 bpolycl 
 |-  ( ( ( K + 1 ) e. NN0 /\ k e. CC ) -> ( ( K + 1 ) BernPoly k ) e. CC )
40 35 38 39 syl2anc 
 |-  ( ( ( K e. NN0 /\ M e. NN0 ) /\ k e. ( 0 ... ( M + 1 ) ) ) -> ( ( K + 1 ) BernPoly k ) e. CC )
41 24 25 26 27 29 33 40 telfsum2 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> sum_ n e. ( 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 e. NN0 /\ M e. NN0 ) -> ( ( K + 1 ) x. sum_ n e. ( 0 ... M ) ( n ^ K ) ) = ( ( ( K + 1 ) BernPoly ( M + 1 ) ) - ( ( K + 1 ) BernPoly 0 ) ) )
43 3 10 11 42 mvllmuld 
 |-  ( ( K e. NN0 /\ M e. NN0 ) -> sum_ n e. ( 0 ... M ) ( n ^ K ) = ( ( ( ( K + 1 ) BernPoly ( M + 1 ) ) - ( ( K + 1 ) BernPoly 0 ) ) / ( K + 1 ) ) )