Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  bpolylem Structured version   Unicode version

Theorem bpolylem 28120
Description: Lemma for bpolyval 28121. (Contributed by Scott Fenton, 22-May-2014.) (Revised by Mario Carneiro, 23-Aug-2014.)
Hypotheses
Ref Expression
bpoly.1  |-  G  =  ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )
bpoly.2  |-  F  = wrecs (  <  ,  NN0 ,  G )
Assertion
Ref Expression
bpolylem  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( N BernPoly  X )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( N  -  k
)  +  1 ) ) ) ) )
Distinct variable groups:    g, k, n, F    g, N, k, n    g, X, k, n
Allowed substitution hints:    G( g, k, n)

Proof of Theorem bpolylem
Dummy variables  m  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6097 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x ^ n )  =  ( X ^
n ) )
21oveq1d 6105 . . . . . . . . . 10  |-  ( x  =  X  ->  (
( x ^ n
)  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) ) )  =  ( ( X ^ n )  -  sum_ k  e.  dom  g
( ( n  _C  k )  x.  (
( g `  k
)  /  ( ( n  -  k )  +  1 ) ) ) ) )
32csbeq2dv 3684 . . . . . . . . 9  |-  ( x  =  X  ->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )  = 
[_ ( # `  dom  g )  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )
43mpteq2dv 4376 . . . . . . . 8  |-  ( x  =  X  ->  (
g  e.  _V  |->  [_ ( # `  dom  g
)  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )  =  ( g  e.  _V  |->  [_ ( # `  dom  g
)  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) )
5 bpoly.1 . . . . . . . 8  |-  G  =  ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )
64, 5syl6eqr 2491 . . . . . . 7  |-  ( x  =  X  ->  (
g  e.  _V  |->  [_ ( # `  dom  g
)  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )  =  G )
7 wrecseq3 27651 . . . . . . 7  |-  ( ( g  e.  _V  |->  [_ ( # `  dom  g
)  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )  =  G  -> wrecs (  <  ,  NN0 ,  ( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) )  = wrecs (  <  ,  NN0 ,  G ) )
86, 7syl 16 . . . . . 6  |-  ( x  =  X  -> wrecs (  <  ,  NN0 ,  ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) ) )  = wrecs (  <  ,  NN0 ,  G ) )
9 bpoly.2 . . . . . 6  |-  F  = wrecs (  <  ,  NN0 ,  G )
108, 9syl6eqr 2491 . . . . 5  |-  ( x  =  X  -> wrecs (  <  ,  NN0 ,  ( g  e.  _V  |->  [_ ( # `
 dom  g )  /  n ]_ ( ( x ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) ) )  =  F )
1110fveq1d 5690 . . . 4  |-  ( x  =  X  ->  (wrecs (  <  ,  NN0 , 
( g  e.  _V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) ) `  m )  =  ( F `  m ) )
12 fveq2 5688 . . . 4  |-  ( m  =  N  ->  ( F `  m )  =  ( F `  N ) )
1311, 12sylan9eqr 2495 . . 3  |-  ( ( m  =  N  /\  x  =  X )  ->  (wrecs (  <  ,  NN0 ,  ( g  e. 
_V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) ) `  m )  =  ( F `  N ) )
14 df-bpoly 28119 . . 3  |- BernPoly  =  ( m  e.  NN0 ,  x  e.  CC  |->  (wrecs (  <  ,  NN0 ,  ( g  e.  _V  |->  [_ ( # `  dom  g
)  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) ) `  m ) )
15 fvex 5698 . . 3  |-  ( F `
 N )  e. 
_V
1613, 14, 15ovmpt2a 6220 . 2  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( N BernPoly  X )  =  ( F `  N ) )
17 ltweuz 11780 . . . . 5  |-  <  We  ( ZZ>= `  0 )
18 nn0uz 10891 . . . . . 6  |-  NN0  =  ( ZZ>= `  0 )
19 weeq2 4705 . . . . . 6  |-  ( NN0  =  ( ZZ>= `  0
)  ->  (  <  We 
NN0 
<->  <  We  ( ZZ>= ` 
0 ) ) )
2018, 19ax-mp 5 . . . . 5  |-  (  < 
We  NN0  <->  <  We  ( ZZ>= ` 
0 ) )
2117, 20mpbir 209 . . . 4  |-  <  We  NN0
22 nn0ex 10581 . . . . 5  |-  NN0  e.  _V
23 exse 4680 . . . . 5  |-  ( NN0 
e.  _V  ->  < Se  NN0 )
2422, 23ax-mp 5 . . . 4  |-  < Se  NN0
2521, 24, 9wfr2 27670 . . 3  |-  ( N  e.  NN0  ->  ( F `
 N )  =  ( G `  ( F  |`  Pred (  <  ,  NN0 ,  N ) ) ) )
2625adantr 462 . 2  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( F `  N
)  =  ( G `
 ( F  |`  Pred (  <  ,  NN0 ,  N ) ) ) )
27 prednn0 27592 . . . . . 6  |-  ( N  e.  NN0  ->  Pred (  <  ,  NN0 ,  N
)  =  ( 0 ... ( N  - 
1 ) ) )
2827adantr 462 . . . . 5  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  Pred (  <  ,  NN0 ,  N )  =  ( 0 ... ( N  -  1 ) ) )
2928reseq2d 5106 . . . 4  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( F  |`  Pred (  <  ,  NN0 ,  N
) )  =  ( F  |`  ( 0 ... ( N  - 
1 ) ) ) )
3029fveq2d 5692 . . 3  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( G `  ( F  |`  Pred (  <  ,  NN0 ,  N ) ) )  =  ( G `
 ( F  |`  ( 0 ... ( N  -  1 ) ) ) ) )
3121, 24, 9wfr1 27669 . . . . . . 7  |-  F  Fn  NN0
32 fnfun 5505 . . . . . . 7  |-  ( F  Fn  NN0  ->  Fun  F
)
3331, 32ax-mp 5 . . . . . 6  |-  Fun  F
34 ovex 6115 . . . . . 6  |-  ( 0 ... ( N  - 
1 ) )  e. 
_V
35 resfunexg 5940 . . . . . 6  |-  ( ( Fun  F  /\  (
0 ... ( N  - 
1 ) )  e. 
_V )  ->  ( F  |`  ( 0 ... ( N  -  1 ) ) )  e. 
_V )
3633, 34, 35mp2an 667 . . . . 5  |-  ( F  |`  ( 0 ... ( N  -  1 ) ) )  e.  _V
37 dmeq 5036 . . . . . . . . . . 11  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  dom  g  =  dom  ( F  |`  ( 0 ... ( N  -  1 ) ) ) )
38 elfznn0 11477 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... ( N  -  1 ) )  ->  k  e.  NN0 )
3938ssriv 3357 . . . . . . . . . . . . 13  |-  ( 0 ... ( N  - 
1 ) )  C_  NN0
40 fnssres 5521 . . . . . . . . . . . . 13  |-  ( ( F  Fn  NN0  /\  ( 0 ... ( N  -  1 ) )  C_  NN0 )  -> 
( F  |`  (
0 ... ( N  - 
1 ) ) )  Fn  ( 0 ... ( N  -  1 ) ) )
4131, 39, 40mp2an 667 . . . . . . . . . . . 12  |-  ( F  |`  ( 0 ... ( N  -  1 ) ) )  Fn  (
0 ... ( N  - 
1 ) )
42 fndm 5507 . . . . . . . . . . . 12  |-  ( ( F  |`  ( 0 ... ( N  - 
1 ) ) )  Fn  ( 0 ... ( N  -  1 ) )  ->  dom  ( F  |`  ( 0 ... ( N  - 
1 ) ) )  =  ( 0 ... ( N  -  1 ) ) )
4341, 42ax-mp 5 . . . . . . . . . . 11  |-  dom  ( F  |`  ( 0 ... ( N  -  1 ) ) )  =  ( 0 ... ( N  -  1 ) )
4437, 43syl6eq 2489 . . . . . . . . . 10  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  dom  g  =  ( 0 ... ( N  - 
1 ) ) )
45 fveq1 5687 . . . . . . . . . . . . 13  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  (
g `  k )  =  ( ( F  |`  ( 0 ... ( N  -  1 ) ) ) `  k
) )
46 fvres 5701 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... ( N  -  1 ) )  ->  (
( F  |`  (
0 ... ( N  - 
1 ) ) ) `
 k )  =  ( F `  k
) )
4745, 46sylan9eq 2493 . . . . . . . . . . . 12  |-  ( ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
g `  k )  =  ( F `  k ) )
4847oveq1d 6105 . . . . . . . . . . 11  |-  ( ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( g `  k
)  /  ( ( n  -  k )  +  1 ) )  =  ( ( F `
 k )  / 
( ( n  -  k )  +  1 ) ) )
4948oveq2d 6106 . . . . . . . . . 10  |-  ( ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) )  =  ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
5044, 49sumeq12rdv 13180 . . . . . . . . 9  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) )  = 
sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) ) ) )
5150oveq2d 6106 . . . . . . . 8  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  (
( X ^ n
)  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `
 k )  / 
( ( n  -  k )  +  1 ) ) ) )  =  ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )
5251csbeq2dv 3684 . . . . . . 7  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  [_ ( # `
 dom  g )  /  n ]_ ( ( X ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )  = 
[_ ( # `  dom  g )  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )
5344fveq2d 5692 . . . . . . . 8  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  ( # `
 dom  g )  =  ( # `  (
0 ... ( N  - 
1 ) ) ) )
5453csbeq1d 3292 . . . . . . 7  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  [_ ( # `
 dom  g )  /  n ]_ ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) ) ) )  =  [_ ( # `  ( 0 ... ( N  - 
1 ) ) )  /  n ]_ (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) )
5552, 54eqtrd 2473 . . . . . 6  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  [_ ( # `
 dom  g )  /  n ]_ ( ( X ^ n )  -  sum_ k  e.  dom  g ( ( n  _C  k )  x.  ( ( g `  k )  /  (
( n  -  k
)  +  1 ) ) ) )  = 
[_ ( # `  (
0 ... ( N  - 
1 ) ) )  /  n ]_ (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) )
56 ovex 6115 . . . . . . 7  |-  ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) ) ) )  e.  _V
5756csbex 4422 . . . . . 6  |-  [_ ( # `
 ( 0 ... ( N  -  1 ) ) )  /  n ]_ ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) ) )  e.  _V
5855, 5, 57fvmpt 5771 . . . . 5  |-  ( ( F  |`  ( 0 ... ( N  - 
1 ) ) )  e.  _V  ->  ( G `  ( F  |`  ( 0 ... ( N  -  1 ) ) ) )  = 
[_ ( # `  (
0 ... ( N  - 
1 ) ) )  /  n ]_ (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) ) )
5936, 58ax-mp 5 . . . 4  |-  ( G `
 ( F  |`  ( 0 ... ( N  -  1 ) ) ) )  = 
[_ ( # `  (
0 ... ( N  - 
1 ) ) )  /  n ]_ (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) )
60 nfcvd 2578 . . . . . . 7  |-  ( N  e.  NN0  ->  F/_ n
( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) ) ) )
61 oveq2 6098 . . . . . . . 8  |-  ( n  =  N  ->  ( X ^ n )  =  ( X ^ N
) )
62 oveq1 6097 . . . . . . . . . 10  |-  ( n  =  N  ->  (
n  _C  k )  =  ( N  _C  k ) )
63 oveq1 6097 . . . . . . . . . . . 12  |-  ( n  =  N  ->  (
n  -  k )  =  ( N  -  k ) )
6463oveq1d 6105 . . . . . . . . . . 11  |-  ( n  =  N  ->  (
( n  -  k
)  +  1 )  =  ( ( N  -  k )  +  1 ) )
6564oveq2d 6106 . . . . . . . . . 10  |-  ( n  =  N  ->  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) )  =  ( ( F `
 k )  / 
( ( N  -  k )  +  1 ) ) )
6662, 65oveq12d 6108 . . . . . . . . 9  |-  ( n  =  N  ->  (
( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) )  =  ( ( N  _C  k )  x.  ( ( F `  k )  /  (
( N  -  k
)  +  1 ) ) ) )
6766sumeq2sdv 13177 . . . . . . . 8  |-  ( n  =  N  ->  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) )  =  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) ) )
6861, 67oveq12d 6108 . . . . . . 7  |-  ( n  =  N  ->  (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) ) ) )
6960, 68csbiegf 3309 . . . . . 6  |-  ( N  e.  NN0  ->  [_ N  /  n ]_ ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) ) ) )  =  ( ( X ^ N
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( N  _C  k )  x.  ( ( F `  k )  /  (
( N  -  k
)  +  1 ) ) ) ) )
7069adantr 462 . . . . 5  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  [_ N  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) ) )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( N  _C  k )  x.  (
( F `  k
)  /  ( ( N  -  k )  +  1 ) ) ) ) )
71 nn0z 10665 . . . . . . . . . 10  |-  ( N  e.  NN0  ->  N  e.  ZZ )
72 fz01en 11473 . . . . . . . . . 10  |-  ( N  e.  ZZ  ->  (
0 ... ( N  - 
1 ) )  ~~  ( 1 ... N
) )
7371, 72syl 16 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( 0 ... ( N  - 
1 ) )  ~~  ( 1 ... N
) )
74 fzfi 11790 . . . . . . . . . 10  |-  ( 0 ... ( N  - 
1 ) )  e. 
Fin
75 fzfi 11790 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
Fin
76 hashen 12114 . . . . . . . . . 10  |-  ( ( ( 0 ... ( N  -  1 ) )  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( # `  (
0 ... ( N  - 
1 ) ) )  =  ( # `  (
1 ... N ) )  <-> 
( 0 ... ( N  -  1 ) )  ~~  ( 1 ... N ) ) )
7774, 75, 76mp2an 667 . . . . . . . . 9  |-  ( (
# `  ( 0 ... ( N  -  1 ) ) )  =  ( # `  (
1 ... N ) )  <-> 
( 0 ... ( N  -  1 ) )  ~~  ( 1 ... N ) )
7873, 77sylibr 212 . . . . . . . 8  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... ( N  -  1 ) ) )  =  (
# `  ( 1 ... N ) ) )
79 hashfz1 12113 . . . . . . . 8  |-  ( N  e.  NN0  ->  ( # `  ( 1 ... N
) )  =  N )
8078, 79eqtrd 2473 . . . . . . 7  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... ( N  -  1 ) ) )  =  N )
8180adantr 462 . . . . . 6  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( # `  (
0 ... ( N  - 
1 ) ) )  =  N )
8281csbeq1d 3292 . . . . 5  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  [_ ( # `  (
0 ... ( N  - 
1 ) ) )  /  n ]_ (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) )  = 
[_ N  /  n ]_ ( ( X ^
n )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) )
83 simpr 458 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  X  e.  CC )
84 fveq2 5688 . . . . . . . . . . . 12  |-  ( m  =  k  ->  ( F `  m )  =  ( F `  k ) )
8511, 84sylan9eqr 2495 . . . . . . . . . . 11  |-  ( ( m  =  k  /\  x  =  X )  ->  (wrecs (  <  ,  NN0 ,  ( g  e. 
_V  |->  [_ ( # `  dom  g )  /  n ]_ ( ( x ^
n )  -  sum_ k  e.  dom  g ( ( n  _C  k
)  x.  ( ( g `  k )  /  ( ( n  -  k )  +  1 ) ) ) ) ) ) `  m )  =  ( F `  k ) )
86 fvex 5698 . . . . . . . . . . 11  |-  ( F `
 k )  e. 
_V
8785, 14, 86ovmpt2a 6220 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  X  e.  CC )  ->  ( k BernPoly  X )  =  ( F `  k ) )
8838, 83, 87syl2anr 475 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  X  e.  CC )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( k BernPoly  X )  =  ( F `
 k ) )
8988oveq1d 6105 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  X  e.  CC )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( (
k BernPoly  X )  /  (
( N  -  k
)  +  1 ) )  =  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) )
9089oveq2d 6106 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  X  e.  CC )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( ( N  _C  k )  x.  ( ( k BernPoly  X
)  /  ( ( N  -  k )  +  1 ) ) )  =  ( ( N  _C  k )  x.  ( ( F `
 k )  / 
( ( N  -  k )  +  1 ) ) ) )
9190sumeq2dv 13176 . . . . . 6  |-  ( ( N  e.  NN0  /\  X  e.  CC )  -> 
sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( N  _C  k )  x.  (
( k BernPoly  X )  /  ( ( N  -  k )  +  1 ) ) )  =  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( N  _C  k )  x.  (
( F `  k
)  /  ( ( N  -  k )  +  1 ) ) ) )
9291oveq2d 6106 . . . . 5  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( N  -  k
)  +  1 ) ) ) )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) ) ) )
9370, 82, 923eqtr4d 2483 . . . 4  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  [_ ( # `  (
0 ... ( N  - 
1 ) ) )  /  n ]_ (
( X ^ n
)  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  ( ( F `  k )  /  (
( n  -  k
)  +  1 ) ) ) )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( N  -  k
)  +  1 ) ) ) ) )
9459, 93syl5eq 2485 . . 3  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( G `  ( F  |`  ( 0 ... ( N  -  1 ) ) ) )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( N  -  k
)  +  1 ) ) ) ) )
9530, 94eqtrd 2473 . 2  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( G `  ( F  |`  Pred (  <  ,  NN0 ,  N ) ) )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( N  _C  k )  x.  (
( k BernPoly  X )  /  ( ( N  -  k )  +  1 ) ) ) ) )
9616, 26, 953eqtrd 2477 1  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( N BernPoly  X )  =  ( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( k BernPoly  X )  /  (
( N  -  k
)  +  1 ) ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1364    e. wcel 1761   _Vcvv 2970   [_csb 3285    C_ wss 3325   class class class wbr 4289    e. cmpt 4347   Se wse 4673    We wwe 4674   dom cdm 4836    |` cres 4838   Fun wfun 5409    Fn wfn 5410   ` cfv 5415  (class class class)co 6090    ~~ cen 7303   Fincfn 7306   CCcc 9276   0cc0 9278   1c1 9279    + caddc 9281    x. cmul 9283    < clt 9414    - cmin 9591    / cdiv 9989   NN0cn0 10575   ZZcz 10642   ZZ>=cuz 10857   ...cfz 11433   ^cexp 11861    _C cbc 12074   #chash 12099   sum_csu 13159   Predcpred 27553  wrecscwrecs 27645   BernPoly cbp 28118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371  ax-inf2 7843  ax-cnex 9334  ax-resscn 9335  ax-1cn 9336  ax-icn 9337  ax-addcl 9338  ax-addrcl 9339  ax-mulcl 9340  ax-mulrcl 9341  ax-mulcom 9342  ax-addass 9343  ax-mulass 9344  ax-distr 9345  ax-i2m1 9346  ax-1ne0 9347  ax-1rid 9348  ax-rnegex 9349  ax-rrecex 9350  ax-cnre 9351  ax-pre-lttri 9352  ax-pre-lttrn 9353  ax-pre-ltadd 9354  ax-pre-mulgt0 9355
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-fal 1370  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rmo 2721  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-se 4676  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-isom 5424  df-riota 6049  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-er 7097  df-en 7307  df-dom 7308  df-sdom 7309  df-fin 7310  df-card 8105  df-pnf 9416  df-mnf 9417  df-xr 9418  df-ltxr 9419  df-le 9420  df-sub 9593  df-neg 9594  df-nn 10319  df-n0 10576  df-z 10643  df-uz 10858  df-fz 11434  df-seq 11803  df-hash 12100  df-sum 13160  df-pred 27554  df-wrecs 27646  df-bpoly 28119
This theorem is referenced by:  bpolyval  28121
  Copyright terms: Public domain W3C validator