Metamath Proof Explorer

Theorem bpolylem

Description: Lemma for bpolyval . (Contributed by Scott Fenton, 22-May-2014) (Revised by Mario Carneiro, 23-Aug-2014)

Ref Expression
Hypotheses 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 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 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 ) ) ) ) )
2 bpoly.2 
 |-  F = wrecs ( < , NN0 , G )
3 oveq1 
 |-  ( x = X -> ( x ^ n ) = ( X ^ n ) )
4 3 oveq1d 
 |-  ( 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 ) ) ) ) )
5 4 csbeq2dv 
 |-  ( 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 ) ) ) ) )
6 5 mpteq2dv 
 |-  ( 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 ) ) ) ) ) )
7 6 1 eqtr4di 
 |-  ( 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 )
8 wrecseq3 
 |-  ( ( 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 ) )
9 7 8 syl 
 |-  ( 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 ) )
10 9 2 eqtr4di 
 |-  ( 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 )
11 10 fveq1d 
 |-  ( 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 
 |-  ( m = N -> ( F ` m ) = ( F ` N ) )
13 11 12 sylan9eqr 
 |-  ( ( 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 
 |-  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 
 |-  ( F ` N ) e. _V
16 13 14 15 ovmpoa 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( F ` N ) )
17 ltweuz 
 |-  < We ( ZZ>= ` 0 )
18 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
19 weeq2 
 |-  ( NN0 = ( ZZ>= ` 0 ) -> ( < We NN0 <-> < We ( ZZ>= ` 0 ) ) )
20 18 19 ax-mp 
 |-  ( < We NN0 <-> < We ( ZZ>= ` 0 ) )
21 17 20 mpbir 
 |-  < We NN0
22 nn0ex 
 |-  NN0 e. _V
23 exse 
 |-  ( NN0 e. _V -> < Se NN0 )
24 22 23 ax-mp 
 |-  < Se NN0
25 21 24 2 wfr2 
 |-  ( N e. NN0 -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
26 25 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
27 prednn0 
 |-  ( N e. NN0 -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
28 27 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
29 28 reseq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( F |` Pred ( < , NN0 , N ) ) = ( F |` ( 0 ... ( N - 1 ) ) ) )
30 29 fveq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( G ` ( F |` Pred ( < , NN0 , N ) ) ) = ( G ` ( F |` ( 0 ... ( N - 1 ) ) ) ) )
31 21 24 2 wfrfun 
 |-  Fun F
32 ovex 
 |-  ( 0 ... ( N - 1 ) ) e. _V
33 resfunexg 
 |-  ( ( Fun F /\ ( 0 ... ( N - 1 ) ) e. _V ) -> ( F |` ( 0 ... ( N - 1 ) ) ) e. _V )
34 31 32 33 mp2an 
 |-  ( F |` ( 0 ... ( N - 1 ) ) ) e. _V
35 dmeq 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> dom g = dom ( F |` ( 0 ... ( N - 1 ) ) ) )
36 21 24 2 wfr1 
 |-  F Fn NN0
37 fz0ssnn0 
 |-  ( 0 ... ( N - 1 ) ) C_ NN0
38 fnssres 
 |-  ( ( F Fn NN0 /\ ( 0 ... ( N - 1 ) ) C_ NN0 ) -> ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) ) )
39 36 37 38 mp2an 
 |-  ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) )
40 39 fndmi 
 |-  dom ( F |` ( 0 ... ( N - 1 ) ) ) = ( 0 ... ( N - 1 ) )
41 35 40 eqtrdi 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> dom g = ( 0 ... ( N - 1 ) ) )
42 fveq1 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> ( g ` k ) = ( ( F |` ( 0 ... ( N - 1 ) ) ) ` k ) )
43 fvres 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( ( F |` ( 0 ... ( N - 1 ) ) ) ` k ) = ( F ` k ) )
44 42 43 sylan9eq 
 |-  ( ( g = ( F |` ( 0 ... ( N - 1 ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( g ` k ) = ( F ` k ) )
45 44 oveq1d 
 |-  ( ( g = ( F |` ( 0 ... ( N - 1 ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( g ` k ) / ( ( n - k ) + 1 ) ) = ( ( F ` k ) / ( ( n - k ) + 1 ) ) )
46 45 oveq2d 
 |-  ( ( 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 ) ) ) )
47 41 46 sumeq12rdv 
 |-  ( 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 ) ) ) )
48 47 oveq2d 
 |-  ( 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 ) ) ) ) )
49 48 csbeq2dv 
 |-  ( 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 ) ) ) ) )
50 41 fveq2d 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> ( # ` dom g ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
51 50 csbeq1d 
 |-  ( 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 ) ) ) ) )
52 49 51 eqtrd 
 |-  ( 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 ) ) ) ) )
53 ovex 
 |-  ( ( X ^ n ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) ) e. _V
54 53 csbex 
 |-  [_ ( # ` ( 0 ... ( N - 1 ) ) ) / n ]_ ( ( X ^ n ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) ) e. _V
55 52 1 54 fvmpt 
 |-  ( ( 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 ) ) ) ) )
56 34 55 ax-mp 
 |-  ( 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 ) ) ) )
57 nfcvd 
 |-  ( N e. NN0 -> F/_ n ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( F ` k ) / ( ( N - k ) + 1 ) ) ) ) )
58 oveq2 
 |-  ( n = N -> ( X ^ n ) = ( X ^ N ) )
59 oveq1 
 |-  ( n = N -> ( n _C k ) = ( N _C k ) )
60 oveq1 
 |-  ( n = N -> ( n - k ) = ( N - k ) )
61 60 oveq1d 
 |-  ( n = N -> ( ( n - k ) + 1 ) = ( ( N - k ) + 1 ) )
62 61 oveq2d 
 |-  ( n = N -> ( ( F ` k ) / ( ( n - k ) + 1 ) ) = ( ( F ` k ) / ( ( N - k ) + 1 ) ) )
63 59 62 oveq12d 
 |-  ( n = N -> ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) = ( ( N _C k ) x. ( ( F ` k ) / ( ( N - k ) + 1 ) ) ) )
64 63 sumeq2sdv 
 |-  ( 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 ) ) ) )
65 58 64 oveq12d 
 |-  ( 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 ) ) ) ) )
66 57 65 csbiegf 
 |-  ( 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 ) ) ) ) )
67 66 adantr 
 |-  ( ( 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 ) ) ) ) )
68 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
69 fz01en 
 |-  ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
70 68 69 syl 
 |-  ( N e. NN0 -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
71 fzfi 
 |-  ( 0 ... ( N - 1 ) ) e. Fin
72 fzfi 
 |-  ( 1 ... N ) e. Fin
73 hashen 
 |-  ( ( ( 0 ... ( N - 1 ) ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) ) )
74 71 72 73 mp2an 
 |-  ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
75 70 74 sylibr 
 |-  ( N e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) )
76 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
77 75 76 eqtrd 
 |-  ( N e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = N )
78 77 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( # ` ( 0 ... ( N - 1 ) ) ) = N )
79 78 csbeq1d 
 |-  ( ( 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 ) ) ) ) )
80 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
81 simpr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> X e. CC )
82 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
83 11 82 sylan9eqr 
 |-  ( ( 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 ) )
84 fvex 
 |-  ( F ` k ) e. _V
85 83 14 84 ovmpoa 
 |-  ( ( k e. NN0 /\ X e. CC ) -> ( k BernPoly X ) = ( F ` k ) )
86 80 81 85 syl2anr 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k BernPoly X ) = ( F ` k ) )
87 86 oveq1d 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) = ( ( F ` k ) / ( ( N - k ) + 1 ) ) )
88 87 oveq2d 
 |-  ( ( ( 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 ) ) ) )
89 88 sumeq2dv 
 |-  ( ( 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 ) ) ) )
90 89 oveq2d 
 |-  ( ( 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 ) ) ) ) )
91 67 79 90 3eqtr4d 
 |-  ( ( 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 ) ) ) ) )
92 56 91 syl5eq 
 |-  ( ( 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 ) ) ) ) )
93 30 92 eqtrd 
 |-  ( ( 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 ) ) ) ) )
94 16 26 93 3eqtrd 
 |-  ( ( 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 ) ) ) ) )