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