Definition df-fwddif 34388

Description: Define the forward difference operator. This is a discrete analogue of the derivative operator. Definition 2.42 of [GramKnuthPat], p. 47. (Contributed by Scott Fenton, 18-May-2020.)

Assertion

Ref	Expression
df-fwddif	⊢ △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))

Distinct variable group:   𝑥,𝑓,𝑦

Detailed syntax breakdown of Definition df-fwddif

Step	Hyp	Ref	Expression
1		cfwddif 34387	. 2 class △
2		vf	. . 3 setvar 𝑓
3		cc 10800	. . . 4 class ℂ
4		cpm 8574	. . . 4 class ↑pm
5	3, 3, 4	co 7255	. . 3 class (ℂ ↑pm ℂ)
6		vx	. . . 4 setvar 𝑥
7		vy	. . . . . . . 8 setvar 𝑦
8	7	cv 1538	. . . . . . 7 class 𝑦
9		c1 10803	. . . . . . 7 class 1
10		caddc 10805	. . . . . . 7 class +
11	8, 9, 10	co 7255	. . . . . 6 class (𝑦 + 1)
12	2	cv 1538	. . . . . . 7 class 𝑓
13	12	cdm 5580	. . . . . 6 class dom 𝑓
14	11, 13	wcel 2108	. . . . 5 wff (𝑦 + 1) ∈ dom 𝑓
15	14, 7, 13	crab 3067	. . . 4 class {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓}
16	6	cv 1538	. . . . . . 7 class 𝑥
17	16, 9, 10	co 7255	. . . . . 6 class (𝑥 + 1)
18	17, 12	cfv 6418	. . . . 5 class (𝑓‘(𝑥 + 1))
19	16, 12	cfv 6418	. . . . 5 class (𝑓‘𝑥)
20		cmin 11135	. . . . 5 class −
21	18, 19, 20	co 7255	. . . 4 class ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))
22	6, 15, 21	cmpt 5153	. . 3 class (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥)))
23	2, 5, 22	cmpt 5153	. 2 class (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))
24	1, 23	wceq 1539	1 wff △ = (𝑓 ∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ dom 𝑓 ∣ (𝑦 + 1) ∈ dom 𝑓} ↦ ((𝑓‘(𝑥 + 1)) − (𝑓‘𝑥))))

This definition is referenced by:  fwddifval  34391