Definition df-fwddif 32266

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	|- _/_\ = ( f e. ( CC ^pm CC ) |-> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) )

Distinct variable group:   x, f, y

Detailed syntax breakdown of Definition df-fwddif

Step	Hyp	Ref	Expression
1		cfwddif 32265	. 2 class _/_\
2		vf	. . 3 setvar f
3		cc 9934	. . . 4 class CC
4		cpm 7858	. . . 4 class ^pm
5	3, 3, 4	co 6650	. . 3 class ( CC ^pm CC )
6		vx	. . . 4 setvar x
7		vy	. . . . . . . 8 setvar y
8	7	cv 1482	. . . . . . 7 class y
9		c1 9937	. . . . . . 7 class 1
10		caddc 9939	. . . . . . 7 class +
11	8, 9, 10	co 6650	. . . . . 6 class ( y + 1 )
12	2	cv 1482	. . . . . . 7 class f
13	12	cdm 5114	. . . . . 6 class dom f
14	11, 13	wcel 1990	. . . . 5 wff ( y + 1 ) e. dom f
15	14, 7, 13	crab 2916	. . . 4 class { y e. dom f | ( y + 1 ) e. dom f }
16	6	cv 1482	. . . . . . 7 class x
17	16, 9, 10	co 6650	. . . . . 6 class ( x + 1 )
18	17, 12	cfv 5888	. . . . 5 class ( f ` ( x + 1 ) )
19	16, 12	cfv 5888	. . . . 5 class ( f ` x )
20		cmin 10266	. . . . 5 class -
21	18, 19, 20	co 6650	. . . 4 class ( ( f ` ( x + 1 ) ) - ( f ` x ) )
22	6, 15, 21	cmpt 4729	. . 3 class ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) )
23	2, 5, 22	cmpt 4729	. 2 class ( f e. ( CC ^pm CC ) |-> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) )
24	1, 23	wceq 1483	1 wff _/_\ = ( f e. ( CC ^pm CC ) |-> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) )

This definition is referenced by:  fwddifval  32269