Definition df-fwddifn 37018

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

Assertion

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

Distinct variable group:   𝑓,𝑛,𝑥,𝑦,𝑘

Detailed syntax breakdown of Definition df-fwddifn

Step	Hyp	Ref	Expression
1		cfwddifn 37017	. 2 class △n
2		vn	. . 3 setvar 𝑛
3		vf	. . 3 setvar 𝑓
4		cn0 12609	. . 3 class ℕ0
5		cc 11201	. . . 4 class ℂ
6		cpm 8851	. . . 4 class ↑pm
7	5, 5, 6	co 7420	. . 3 class (ℂ ↑pm ℂ)
8		vx	. . . 4 setvar 𝑥
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1568	. . . . . . . 8 class 𝑦
11		vk	. . . . . . . . 9 setvar 𝑘
12	11	cv 1568	. . . . . . . 8 class 𝑘
13		caddc 11206	. . . . . . . 8 class +
14	10, 12, 13	co 7420	. . . . . . 7 class (𝑦 + 𝑘)
15	3	cv 1568	. . . . . . . 8 class 𝑓
16	15	cdm 5650	. . . . . . 7 class dom 𝑓
17	14, 16	wcel 2144	. . . . . 6 wff (𝑦 + 𝑘) ∈ dom 𝑓
18		cc0 11203	. . . . . . 7 class 0
19	2	cv 1568	. . . . . . 7 class 𝑛
20		cfz 13642	. . . . . . 7 class ...
21	18, 19, 20	co 7420	. . . . . 6 class (0...𝑛)
22	17, 11, 21	wral 3076	. . . . 5 wff ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓
23	22, 9, 5	crab 3412	. . . 4 class {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓}
24		cbc 14449	. . . . . . 7 class C
25	19, 12, 24	co 7420	. . . . . 6 class (𝑛C𝑘)
26		c1 11204	. . . . . . . . 9 class 1
27	26	cneg 11545	. . . . . . . 8 class -1
28		cmin 11544	. . . . . . . . 9 class −
29	19, 12, 28	co 7420	. . . . . . . 8 class (𝑛 − 𝑘)
30		cexp 14207	. . . . . . . 8 class ↑
31	27, 29, 30	co 7420	. . . . . . 7 class ( -1↑(𝑛 − 𝑘))
32	8	cv 1568	. . . . . . . . 9 class 𝑥
33	32, 12, 13	co 7420	. . . . . . . 8 class (𝑥 + 𝑘)
34	33, 15	cfv 6538	. . . . . . 7 class (𝑓‘(𝑥 + 𝑘))
35		cmul 11208	. . . . . . 7 class ·
36	31, 34, 35	co 7420	. . . . . 6 class (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))
37	25, 36, 35	co 7420	. . . . 5 class ((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))
38	21, 37, 11	csu 15858	. . . 4 class Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))
39	8, 23, 38	cmpt 5185	. . 3 class (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))
40	2, 3, 4, 7, 39	cmpo 7422	. 2 class (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))
41	1, 40	wceq 1569	1 wff △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · (( -1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))

This definition is used by:  fwddifnval  37020