Definition df-fwddif

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfwddif	⊢ △
1		vf	⊢ 𝑓
2		cc	⊢ ℂ
3		cpm	⊢ ↑pm
4	2 2 3	co	⊢ ( ℂ ↑pm ℂ )
5		vx	⊢ 𝑥
6		vy	⊢ 𝑦
7	1	cv	⊢ 𝑓
8	7	cdm	⊢ dom 𝑓
9	6	cv	⊢ 𝑦
10		caddc	⊢ +
11		c1	⊢ 1
12	9 11 10	co	⊢ ( 𝑦 + 1 )
13	12 8	wcel	⊢ ( 𝑦 + 1 ) ∈ dom 𝑓
14	13 6 8	crab	⊢ { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 }
15	5	cv	⊢ 𝑥
16	15 11 10	co	⊢ ( 𝑥 + 1 )
17	16 7	cfv	⊢ ( 𝑓 ‘ ( 𝑥 + 1 ) )
18		cmin	⊢ −
19	15 7	cfv	⊢ ( 𝑓 ‘ 𝑥 )
20	17 19 18	co	⊢ ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) )
21	5 14 20	cmpt	⊢ ( 𝑥 ∈ { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 } ↦ ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) ) )
22	1 4 21	cmpt	⊢ ( 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 } ↦ ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) ) ) )
23	0 22	wceq	⊢ △ = ( 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ dom 𝑓 ∣ ( 𝑦 + 1 ) ∈ dom 𝑓 } ↦ ( ( 𝑓 ‘ ( 𝑥 + 1 ) ) − ( 𝑓 ‘ 𝑥 ) ) ) )