fwddifnp1

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

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

Proof

Step	Hyp	Ref	Expression
1		fwddifnp1.1	$⊢ φ \to N \in ℕ_{0}$
2		fwddifnp1.2	$⊢ φ \to A \subseteq ℂ$
3		fwddifnp1.3	$⊢ φ \to F : A ⟶ ℂ$
4		fwddifnp1.4	$⊢ φ \to X \in ℂ$
5		fwddifnp1.5	$⊢ (φ \land k \in (0 \dots N + 1)) \to X + k \in A$
6		elfzelz	$⊢ k \in (0 \dots N + 1) \to k \in ℤ$
7		bcpasc	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
8	1 6 7	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N + 1}{k})$
9	8	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N + 1}{k}) {(- 1)}^{N + 1 - k} F (X + k)$
10		bccl	$⊢ (N \in ℕ_{0} \land k \in ℤ) \to (\binom{N}{k}) \in ℕ_{0}$
11	1 6 10	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℕ_{0}$
12	11	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) \in ℂ$
13		peano2zm	$⊢ k \in ℤ \to k - 1 \in ℤ$
14	6 13	syl	$⊢ k \in (0 \dots N + 1) \to k - 1 \in ℤ$
15		bccl	$⊢ (N \in ℕ_{0} \land k - 1 \in ℤ) \to (\binom{N}{k - 1}) \in ℕ_{0}$
16	1 14 15	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℕ_{0}$
17	16	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) \in ℂ$
18	12 17	addcomd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) + (\binom{N}{k - 1}) = (\binom{N}{k - 1}) + (\binom{N}{k})$
19	18	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) {(- 1)}^{N + 1 - k} F (X + k) = ((\binom{N}{k - 1}) + (\binom{N}{k})) {(- 1)}^{N + 1 - k} F (X + k)$
20		peano2nn0	$⊢ N \in ℕ_{0} \to N + 1 \in ℕ_{0}$
21	1 20	syl	$⊢ φ \to N + 1 \in ℕ_{0}$
22	21	nn0zd	$⊢ φ \to N + 1 \in ℤ$
23		zsubcl	$⊢ (N + 1 \in ℤ \land k \in ℤ) \to N + 1 - k \in ℤ$
24	22 6 23	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k \in ℤ$
25		m1expcl	$⊢ N + 1 - k \in ℤ \to {(- 1)}^{N + 1 - k} \in ℤ$
26	24 25	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} \in ℤ$
27	26	zcnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} \in ℂ$
28	3	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to F : A ⟶ ℂ$
29	28 5	ffvelcdmd	$⊢ (φ \land k \in (0 \dots N + 1)) \to F (X + k) \in ℂ$
30	27 29	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} F (X + k) \in ℂ$
31	17 12 30	adddird	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k - 1}) + (\binom{N}{k})) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k - 1}) {(- 1)}^{N + 1 - k} F (X + k) + (\binom{N}{k}) {(- 1)}^{N + 1 - k} F (X + k)$
32	19 31	eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k - 1}) {(- 1)}^{N + 1 - k} F (X + k) + (\binom{N}{k}) {(- 1)}^{N + 1 - k} F (X + k)$
33	1	adantr	$⊢ (φ \land k \in (0 \dots N + 1)) \to N \in ℕ_{0}$
34	33	nn0cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to N \in ℂ$
35	6	adantl	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℤ$
36	35	zcnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to k \in ℂ$
37		1cnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to 1 \in ℂ$
38	34 36 37	subsub3d	$⊢ (φ \land k \in (0 \dots N + 1)) \to N - (k - 1) = N + 1 - k$
39	38	eqcomd	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k = N - (k - 1)$
40	39	oveq2d	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} = {(- 1)}^{N - (k - 1)}$
41	40	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} F (X + k) = {(- 1)}^{N - (k - 1)} F (X + k)$
42	41	oveq2d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
43	34 37 36	addsubd	$⊢ (φ \land k \in (0 \dots N + 1)) \to N + 1 - k = N - k + 1$
44	43	oveq2d	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} = {(- 1)}^{N - k + 1}$
45		neg1cn	$⊢ - 1 \in ℂ$
46	45	a1i	$⊢ (φ \land k \in (0 \dots N + 1)) \to - 1 \in ℂ$
47		neg1ne0	$⊢ - 1 \neq 0$
48	47	a1i	$⊢ (φ \land k \in (0 \dots N + 1)) \to - 1 \neq 0$
49	1	nn0zd	$⊢ φ \to N \in ℤ$
50		zsubcl	$⊢ (N \in ℤ \land k \in ℤ) \to N - k \in ℤ$
51	49 6 50	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to N - k \in ℤ$
52	46 48 51	expp1zd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - k + 1} = {(- 1)}^{N - k} -1$
53	44 52	eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} = {(- 1)}^{N - k} -1$
54		m1expcl	$⊢ N - k \in ℤ \to {(- 1)}^{N - k} \in ℤ$
55	51 54	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - k} \in ℤ$
56	55	zcnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - k} \in ℂ$
57	56 46	mulcomd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - k} -1 = -1 {(- 1)}^{N - k}$
58	56	mulm1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to -1 {(- 1)}^{N - k} = - {(- 1)}^{N - k}$
59	53 57 58	3eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} = - {(- 1)}^{N - k}$
60	59	oveq1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} F (X + k) = (- {(- 1)}^{N - k}) F (X + k)$
61	56 29	mulneg1d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (- {(- 1)}^{N - k}) F (X + k) = - {(- 1)}^{N - k} F (X + k)$
62	60 61	eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N + 1 - k} F (X + k) = - {(- 1)}^{N - k} F (X + k)$
63	62	oveq2d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k}) (- {(- 1)}^{N - k} F (X + k))$
64	56 29	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - k} F (X + k) \in ℂ$
65	12 64	mulneg2d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) (- {(- 1)}^{N - k} F (X + k)) = - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
66	63 65	eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) {(- 1)}^{N + 1 - k} F (X + k) = - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
67	42 66	oveq12d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) {(- 1)}^{N + 1 - k} F (X + k) + (\binom{N}{k}) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) + (- (\binom{N}{k}) {(- 1)}^{N - k} F (X + k))$
68		zsubcl	$⊢ (N \in ℤ \land k - 1 \in ℤ) \to N - (k - 1) \in ℤ$
69	49 14 68	syl2an	$⊢ (φ \land k \in (0 \dots N + 1)) \to N - (k - 1) \in ℤ$
70		m1expcl	$⊢ N - (k - 1) \in ℤ \to {(- 1)}^{N - (k - 1)} \in ℤ$
71	69 70	syl	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - (k - 1)} \in ℤ$
72	71	zcnd	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - (k - 1)} \in ℂ$
73	72 29	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to {(- 1)}^{N - (k - 1)} F (X + k) \in ℂ$
74	17 73	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) \in ℂ$
75	12 64	mulcld	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) \in ℂ$
76	74 75	negsubd	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) + (- (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
77	32 67 76	3eqtrd	$⊢ (φ \land k \in (0 \dots N + 1)) \to ((\binom{N}{k}) + (\binom{N}{k - 1})) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
78	9 77	eqtr3d	$⊢ (φ \land k \in (0 \dots N + 1)) \to (\binom{N + 1}{k}) {(- 1)}^{N + 1 - k} F (X + k) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
79	78	sumeq2dv	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) {(- 1)}^{N + 1 - k} F (X + k) = \sum_{k = 0}^{N + 1} ((\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k))$
80		fzfid	$⊢ φ \to (0 \dots N + 1) \in Fin$
81	80 74 75	fsumsub	$⊢ φ \to \sum_{k = 0}^{N + 1} ((\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)) = \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - \sum_{k = 0}^{N + 1} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
82		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
83	21 82	eleqtrdi	$⊢ φ \to N + 1 \in ℤ_{\geq 0}$
84		oveq1	$⊢ k = 0 \to k - 1 = 0 - 1$
85	84	oveq2d	$⊢ k = 0 \to (\binom{N}{k - 1}) = (\binom{N}{0 - 1})$
86	84	oveq2d	$⊢ k = 0 \to N - (k - 1) = N - (0 - 1)$
87	86	oveq2d	$⊢ k = 0 \to {(- 1)}^{N - (k - 1)} = {(- 1)}^{N - (0 - 1)}$
88		oveq2	$⊢ k = 0 \to X + k = X + 0$
89	88	fveq2d	$⊢ k = 0 \to F (X + k) = F (X + 0)$
90	87 89	oveq12d	$⊢ k = 0 \to {(- 1)}^{N - (k - 1)} F (X + k) = {(- 1)}^{N - (0 - 1)} F (X + 0)$
91	85 90	oveq12d	$⊢ k = 0 \to (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) = (\binom{N}{0 - 1}) {(- 1)}^{N - (0 - 1)} F (X + 0)$
92	83 74 91	fsum1p	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) = (\binom{N}{0 - 1}) {(- 1)}^{N - (0 - 1)} F (X + 0) + \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
93		df-neg	$⊢ - 1 = 0 - 1$
94	93	oveq2i	$⊢ (\binom{N}{- 1}) = (\binom{N}{0 - 1})$
95		bcneg1	$⊢ N \in ℕ_{0} \to (\binom{N}{- 1}) = 0$
96	1 95	syl	$⊢ φ \to (\binom{N}{- 1}) = 0$
97	94 96	eqtr3id	$⊢ φ \to (\binom{N}{0 - 1}) = 0$
98	97	oveq1d	$⊢ φ \to (\binom{N}{0 - 1}) {(- 1)}^{N - (0 - 1)} F (X + 0) = 0 \cdot {(- 1)}^{N - (0 - 1)} F (X + 0)$
99		0z	$⊢ 0 \in ℤ$
100		1z	$⊢ 1 \in ℤ$
101		zsubcl	$⊢ (0 \in ℤ \land 1 \in ℤ) \to 0 - 1 \in ℤ$
102	99 100 101	mp2an	$⊢ 0 - 1 \in ℤ$
103	102	a1i	$⊢ φ \to 0 - 1 \in ℤ$
104	49 103	zsubcld	$⊢ φ \to N - (0 - 1) \in ℤ$
105		m1expcl	$⊢ N - (0 - 1) \in ℤ \to {(- 1)}^{N - (0 - 1)} \in ℤ$
106	104 105	syl	$⊢ φ \to {(- 1)}^{N - (0 - 1)} \in ℤ$
107	106	zcnd	$⊢ φ \to {(- 1)}^{N - (0 - 1)} \in ℂ$
108		eluzfz1	$⊢ N + 1 \in ℤ_{\geq 0} \to 0 \in (0 \dots N + 1)$
109	83 108	syl	$⊢ φ \to 0 \in (0 \dots N + 1)$
110	5	ralrimiva	$⊢ φ \to \forall k \in (0 \dots N + 1) X + k \in A$
111	88	eleq1d	$⊢ k = 0 \to (X + k \in A \leftrightarrow X + 0 \in A)$
112	111	rspcva	$⊢ (0 \in (0 \dots N + 1) \land \forall k \in (0 \dots N + 1) X + k \in A) \to X + 0 \in A$
113	109 110 112	syl2anc	$⊢ φ \to X + 0 \in A$
114	3 113	ffvelcdmd	$⊢ φ \to F (X + 0) \in ℂ$
115	107 114	mulcld	$⊢ φ \to {(- 1)}^{N - (0 - 1)} F (X + 0) \in ℂ$
116	115	mul02d	$⊢ φ \to 0 \cdot {(- 1)}^{N - (0 - 1)} F (X + 0) = 0$
117	98 116	eqtrd	$⊢ φ \to (\binom{N}{0 - 1}) {(- 1)}^{N - (0 - 1)} F (X + 0) = 0$
118	117	oveq1d	$⊢ φ \to (\binom{N}{0 - 1}) {(- 1)}^{N - (0 - 1)} F (X + 0) + \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) = 0 + \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
119		fzfid	$⊢ φ \to (0 + 1 \dots N + 1) \in Fin$
120		olc	$⊢ k \in (0 + 1 \dots N + 1) \to (k = 0 \lor k \in (0 + 1 \dots N + 1))$
121		elfzp12	$⊢ N + 1 \in ℤ_{\geq 0} \to (k \in (0 \dots N + 1) \leftrightarrow (k = 0 \lor k \in (0 + 1 \dots N + 1)))$
122	83 121	syl	$⊢ φ \to (k \in (0 \dots N + 1) \leftrightarrow (k = 0 \lor k \in (0 + 1 \dots N + 1)))$
123	122	biimpar	$⊢ (φ \land (k = 0 \lor k \in (0 + 1 \dots N + 1))) \to k \in (0 \dots N + 1)$
124	120 123	sylan2	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in (0 \dots N + 1)$
125	124 74	syldan	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) \in ℂ$
126	119 125	fsumcl	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) \in ℂ$
127	126	addlidd	$⊢ φ \to 0 + \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
128	92 118 127	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
129	4	adantr	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to X \in ℂ$
130		1cnd	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to 1 \in ℂ$
131		elfzelz	$⊢ k \in (0 + 1 \dots N + 1) \to k \in ℤ$
132	131	zcnd	$⊢ k \in (0 + 1 \dots N + 1) \to k \in ℂ$
133	132	adantl	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to k \in ℂ$
134	129 130 133	ppncand	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to X + 1 + (k - 1) = X + k$
135	134	fveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to F (X + 1 + (k - 1)) = F (X + k)$
136	135	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1)) = {(- 1)}^{N - (k - 1)} F (X + k)$
137	136	oveq2d	$⊢ (φ \land k \in (0 + 1 \dots N + 1)) \to (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1)) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
138	137	sumeq2dv	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1)) = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k)$
139		1zzd	$⊢ φ \to 1 \in ℤ$
140		0zd	$⊢ φ \to 0 \in ℤ$
141		elfzelz	$⊢ j \in (0 \dots N) \to j \in ℤ$
142		bccl	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to (\binom{N}{j}) \in ℕ_{0}$
143	142	nn0cnd	$⊢ (N \in ℕ_{0} \land j \in ℤ) \to (\binom{N}{j}) \in ℂ$
144	1 141 143	syl2an	$⊢ (φ \land j \in (0 \dots N)) \to (\binom{N}{j}) \in ℂ$
145		zsubcl	$⊢ (N \in ℤ \land j \in ℤ) \to N - j \in ℤ$
146	49 141 145	syl2an	$⊢ (φ \land j \in (0 \dots N)) \to N - j \in ℤ$
147		m1expcl	$⊢ N - j \in ℤ \to {(- 1)}^{N - j} \in ℤ$
148	146 147	syl	$⊢ (φ \land j \in (0 \dots N)) \to {(- 1)}^{N - j} \in ℤ$
149	148	zcnd	$⊢ (φ \land j \in (0 \dots N)) \to {(- 1)}^{N - j} \in ℂ$
150	3	adantr	$⊢ (φ \land j \in (0 \dots N)) \to F : A ⟶ ℂ$
151	4	adantr	$⊢ (φ \land j \in (0 \dots N)) \to X \in ℂ$
152		1cnd	$⊢ (φ \land j \in (0 \dots N)) \to 1 \in ℂ$
153	141	zcnd	$⊢ j \in (0 \dots N) \to j \in ℂ$
154	153	adantl	$⊢ (φ \land j \in (0 \dots N)) \to j \in ℂ$
155	151 152 154	addassd	$⊢ (φ \land j \in (0 \dots N)) \to X + 1 + j = X + 1 + j$
156	152 154	addcomd	$⊢ (φ \land j \in (0 \dots N)) \to 1 + j = j + 1$
157	156	oveq2d	$⊢ (φ \land j \in (0 \dots N)) \to X + 1 + j = X + j + 1$
158	155 157	eqtrd	$⊢ (φ \land j \in (0 \dots N)) \to X + 1 + j = X + j + 1$
159		fzp1elp1	$⊢ j \in (0 \dots N) \to j + 1 \in (0 \dots N + 1)$
160		oveq2	$⊢ k = j + 1 \to X + k = X + j + 1$
161	160	eleq1d	$⊢ k = j + 1 \to (X + k \in A \leftrightarrow X + j + 1 \in A)$
162	161	rspccv	$⊢ \forall k \in (0 \dots N + 1) X + k \in A \to (j + 1 \in (0 \dots N + 1) \to X + j + 1 \in A)$
163	110 162	syl	$⊢ φ \to (j + 1 \in (0 \dots N + 1) \to X + j + 1 \in A)$
164	163	imp	$⊢ (φ \land j + 1 \in (0 \dots N + 1)) \to X + j + 1 \in A$
165	159 164	sylan2	$⊢ (φ \land j \in (0 \dots N)) \to X + j + 1 \in A$
166	158 165	eqeltrd	$⊢ (φ \land j \in (0 \dots N)) \to X + 1 + j \in A$
167	150 166	ffvelcdmd	$⊢ (φ \land j \in (0 \dots N)) \to F (X + 1 + j) \in ℂ$
168	149 167	mulcld	$⊢ (φ \land j \in (0 \dots N)) \to {(- 1)}^{N - j} F (X + 1 + j) \in ℂ$
169	144 168	mulcld	$⊢ (φ \land j \in (0 \dots N)) \to (\binom{N}{j}) {(- 1)}^{N - j} F (X + 1 + j) \in ℂ$
170		oveq2	$⊢ j = k - 1 \to (\binom{N}{j}) = (\binom{N}{k - 1})$
171		oveq2	$⊢ j = k - 1 \to N - j = N - (k - 1)$
172	171	oveq2d	$⊢ j = k - 1 \to {(- 1)}^{N - j} = {(- 1)}^{N - (k - 1)}$
173		oveq2	$⊢ j = k - 1 \to X + 1 + j = X + 1 + (k - 1)$
174	173	fveq2d	$⊢ j = k - 1 \to F (X + 1 + j) = F (X + 1 + (k - 1))$
175	172 174	oveq12d	$⊢ j = k - 1 \to {(- 1)}^{N - j} F (X + 1 + j) = {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1))$
176	170 175	oveq12d	$⊢ j = k - 1 \to (\binom{N}{j}) {(- 1)}^{N - j} F (X + 1 + j) = (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1))$
177	139 140 49 169 176	fsumshft	$⊢ φ \to \sum_{j = 0}^{N} (\binom{N}{j}) {(- 1)}^{N - j} F (X + 1 + j) = \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1))$
178		oveq2	$⊢ j = k \to (\binom{N}{j}) = (\binom{N}{k})$
179		oveq2	$⊢ j = k \to N - j = N - k$
180	179	oveq2d	$⊢ j = k \to {(- 1)}^{N - j} = {(- 1)}^{N - k}$
181		oveq2	$⊢ j = k \to X + 1 + j = X + 1 + k$
182	181	fveq2d	$⊢ j = k \to F (X + 1 + j) = F (X + 1 + k)$
183	180 182	oveq12d	$⊢ j = k \to {(- 1)}^{N - j} F (X + 1 + j) = {(- 1)}^{N - k} F (X + 1 + k)$
184	178 183	oveq12d	$⊢ j = k \to (\binom{N}{j}) {(- 1)}^{N - j} F (X + 1 + j) = (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k)$
185	184	cbvsumv	$⊢ \sum_{j = 0}^{N} (\binom{N}{j}) {(- 1)}^{N - j} F (X + 1 + j) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k)$
186	177 185	eqtr3di	$⊢ φ \to \sum_{k = 0 + 1}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + 1 + (k - 1)) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k)$
187	128 138 186	3eqtr2d	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k)$
188	1 82	eleqtrdi	$⊢ φ \to N \in ℤ_{\geq 0}$
189		oveq2	$⊢ k = N + 1 \to (\binom{N}{k}) = (\binom{N}{N + 1})$
190		oveq2	$⊢ k = N + 1 \to N - k = N - (N + 1)$
191	190	oveq2d	$⊢ k = N + 1 \to {(- 1)}^{N - k} = {(- 1)}^{N - (N + 1)}$
192		oveq2	$⊢ k = N + 1 \to X + k = X + N + 1$
193	192	fveq2d	$⊢ k = N + 1 \to F (X + k) = F (X + N + 1)$
194	191 193	oveq12d	$⊢ k = N + 1 \to {(- 1)}^{N - k} F (X + k) = {(- 1)}^{N - (N + 1)} F (X + N + 1)$
195	189 194	oveq12d	$⊢ k = N + 1 \to (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) = (\binom{N}{N + 1}) {(- 1)}^{N - (N + 1)} F (X + N + 1)$
196	188 75 195	fsump1	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) + (\binom{N}{N + 1}) {(- 1)}^{N - (N + 1)} F (X + N + 1)$
197		bcval	$⊢ (N \in ℕ_{0} \land N + 1 \in ℤ) \to (\binom{N}{N + 1}) = if (N + 1 \in (0 \dots N), \frac{N!}{(N - (N + 1))! (N + 1)!}, 0)$
198	1 22 197	syl2anc	$⊢ φ \to (\binom{N}{N + 1}) = if (N + 1 \in (0 \dots N), \frac{N!}{(N - (N + 1))! (N + 1)!}, 0)$
199		fzp1nel	$⊢ \neg N + 1 \in (0 \dots N)$
200	199	iffalsei	$⊢ if (N + 1 \in (0 \dots N), \frac{N!}{(N - (N + 1))! (N + 1)!}, 0) = 0$
201	198 200	eqtrdi	$⊢ φ \to (\binom{N}{N + 1}) = 0$
202	201	oveq1d	$⊢ φ \to (\binom{N}{N + 1}) {(- 1)}^{N - (N + 1)} F (X + N + 1) = 0 \cdot {(- 1)}^{N - (N + 1)} F (X + N + 1)$
203	49 22	zsubcld	$⊢ φ \to N - (N + 1) \in ℤ$
204		m1expcl	$⊢ N - (N + 1) \in ℤ \to {(- 1)}^{N - (N + 1)} \in ℤ$
205	204	zcnd	$⊢ N - (N + 1) \in ℤ \to {(- 1)}^{N - (N + 1)} \in ℂ$
206	203 205	syl	$⊢ φ \to {(- 1)}^{N - (N + 1)} \in ℂ$
207		eluzfz2	$⊢ N + 1 \in ℤ_{\geq 0} \to N + 1 \in (0 \dots N + 1)$
208	83 207	syl	$⊢ φ \to N + 1 \in (0 \dots N + 1)$
209	192	eleq1d	$⊢ k = N + 1 \to (X + k \in A \leftrightarrow X + N + 1 \in A)$
210	209	rspcv	$⊢ N + 1 \in (0 \dots N + 1) \to (\forall k \in (0 \dots N + 1) X + k \in A \to X + N + 1 \in A)$
211	208 110 210	sylc	$⊢ φ \to X + N + 1 \in A$
212	3 211	ffvelcdmd	$⊢ φ \to F (X + N + 1) \in ℂ$
213	206 212	mulcld	$⊢ φ \to {(- 1)}^{N - (N + 1)} F (X + N + 1) \in ℂ$
214	213	mul02d	$⊢ φ \to 0 \cdot {(- 1)}^{N - (N + 1)} F (X + N + 1) = 0$
215	202 214	eqtrd	$⊢ φ \to (\binom{N}{N + 1}) {(- 1)}^{N - (N + 1)} F (X + N + 1) = 0$
216	215	oveq2d	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) + (\binom{N}{N + 1}) {(- 1)}^{N - (N + 1)} F (X + N + 1) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) + 0$
217		fzfid	$⊢ φ \to (0 \dots N) \in Fin$
218		fzelp1	$⊢ k \in (0 \dots N) \to k \in (0 \dots N + 1)$
219	218 75	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) \in ℂ$
220	217 219	fsumcl	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) \in ℂ$
221	220	addridd	$⊢ φ \to \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) + 0 = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
222	196 216 221	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
223	187 222	oveq12d	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N}{k - 1}) {(- 1)}^{N - (k - 1)} F (X + k) - \sum_{k = 0}^{N + 1} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k) - \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
224	79 81 223	3eqtrd	$⊢ φ \to \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) {(- 1)}^{N + 1 - k} F (X + k) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k) - \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
225	21 2 3 4 5	fwddifnval	$⊢ φ \to ((N + 1) △^{n} F) (X) = \sum_{k = 0}^{N + 1} (\binom{N + 1}{k}) {(- 1)}^{N + 1 - k} F (X + k)$
226		peano2cn	$⊢ X \in ℂ \to X + 1 \in ℂ$
227	4 226	syl	$⊢ φ \to X + 1 \in ℂ$
228	4	adantr	$⊢ (φ \land k \in (0 \dots N)) \to X \in ℂ$
229		1cnd	$⊢ (φ \land k \in (0 \dots N)) \to 1 \in ℂ$
230		elfzelz	$⊢ k \in (0 \dots N) \to k \in ℤ$
231	230	zcnd	$⊢ k \in (0 \dots N) \to k \in ℂ$
232	231	adantl	$⊢ (φ \land k \in (0 \dots N)) \to k \in ℂ$
233	228 229 232	addassd	$⊢ (φ \land k \in (0 \dots N)) \to X + 1 + k = X + 1 + k$
234	229 232	addcomd	$⊢ (φ \land k \in (0 \dots N)) \to 1 + k = k + 1$
235	234	oveq2d	$⊢ (φ \land k \in (0 \dots N)) \to X + 1 + k = X + k + 1$
236	233 235	eqtrd	$⊢ (φ \land k \in (0 \dots N)) \to X + 1 + k = X + k + 1$
237		fzp1elp1	$⊢ k \in (0 \dots N) \to k + 1 \in (0 \dots N + 1)$
238		oveq1	$⊢ j = k \to j + 1 = k + 1$
239	238	eleq1d	$⊢ j = k \to (j + 1 \in (0 \dots N + 1) \leftrightarrow k + 1 \in (0 \dots N + 1))$
240	239	anbi2d	$⊢ j = k \to ((φ \land j + 1 \in (0 \dots N + 1)) \leftrightarrow (φ \land k + 1 \in (0 \dots N + 1)))$
241	238	oveq2d	$⊢ j = k \to X + j + 1 = X + k + 1$
242	241	eleq1d	$⊢ j = k \to (X + j + 1 \in A \leftrightarrow X + k + 1 \in A)$
243	240 242	imbi12d	$⊢ j = k \to (((φ \land j + 1 \in (0 \dots N + 1)) \to X + j + 1 \in A) \leftrightarrow ((φ \land k + 1 \in (0 \dots N + 1)) \to X + k + 1 \in A))$
244	243 164	chvarvv	$⊢ (φ \land k + 1 \in (0 \dots N + 1)) \to X + k + 1 \in A$
245	237 244	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to X + k + 1 \in A$
246	236 245	eqeltrd	$⊢ (φ \land k \in (0 \dots N)) \to X + 1 + k \in A$
247	1 2 3 227 246	fwddifnval	$⊢ φ \to (N △^{n} F) (X + 1) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k)$
248	218 5	sylan2	$⊢ (φ \land k \in (0 \dots N)) \to X + k \in A$
249	1 2 3 4 248	fwddifnval	$⊢ φ \to (N △^{n} F) (X) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
250	247 249	oveq12d	$⊢ φ \to (N △^{n} F) (X + 1) - (N △^{n} F) (X) = \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + 1 + k) - \sum_{k = 0}^{N} (\binom{N}{k}) {(- 1)}^{N - k} F (X + k)$
251	224 225 250	3eqtr4d	$⊢ φ \to ((N + 1) △^{n} F) (X) = (N △^{n} F) (X + 1) - (N △^{n} F) (X)$

Metamath Proof Explorer

Theorem fwddifnp1

Proof