Metamath Proof Explorer

Theorem bpolycl

Description: Closure law for Bernoulli polynomials. (Contributed by Scott Fenton, 16-May-2014) (Proof shortened by Mario Carneiro, 22-May-2014)

Ref Expression
Assertion bpolycl 
|- ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) e. CC )

Proof

Step Hyp Ref Expression
1 oveq1 
 |-  ( n = k -> ( n BernPoly X ) = ( k BernPoly X ) )
2 1 eleq1d 
 |-  ( n = k -> ( ( n BernPoly X ) e. CC <-> ( k BernPoly X ) e. CC ) )
3 2 imbi2d 
 |-  ( n = k -> ( ( X e. CC -> ( n BernPoly X ) e. CC ) <-> ( X e. CC -> ( k BernPoly X ) e. CC ) ) )
4 oveq1 
 |-  ( n = N -> ( n BernPoly X ) = ( N BernPoly X ) )
5 4 eleq1d 
 |-  ( n = N -> ( ( n BernPoly X ) e. CC <-> ( N BernPoly X ) e. CC ) )
6 5 imbi2d 
 |-  ( n = N -> ( ( X e. CC -> ( n BernPoly X ) e. CC ) <-> ( X e. CC -> ( N BernPoly X ) e. CC ) ) )
7 r19.21v 
 |-  ( A. k e. ( 0 ... ( n - 1 ) ) ( X e. CC -> ( k BernPoly X ) e. CC ) <-> ( X e. CC -> A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) )
8 bpolyval 
 |-  ( ( n e. NN0 /\ X e. CC ) -> ( n BernPoly X ) = ( ( X ^ n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( ( n _C m ) x. ( ( m BernPoly X ) / ( ( n - m ) + 1 ) ) ) ) )
9 8 3adant3 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( n BernPoly X ) = ( ( X ^ n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( ( n _C m ) x. ( ( m BernPoly X ) / ( ( n - m ) + 1 ) ) ) ) )
10 simp2 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> X e. CC )
11 simp1 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> n e. NN0 )
12 10 11 expcld 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( X ^ n ) e. CC )
13 fzfid 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( 0 ... ( n - 1 ) ) e. Fin )
14 elfzelz 
 |-  ( m e. ( 0 ... ( n - 1 ) ) -> m e. ZZ )
15 bccl 
 |-  ( ( n e. NN0 /\ m e. ZZ ) -> ( n _C m ) e. NN0 )
16 11 14 15 syl2an 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( n _C m ) e. NN0 )
17 16 nn0cnd 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( n _C m ) e. CC )
18 oveq1 
 |-  ( k = m -> ( k BernPoly X ) = ( m BernPoly X ) )
19 18 eleq1d 
 |-  ( k = m -> ( ( k BernPoly X ) e. CC <-> ( m BernPoly X ) e. CC ) )
20 19 rspccva 
 |-  ( ( A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( m BernPoly X ) e. CC )
21 20 3ad2antl3 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( m BernPoly X ) e. CC )
22 fzssp1 
 |-  ( 0 ... ( n - 1 ) ) C_ ( 0 ... ( ( n - 1 ) + 1 ) )
23 11 nn0cnd 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> n e. CC )
24 ax-1cn 
 |-  1 e. CC
25 npcan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n - 1 ) + 1 ) = n )
26 23 24 25 sylancl 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( ( n - 1 ) + 1 ) = n )
27 26 oveq2d 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( 0 ... ( ( n - 1 ) + 1 ) ) = ( 0 ... n ) )
28 22 27 sseqtrid 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( 0 ... ( n - 1 ) ) C_ ( 0 ... n ) )
29 28 sselda 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> m e. ( 0 ... n ) )
30 fznn0sub 
 |-  ( m e. ( 0 ... n ) -> ( n - m ) e. NN0 )
31 nn0p1nn 
 |-  ( ( n - m ) e. NN0 -> ( ( n - m ) + 1 ) e. NN )
32 29 30 31 3syl 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( ( n - m ) + 1 ) e. NN )
33 32 nncnd 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( ( n - m ) + 1 ) e. CC )
34 32 nnne0d 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( ( n - m ) + 1 ) =/= 0 )
35 21 33 34 divcld 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( ( m BernPoly X ) / ( ( n - m ) + 1 ) ) e. CC )
36 17 35 mulcld 
 |-  ( ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) /\ m e. ( 0 ... ( n - 1 ) ) ) -> ( ( n _C m ) x. ( ( m BernPoly X ) / ( ( n - m ) + 1 ) ) ) e. CC )
37 13 36 fsumcl 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> sum_ m e. ( 0 ... ( n - 1 ) ) ( ( n _C m ) x. ( ( m BernPoly X ) / ( ( n - m ) + 1 ) ) ) e. CC )
38 12 37 subcld 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( ( X ^ n ) - sum_ m e. ( 0 ... ( n - 1 ) ) ( ( n _C m ) x. ( ( m BernPoly X ) / ( ( n - m ) + 1 ) ) ) ) e. CC )
39 9 38 eqeltrd 
 |-  ( ( n e. NN0 /\ X e. CC /\ A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( n BernPoly X ) e. CC )
40 39 3exp 
 |-  ( n e. NN0 -> ( X e. CC -> ( A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC -> ( n BernPoly X ) e. CC ) ) )
41 40 a2d 
 |-  ( n e. NN0 -> ( ( X e. CC -> A. k e. ( 0 ... ( n - 1 ) ) ( k BernPoly X ) e. CC ) -> ( X e. CC -> ( n BernPoly X ) e. CC ) ) )
42 7 41 syl5bi 
 |-  ( n e. NN0 -> ( A. k e. ( 0 ... ( n - 1 ) ) ( X e. CC -> ( k BernPoly X ) e. CC ) -> ( X e. CC -> ( n BernPoly X ) e. CC ) ) )
43 3 6 42 nn0sinds 
 |-  ( N e. NN0 -> ( X e. CC -> ( N BernPoly X ) e. CC ) )
44 43 imp 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) e. CC )