fwddifnval

Description: The value of the forward difference operator at a point. (Contributed by Scott Fenton, 28-May-2020)

	Ref	Expression
Hypotheses	fwddifnval.1	$⊢ φ \to N \in ℕ_{0}$
	fwddifnval.2	$⊢ φ \to A \subseteq ℂ$
	fwddifnval.3	$⊢ φ \to F : A ⟶ ℂ$
	fwddifnval.4	$⊢ φ \to X \in ℂ$
	fwddifnval.5	$⊢ (φ \land k \in (0 \dots N)) \to X + k \in A$
Assertion	fwddifnval	$⊢ φ \to (N △^{n} F) (X) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$

Proof

Step	Hyp	Ref	Expression
1		fwddifnval.1	$⊢ φ \to N \in ℕ_{0}$
2		fwddifnval.2	$⊢ φ \to A \subseteq ℂ$
3		fwddifnval.3	$⊢ φ \to F : A ⟶ ℂ$
4		fwddifnval.4	$⊢ φ \to X \in ℂ$
5		fwddifnval.5	$⊢ (φ \land k \in (0 \dots N)) \to X + k \in A$
6		df-fwddifn	$⊢ △^{n} = (n \in ℕ_{0}, f \in (ℂ ↑_{𝑝𝑚} ℂ) ⟼ (x \in \{y \in ℂ \| \forall k \in (0 \dots n) y + k \in dom f\} ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) {(- 1)}^{n - k} f (x + k)))$
7	6	a1i	$⊢ φ \to △^{n} = (n \in ℕ_{0}, f \in (ℂ ↑_{𝑝𝑚} ℂ) ⟼ (x \in \{y \in ℂ \| \forall k \in (0 \dots n) y + k \in dom f\} ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) {(- 1)}^{n - k} f (x + k)))$
8		oveq2	$⊢ n = N \to (0 \dots n) = (0 \dots N)$
9	8	adantr	$⊢ (n = N \land f = F) \to (0 \dots n) = (0 \dots N)$
10		dmeq	$⊢ f = F \to dom f = dom F$
11	10	eleq2d	$⊢ f = F \to (y + k \in dom f \leftrightarrow y + k \in dom F)$
12	11	adantl	$⊢ (n = N \land f = F) \to (y + k \in dom f \leftrightarrow y + k \in dom F)$
13	9 12	raleqbidv	$⊢ (n = N \land f = F) \to (\forall k \in (0 \dots n) y + k \in dom f \leftrightarrow \forall k \in (0 \dots N) y + k \in dom F)$
14	13	rabbidv	$⊢ (n = N \land f = F) \to \{y \in ℂ \| \forall k \in (0 \dots n) y + k \in dom f\} = \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\}$
15		oveq1	$⊢ n = N \to (\binom{n}{k}) = (\binom{N}{k})$
16	15	adantr	$⊢ (n = N \land f = F) \to (\binom{n}{k}) = (\binom{N}{k})$
17		oveq1	$⊢ n = N \to n - k = N - k$
18	17	oveq2d	$⊢ n = N \to {(- 1)}^{n - k} = {(- 1)}^{N - k}$
19		fveq1	$⊢ f = F \to f (x + k) = F (x + k)$
20	18 19	oveqan12d	$⊢ (n = N \land f = F) \to {(- 1)}^{n - k} f (x + k) = {(- 1)}^{N - k} F (x + k)$
21	16 20	oveq12d	$⊢ (n = N \land f = F) \to (\binom{n}{k}) {(- 1)}^{n - k} f (x + k) = (\binom{N}{k}) {(- 1)}^{N - k} F (x + k)$
22	21	adantr	$⊢ ((n = N \land f = F) \land k \in (0 \dots n)) \to (\binom{n}{k}) {(- 1)}^{n - k} f (x + k) = (\binom{N}{k}) {(- 1)}^{N - k} F (x + k)$
23	9 22	sumeq12dv	$⊢ (n = N \land f = F) \to \sum_{k = 0}^{n} (\binom{n}{k}) {(- 1)}^{n - k} f (x + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k)$
24	14 23	mpteq12dv	$⊢ (n = N \land f = F) \to (x \in \{y \in ℂ \| \forall k \in (0 \dots n) y + k \in dom f\} ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) {(- 1)}^{n - k} f (x + k)) = (x \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\} ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k))$
25	24	adantl	$⊢ (φ \land (n = N \land f = F)) \to (x \in \{y \in ℂ \| \forall k \in (0 \dots n) y + k \in dom f\} ⟼ \sum_{k = 0}^{n} (\binom{n}{k}) {(- 1)}^{n - k} f (x + k)) = (x \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\} ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k))$
26		cnex	$⊢ ℂ \in V$
27		elpm2r	$⊢ ((ℂ \in V \land ℂ \in V) \land (F : A ⟶ ℂ \land A \subseteq ℂ)) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
28	26 26 27	mpanl12	$⊢ (F : A ⟶ ℂ \land A \subseteq ℂ) \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
29	3 2 28	syl2anc	$⊢ φ \to F \in (ℂ ↑_{𝑝𝑚} ℂ)$
30	26	mptrabex	$⊢ (x \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\} ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k)) \in V$
31	30	a1i	$⊢ φ \to (x \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\} ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k)) \in V$
32	7 25 1 29 31	ovmpod	$⊢ φ \to N △^{n} F = (x \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\} ⟼ \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k))$
33		fvoveq1	$⊢ x = X \to F (x + k) = F (X + k)$
34	33	oveq2d	$⊢ x = X \to {(- 1)}^{N - k} F (x + k) = {(- 1)}^{N - k} F (X + k)$
35	34	oveq2d	$⊢ x = X \to (\binom{N}{k}) {(- 1)}^{N - k} F (x + k) = (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
36	35	sumeq2sdv	$⊢ x = X \to \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
37	36	adantl	$⊢ (φ \land x = X) \to \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (x + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
38	3	fdmd	$⊢ φ \to dom F = A$
39	38	adantr	$⊢ (φ \land k \in (0 \dots N)) \to dom F = A$
40	5 39	eleqtrrd	$⊢ (φ \land k \in (0 \dots N)) \to X + k \in dom F$
41	40	ralrimiva	$⊢ φ \to \forall k \in (0 \dots N) X + k \in dom F$
42		oveq1	$⊢ y = X \to y + k = X + k$
43	42	eleq1d	$⊢ y = X \to (y + k \in dom F \leftrightarrow X + k \in dom F)$
44	43	ralbidv	$⊢ y = X \to (\forall k \in (0 \dots N) y + k \in dom F \leftrightarrow \forall k \in (0 \dots N) X + k \in dom F)$
45	44	elrab	$⊢ X \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\} \leftrightarrow (X \in ℂ \land \forall k \in (0 \dots N) X + k \in dom F)$
46	4 41 45	sylanbrc	$⊢ φ \to X \in \{y \in ℂ \| \forall k \in (0 \dots N) y + k \in dom F\}$
47		sumex	$⊢ \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) \in V$
48	47	a1i	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) \in V$
49	32 37 46 48	fvmptd	$⊢ φ \to (N △^{n} F) (X) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$

Metamath Proof Explorer

Theorem fwddifnval

Proof