Definition df-fwddifn 31438

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 31437	. 2 class △n
2		vn	. . 3 setvar 𝑛
3		vf	. . 3 setvar 𝑓
4		cn0 11169	. . 3 class ℕ0
5		cc 9813	. . . 4 class ℂ
6		cpm 7745	. . . 4 class ↑pm
7	5, 5, 6	co 6549	. . 3 class (ℂ ↑pm ℂ)
8		vx	. . . 4 setvar 𝑥
9		vy	. . . . . . . . 9 setvar 𝑦
10	9	cv 1474	. . . . . . . 8 class 𝑦
11		vk	. . . . . . . . 9 setvar 𝑘
12	11	cv 1474	. . . . . . . 8 class 𝑘
13		caddc 9818	. . . . . . . 8 class +
14	10, 12, 13	co 6549	. . . . . . 7 class (𝑦 + 𝑘)
15	3	cv 1474	. . . . . . . 8 class 𝑓
16	15	cdm 5038	. . . . . . 7 class dom 𝑓
17	14, 16	wcel 1977	. . . . . 6 wff (𝑦 + 𝑘) ∈ dom 𝑓
18		cc0 9815	. . . . . . 7 class 0
19	2	cv 1474	. . . . . . 7 class 𝑛
20		cfz 12197	. . . . . . 7 class ...
21	18, 19, 20	co 6549	. . . . . 6 class (0...𝑛)
22	17, 11, 21	wral 2896	. . . . 5 wff ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓
23	22, 9, 5	crab 2900	. . . 4 class {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓}
24		cbc 12951	. . . . . . 7 class C
25	19, 12, 24	co 6549	. . . . . 6 class (𝑛C𝑘)
26		c1 9816	. . . . . . . . 9 class 1
27	26	cneg 10146	. . . . . . . 8 class -1
28		cmin 10145	. . . . . . . . 9 class −
29	19, 12, 28	co 6549	. . . . . . . 8 class (𝑛 − 𝑘)
30		cexp 12722	. . . . . . . 8 class ↑
31	27, 29, 30	co 6549	. . . . . . 7 class (-1↑(𝑛 − 𝑘))
32	8	cv 1474	. . . . . . . . 9 class 𝑥
33	32, 12, 13	co 6549	. . . . . . . 8 class (𝑥 + 𝑘)
34	33, 15	cfv 5804	. . . . . . 7 class (𝑓‘(𝑥 + 𝑘))
35		cmul 9820	. . . . . . 7 class ·
36	31, 34, 35	co 6549	. . . . . 6 class ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))
37	25, 36, 35	co 6549	. . . . 5 class ((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))
38	21, 37, 11	csu 14264	. . . 4 class Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))
39	8, 23, 38	cmpt 4643	. . 3 class (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))
40	2, 3, 4, 7, 39	cmpt2 6551	. 2 class (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))
41	1, 40	wceq 1475	1 wff △n = (𝑛 ∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))

This definition is referenced by:  fwddifnval  31440