Metamath Proof Explorer

Theorem bpolydif

Description: Calculate the difference between successive values of the Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014) (Proof shortened by Mario Carneiro, 26-May-2014)

Ref Expression
Assertion bpolydif ⊢N∈ℕ∧X∈ℂ→NBernPolyX+1−NBernPolyX=N⁢XN−1

Proof

Step Hyp Ref Expression
1 oveq1 ⊢n=k→nBernPolyX+1=kBernPolyX+1
2 oveq1 ⊢n=k→nBernPolyX=kBernPolyX
3 1 2 oveq12d ⊢n=k→nBernPolyX+1−nBernPolyX=kBernPolyX+1−kBernPolyX
4 id ⊢n=k→n=k
5 oveq1 ⊢n=k→n−1=k−1
6 5 oveq2d ⊢n=k→Xn−1=Xk−1
7 4 6 oveq12d ⊢n=k→n⁢Xn−1=k⁢Xk−1
8 3 7 eqeq12d ⊢n=k→nBernPolyX+1−nBernPolyX=n⁢Xn−1↔kBernPolyX+1−kBernPolyX=k⁢Xk−1
9 8 imbi2d ⊢n=k→X∈ℂ→nBernPolyX+1−nBernPolyX=n⁢Xn−1↔X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1
10 oveq1 ⊢n=N→nBernPolyX+1=NBernPolyX+1
11 oveq1 ⊢n=N→nBernPolyX=NBernPolyX
12 10 11 oveq12d ⊢n=N→nBernPolyX+1−nBernPolyX=NBernPolyX+1−NBernPolyX
13 id ⊢n=N→n=N
14 oveq1 ⊢n=N→n−1=N−1
15 14 oveq2d ⊢n=N→Xn−1=XN−1
16 13 15 oveq12d ⊢n=N→n⁢Xn−1=N⁢XN−1
17 12 16 eqeq12d ⊢n=N→nBernPolyX+1−nBernPolyX=n⁢Xn−1↔NBernPolyX+1−NBernPolyX=N⁢XN−1
18 17 imbi2d ⊢n=N→X∈ℂ→nBernPolyX+1−nBernPolyX=n⁢Xn−1↔X∈ℂ→NBernPolyX+1−NBernPolyX=N⁢XN−1
19 simp1 ⊢n∈ℕ∧∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧X∈ℂ→n∈ℕ
20 simp3 ⊢n∈ℕ∧∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧X∈ℂ→X∈ℂ
21 simpl3 ⊢n∈ℕ∧∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧X∈ℂ∧m∈1…n−1→X∈ℂ
22 oveq1 ⊢k=m→kBernPolyX+1=mBernPolyX+1
23 oveq1 ⊢k=m→kBernPolyX=mBernPolyX
24 22 23 oveq12d ⊢k=m→kBernPolyX+1−kBernPolyX=mBernPolyX+1−mBernPolyX
25 id ⊢k=m→k=m
26 oveq1 ⊢k=m→k−1=m−1
27 26 oveq2d ⊢k=m→Xk−1=Xm−1
28 25 27 oveq12d ⊢k=m→k⁢Xk−1=m⁢Xm−1
29 24 28 eqeq12d ⊢k=m→kBernPolyX+1−kBernPolyX=k⁢Xk−1↔mBernPolyX+1−mBernPolyX=m⁢Xm−1
30 29 imbi2d ⊢k=m→X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1↔X∈ℂ→mBernPolyX+1−mBernPolyX=m⁢Xm−1
31 30 rspccva ⊢∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧m∈1…n−1→X∈ℂ→mBernPolyX+1−mBernPolyX=m⁢Xm−1
32 31 3ad2antl2 ⊢n∈ℕ∧∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧X∈ℂ∧m∈1…n−1→X∈ℂ→mBernPolyX+1−mBernPolyX=m⁢Xm−1
33 21 32 mpd ⊢n∈ℕ∧∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧X∈ℂ∧m∈1…n−1→mBernPolyX+1−mBernPolyX=m⁢Xm−1
34 19 20 33 bpolydiflem ⊢n∈ℕ∧∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1∧X∈ℂ→nBernPolyX+1−nBernPolyX=n⁢Xn−1
35 34 3exp ⊢n∈ℕ→∀k∈1…n−1X∈ℂ→kBernPolyX+1−kBernPolyX=k⁢Xk−1→X∈ℂ→nBernPolyX+1−nBernPolyX=n⁢Xn−1
36 9 18 35 nnsinds ⊢N∈ℕ→X∈ℂ→NBernPolyX+1−NBernPolyX=N⁢XN−1
37 36 imp ⊢N∈ℕ∧X∈ℂ→NBernPolyX+1−NBernPolyX=N⁢XN−1