Metamath Proof Explorer


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 𝑝𝑚 x y dom f | y + 1 dom f f x + 1 f x

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfwddif class
1 vf setvar f
2 cc class
3 cpm class 𝑝𝑚
4 2 2 3 co class 𝑝𝑚
5 vx setvar x
6 vy setvar y
7 1 cv setvar f
8 7 cdm class dom f
9 6 cv setvar y
10 caddc class +
11 c1 class 1
12 9 11 10 co class y + 1
13 12 8 wcel wff y + 1 dom f
14 13 6 8 crab class y dom f | y + 1 dom f
15 5 cv setvar x
16 15 11 10 co class x + 1
17 16 7 cfv class f x + 1
18 cmin class
19 15 7 cfv class f x
20 17 19 18 co class f x + 1 f x
21 5 14 20 cmpt class x y dom f | y + 1 dom f f x + 1 f x
22 1 4 21 cmpt class f 𝑝𝑚 x y dom f | y + 1 dom f f x + 1 f x
23 0 22 wceq wff = f 𝑝𝑚 x y dom f | y + 1 dom f f x + 1 f x