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 0 X k = 0 N ( N k) k BernPoly X N - k + 1 = X N

Proof

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