Definition df-fwddifn 32268

Description: Define the nth forward difference operator. This works out to be the forward difference operator iterated n times. (Contributed by Scott Fenton, 28-May-2020.)

Assertion

Ref	Expression
df-fwddifn	|- _/_\^nn = ( n e. NN0 , f e. ( CC ^pm CC ) |-> ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) ) )

Distinct variable group:   f, n, x, y, k

Detailed syntax breakdown of Definition df-fwddifn

Step	Hyp	Ref	Expression
1		cfwddifn 32267	. 2 class _/_\^nn
2		vn	. . 3 setvar n
3		vf	. . 3 setvar f
4		cn0 11292	. . 3 class NN0
5		cc 9934	. . . 4 class CC
6		cpm 7858	. . . 4 class ^pm
7	5, 5, 6	co 6650	. . 3 class ( CC ^pm CC )
8		vx	. . . 4 setvar x
9		vy	. . . . . . . . 9 setvar y
10	9	cv 1482	. . . . . . . 8 class y
11		vk	. . . . . . . . 9 setvar k
12	11	cv 1482	. . . . . . . 8 class k
13		caddc 9939	. . . . . . . 8 class +
14	10, 12, 13	co 6650	. . . . . . 7 class ( y + k )
15	3	cv 1482	. . . . . . . 8 class f
16	15	cdm 5114	. . . . . . 7 class dom f
17	14, 16	wcel 1990	. . . . . 6 wff ( y + k ) e. dom f
18		cc0 9936	. . . . . . 7 class 0
19	2	cv 1482	. . . . . . 7 class n
20		cfz 12326	. . . . . . 7 class ...
21	18, 19, 20	co 6650	. . . . . 6 class ( 0 ... n )
22	17, 11, 21	wral 2912	. . . . 5 wff A. k e. ( 0 ... n ) ( y + k ) e. dom f
23	22, 9, 5	crab 2916	. . . 4 class { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f }
24		cbc 13089	. . . . . . 7 class _C
25	19, 12, 24	co 6650	. . . . . 6 class ( n _C k )
26		c1 9937	. . . . . . . . 9 class 1
27	26	cneg 10267	. . . . . . . 8 class -u 1
28		cmin 10266	. . . . . . . . 9 class -
29	19, 12, 28	co 6650	. . . . . . . 8 class ( n - k )
30		cexp 12860	. . . . . . . 8 class ^
31	27, 29, 30	co 6650	. . . . . . 7 class ( -u 1 ^ ( n - k ) )
32	8	cv 1482	. . . . . . . . 9 class x
33	32, 12, 13	co 6650	. . . . . . . 8 class ( x + k )
34	33, 15	cfv 5888	. . . . . . 7 class ( f ` ( x + k ) )
35		cmul 9941	. . . . . . 7 class x.
36	31, 34, 35	co 6650	. . . . . 6 class ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) )
37	25, 36, 35	co 6650	. . . . 5 class ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) )
38	21, 37, 11	csu 14416	. . . 4 class sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) )
39	8, 23, 38	cmpt 4729	. . 3 class ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) )
40	2, 3, 4, 7, 39	cmpt2 6652	. 2 class ( n e. NN0 , f e. ( CC ^pm CC ) |-> ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) ) )
41	1, 40	wceq 1483	1 wff _/_\^nn = ( n e. NN0 , f e. ( CC ^pm CC ) |-> ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) ) )

This definition is referenced by:  fwddifnval  32270