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 e. NN /\ X e. CC ) -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( 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. ( X ^ ( n - 1 ) ) ) = ( k x. ( X ^ ( k - 1 ) ) ) )
8 3 7 eqeq12d 
 |-  ( n = k -> ( ( ( n BernPoly ( X + 1 ) ) - ( n BernPoly X ) ) = ( n x. ( X ^ ( n - 1 ) ) ) <-> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) )
9 8 imbi2d 
 |-  ( n = k -> ( ( X e. CC -> ( ( n BernPoly ( X + 1 ) ) - ( n BernPoly X ) ) = ( n x. ( X ^ ( n - 1 ) ) ) ) <-> ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( 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. ( X ^ ( n - 1 ) ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )
17 12 16 eqeq12d 
 |-  ( n = N -> ( ( ( n BernPoly ( X + 1 ) ) - ( n BernPoly X ) ) = ( n x. ( X ^ ( n - 1 ) ) ) <-> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) ) )
18 17 imbi2d 
 |-  ( n = N -> ( ( X e. CC -> ( ( n BernPoly ( X + 1 ) ) - ( n BernPoly X ) ) = ( n x. ( X ^ ( n - 1 ) ) ) ) <-> ( X e. CC -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) ) ) )
19 simp1 
 |-  ( ( n e. NN /\ A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ X e. CC ) -> n e. NN )
20 simp3 
 |-  ( ( n e. NN /\ A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ X e. CC ) -> X e. CC )
21 simpl3 
 |-  ( ( ( n e. NN /\ A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ X e. CC ) /\ m e. ( 1 ... ( n - 1 ) ) ) -> X e. CC )
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. ( X ^ ( k - 1 ) ) ) = ( m x. ( X ^ ( m - 1 ) ) ) )
29 24 28 eqeq12d 
 |-  ( k = m -> ( ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) <-> ( ( m BernPoly ( X + 1 ) ) - ( m BernPoly X ) ) = ( m x. ( X ^ ( m - 1 ) ) ) ) )
30 29 imbi2d 
 |-  ( k = m -> ( ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) <-> ( X e. CC -> ( ( m BernPoly ( X + 1 ) ) - ( m BernPoly X ) ) = ( m x. ( X ^ ( m - 1 ) ) ) ) ) )
31 30 rspccva 
 |-  ( ( A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ m e. ( 1 ... ( n - 1 ) ) ) -> ( X e. CC -> ( ( m BernPoly ( X + 1 ) ) - ( m BernPoly X ) ) = ( m x. ( X ^ ( m - 1 ) ) ) ) )
32 31 3ad2antl2 
 |-  ( ( ( n e. NN /\ A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ X e. CC ) /\ m e. ( 1 ... ( n - 1 ) ) ) -> ( X e. CC -> ( ( m BernPoly ( X + 1 ) ) - ( m BernPoly X ) ) = ( m x. ( X ^ ( m - 1 ) ) ) ) )
33 21 32 mpd 
 |-  ( ( ( n e. NN /\ A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ X e. CC ) /\ m e. ( 1 ... ( n - 1 ) ) ) -> ( ( m BernPoly ( X + 1 ) ) - ( m BernPoly X ) ) = ( m x. ( X ^ ( m - 1 ) ) ) )
34 19 20 33 bpolydiflem 
 |-  ( ( n e. NN /\ A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) /\ X e. CC ) -> ( ( n BernPoly ( X + 1 ) ) - ( n BernPoly X ) ) = ( n x. ( X ^ ( n - 1 ) ) ) )
35 34 3exp 
 |-  ( n e. NN -> ( A. k e. ( 1 ... ( n - 1 ) ) ( X e. CC -> ( ( k BernPoly ( X + 1 ) ) - ( k BernPoly X ) ) = ( k x. ( X ^ ( k - 1 ) ) ) ) -> ( X e. CC -> ( ( n BernPoly ( X + 1 ) ) - ( n BernPoly X ) ) = ( n x. ( X ^ ( n - 1 ) ) ) ) ) )
36 9 18 35 nnsinds 
 |-  ( N e. NN -> ( X e. CC -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) ) )
37 36 imp 
 |-  ( ( N e. NN /\ X e. CC ) -> ( ( N BernPoly ( X + 1 ) ) - ( N BernPoly X ) ) = ( N x. ( X ^ ( N - 1 ) ) ) )