Definition df-fwddifn 36163

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 36162	. 2 class △n
2		vn	. . 3 setvar 𝑛
3		vf	. . 3 setvar 𝑓
4		cn0 12528	. . 3 class ℕ0
5		cc 11154	. . . 4 class ℂ
6		cpm 8868	. . . 4 class ↑pm
7	5, 5, 6	co 7432	. . 3 class (ℂ ↑pm ℂ)
8		vx	. . . 4 setvar 𝑥
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1538	. . . . . . . 8 class 𝑦
11		vk	. . . . . . . . 9 setvar 𝑘
12	11	cv 1538	. . . . . . . 8 class 𝑘
13		caddc 11159	. . . . . . . 8 class +
14	10, 12, 13	co 7432	. . . . . . 7 class (𝑦 + 𝑘)
15	3	cv 1538	. . . . . . . 8 class 𝑓
16	15	cdm 5684	. . . . . . 7 class dom 𝑓
17	14, 16	wcel 2107	. . . . . 6 wff (𝑦 + 𝑘) ∈ dom 𝑓
18		cc0 11156	. . . . . . 7 class 0
19	2	cv 1538	. . . . . . 7 class 𝑛
20		cfz 13548	. . . . . . 7 class ...
21	18, 19, 20	co 7432	. . . . . 6 class (0...𝑛)
22	17, 11, 21	wral 3060	. . . . 5 wff ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓
23	22, 9, 5	crab 3435	. . . 4 class {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓}
24		cbc 14342	. . . . . . 7 class C
25	19, 12, 24	co 7432	. . . . . 6 class (𝑛C𝑘)
26		c1 11157	. . . . . . . . 9 class 1
27	26	cneg 11494	. . . . . . . 8 class -1
28		cmin 11493	. . . . . . . . 9 class −
29	19, 12, 28	co 7432	. . . . . . . 8 class (𝑛 − 𝑘)
30		cexp 14103	. . . . . . . 8 class ↑
31	27, 29, 30	co 7432	. . . . . . 7 class (-1↑(𝑛 − 𝑘))
32	8	cv 1538	. . . . . . . . 9 class 𝑥
33	32, 12, 13	co 7432	. . . . . . . 8 class (𝑥 + 𝑘)
34	33, 15	cfv 6560	. . . . . . 7 class (𝑓‘(𝑥 + 𝑘))
35		cmul 11161	. . . . . . 7 class ·
36	31, 34, 35	co 7432	. . . . . 6 class ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))
37	25, 36, 35	co 7432	. . . . 5 class ((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))
38	21, 37, 11	csu 15723	. . . 4 class Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))
39	8, 23, 38	cmpt 5224	. . 3 class (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))
40	2, 3, 4, 7, 39	cmpo 7434	. 2 class (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))
41	1, 40	wceq 1539	1 wff △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))

This definition is referenced by:  fwddifnval  36165