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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cfwddif	|- _/_\
1		vf	|- f
2		cc	|- CC
3		cpm	|- ^pm
4	2 2 3	co	|- ( CC ^pm CC )
5		vx	|- x
6		vy	|- y
7	1	cv	|- f
8	7	cdm	|- dom f
9	6	cv	|- y
10		caddc	|- +
11		c1	|- 1
12	9 11 10	co	|- ( y + 1 )
13	12 8	wcel	|- ( y + 1 ) e. dom f
14	13 6 8	crab	|- { y e. dom f | ( y + 1 ) e. dom f }
15	5	cv	|- x
16	15 11 10	co	|- ( x + 1 )
17	16 7	cfv	|- ( f ` ( x + 1 ) )
18		cmin	|- -
19	15 7	cfv	|- ( f ` x )
20	17 19 18	co	|- ( ( f ` ( x + 1 ) ) - ( f ` x ) )
21	5 14 20	cmpt	|- ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) )
22	1 4 21	cmpt	|- ( f e. ( CC ^pm CC ) |-> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) )
23	0 22	wceq	|- _/_\ = ( f e. ( CC ^pm CC ) |-> ( x e. { y e. dom f | ( y + 1 ) e. dom f } |-> ( ( f ` ( x + 1 ) ) - ( f ` x ) ) ) )