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 \in (ℂ ↑_{𝑝𝑚} ℂ) ⟼ (x \in \{y \in dom f \| y + 1 \in 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 \in dom f$
14	13 6 8	crab	$class \{y \in dom f \| y + 1 \in 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 \in \{y \in dom f \| y + 1 \in dom f\} ⟼ f (x + 1) - f (x))$
22	1 4 21	cmpt	$class (f \in (ℂ ↑_{𝑝𝑚} ℂ) ⟼ (x \in \{y \in dom f \| y + 1 \in dom f\} ⟼ f (x + 1) - f (x)))$
23	0 22	wceq	$wff △ = (f \in (ℂ ↑_{𝑝𝑚} ℂ) ⟼ (x \in \{y \in dom f \| y + 1 \in dom f\} ⟼ f (x + 1) - f (x)))$

Metamath Proof Explorer

Definition df-fwddif

Detailed syntax breakdown