Metamath Proof Explorer

Theorem 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 e. NN0 /\ X e. CC ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( X ^ N ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( N e. NN0 /\ X e. CC ) -> N e. NN0 )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 1 2 eleqtrdi 
 |-  ( ( N e. NN0 /\ X e. CC ) -> N e. ( ZZ>= ` 0 ) )
4 elfzelz 
 |-  ( k e. ( 0 ... N ) -> k e. ZZ )
5 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
6 1 4 5 syl2an 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. NN0 )
7 6 nn0cnd 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( N _C k ) e. CC )
8 elfznn0 
 |-  ( k e. ( 0 ... N ) -> k e. NN0 )
9 simpr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> X e. CC )
10 bpolycl 
 |-  ( ( k e. NN0 /\ X e. CC ) -> ( k BernPoly X ) e. CC )
11 8 9 10 syl2anr 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( k BernPoly X ) e. CC )
12 fznn0sub 
 |-  ( k e. ( 0 ... N ) -> ( N - k ) e. NN0 )
13 12 adantl 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( N - k ) e. NN0 )
14 nn0p1nn 
 |-  ( ( N - k ) e. NN0 -> ( ( N - k ) + 1 ) e. NN )
15 13 14 syl 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) + 1 ) e. NN )
16 15 nncnd 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) + 1 ) e. CC )
17 15 nnne0d 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( N - k ) + 1 ) =/= 0 )
18 11 16 17 divcld 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) e. CC )
19 7 18 mulcld 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
20 oveq2 
 |-  ( k = N -> ( N _C k ) = ( N _C N ) )
21 oveq1 
 |-  ( k = N -> ( k BernPoly X ) = ( N BernPoly X ) )
22 oveq2 
 |-  ( k = N -> ( N - k ) = ( N - N ) )
23 22 oveq1d 
 |-  ( k = N -> ( ( N - k ) + 1 ) = ( ( N - N ) + 1 ) )
24 21 23 oveq12d 
 |-  ( k = N -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) = ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) )
25 20 24 oveq12d 
 |-  ( k = N -> ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( ( N _C N ) x. ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) ) )
26 3 19 25 fsumm1 
 |-  ( ( N e. NN0 /\ X e. CC ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) + ( ( N _C N ) x. ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) ) ) )
27 bcnn 
 |-  ( N e. NN0 -> ( N _C N ) = 1 )
28 27 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N _C N ) = 1 )
29 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
30 29 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> N e. CC )
31 30 subidd 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N - N ) = 0 )
32 31 oveq1d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N - N ) + 1 ) = ( 0 + 1 ) )
33 0p1e1 
 |-  ( 0 + 1 ) = 1
34 32 33 eqtrdi 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N - N ) + 1 ) = 1 )
35 34 oveq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) = ( ( N BernPoly X ) / 1 ) )
36 bpolycl 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) e. CC )
37 36 div1d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N BernPoly X ) / 1 ) = ( N BernPoly X ) )
38 35 37 eqtrd 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) = ( N BernPoly X ) )
39 28 38 oveq12d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N _C N ) x. ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) ) = ( 1 x. ( N BernPoly X ) ) )
40 36 mulid2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( 1 x. ( N BernPoly X ) ) = ( N BernPoly X ) )
41 39 40 eqtrd 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N _C N ) x. ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) ) = ( N BernPoly X ) )
42 41 oveq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) + ( ( N _C N ) x. ( ( N BernPoly X ) / ( ( N - N ) + 1 ) ) ) ) = ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) + ( N BernPoly X ) ) )
43 bpolyval 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) )
44 43 eqcomd 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( N BernPoly X ) )
45 expcl 
 |-  ( ( X e. CC /\ N e. NN0 ) -> ( X ^ N ) e. CC )
46 45 ancoms 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( X ^ N ) e. CC )
47 fzfid 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( 0 ... ( N - 1 ) ) e. Fin )
48 fzssp1 
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
49 ax-1cn 
 |-  1 e. CC
50 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
51 30 49 50 sylancl 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( N - 1 ) + 1 ) = N )
52 51 oveq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
53 48 52 sseqtrid 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
54 53 sselda 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> k e. ( 0 ... N ) )
55 54 19 syldan 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
56 47 55 fsumcl 
 |-  ( ( N e. NN0 /\ X e. CC ) -> sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) e. CC )
57 46 56 36 subaddd 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) ) = ( N BernPoly X ) <-> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) + ( N BernPoly X ) ) = ( X ^ N ) ) )
58 44 57 mpbid 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) + ( N BernPoly X ) ) = ( X ^ N ) )
59 26 42 58 3eqtrd 
 |-  ( ( N e. NN0 /\ X e. CC ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) ) = ( X ^ N ) )