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 ( ( 𝑁 ∈ ℕ ∧ 𝑋 ∈ ℂ ) → ( ( 𝑁 BernPoly ( 𝑋 + 1 ) ) − ( 𝑁 BernPoly 𝑋 ) ) = ( 𝑁 · ( 𝑋 ↑ ( 𝑁 − 1 ) ) ) )

Proof

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