fwddifn0

Description: The value of the n-iterated forward difference operator at zero is just the function value. (Contributed by Scott Fenton, 28-May-2020)

	Ref	Expression
Hypotheses	fwddifn0.1	$⊢ φ \to A \subseteq ℂ$
	fwddifn0.2	$⊢ φ \to F : A ⟶ ℂ$
	fwddifn0.3	$⊢ φ \to X \in A$
Assertion	fwddifn0	$⊢ φ \to (0 △^{n} F) (X) = F (X)$

Proof

Step	Hyp	Ref	Expression
1		fwddifn0.1	$⊢ φ \to A \subseteq ℂ$
2		fwddifn0.2	$⊢ φ \to F : A ⟶ ℂ$
3		fwddifn0.3	$⊢ φ \to X \in A$
4		0nn0	$⊢ 0 \in ℕ_{0}$
5	4	a1i	$⊢ φ \to 0 \in ℕ_{0}$
6	1 3	sseldd	$⊢ φ \to X \in ℂ$
7		0z	$⊢ 0 \in ℤ$
8		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
9	7 8	ax-mp	$⊢ (0 \dots 0) = \{0\}$
10	9	eleq2i	$⊢ k \in (0 \dots 0) \leftrightarrow k \in \{0\}$
11		velsn	$⊢ k \in \{0\} \leftrightarrow k = 0$
12	10 11	bitri	$⊢ k \in (0 \dots 0) \leftrightarrow k = 0$
13		oveq2	$⊢ k = 0 \to X + k = X + 0$
14	13	adantl	$⊢ (φ \land k = 0) \to X + k = X + 0$
15	6	addid1d	$⊢ φ \to X + 0 = X$
16	15 3	eqeltrd	$⊢ φ \to X + 0 \in A$
17	16	adantr	$⊢ (φ \land k = 0) \to X + 0 \in A$
18	14 17	eqeltrd	$⊢ (φ \land k = 0) \to X + k \in A$
19	12 18	sylan2b	$⊢ (φ \land k \in (0 \dots 0)) \to X + k \in A$
20	5 1 2 6 19	fwddifnval	$⊢ φ \to (0 △^{n} F) (X) = \sum_{k = 0}^{0} (\binom{0}{k}) {(- 1)}^{0 - k} F (X + k)$
21	15	fveq2d	$⊢ φ \to F (X + 0) = F (X)$
22	21	oveq2d	$⊢ φ \to 1 F (X + 0) = 1 F (X)$
23	2 3	ffvelrnd	$⊢ φ \to F (X) \in ℂ$
24	23	mulid2d	$⊢ φ \to 1 F (X) = F (X)$
25	22 24	eqtrd	$⊢ φ \to 1 F (X + 0) = F (X)$
26	25	oveq2d	$⊢ φ \to 1 1 F (X + 0) = 1 F (X)$
27	26 24	eqtrd	$⊢ φ \to 1 1 F (X + 0) = F (X)$
28	27 23	eqeltrd	$⊢ φ \to 1 1 F (X + 0) \in ℂ$
29		oveq2	$⊢ k = 0 \to (\binom{0}{k}) = (\binom{0}{0})$
30		bcnn	$⊢ 0 \in ℕ_{0} \to (\binom{0}{0}) = 1$
31	4 30	ax-mp	$⊢ (\binom{0}{0}) = 1$
32	29 31	eqtrdi	$⊢ k = 0 \to (\binom{0}{k}) = 1$
33		oveq2	$⊢ k = 0 \to 0 - k = 0 - 0$
34		0m0e0	$⊢ 0 - 0 = 0$
35	33 34	eqtrdi	$⊢ k = 0 \to 0 - k = 0$
36	35	oveq2d	$⊢ k = 0 \to {(- 1)}^{0 - k} = {(- 1)}^{0}$
37		neg1cn	$⊢ - 1 \in ℂ$
38		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
39	37 38	ax-mp	$⊢ {(- 1)}^{0} = 1$
40	36 39	eqtrdi	$⊢ k = 0 \to {(- 1)}^{0 - k} = 1$
41	13	fveq2d	$⊢ k = 0 \to F (X + k) = F (X + 0)$
42	40 41	oveq12d	$⊢ k = 0 \to {(- 1)}^{0 - k} F (X + k) = 1 F (X + 0)$
43	32 42	oveq12d	$⊢ k = 0 \to (\binom{0}{k}) {(- 1)}^{0 - k} F (X + k) = 1 1 F (X + 0)$
44	43	fsum1	$⊢ (0 \in ℤ \land 1 1 F (X + 0) \in ℂ) \to \sum_{k = 0}^{0} (\binom{0}{k}) {(- 1)}^{0 - k} F (X + k) = 1 1 F (X + 0)$
45	7 28 44	sylancr	$⊢ φ \to \sum_{k = 0}^{0} (\binom{0}{k}) {(- 1)}^{0 - k} F (X + k) = 1 1 F (X + 0)$
46	45 27	eqtrd	$⊢ φ \to \sum_{k = 0}^{0} (\binom{0}{k}) {(- 1)}^{0 - k} F (X + k) = F (X)$
47	20 46	eqtrd	$⊢ φ \to (0 △^{n} F) (X) = F (X)$

Metamath Proof Explorer

Theorem fwddifn0

Proof