MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bpolylem Structured version   Unicode version

Theorem bpolylem 14101
Description: Lemma for bpolyval 14102. (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 6313 . . . . . . . . . . 11  |-  ( x  =  X  ->  (
x ^ n )  =  ( X ^
n ) )
21oveq1d 6321 . . . . . . . . . 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 3811 . . . . . . . . 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 4511 . . . . . . . 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 2481 . . . . . . 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 7045 . . . . . . 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 17 . . . . . 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 2481 . . . . 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 5884 . . . 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 5882 . . . 4  |-  ( m  =  N  ->  ( F `  m )  =  ( F `  N ) )
1311, 12sylan9eqr 2485 . . 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 14100 . . 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 5892 . . 3  |-  ( F `
 N )  e. 
_V
1613, 14, 15ovmpt2a 6442 . 2  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( N BernPoly  X )  =  ( F `  N ) )
17 ltweuz 12182 . . . . 5  |-  <  We  ( ZZ>= `  0 )
18 nn0uz 11201 . . . . . 6  |-  NN0  =  ( ZZ>= `  0 )
19 weeq2 4842 . . . . . 6  |-  ( NN0  =  ( ZZ>= `  0
)  ->  (  <  We 
NN0 
<->  <  We  ( ZZ>= ` 
0 ) ) )
2018, 19ax-mp 5 . . . . 5  |-  (  < 
We  NN0  <->  <  We  ( ZZ>= ` 
0 ) )
2117, 20mpbir 212 . . . 4  |-  <  We  NN0
22 nn0ex 10883 . . . . 5  |-  NN0  e.  _V
23 exse 4817 . . . . 5  |-  ( NN0 
e.  _V  ->  < Se  NN0 )
2422, 23ax-mp 5 . . . 4  |-  < Se  NN0
2521, 24, 9wfr2 7067 . . 3  |-  ( N  e.  NN0  ->  ( F `
 N )  =  ( G `  ( F  |`  Pred (  <  ,  NN0 ,  N ) ) ) )
2625adantr 466 . 2  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( F `  N
)  =  ( G `
 ( F  |`  Pred (  <  ,  NN0 ,  N ) ) ) )
27 prednn0 11921 . . . . . 6  |-  ( N  e.  NN0  ->  Pred (  <  ,  NN0 ,  N
)  =  ( 0 ... ( N  - 
1 ) ) )
2827adantr 466 . . . . 5  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  Pred (  <  ,  NN0 ,  N )  =  ( 0 ... ( N  -  1 ) ) )
2928reseq2d 5124 . . . 4  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( F  |`  Pred (  <  ,  NN0 ,  N
) )  =  ( F  |`  ( 0 ... ( N  - 
1 ) ) ) )
3029fveq2d 5886 . . 3  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( G `  ( F  |`  Pred (  <  ,  NN0 ,  N ) ) )  =  ( G `
 ( F  |`  ( 0 ... ( N  -  1 ) ) ) ) )
3121, 24, 9wfrfun 7058 . . . . . 6  |-  Fun  F
32 ovex 6334 . . . . . 6  |-  ( 0 ... ( N  - 
1 ) )  e. 
_V
33 resfunexg 6146 . . . . . 6  |-  ( ( Fun  F  /\  (
0 ... ( N  - 
1 ) )  e. 
_V )  ->  ( F  |`  ( 0 ... ( N  -  1 ) ) )  e. 
_V )
3431, 32, 33mp2an 676 . . . . 5  |-  ( F  |`  ( 0 ... ( N  -  1 ) ) )  e.  _V
35 dmeq 5054 . . . . . . . . . . 11  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  dom  g  =  dom  ( F  |`  ( 0 ... ( N  -  1 ) ) ) )
3621, 24, 9wfr1 7066 . . . . . . . . . . . . 13  |-  F  Fn  NN0
37 elfznn0 11895 . . . . . . . . . . . . . 14  |-  ( k  e.  ( 0 ... ( N  -  1 ) )  ->  k  e.  NN0 )
3837ssriv 3468 . . . . . . . . . . . . 13  |-  ( 0 ... ( N  - 
1 ) )  C_  NN0
39 fnssres 5707 . . . . . . . . . . . . 13  |-  ( ( F  Fn  NN0  /\  ( 0 ... ( N  -  1 ) )  C_  NN0 )  -> 
( F  |`  (
0 ... ( N  - 
1 ) ) )  Fn  ( 0 ... ( N  -  1 ) ) )
4036, 38, 39mp2an 676 . . . . . . . . . . . 12  |-  ( F  |`  ( 0 ... ( N  -  1 ) ) )  Fn  (
0 ... ( N  - 
1 ) )
41 fndm 5693 . . . . . . . . . . . 12  |-  ( ( F  |`  ( 0 ... ( N  - 
1 ) ) )  Fn  ( 0 ... ( N  -  1 ) )  ->  dom  ( F  |`  ( 0 ... ( N  - 
1 ) ) )  =  ( 0 ... ( N  -  1 ) ) )
4240, 41ax-mp 5 . . . . . . . . . . 11  |-  dom  ( F  |`  ( 0 ... ( N  -  1 ) ) )  =  ( 0 ... ( N  -  1 ) )
4335, 42syl6eq 2479 . . . . . . . . . 10  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  dom  g  =  ( 0 ... ( N  - 
1 ) ) )
44 fveq1 5881 . . . . . . . . . . . . 13  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  (
g `  k )  =  ( ( F  |`  ( 0 ... ( N  -  1 ) ) ) `  k
) )
45 fvres 5896 . . . . . . . . . . . . 13  |-  ( k  e.  ( 0 ... ( N  -  1 ) )  ->  (
( F  |`  (
0 ... ( N  - 
1 ) ) ) `
 k )  =  ( F `  k
) )
4644, 45sylan9eq 2483 . . . . . . . . . . . 12  |-  ( ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
g `  k )  =  ( F `  k ) )
4746oveq1d 6321 . . . . . . . . . . 11  |-  ( ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( g `  k
)  /  ( ( n  -  k )  +  1 ) )  =  ( ( F `
 k )  / 
( ( n  -  k )  +  1 ) ) )
4847oveq2d 6322 . . . . . . . . . 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 ) ) ) )
4943, 48sumeq12rdv 13773 . . . . . . . . 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 ) ) ) )
5049oveq2d 6322 . . . . . . . 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 ) ) ) ) )
5150csbeq2dv 3811 . . . . . . 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 ) ) ) ) )
5243fveq2d 5886 . . . . . . . 8  |-  ( g  =  ( F  |`  ( 0 ... ( N  -  1 ) ) )  ->  ( # `
 dom  g )  =  ( # `  (
0 ... ( N  - 
1 ) ) ) )
5352csbeq1d 3402 . . . . . . 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 ) ) ) ) )
5451, 53eqtrd 2463 . . . . . 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 ) ) ) ) )
55 ovex 6334 . . . . . . 7  |-  ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  -  1 ) ) ( ( n  _C  k )  x.  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) ) ) )  e.  _V
5655csbex 4559 . . . . . 6  |-  [_ ( # `
 ( 0 ... ( N  -  1 ) ) )  /  n ]_ ( ( X ^ n )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) ) )  e.  _V
5754, 5, 56fvmpt 5965 . . . . 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 ) ) ) ) )
5834, 57ax-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 ) ) ) )
59 nfcvd 2581 . . . . . . 7  |-  ( N  e.  NN0  ->  F/_ n
( ( X ^ N )  -  sum_ k  e.  ( 0 ... ( N  - 
1 ) ) ( ( N  _C  k
)  x.  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) ) ) )
60 oveq2 6314 . . . . . . . 8  |-  ( n  =  N  ->  ( X ^ n )  =  ( X ^ N
) )
61 oveq1 6313 . . . . . . . . . 10  |-  ( n  =  N  ->  (
n  _C  k )  =  ( N  _C  k ) )
62 oveq1 6313 . . . . . . . . . . . 12  |-  ( n  =  N  ->  (
n  -  k )  =  ( N  -  k ) )
6362oveq1d 6321 . . . . . . . . . . 11  |-  ( n  =  N  ->  (
( n  -  k
)  +  1 )  =  ( ( N  -  k )  +  1 ) )
6463oveq2d 6322 . . . . . . . . . 10  |-  ( n  =  N  ->  (
( F `  k
)  /  ( ( n  -  k )  +  1 ) )  =  ( ( F `
 k )  / 
( ( N  -  k )  +  1 ) ) )
6561, 64oveq12d 6324 . . . . . . . . 9  |-  ( n  =  N  ->  (
( n  _C  k
)  x.  ( ( F `  k )  /  ( ( n  -  k )  +  1 ) ) )  =  ( ( N  _C  k )  x.  ( ( F `  k )  /  (
( N  -  k
)  +  1 ) ) ) )
6665sumeq2sdv 13770 . . . . . . . 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 ) ) ) )
6760, 66oveq12d 6324 . . . . . . 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 ) ) ) ) )
6859, 67csbiegf 3419 . . . . . 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 ) ) ) ) )
6968adantr 466 . . . . 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 ) ) ) ) )
70 nn0z 10968 . . . . . . . . . 10  |-  ( N  e.  NN0  ->  N  e.  ZZ )
71 fz01en 11835 . . . . . . . . . 10  |-  ( N  e.  ZZ  ->  (
0 ... ( N  - 
1 ) )  ~~  ( 1 ... N
) )
7270, 71syl 17 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( 0 ... ( N  - 
1 ) )  ~~  ( 1 ... N
) )
73 fzfi 12192 . . . . . . . . . 10  |-  ( 0 ... ( N  - 
1 ) )  e. 
Fin
74 fzfi 12192 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
Fin
75 hashen 12537 . . . . . . . . . 10  |-  ( ( ( 0 ... ( N  -  1 ) )  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( # `  (
0 ... ( N  - 
1 ) ) )  =  ( # `  (
1 ... N ) )  <-> 
( 0 ... ( N  -  1 ) )  ~~  ( 1 ... N ) ) )
7673, 74, 75mp2an 676 . . . . . . . . 9  |-  ( (
# `  ( 0 ... ( N  -  1 ) ) )  =  ( # `  (
1 ... N ) )  <-> 
( 0 ... ( N  -  1 ) )  ~~  ( 1 ... N ) )
7772, 76sylibr 215 . . . . . . . 8  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... ( N  -  1 ) ) )  =  (
# `  ( 1 ... N ) ) )
78 hashfz1 12536 . . . . . . . 8  |-  ( N  e.  NN0  ->  ( # `  ( 1 ... N
) )  =  N )
7977, 78eqtrd 2463 . . . . . . 7  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... ( N  -  1 ) ) )  =  N )
8079adantr 466 . . . . . 6  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  ( # `  (
0 ... ( N  - 
1 ) ) )  =  N )
8180csbeq1d 3402 . . . . 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 ) ) ) ) )
82 simpr 462 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  X  e.  CC )  ->  X  e.  CC )
83 fveq2 5882 . . . . . . . . . . . 12  |-  ( m  =  k  ->  ( F `  m )  =  ( F `  k ) )
8411, 83sylan9eqr 2485 . . . . . . . . . . 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 ) )
85 fvex 5892 . . . . . . . . . . 11  |-  ( F `
 k )  e. 
_V
8684, 14, 85ovmpt2a 6442 . . . . . . . . . 10  |-  ( ( k  e.  NN0  /\  X  e.  CC )  ->  ( k BernPoly  X )  =  ( F `  k ) )
8737, 82, 86syl2anr 480 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  X  e.  CC )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( k BernPoly  X )  =  ( F `
 k ) )
8887oveq1d 6321 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  X  e.  CC )  /\  k  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( (
k BernPoly  X )  /  (
( N  -  k
)  +  1 ) )  =  ( ( F `  k )  /  ( ( N  -  k )  +  1 ) ) )
8988oveq2d 6322 . . . . . . 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 ) ) ) )
9089sumeq2dv 13769 . . . . . 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 ) ) ) )
9190oveq2d 6322 . . . . 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 ) ) ) ) )
9269, 81, 913eqtr4d 2473 . . . 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 ) ) ) ) )
9358, 92syl5eq 2475 . . 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 ) ) ) ) )
9430, 93eqtrd 2463 . 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 ) ) ) ) )
9516, 26, 943eqtrd 2467 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 187    /\ wa 370    = wceq 1437    e. wcel 1872   _Vcvv 3080   [_csb 3395    C_ wss 3436   class class class wbr 4423    |-> cmpt 4482   Se wse 4810    We wwe 4811   dom cdm 4853    |` cres 4855   Predcpred 5398   Fun wfun 5595    Fn wfn 5596   ` cfv 5601  (class class class)co 6306  wrecscwrecs 7039    ~~ cen 7578   Fincfn 7581   CCcc 9545   0cc0 9547   1c1 9548    + caddc 9550    x. cmul 9552    < clt 9683    - cmin 9868    / cdiv 10277   NN0cn0 10877   ZZcz 10945   ZZ>=cuz 11167   ...cfz 11792   ^cexp 12279    _C cbc 12494   #chash 12522   sum_csu 13752   BernPoly cbp 14099
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-rep 4536  ax-sep 4546  ax-nul 4555  ax-pow 4602  ax-pr 4660  ax-un 6598  ax-inf2 8156  ax-cnex 9603  ax-resscn 9604  ax-1cn 9605  ax-icn 9606  ax-addcl 9607  ax-addrcl 9608  ax-mulcl 9609  ax-mulrcl 9610  ax-mulcom 9611  ax-addass 9612  ax-mulass 9613  ax-distr 9614  ax-i2m1 9615  ax-1ne0 9616  ax-1rid 9617  ax-rnegex 9618  ax-rrecex 9619  ax-cnre 9620  ax-pre-lttri 9621  ax-pre-lttrn 9622  ax-pre-ltadd 9623  ax-pre-mulgt0 9624
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2273  df-mo 2274  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-nel 2617  df-ral 2776  df-rex 2777  df-reu 2778  df-rmo 2779  df-rab 2780  df-v 3082  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-pss 3452  df-nul 3762  df-if 3912  df-pw 3983  df-sn 3999  df-pr 4001  df-tp 4003  df-op 4005  df-uni 4220  df-int 4256  df-iun 4301  df-br 4424  df-opab 4483  df-mpt 4484  df-tr 4519  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-se 4813  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-isom 5610  df-riota 6268  df-ov 6309  df-oprab 6310  df-mpt2 6311  df-om 6708  df-1st 6808  df-2nd 6809  df-wrecs 7040  df-recs 7102  df-rdg 7140  df-1o 7194  df-er 7375  df-en 7582  df-dom 7583  df-sdom 7584  df-fin 7585  df-card 8382  df-pnf 9685  df-mnf 9686  df-xr 9687  df-ltxr 9688  df-le 9689  df-sub 9870  df-neg 9871  df-nn 10618  df-n0 10878  df-z 10946  df-uz 11168  df-fz 11793  df-seq 12221  df-hash 12523  df-sum 13753  df-bpoly 14100
This theorem is referenced by:  bpolyval  14102
  Copyright terms: Public domain W3C validator