Metamath Proof Explorer

Definition df-fwddifn

Description: Define the nth forward difference operator. This works out to be the forward difference operator iterated n times. (Contributed by Scott Fenton, 28-May-2020)

Ref Expression
Assertion df-fwddifn 
|- _/_\^n = ( n e. NN0 , f e. ( CC ^pm CC ) |-> ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfwddifn 
 |-  _/_\^n
1 vn 
 |-  n
2 cn0 
 |-  NN0
3 vf 
 |-  f
4 cc 
 |-  CC
5 cpm 
 |-  ^pm
6 4 4 5 co 
 |-  ( CC ^pm CC )
7 vx 
 |-  x
8 vy 
 |-  y
9 vk 
 |-  k
10 cc0 
 |-  0
11 cfz 
 |-  ...
12 1 cv 
 |-  n
13 10 12 11 co 
 |-  ( 0 ... n )
14 8 cv 
 |-  y
15 caddc 
 |-  +
16 9 cv 
 |-  k
17 14 16 15 co 
 |-  ( y + k )
18 3 cv 
 |-  f
19 18 cdm 
 |-  dom f
20 17 19 wcel 
 |-  ( y + k ) e. dom f
21 20 9 13 wral 
 |-  A. k e. ( 0 ... n ) ( y + k ) e. dom f
22 21 8 4 crab 
 |-  { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f }
23 cbc 
 |-  _C
24 12 16 23 co 
 |-  ( n _C k )
25 cmul 
 |-  x.
26 c1 
 |-  1
27 26 cneg 
 |-  -u 1
28 cexp 
 |-  ^
29 cmin 
 |-  -
30 12 16 29 co 
 |-  ( n - k )
31 27 30 28 co 
 |-  ( -u 1 ^ ( n - k ) )
32 7 cv 
 |-  x
33 32 16 15 co 
 |-  ( x + k )
34 33 18 cfv 
 |-  ( f ` ( x + k ) )
35 31 34 25 co 
 |-  ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) )
36 24 35 25 co 
 |-  ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) )
37 13 36 9 csu 
 |-  sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) )
38 7 22 37 cmpt 
 |-  ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) )
39 1 3 2 6 38 cmpo 
 |-  ( n e. NN0 , f e. ( CC ^pm CC ) |-> ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) ) )
40 0 39 wceq 
 |-  _/_\^n = ( n e. NN0 , f e. ( CC ^pm CC ) |-> ( x e. { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } |-> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) ) )