Metamath Proof Explorer


Theorem 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 φ N 0
fwddifnp1.2 φ A
fwddifnp1.3 φ F : A
fwddifnp1.4 φ X
fwddifnp1.5 φ k 0 N + 1 X + k A
Assertion fwddifnp1 φ N + 1 n F X = N n F X + 1 N n F X

Proof

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