Metamath Proof Explorer

Theorem bpolyval

Description: The value of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014)

Ref Expression
Assertion bpolyval ⊢N∈ℕ0∧X∈ℂ→NBernPolyX=XN−∑k=0N−1(Nk)⁢kBernPolyXN-k+1

Proof

Step Hyp Ref Expression
1 fvex ⊢dom⁡c∈V
2 oveq2 ⊢n=dom⁡c→Xn=Xdom⁡c
3 oveq1 ⊢n=dom⁡c→(nm)=(dom⁡cm)
4 oveq1 ⊢n=dom⁡c→n−m=dom⁡c−m
5 4 oveq1d ⊢n=dom⁡c→n-m+1=dom⁡c-m+1
6 5 oveq2d ⊢n=dom⁡c→c⁡mn-m+1=c⁡mdom⁡c-m+1
7 3 6 oveq12d ⊢n=dom⁡c→(nm)⁢c⁡mn-m+1=(dom⁡cm)⁢c⁡mdom⁡c-m+1
8 7 sumeq2sdv ⊢n=dom⁡c→∑m∈dom⁡c(nm)⁢c⁡mn-m+1=∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1
9 2 8 oveq12d ⊢n=dom⁡c→Xn−∑m∈dom⁡c(nm)⁢c⁡mn-m+1=Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1
10 1 9 csbie ⊢⦋dom⁡c/n⦌Xn−∑m∈dom⁡c(nm)⁢c⁡mn-m+1=Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1
11 oveq2 ⊢m=k→(nm)=(nk)
12 fveq2 ⊢m=k→c⁡m=c⁡k
13 oveq2 ⊢m=k→n−m=n−k
14 13 oveq1d ⊢m=k→n-m+1=n-k+1
15 12 14 oveq12d ⊢m=k→c⁡mn-m+1=c⁡kn-k+1
16 11 15 oveq12d ⊢m=k→(nm)⁢c⁡mn-m+1=(nk)⁢c⁡kn-k+1
17 16 cbvsumv ⊢∑m∈dom⁡c(nm)⁢c⁡mn-m+1=∑k∈dom⁡c(nk)⁢c⁡kn-k+1
18 dmeq ⊢c=g→dom⁡c=dom⁡g
19 fveq1 ⊢c=g→c⁡k=g⁡k
20 19 oveq1d ⊢c=g→c⁡kn-k+1=g⁡kn-k+1
21 20 oveq2d ⊢c=g→(nk)⁢c⁡kn-k+1=(nk)⁢g⁡kn-k+1
22 21 adantr ⊢c=g∧k∈dom⁡c→(nk)⁢c⁡kn-k+1=(nk)⁢g⁡kn-k+1
23 18 22 sumeq12dv ⊢c=g→∑k∈dom⁡c(nk)⁢c⁡kn-k+1=∑k∈dom⁡g(nk)⁢g⁡kn-k+1
24 17 23 eqtrid ⊢c=g→∑m∈dom⁡c(nm)⁢c⁡mn-m+1=∑k∈dom⁡g(nk)⁢g⁡kn-k+1
25 24 oveq2d ⊢c=g→Xn−∑m∈dom⁡c(nm)⁢c⁡mn-m+1=Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
26 25 csbeq2dv ⊢c=g→⦋dom⁡c/n⦌Xn−∑m∈dom⁡c(nm)⁢c⁡mn-m+1=⦋dom⁡c/n⦌Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
27 10 26 eqtr3id ⊢c=g→Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1=⦋dom⁡c/n⦌Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
28 18 fveq2d ⊢c=g→dom⁡c=dom⁡g
29 28 csbeq1d ⊢c=g→⦋dom⁡c/n⦌Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1=⦋dom⁡g/n⦌Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
30 27 29 eqtrd ⊢c=g→Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1=⦋dom⁡g/n⦌Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
31 30 cbvmptv ⊢c∈V⟼Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1=g∈V⟼⦋dom⁡g/n⦌Xn−∑k∈dom⁡g(nk)⁢g⁡kn-k+1
32 eqid ⊢wrecs⁡<ℕ0c∈V⟼Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1=wrecs⁡<ℕ0c∈V⟼Xdom⁡c−∑m∈dom⁡c(dom⁡cm)⁢c⁡mdom⁡c-m+1
33 31 32 bpolylem ⊢N∈ℕ0∧X∈ℂ→NBernPolyX=XN−∑k=0N−1(Nk)⁢kBernPolyXN-k+1