Definition df-fwddifn

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)

	Ref	Expression
Assertion	df-fwddifn	⊢ △n = ( 𝑛 ∈ ℕ0 , 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfwddifn	⊢ △n
1		vn	⊢ 𝑛
2		cn0	⊢ ℕ0
3		vf	⊢ 𝑓
4		cc	⊢ ℂ
5		cpm	⊢ ↑pm
6	4 4 5	co	⊢ ( ℂ ↑pm ℂ )
7		vx	⊢ 𝑥
8		vy	⊢ 𝑦
9		vk	⊢ 𝑘
10		cc0	⊢ 0
11		cfz	⊢ ...
12	1	cv	⊢ 𝑛
13	10 12 11	co	⊢ ( 0 ... 𝑛 )
14	8	cv	⊢ 𝑦
15		caddc	⊢ +
16	9	cv	⊢ 𝑘
17	14 16 15	co	⊢ ( 𝑦 + 𝑘 )
18	3	cv	⊢ 𝑓
19	18	cdm	⊢ dom 𝑓
20	17 19	wcel	⊢ ( 𝑦 + 𝑘 ) ∈ dom 𝑓
21	20 9 13	wral	⊢ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓
22	21 8 4	crab	⊢ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 }
23		cbc	⊢ C
24	12 16 23	co	⊢ ( 𝑛 C 𝑘 )
25		cmul	⊢ ·
26		c1	⊢ 1
27	26	cneg	⊢ - 1
28		cexp	⊢ ↑
29		cmin	⊢ −
30	12 16 29	co	⊢ ( 𝑛 − 𝑘 )
31	27 30 28	co	⊢ ( - 1 ↑ ( 𝑛 − 𝑘 ) )
32	7	cv	⊢ 𝑥
33	32 16 15	co	⊢ ( 𝑥 + 𝑘 )
34	33 18	cfv	⊢ ( 𝑓 ‘ ( 𝑥 + 𝑘 ) )
35	31 34 25	co	⊢ ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) )
36	24 35 25	co	⊢ ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) )
37	13 36 9	csu	⊢ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) )
38	7 22 37	cmpt	⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) )
39	1 3 2 6 38	cmpo	⊢ ( 𝑛 ∈ ℕ0 , 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )
40	0 39	wceq	⊢ △n = ( 𝑛 ∈ ℕ0 , 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )