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 2 wfr2 
 |-  ( ( ( < We NN0 /\ < Se NN0 ) /\ N e. NN0 ) -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
26 21 24 25 mpanl12 
 |-  ( N e. NN0 -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
27 26 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
28 prednn0 
 |-  ( N e. NN0 -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
29 28 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
30 29 reseq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( F |` Pred ( < , NN0 , N ) ) = ( F |` ( 0 ... ( N - 1 ) ) ) )
31 30 fveq2d 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( G ` ( F |` Pred ( < , NN0 , N ) ) ) = ( G ` ( F |` ( 0 ... ( N - 1 ) ) ) ) )
32 2 wfrfun 
 |-  ( ( < We NN0 /\ < Se NN0 ) -> Fun F )
33 21 24 32 mp2an 
 |-  Fun F
34 ovex 
 |-  ( 0 ... ( N - 1 ) ) e. _V
35 resfunexg 
 |-  ( ( Fun F /\ ( 0 ... ( N - 1 ) ) e. _V ) -> ( F |` ( 0 ... ( N - 1 ) ) ) e. _V )
36 33 34 35 mp2an 
 |-  ( F |` ( 0 ... ( N - 1 ) ) ) e. _V
37 dmeq 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> dom g = dom ( F |` ( 0 ... ( N - 1 ) ) ) )
38 2 wfr1 
 |-  ( ( < We NN0 /\ < Se NN0 ) -> F Fn NN0 )
39 21 24 38 mp2an 
 |-  F Fn NN0
40 fz0ssnn0 
 |-  ( 0 ... ( N - 1 ) ) C_ NN0
41 fnssres 
 |-  ( ( F Fn NN0 /\ ( 0 ... ( N - 1 ) ) C_ NN0 ) -> ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) ) )
42 39 40 41 mp2an 
 |-  ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) )
43 42 fndmi 
 |-  dom ( F |` ( 0 ... ( N - 1 ) ) ) = ( 0 ... ( N - 1 ) )
44 37 43 eqtrdi 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> dom g = ( 0 ... ( N - 1 ) ) )
45 44 fveq2d 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> ( # ` dom g ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
46 fveq1 
 |-  ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> ( g ` k ) = ( ( F |` ( 0 ... ( N - 1 ) ) ) ` k ) )
47 fvres 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> ( ( F |` ( 0 ... ( N - 1 ) ) ) ` k ) = ( F ` k ) )
48 46 47 sylan9eq 
 |-  ( ( g = ( F |` ( 0 ... ( N - 1 ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( g ` k ) = ( F ` k ) )
49 48 oveq1d 
 |-  ( ( g = ( F |` ( 0 ... ( N - 1 ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( g ` k ) / ( ( n - k ) + 1 ) ) = ( ( F ` k ) / ( ( n - k ) + 1 ) ) )
50 49 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 ) ) ) )
51 44 50 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 ) ) ) )
52 51 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 ) ) ) ) )
53 45 52 csbeq12dv 
 |-  ( 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 ) ) ) ) )
54 ovex 
 |-  ( ( X ^ n ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) ) e. _V
55 54 csbex 
 |-  [_ ( # ` ( 0 ... ( N - 1 ) ) ) / n ]_ ( ( X ^ n ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) ) e. _V
56 53 1 55 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 ) ) ) ) )
57 36 56 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 ) ) ) )
58 nfcvd 
 |-  ( N e. NN0 -> F/_ n ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( F ` k ) / ( ( N - k ) + 1 ) ) ) ) )
59 oveq2 
 |-  ( n = N -> ( X ^ n ) = ( X ^ N ) )
60 oveq1 
 |-  ( n = N -> ( n _C k ) = ( N _C k ) )
61 oveq1 
 |-  ( n = N -> ( n - k ) = ( N - k ) )
62 61 oveq1d 
 |-  ( n = N -> ( ( n - k ) + 1 ) = ( ( N - k ) + 1 ) )
63 62 oveq2d 
 |-  ( n = N -> ( ( F ` k ) / ( ( n - k ) + 1 ) ) = ( ( F ` k ) / ( ( N - k ) + 1 ) ) )
64 60 63 oveq12d 
 |-  ( n = N -> ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) = ( ( N _C k ) x. ( ( F ` k ) / ( ( N - k ) + 1 ) ) ) )
65 64 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 ) ) ) )
66 59 65 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 ) ) ) ) )
67 58 66 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 ) ) ) ) )
68 67 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 ) ) ) ) )
69 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
70 fz01en 
 |-  ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
71 69 70 syl 
 |-  ( N e. NN0 -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
72 fzfi 
 |-  ( 0 ... ( N - 1 ) ) e. Fin
73 fzfi 
 |-  ( 1 ... N ) e. Fin
74 hashen 
 |-  ( ( ( 0 ... ( N - 1 ) ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) ) )
75 72 73 74 mp2an 
 |-  ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
76 71 75 sylibr 
 |-  ( N e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) )
77 hashfz1 
 |-  ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
78 76 77 eqtrd 
 |-  ( N e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = N )
79 78 adantr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> ( # ` ( 0 ... ( N - 1 ) ) ) = N )
80 79 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 ) ) ) ) )
81 elfznn0 
 |-  ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
82 simpr 
 |-  ( ( N e. NN0 /\ X e. CC ) -> X e. CC )
83 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
84 11 83 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 ) )
85 fvex 
 |-  ( F ` k ) e. _V
86 84 14 85 ovmpoa 
 |-  ( ( k e. NN0 /\ X e. CC ) -> ( k BernPoly X ) = ( F ` k ) )
87 81 82 86 syl2anr 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k BernPoly X ) = ( F ` k ) )
88 87 oveq1d 
 |-  ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) = ( ( F ` k ) / ( ( N - k ) + 1 ) ) )
89 88 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 ) ) ) )
90 89 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 ) ) ) )
91 90 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 ) ) ) ) )
92 68 80 91 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 ) ) ) ) )
93 57 92 eqtrid 
 |-  ( ( 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 ) ) ) ) )
94 31 93 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 ) ) ) ) )
95 16 27 94 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 ) ) ) ) )