Theorem bpolylem 26006

Description: Lemma for bpolyval 26007. (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 = U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) }

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:   e, f, g, k, n, s, F   e, N, g, k, n   e, X, f, g, k, n, s   e, G, f, s

Allowed substitution hints:   G( g, k, n)   N( f, s)

Proof of Theorem bpolylem

Dummy variables m x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq1 6055	. . . . . . . . . . . . . . . . 17 |- ( x = X -> ( x ^ n ) = ( X ^ n ) )
2	1	oveq1d 6063	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) ) )
3	2	csbeq2dv 3244	. . . . . . . . . . . . . . 15 |- ( 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 ) ) ) ) )
4	3	mpteq2dv 4264	. . . . . . . . . . . . . 14 |- ( 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	. . . . . . . . . . . . . 14 |- G = ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( X ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) )
6	4, 5	syl6eqr 2462	. . . . . . . . . . . . 13 |- ( 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	6	fveq1d 5697	. . . . . . . . . . . 12 |- ( x = X -> ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) )
8	7	eqeq2d 2423	. . . . . . . . . . 11 |- ( x = X -> ( ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) <-> ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) )
9	8	ralbidv 2694	. . . . . . . . . 10 |- ( x = X -> ( A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) <-> A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) )
10	9	3anbi3d 1260	. . . . . . . . 9 |- ( x = X -> ( ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) <-> ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) ) )
11	10	exbidv 1633	. . . . . . . 8 |- ( x = X -> ( E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) <-> E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) ) )
12	11	abbidv 2526	. . . . . . 7 |- ( x = X -> { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } = { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) } )
13	12	unieqd 3994	. . . . . 6 |- ( x = X -> U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } = U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) } )
14		bpoly.2	. . . . . 6 |- F = U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) }
15	13, 14	syl6eqr 2462	. . . . 5 |- ( x = X -> U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } = F )
16	15	fveq1d 5697	. . . 4 |- ( x = X -> ( U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } ` m ) = ( F ` m ) )
17		fveq2 5695	. . . 4 |- ( m = N -> ( F ` m ) = ( F ` N ) )
18	16, 17	sylan9eqr 2466	. . 3 |- ( ( m = N /\ x = X ) -> ( U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } ` m ) = ( F ` N ) )
19		df-bpoly 26005	. . 3 |- BernPoly = ( m e. NN0 , x e. CC |-> ( U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } ` m ) )
20		fvex 5709	. . 3 |- ( F ` N ) e. _V
21	18, 19, 20	ovmpt2a 6171	. 2 |- ( ( N e. NN0 /\ X e. CC ) -> ( N BernPoly X ) = ( F ` N ) )
22		ltweuz 11264	. . . . 5 |- < We ( ZZ>= ` 0 )
23		nn0uz 10484	. . . . . 6 |- NN0 = ( ZZ>= ` 0 )
24		weeq2 4539	. . . . . 6 |- ( NN0 = ( ZZ>= ` 0 ) -> ( < We NN0 <-> < We ( ZZ>= ` 0 ) ) )
25	23, 24	ax-mp 8	. . . . 5 |- ( < We NN0 <-> < We ( ZZ>= ` 0 ) )
26	22, 25	mpbir 201	. . . 4 |- < We NN0
27		nn0ex 10191	. . . . 5 |- NN0 e. _V
28		exse 4514	. . . . 5 |- ( NN0 e. _V -> < Se NN0 )
29	27, 28	ax-mp 8	. . . 4 |- < Se NN0
30		eqid 2412	. . . 4 |- { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) } = { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( G ` ( f |` Pred ( < , NN0 , e ) ) ) ) }
31	26, 29, 30, 14	wfr2c 25496	. . 3 |- ( N e. NN0 -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
32	31	adantr 452	. 2 |- ( ( N e. NN0 /\ X e. CC ) -> ( F ` N ) = ( G ` ( F |` Pred ( < , NN0 , N ) ) ) )
33		prednn0 25424	. . . . . 6 |- ( N e. NN0 -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
34	33	adantr 452	. . . . 5 |- ( ( N e. NN0 /\ X e. CC ) -> Pred ( < , NN0 , N ) = ( 0 ... ( N - 1 ) ) )
35	34	reseq2d 5113	. . . 4 |- ( ( N e. NN0 /\ X e. CC ) -> ( F |` Pred ( < , NN0 , N ) ) = ( F |` ( 0 ... ( N - 1 ) ) ) )
36	35	fveq2d 5699	. . 3 |- ( ( N e. NN0 /\ X e. CC ) -> ( G ` ( F |` Pred ( < , NN0 , N ) ) ) = ( G ` ( F |` ( 0 ... ( N - 1 ) ) ) ) )
37	26, 29, 30, 14	wfr1 25494	. . . . . . 7 |- F Fn NN0
38		fnfun 5509	. . . . . . 7 |- ( F Fn NN0 -> Fun F )
39	37, 38	ax-mp 8	. . . . . 6 |- Fun F
40		ovex 6073	. . . . . 6 |- ( 0 ... ( N - 1 ) ) e. _V
41		resfunexg 5924	. . . . . 6 |- ( ( Fun F /\ ( 0 ... ( N - 1 ) ) e. _V ) -> ( F |` ( 0 ... ( N - 1 ) ) ) e. _V )
42	39, 40, 41	mp2an 654	. . . . 5 |- ( F |` ( 0 ... ( N - 1 ) ) ) e. _V
43		dmeq 5037	. . . . . . . . . . 11 |- ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> dom g = dom ( F |` ( 0 ... ( N - 1 ) ) ) )
44		elfznn0 11047	. . . . . . . . . . . . . 14 |- ( k e. ( 0 ... ( N - 1 ) ) -> k e. NN0 )
45	44	ssriv 3320	. . . . . . . . . . . . 13 |- ( 0 ... ( N - 1 ) ) C_ NN0
46		fnssres 5525	. . . . . . . . . . . . 13 |- ( ( F Fn NN0 /\ ( 0 ... ( N - 1 ) ) C_ NN0 ) -> ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) ) )
47	37, 45, 46	mp2an 654	. . . . . . . . . . . 12 |- ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) )
48		fndm 5511	. . . . . . . . . . . 12 |- ( ( F |` ( 0 ... ( N - 1 ) ) ) Fn ( 0 ... ( N - 1 ) ) -> dom ( F |` ( 0 ... ( N - 1 ) ) ) = ( 0 ... ( N - 1 ) ) )
49	47, 48	ax-mp 8	. . . . . . . . . . 11 |- dom ( F |` ( 0 ... ( N - 1 ) ) ) = ( 0 ... ( N - 1 ) )
50	43, 49	syl6eq 2460	. . . . . . . . . 10 |- ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> dom g = ( 0 ... ( N - 1 ) ) )
51		fveq1 5694	. . . . . . . . . . . . 13 |- ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> ( g ` k ) = ( ( F |` ( 0 ... ( N - 1 ) ) ) ` k ) )
52		fvres 5712	. . . . . . . . . . . . 13 |- ( k e. ( 0 ... ( N - 1 ) ) -> ( ( F |` ( 0 ... ( N - 1 ) ) ) ` k ) = ( F ` k ) )
53	51, 52	sylan9eq 2464	. . . . . . . . . . . 12 |- ( ( g = ( F |` ( 0 ... ( N - 1 ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( g ` k ) = ( F ` k ) )
54	53	oveq1d 6063	. . . . . . . . . . 11 |- ( ( g = ( F |` ( 0 ... ( N - 1 ) ) ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( g ` k ) / ( ( n - k ) + 1 ) ) = ( ( F ` k ) / ( ( n - k ) + 1 ) ) )
55	54	oveq2d 6064	. . . . . . . . . 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 ) ) ) )
56	50, 55	sumeq12rdv 12464	. . . . . . . . 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 ) ) ) )
57	56	oveq2d 6064	. . . . . . . 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 ) ) ) ) )
58	57	csbeq2dv 3244	. . . . . . 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 ) ) ) ) )
59	50	fveq2d 5699	. . . . . . . 8 |- ( g = ( F |` ( 0 ... ( N - 1 ) ) ) -> ( # ` dom g ) = ( # ` ( 0 ... ( N - 1 ) ) ) )
60	59	csbeq1d 3225	. . . . . . 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 ) ) ) ) )
61	58, 60	eqtrd 2444	. . . . . 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 ) ) ) ) )
62		fvex 5709	. . . . . . 7 |- ( # ` ( 0 ... ( N - 1 ) ) ) e. _V
63		ovex 6073	. . . . . . 7 |- ( ( X ^ n ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) ) e. _V
64	62, 63	csbex 3230	. . . . . 6 |- [_ ( # ` ( 0 ... ( N - 1 ) ) ) / n ]_ ( ( X ^ n ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) ) e. _V
65	61, 5, 64	fvmpt 5773	. . . . 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 ) ) ) ) )
66	42, 65	ax-mp 8	. . . 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 ) ) ) )
67		nfcvd 2549	. . . . . . 7 |- ( N e. NN0 -> F/_ n ( ( X ^ N ) - sum_ k e. ( 0 ... ( N - 1 ) ) ( ( N _C k ) x. ( ( F ` k ) / ( ( N - k ) + 1 ) ) ) ) )
68		oveq2 6056	. . . . . . . 8 |- ( n = N -> ( X ^ n ) = ( X ^ N ) )
69		oveq1 6055	. . . . . . . . . 10 |- ( n = N -> ( n _C k ) = ( N _C k ) )
70		oveq1 6055	. . . . . . . . . . . 12 |- ( n = N -> ( n - k ) = ( N - k ) )
71	70	oveq1d 6063	. . . . . . . . . . 11 |- ( n = N -> ( ( n - k ) + 1 ) = ( ( N - k ) + 1 ) )
72	71	oveq2d 6064	. . . . . . . . . 10 |- ( n = N -> ( ( F ` k ) / ( ( n - k ) + 1 ) ) = ( ( F ` k ) / ( ( N - k ) + 1 ) ) )
73	69, 72	oveq12d 6066	. . . . . . . . 9 |- ( n = N -> ( ( n _C k ) x. ( ( F ` k ) / ( ( n - k ) + 1 ) ) ) = ( ( N _C k ) x. ( ( F ` k ) / ( ( N - k ) + 1 ) ) ) )
74	73	sumeq2sdv 12461	. . . . . . . 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 ) ) ) )
75	68, 74	oveq12d 6066	. . . . . . 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 ) ) ) ) )
76	67, 75	csbiegf 3259	. . . . . 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 ) ) ) ) )
77	76	adantr 452	. . . . 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 ) ) ) ) )
78		nn0z 10268	. . . . . . . . . 10 |- ( N e. NN0 -> N e. ZZ )
79		fz01en 11043	. . . . . . . . . 10 |- ( N e. ZZ -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
80	78, 79	syl 16	. . . . . . . . 9 |- ( N e. NN0 -> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
81		fzfi 11274	. . . . . . . . . 10 |- ( 0 ... ( N - 1 ) ) e. Fin
82		fzfi 11274	. . . . . . . . . 10 |- ( 1 ... N ) e. Fin
83		hashen 11594	. . . . . . . . . 10 |- ( ( ( 0 ... ( N - 1 ) ) e. Fin /\ ( 1 ... N ) e. Fin ) -> ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) ) )
84	81, 82, 83	mp2an 654	. . . . . . . . 9 |- ( ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) <-> ( 0 ... ( N - 1 ) ) ~~ ( 1 ... N ) )
85	80, 84	sylibr 204	. . . . . . . 8 |- ( N e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = ( # ` ( 1 ... N ) ) )
86		hashfz1 11593	. . . . . . . 8 |- ( N e. NN0 -> ( # ` ( 1 ... N ) ) = N )
87	85, 86	eqtrd 2444	. . . . . . 7 |- ( N e. NN0 -> ( # ` ( 0 ... ( N - 1 ) ) ) = N )
88	87	adantr 452	. . . . . 6 |- ( ( N e. NN0 /\ X e. CC ) -> ( # ` ( 0 ... ( N - 1 ) ) ) = N )
89	88	csbeq1d 3225	. . . . 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 ) ) ) ) )
90		simpr 448	. . . . . . . . . 10 |- ( ( N e. NN0 /\ X e. CC ) -> X e. CC )
91		fveq2 5695	. . . . . . . . . . . 12 |- ( m = k -> ( F ` m ) = ( F ` k ) )
92	16, 91	sylan9eqr 2466	. . . . . . . . . . 11 |- ( ( m = k /\ x = X ) -> ( U. { f | E. s ( f Fn s /\ ( s C_ NN0 /\ A. e e. s Pred ( < , NN0 , e ) C_ s ) /\ A. e e. s ( f ` e ) = ( ( g e. _V |-> [_ ( # ` dom g ) / n ]_ ( ( x ^ n ) - sum_ k e. dom g ( ( n _C k ) x. ( ( g ` k ) / ( ( n - k ) + 1 ) ) ) ) ) ` ( f |` Pred ( < , NN0 , e ) ) ) ) } ` m ) = ( F ` k ) )
93		fvex 5709	. . . . . . . . . . 11 |- ( F ` k ) e. _V
94	92, 19, 93	ovmpt2a 6171	. . . . . . . . . 10 |- ( ( k e. NN0 /\ X e. CC ) -> ( k BernPoly X ) = ( F ` k ) )
95	44, 90, 94	syl2anr 465	. . . . . . . . 9 |- ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( k BernPoly X ) = ( F ` k ) )
96	95	oveq1d 6063	. . . . . . . 8 |- ( ( ( N e. NN0 /\ X e. CC ) /\ k e. ( 0 ... ( N - 1 ) ) ) -> ( ( k BernPoly X ) / ( ( N - k ) + 1 ) ) = ( ( F ` k ) / ( ( N - k ) + 1 ) ) )
97	96	oveq2d 6064	. . . . . . 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 ) ) ) )
98	97	sumeq2dv 12460	. . . . . 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 ) ) ) )
99	98	oveq2d 6064	. . . . 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 ) ) ) ) )
100	77, 89, 99	3eqtr4d 2454	. . . 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 ) ) ) ) )
101	66, 100	syl5eq 2456	. . 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 ) ) ) ) )
102	36, 101	eqtrd 2444	. 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 ) ) ) ) )
103	21, 32, 102	3eqtrd 2448	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 ) ) ) ) )

Syntax hints:   -> wi 4   <-> wb 177   /\ wa 359   /\ w3a 936   E.wex 1547   = wceq 1649   e. wcel 1721   {cab 2398   A.wral 2674   _Vcvv 2924   [_csb 3219   C_ wss 3288   U.cuni 3983   class class class wbr 4180   e. cmpt 4234   Se wse 4507   We wwe 4508   dom cdm 4845   |` cres 4847   Fun wfun 5415   Fn wfn 5416   ` cfv 5421  (class class class)co 6048   ~~ cen 7073   Fincfn 7076   CCcc 8952   0cc0 8954   1c1 8955   + caddc 8957   x. cmul 8959   < clt 9084   - cmin 9255   / cdiv 9641   NN0cn0 10185   ZZcz 10246   ZZ>=cuz 10452   ...cfz 11007   ^cexp 11345   _C cbc 11556   #chash 11581   sum_csu 12442   Predcpred 25389   BernPoly cbp 26004

This theorem is referenced by:  bpolyval  26007

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-rep 4288  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-inf2 7560  ax-cnex 9010  ax-resscn 9011  ax-1cn 9012  ax-icn 9013  ax-addcl 9014  ax-addrcl 9015  ax-mulcl 9016  ax-mulrcl 9017  ax-mulcom 9018  ax-addass 9019  ax-mulass 9020  ax-distr 9021  ax-i2m1 9022  ax-1ne0 9023  ax-1rid 9024  ax-rnegex 9025  ax-rrecex 9026  ax-cnre 9027  ax-pre-lttri 9028  ax-pre-lttrn 9029  ax-pre-ltadd 9030  ax-pre-mulgt0 9031

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-nel 2578  df-ral 2679  df-rex 2680  df-reu 2681  df-rmo 2682  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-int 4019  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-se 4510  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-isom 5430  df-ov 6051  df-oprab 6052  df-mpt2 6053  df-1st 6316  df-2nd 6317  df-riota 6516  df-recs 6600  df-rdg 6635  df-1o 6691  df-er 6872  df-en 7077  df-dom 7078  df-sdom 7079  df-fin 7080  df-card 7790  df-pnf 9086  df-mnf 9087  df-xr 9088  df-ltxr 9089  df-le 9090  df-sub 9257  df-neg 9258  df-nn 9965  df-n0 10186  df-z 10247  df-uz 10453  df-fz 11008  df-seq 11287  df-hash 11582  df-sum 12443  df-pred 25390  df-bpoly 26005