Metamath Proof Explorer


Theorem bpolycl

Description: Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014) (Proof shortened by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion bpolycl N 0 X N BernPoly X

Proof

Step Hyp Ref Expression
1 oveq1 n = k n BernPoly X = k BernPoly X
2 1 eleq1d n = k n BernPoly X k BernPoly X
3 2 imbi2d n = k X n BernPoly X X k BernPoly X
4 oveq1 n = N n BernPoly X = N BernPoly X
5 4 eleq1d n = N n BernPoly X N BernPoly X
6 5 imbi2d n = N X n BernPoly X X N BernPoly X
7 r19.21v k 0 n 1 X k BernPoly X X k 0 n 1 k BernPoly X
8 bpolyval n 0 X n BernPoly X = X n m = 0 n 1 ( n m) m BernPoly X n - m + 1
9 8 3adant3 n 0 X k 0 n 1 k BernPoly X n BernPoly X = X n m = 0 n 1 ( n m) m BernPoly X n - m + 1
10 simp2 n 0 X k 0 n 1 k BernPoly X X
11 simp1 n 0 X k 0 n 1 k BernPoly X n 0
12 10 11 expcld n 0 X k 0 n 1 k BernPoly X X n
13 fzfid n 0 X k 0 n 1 k BernPoly X 0 n 1 Fin
14 elfzelz m 0 n 1 m
15 bccl n 0 m ( n m) 0
16 11 14 15 syl2an n 0 X k 0 n 1 k BernPoly X m 0 n 1 ( n m) 0
17 16 nn0cnd n 0 X k 0 n 1 k BernPoly X m 0 n 1 ( n m)
18 oveq1 k = m k BernPoly X = m BernPoly X
19 18 eleq1d k = m k BernPoly X m BernPoly X
20 19 rspccva k 0 n 1 k BernPoly X m 0 n 1 m BernPoly X
21 20 3ad2antl3 n 0 X k 0 n 1 k BernPoly X m 0 n 1 m BernPoly X
22 fzssp1 0 n 1 0 n - 1 + 1
23 11 nn0cnd n 0 X k 0 n 1 k BernPoly X n
24 ax-1cn 1
25 npcan n 1 n - 1 + 1 = n
26 23 24 25 sylancl n 0 X k 0 n 1 k BernPoly X n - 1 + 1 = n
27 26 oveq2d n 0 X k 0 n 1 k BernPoly X 0 n - 1 + 1 = 0 n
28 22 27 sseqtrid n 0 X k 0 n 1 k BernPoly X 0 n 1 0 n
29 28 sselda n 0 X k 0 n 1 k BernPoly X m 0 n 1 m 0 n
30 fznn0sub m 0 n n m 0
31 nn0p1nn n m 0 n - m + 1
32 29 30 31 3syl n 0 X k 0 n 1 k BernPoly X m 0 n 1 n - m + 1
33 32 nncnd n 0 X k 0 n 1 k BernPoly X m 0 n 1 n - m + 1
34 32 nnne0d n 0 X k 0 n 1 k BernPoly X m 0 n 1 n - m + 1 0
35 21 33 34 divcld n 0 X k 0 n 1 k BernPoly X m 0 n 1 m BernPoly X n - m + 1
36 17 35 mulcld n 0 X k 0 n 1 k BernPoly X m 0 n 1 ( n m) m BernPoly X n - m + 1
37 13 36 fsumcl n 0 X k 0 n 1 k BernPoly X m = 0 n 1 ( n m) m BernPoly X n - m + 1
38 12 37 subcld n 0 X k 0 n 1 k BernPoly X X n m = 0 n 1 ( n m) m BernPoly X n - m + 1
39 9 38 eqeltrd n 0 X k 0 n 1 k BernPoly X n BernPoly X
40 39 3exp n 0 X k 0 n 1 k BernPoly X n BernPoly X
41 40 a2d n 0 X k 0 n 1 k BernPoly X X n BernPoly X
42 7 41 syl5bi n 0 k 0 n 1 X k BernPoly X X n BernPoly X
43 3 6 42 nn0sinds N 0 X N BernPoly X
44 43 imp N 0 X N BernPoly X