Theorem fwddifnp1

Description: The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020)

	Ref	Expression
Hypotheses	fwddifnp1.1	|- ( ph -> N e. NN0 )
	fwddifnp1.2	|- ( ph -> A C_ CC )
	fwddifnp1.3	|- ( ph -> F : A --> CC )
	fwddifnp1.4	|- ( ph -> X e. CC )
	fwddifnp1.5	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( X + k ) e. A )
Assertion	fwddifnp1	|- ( ph -> ( ( ( N + 1 ) _/_\^n F ) ` X ) = ( ( ( N _/_\^n F ) ` ( X + 1 ) ) - ( ( N _/_\^n F ) ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		fwddifnp1.1	|- ( ph -> N e. NN0 )
2		fwddifnp1.2	|- ( ph -> A C_ CC )
3		fwddifnp1.3	|- ( ph -> F : A --> CC )
4		fwddifnp1.4	|- ( ph -> X e. CC )
5		fwddifnp1.5	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( X + k ) e. A )
6		elfzelz	|- ( k e. ( 0 ... ( N + 1 ) ) -> k e. ZZ )
7		bcpasc	|- ( ( N e. NN0 /\ k e. ZZ ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
8	1 6 7	syl2an	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N + 1 ) _C k ) )
9	8	oveq1d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N + 1 ) _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) )
10		bccl	|- ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
11	1 6 10	syl2an	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. NN0 )
12	11	nn0cnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C k ) e. CC )
13		peano2zm	|- ( k e. ZZ -> ( k - 1 ) e. ZZ )
14	6 13	syl	|- ( k e. ( 0 ... ( N + 1 ) ) -> ( k - 1 ) e. ZZ )
15		bccl	|- ( ( N e. NN0 /\ ( k - 1 ) e. ZZ ) -> ( N _C ( k - 1 ) ) e. NN0 )
16	1 14 15	syl2an	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. NN0 )
17	16	nn0cnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N _C ( k - 1 ) ) e. CC )
18	12 17	addcomd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) + ( N _C ( k - 1 ) ) ) = ( ( N _C ( k - 1 ) ) + ( N _C k ) ) )
19	18	oveq1d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N _C ( k - 1 ) ) + ( N _C k ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) )
20		peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )
21	1 20	syl	|- ( ph -> ( N + 1 ) e. NN0 )
22	21	nn0zd	|- ( ph -> ( N + 1 ) e. ZZ )
23		zsubcl	|- ( ( ( N + 1 ) e. ZZ /\ k e. ZZ ) -> ( ( N + 1 ) - k ) e. ZZ )
24	22 6 23	syl2an	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) e. ZZ )
25		m1expcl	|- ( ( ( N + 1 ) - k ) e. ZZ -> ( -u 1 ^ ( ( N + 1 ) - k ) ) e. ZZ )
26	24 25	syl	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N + 1 ) - k ) ) e. ZZ )
27	26	zcnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N + 1 ) - k ) ) e. CC )
28	3	adantr	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> F : A --> CC )
29	28 5	ffvelrnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( F ` ( X + k ) ) e. CC )
30	27 29	mulcld	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) e. CC )
31	17 12 30	adddird	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) + ( N _C k ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) + ( ( N _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
32	19 31	eqtrd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) + ( ( N _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
33	1	adantr	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> N e. NN0 )
34	33	nn0cnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> N e. CC )
35	6	adantl	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. ZZ )
36	35	zcnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> k e. CC )
37		1cnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> 1 e. CC )
38	34 36 37	subsub3d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N - ( k - 1 ) ) = ( ( N + 1 ) - k ) )
39	38	eqcomd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) = ( N - ( k - 1 ) ) )
40	39	oveq2d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N + 1 ) - k ) ) = ( -u 1 ^ ( N - ( k - 1 ) ) ) )
41	40	oveq1d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) = ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) )
42	41	oveq2d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) )
43	34 37 36	addsubd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N + 1 ) - k ) = ( ( N - k ) + 1 ) )
44	43	oveq2d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N + 1 ) - k ) ) = ( -u 1 ^ ( ( N - k ) + 1 ) ) )
45		neg1cn	|- -u 1 e. CC
46	45	a1i	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> -u 1 e. CC )
47		neg1ne0	|- -u 1 =/= 0
48	47	a1i	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> -u 1 =/= 0 )
49	1	nn0zd	|- ( ph -> N e. ZZ )
50		zsubcl	|- ( ( N e. ZZ /\ k e. ZZ ) -> ( N - k ) e. ZZ )
51	49 6 50	syl2an	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N - k ) e. ZZ )
52	46 48 51	expp1zd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N - k ) + 1 ) ) = ( ( -u 1 ^ ( N - k ) ) x. -u 1 ) )
53	44 52	eqtrd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N + 1 ) - k ) ) = ( ( -u 1 ^ ( N - k ) ) x. -u 1 ) )
54		m1expcl	|- ( ( N - k ) e. ZZ -> ( -u 1 ^ ( N - k ) ) e. ZZ )
55	51 54	syl	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( N - k ) ) e. ZZ )
56	55	zcnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( N - k ) ) e. CC )
57	56 46	mulcomd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( N - k ) ) x. -u 1 ) = ( -u 1 x. ( -u 1 ^ ( N - k ) ) ) )
58	56	mulm1d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 x. ( -u 1 ^ ( N - k ) ) ) = -u ( -u 1 ^ ( N - k ) ) )
59	53 57 58	3eqtrd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( ( N + 1 ) - k ) ) = -u ( -u 1 ^ ( N - k ) ) )
60	59	oveq1d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) = ( -u ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) )
61	56 29	mulneg1d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) = -u ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) )
62	60 61	eqtrd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) = -u ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) )
63	62	oveq2d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( N _C k ) x. -u ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
64	56 29	mulcld	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) e. CC )
65	12 64	mulneg2d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) x. -u ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) = -u ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
66	63 65	eqtrd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = -u ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
67	42 66	oveq12d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) + ( ( N _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) + -u ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
68		zsubcl	|- ( ( N e. ZZ /\ ( k - 1 ) e. ZZ ) -> ( N - ( k - 1 ) ) e. ZZ )
69	49 14 68	syl2an	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( N - ( k - 1 ) ) e. ZZ )
70		m1expcl	|- ( ( N - ( k - 1 ) ) e. ZZ -> ( -u 1 ^ ( N - ( k - 1 ) ) ) e. ZZ )
71	69 70	syl	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( N - ( k - 1 ) ) ) e. ZZ )
72	71	zcnd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( -u 1 ^ ( N - ( k - 1 ) ) ) e. CC )
73	72 29	mulcld	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) e. CC )
74	17 73	mulcld	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) e. CC )
75	12 64	mulcld	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) e. CC )
76	74 75	negsubd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) + -u ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
77	32 67 76	3eqtrd	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N _C k ) + ( N _C ( k - 1 ) ) ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
78	9 77	eqtr3d	|- ( ( ph /\ k e. ( 0 ... ( N + 1 ) ) ) -> ( ( ( N + 1 ) _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
79	78	sumeq2dv	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
80		fzfid	|- ( ph -> ( 0 ... ( N + 1 ) ) e. Fin )
81	80 74 75	fsumsub	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) = ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
82		nn0uz	|- NN0 = ( ZZ>= ` 0 )
83	21 82	eleqtrdi	|- ( ph -> ( N + 1 ) e. ( ZZ>= ` 0 ) )
84		oveq1	|- ( k = 0 -> ( k - 1 ) = ( 0 - 1 ) )
85	84	oveq2d	|- ( k = 0 -> ( N _C ( k - 1 ) ) = ( N _C ( 0 - 1 ) ) )
86	84	oveq2d	|- ( k = 0 -> ( N - ( k - 1 ) ) = ( N - ( 0 - 1 ) ) )
87	86	oveq2d	|- ( k = 0 -> ( -u 1 ^ ( N - ( k - 1 ) ) ) = ( -u 1 ^ ( N - ( 0 - 1 ) ) ) )
88		oveq2	|- ( k = 0 -> ( X + k ) = ( X + 0 ) )
89	88	fveq2d	|- ( k = 0 -> ( F ` ( X + k ) ) = ( F ` ( X + 0 ) ) )
90	87 89	oveq12d	|- ( k = 0 -> ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) = ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) )
91	85 90	oveq12d	|- ( k = 0 -> ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) = ( ( N _C ( 0 - 1 ) ) x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) )
92	83 74 91	fsum1p	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) = ( ( ( N _C ( 0 - 1 ) ) x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) ) )
93		df-neg	|- -u 1 = ( 0 - 1 )
94	93	oveq2i	|- ( N _C -u 1 ) = ( N _C ( 0 - 1 ) )
95		bcneg1	|- ( N e. NN0 -> ( N _C -u 1 ) = 0 )
96	1 95	syl	|- ( ph -> ( N _C -u 1 ) = 0 )
97	94 96	eqtr3id	|- ( ph -> ( N _C ( 0 - 1 ) ) = 0 )
98	97	oveq1d	|- ( ph -> ( ( N _C ( 0 - 1 ) ) x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) = ( 0 x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) )
99		0z	|- 0 e. ZZ
100		1z	|- 1 e. ZZ
101		zsubcl	|- ( ( 0 e. ZZ /\ 1 e. ZZ ) -> ( 0 - 1 ) e. ZZ )
102	99 100 101	mp2an	|- ( 0 - 1 ) e. ZZ
103	102	a1i	|- ( ph -> ( 0 - 1 ) e. ZZ )
104	49 103	zsubcld	|- ( ph -> ( N - ( 0 - 1 ) ) e. ZZ )
105		m1expcl	|- ( ( N - ( 0 - 1 ) ) e. ZZ -> ( -u 1 ^ ( N - ( 0 - 1 ) ) ) e. ZZ )
106	104 105	syl	|- ( ph -> ( -u 1 ^ ( N - ( 0 - 1 ) ) ) e. ZZ )
107	106	zcnd	|- ( ph -> ( -u 1 ^ ( N - ( 0 - 1 ) ) ) e. CC )
108		eluzfz1	|- ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> 0 e. ( 0 ... ( N + 1 ) ) )
109	83 108	syl	|- ( ph -> 0 e. ( 0 ... ( N + 1 ) ) )
110	5	ralrimiva	|- ( ph -> A. k e. ( 0 ... ( N + 1 ) ) ( X + k ) e. A )
111	88	eleq1d	|- ( k = 0 -> ( ( X + k ) e. A <-> ( X + 0 ) e. A ) )
112	111	rspcva	|- ( ( 0 e. ( 0 ... ( N + 1 ) ) /\ A. k e. ( 0 ... ( N + 1 ) ) ( X + k ) e. A ) -> ( X + 0 ) e. A )
113	109 110 112	syl2anc	|- ( ph -> ( X + 0 ) e. A )
114	3 113	ffvelrnd	|- ( ph -> ( F ` ( X + 0 ) ) e. CC )
115	107 114	mulcld	|- ( ph -> ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) e. CC )
116	115	mul02d	|- ( ph -> ( 0 x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) = 0 )
117	98 116	eqtrd	|- ( ph -> ( ( N _C ( 0 - 1 ) ) x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) = 0 )
118	117	oveq1d	|- ( ph -> ( ( ( N _C ( 0 - 1 ) ) x. ( ( -u 1 ^ ( N - ( 0 - 1 ) ) ) x. ( F ` ( X + 0 ) ) ) ) + sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) ) = ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) ) )
119		fzfid	|- ( ph -> ( ( 0 + 1 ) ... ( N + 1 ) ) e. Fin )
120		olc	|- ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> ( k = 0 \/ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) )
121		elfzp12	|- ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( k e. ( 0 ... ( N + 1 ) ) <-> ( k = 0 \/ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) )
122	83 121	syl	|- ( ph -> ( k e. ( 0 ... ( N + 1 ) ) <-> ( k = 0 \/ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) )
123	122	biimpar	|- ( ( ph /\ ( k = 0 \/ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) ) -> k e. ( 0 ... ( N + 1 ) ) )
124	120 123	sylan2	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. ( 0 ... ( N + 1 ) ) )
125	124 74	syldan	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) e. CC )
126	119 125	fsumcl	|- ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) e. CC )
127	126	addid2d	|- ( ph -> ( 0 + sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) )
128	92 118 127	3eqtrd	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) )
129	4	adantr	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> X e. CC )
130		1cnd	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> 1 e. CC )
131		elfzelz	|- ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> k e. ZZ )
132	131	zcnd	|- ( k e. ( ( 0 + 1 ) ... ( N + 1 ) ) -> k e. CC )
133	132	adantl	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> k e. CC )
134	129 130 133	ppncand	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( X + 1 ) + ( k - 1 ) ) = ( X + k ) )
135	134	fveq2d	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) = ( F ` ( X + k ) ) )
136	135	oveq2d	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) = ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) )
137	136	oveq2d	|- ( ( ph /\ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ) -> ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) )
138	137	sumeq2dv	|- ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) )
139		1zzd	|- ( ph -> 1 e. ZZ )
140		0zd	|- ( ph -> 0 e. ZZ )
141		elfzelz	|- ( j e. ( 0 ... N ) -> j e. ZZ )
142		bccl	|- ( ( N e. NN0 /\ j e. ZZ ) -> ( N _C j ) e. NN0 )
143	142	nn0cnd	|- ( ( N e. NN0 /\ j e. ZZ ) -> ( N _C j ) e. CC )
144	1 141 143	syl2an	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( N _C j ) e. CC )
145		zsubcl	|- ( ( N e. ZZ /\ j e. ZZ ) -> ( N - j ) e. ZZ )
146	49 141 145	syl2an	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( N - j ) e. ZZ )
147		m1expcl	|- ( ( N - j ) e. ZZ -> ( -u 1 ^ ( N - j ) ) e. ZZ )
148	146 147	syl	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( -u 1 ^ ( N - j ) ) e. ZZ )
149	148	zcnd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( -u 1 ^ ( N - j ) ) e. CC )
150	3	adantr	|- ( ( ph /\ j e. ( 0 ... N ) ) -> F : A --> CC )
151	4	adantr	|- ( ( ph /\ j e. ( 0 ... N ) ) -> X e. CC )
152		1cnd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> 1 e. CC )
153	141	zcnd	|- ( j e. ( 0 ... N ) -> j e. CC )
154	153	adantl	|- ( ( ph /\ j e. ( 0 ... N ) ) -> j e. CC )
155	151 152 154	addassd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( X + 1 ) + j ) = ( X + ( 1 + j ) ) )
156	152 154	addcomd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( 1 + j ) = ( j + 1 ) )
157	156	oveq2d	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( X + ( 1 + j ) ) = ( X + ( j + 1 ) ) )
158	155 157	eqtrd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( X + 1 ) + j ) = ( X + ( j + 1 ) ) )
159		fzp1elp1	|- ( j e. ( 0 ... N ) -> ( j + 1 ) e. ( 0 ... ( N + 1 ) ) )
160		oveq2	|- ( k = ( j + 1 ) -> ( X + k ) = ( X + ( j + 1 ) ) )
161	160	eleq1d	|- ( k = ( j + 1 ) -> ( ( X + k ) e. A <-> ( X + ( j + 1 ) ) e. A ) )
162	161	rspccv	|- ( A. k e. ( 0 ... ( N + 1 ) ) ( X + k ) e. A -> ( ( j + 1 ) e. ( 0 ... ( N + 1 ) ) -> ( X + ( j + 1 ) ) e. A ) )
163	110 162	syl	|- ( ph -> ( ( j + 1 ) e. ( 0 ... ( N + 1 ) ) -> ( X + ( j + 1 ) ) e. A ) )
164	163	imp	|- ( ( ph /\ ( j + 1 ) e. ( 0 ... ( N + 1 ) ) ) -> ( X + ( j + 1 ) ) e. A )
165	159 164	sylan2	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( X + ( j + 1 ) ) e. A )
166	158 165	eqeltrd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( X + 1 ) + j ) e. A )
167	150 166	ffvelrnd	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( F ` ( ( X + 1 ) + j ) ) e. CC )
168	149 167	mulcld	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) e. CC )
169	144 168	mulcld	|- ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( N _C j ) x. ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) ) e. CC )
170		oveq2	|- ( j = ( k - 1 ) -> ( N _C j ) = ( N _C ( k - 1 ) ) )
171		oveq2	|- ( j = ( k - 1 ) -> ( N - j ) = ( N - ( k - 1 ) ) )
172	171	oveq2d	|- ( j = ( k - 1 ) -> ( -u 1 ^ ( N - j ) ) = ( -u 1 ^ ( N - ( k - 1 ) ) ) )
173		oveq2	|- ( j = ( k - 1 ) -> ( ( X + 1 ) + j ) = ( ( X + 1 ) + ( k - 1 ) ) )
174	173	fveq2d	|- ( j = ( k - 1 ) -> ( F ` ( ( X + 1 ) + j ) ) = ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) )
175	172 174	oveq12d	|- ( j = ( k - 1 ) -> ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) = ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) )
176	170 175	oveq12d	|- ( j = ( k - 1 ) -> ( ( N _C j ) x. ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) ) = ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) ) )
177	139 140 49 169 176	fsumshft	|- ( ph -> sum_ j e. ( 0 ... N ) ( ( N _C j ) x. ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) ) = sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) ) )
178		oveq2	|- ( j = k -> ( N _C j ) = ( N _C k ) )
179		oveq2	|- ( j = k -> ( N - j ) = ( N - k ) )
180	179	oveq2d	|- ( j = k -> ( -u 1 ^ ( N - j ) ) = ( -u 1 ^ ( N - k ) ) )
181		oveq2	|- ( j = k -> ( ( X + 1 ) + j ) = ( ( X + 1 ) + k ) )
182	181	fveq2d	|- ( j = k -> ( F ` ( ( X + 1 ) + j ) ) = ( F ` ( ( X + 1 ) + k ) ) )
183	180 182	oveq12d	|- ( j = k -> ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) = ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) )
184	178 183	oveq12d	|- ( j = k -> ( ( N _C j ) x. ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) ) = ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) )
185	184	cbvsumv	|- sum_ j e. ( 0 ... N ) ( ( N _C j ) x. ( ( -u 1 ^ ( N - j ) ) x. ( F ` ( ( X + 1 ) + j ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) )
186	177 185	eqtr3di	|- ( ph -> sum_ k e. ( ( 0 + 1 ) ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( ( X + 1 ) + ( k - 1 ) ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) )
187	128 138 186	3eqtr2d	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) )
188	1 82	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 0 ) )
189		oveq2	|- ( k = ( N + 1 ) -> ( N _C k ) = ( N _C ( N + 1 ) ) )
190		oveq2	|- ( k = ( N + 1 ) -> ( N - k ) = ( N - ( N + 1 ) ) )
191	190	oveq2d	|- ( k = ( N + 1 ) -> ( -u 1 ^ ( N - k ) ) = ( -u 1 ^ ( N - ( N + 1 ) ) ) )
192		oveq2	|- ( k = ( N + 1 ) -> ( X + k ) = ( X + ( N + 1 ) ) )
193	192	fveq2d	|- ( k = ( N + 1 ) -> ( F ` ( X + k ) ) = ( F ` ( X + ( N + 1 ) ) ) )
194	191 193	oveq12d	|- ( k = ( N + 1 ) -> ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) = ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) )
195	189 194	oveq12d	|- ( k = ( N + 1 ) -> ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) = ( ( N _C ( N + 1 ) ) x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) )
196	188 75 195	fsump1	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) + ( ( N _C ( N + 1 ) ) x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) ) )
197		bcval	|- ( ( N e. NN0 /\ ( N + 1 ) e. ZZ ) -> ( N _C ( N + 1 ) ) = if ( ( N + 1 ) e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) ) , 0 ) )
198	1 22 197	syl2anc	|- ( ph -> ( N _C ( N + 1 ) ) = if ( ( N + 1 ) e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) ) , 0 ) )
199		fzp1nel	|- -. ( N + 1 ) e. ( 0 ... N )
200	199	iffalsei	|- if ( ( N + 1 ) e. ( 0 ... N ) , ( ( ! ` N ) / ( ( ! ` ( N - ( N + 1 ) ) ) x. ( ! ` ( N + 1 ) ) ) ) , 0 ) = 0
201	198 200	eqtrdi	|- ( ph -> ( N _C ( N + 1 ) ) = 0 )
202	201	oveq1d	|- ( ph -> ( ( N _C ( N + 1 ) ) x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) = ( 0 x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) )
203	49 22	zsubcld	|- ( ph -> ( N - ( N + 1 ) ) e. ZZ )
204		m1expcl	|- ( ( N - ( N + 1 ) ) e. ZZ -> ( -u 1 ^ ( N - ( N + 1 ) ) ) e. ZZ )
205	204	zcnd	|- ( ( N - ( N + 1 ) ) e. ZZ -> ( -u 1 ^ ( N - ( N + 1 ) ) ) e. CC )
206	203 205	syl	|- ( ph -> ( -u 1 ^ ( N - ( N + 1 ) ) ) e. CC )
207		eluzfz2	|- ( ( N + 1 ) e. ( ZZ>= ` 0 ) -> ( N + 1 ) e. ( 0 ... ( N + 1 ) ) )
208	83 207	syl	|- ( ph -> ( N + 1 ) e. ( 0 ... ( N + 1 ) ) )
209	192	eleq1d	|- ( k = ( N + 1 ) -> ( ( X + k ) e. A <-> ( X + ( N + 1 ) ) e. A ) )
210	209	rspcv	|- ( ( N + 1 ) e. ( 0 ... ( N + 1 ) ) -> ( A. k e. ( 0 ... ( N + 1 ) ) ( X + k ) e. A -> ( X + ( N + 1 ) ) e. A ) )
211	208 110 210	sylc	|- ( ph -> ( X + ( N + 1 ) ) e. A )
212	3 211	ffvelrnd	|- ( ph -> ( F ` ( X + ( N + 1 ) ) ) e. CC )
213	206 212	mulcld	|- ( ph -> ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) e. CC )
214	213	mul02d	|- ( ph -> ( 0 x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) = 0 )
215	202 214	eqtrd	|- ( ph -> ( ( N _C ( N + 1 ) ) x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) = 0 )
216	215	oveq2d	|- ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) + ( ( N _C ( N + 1 ) ) x. ( ( -u 1 ^ ( N - ( N + 1 ) ) ) x. ( F ` ( X + ( N + 1 ) ) ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) + 0 ) )
217		fzfid	|- ( ph -> ( 0 ... N ) e. Fin )
218		fzelp1	|- ( k e. ( 0 ... N ) -> k e. ( 0 ... ( N + 1 ) ) )
219	218 75	sylan2	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) e. CC )
220	217 219	fsumcl	|- ( ph -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) e. CC )
221	220	addid1d	|- ( ph -> ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) + 0 ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
222	196 216 221	3eqtrd	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
223	187 222	oveq12d	|- ( ph -> ( sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C ( k - 1 ) ) x. ( ( -u 1 ^ ( N - ( k - 1 ) ) ) x. ( F ` ( X + k ) ) ) ) - sum_ k e. ( 0 ... ( N + 1 ) ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) - sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
224	79 81 223	3eqtrd	|- ( ph -> sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) - sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
225	21 2 3 4 5	fwddifnval	|- ( ph -> ( ( ( N + 1 ) _/_\^n F ) ` X ) = sum_ k e. ( 0 ... ( N + 1 ) ) ( ( ( N + 1 ) _C k ) x. ( ( -u 1 ^ ( ( N + 1 ) - k ) ) x. ( F ` ( X + k ) ) ) ) )
226		peano2cn	|- ( X e. CC -> ( X + 1 ) e. CC )
227	4 226	syl	|- ( ph -> ( X + 1 ) e. CC )
228	4	adantr	|- ( ( ph /\ k e. ( 0 ... N ) ) -> X e. CC )
229		1cnd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> 1 e. CC )
230		elfzelz	|- ( k e. ( 0 ... N ) -> k e. ZZ )
231	230	zcnd	|- ( k e. ( 0 ... N ) -> k e. CC )
232	231	adantl	|- ( ( ph /\ k e. ( 0 ... N ) ) -> k e. CC )
233	228 229 232	addassd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( X + 1 ) + k ) = ( X + ( 1 + k ) ) )
234	229 232	addcomd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( 1 + k ) = ( k + 1 ) )
235	234	oveq2d	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( X + ( 1 + k ) ) = ( X + ( k + 1 ) ) )
236	233 235	eqtrd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( X + 1 ) + k ) = ( X + ( k + 1 ) ) )
237		fzp1elp1	|- ( k e. ( 0 ... N ) -> ( k + 1 ) e. ( 0 ... ( N + 1 ) ) )
238		oveq1	|- ( j = k -> ( j + 1 ) = ( k + 1 ) )
239	238	eleq1d	|- ( j = k -> ( ( j + 1 ) e. ( 0 ... ( N + 1 ) ) <-> ( k + 1 ) e. ( 0 ... ( N + 1 ) ) ) )
240	239	anbi2d	|- ( j = k -> ( ( ph /\ ( j + 1 ) e. ( 0 ... ( N + 1 ) ) ) <-> ( ph /\ ( k + 1 ) e. ( 0 ... ( N + 1 ) ) ) ) )
241	238	oveq2d	|- ( j = k -> ( X + ( j + 1 ) ) = ( X + ( k + 1 ) ) )
242	241	eleq1d	|- ( j = k -> ( ( X + ( j + 1 ) ) e. A <-> ( X + ( k + 1 ) ) e. A ) )
243	240 242	imbi12d	|- ( j = k -> ( ( ( ph /\ ( j + 1 ) e. ( 0 ... ( N + 1 ) ) ) -> ( X + ( j + 1 ) ) e. A ) <-> ( ( ph /\ ( k + 1 ) e. ( 0 ... ( N + 1 ) ) ) -> ( X + ( k + 1 ) ) e. A ) ) )
244	243 164	chvarvv	|- ( ( ph /\ ( k + 1 ) e. ( 0 ... ( N + 1 ) ) ) -> ( X + ( k + 1 ) ) e. A )
245	237 244	sylan2	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( X + ( k + 1 ) ) e. A )
246	236 245	eqeltrd	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( ( X + 1 ) + k ) e. A )
247	1 2 3 227 246	fwddifnval	|- ( ph -> ( ( N _/_\^n F ) ` ( X + 1 ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) )
248	218 5	sylan2	|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( X + k ) e. A )
249	1 2 3 4 248	fwddifnval	|- ( ph -> ( ( N _/_\^n F ) ` X ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
250	247 249	oveq12d	|- ( ph -> ( ( ( N _/_\^n F ) ` ( X + 1 ) ) - ( ( N _/_\^n F ) ` X ) ) = ( sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( ( X + 1 ) + k ) ) ) ) - sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) ) )
251	224 225 250	3eqtr4d	|- ( ph -> ( ( ( N + 1 ) _/_\^n F ) ` X ) = ( ( ( N _/_\^n F ) ` ( X + 1 ) ) - ( ( N _/_\^n F ) ` X ) ) )