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 ∈ ℂ → N BernPoly X + 1 − N BernPoly X = N ⁢ X N − 1

Proof

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