Metamath Proof Explorer

Theorem fwddifnval

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

Ref Expression
Hypotheses fwddifnval.1 
|- ( ph -> N e. NN0 )
fwddifnval.2 
|- ( ph -> A C_ CC )
fwddifnval.3 
|- ( ph -> F : A --> CC )
fwddifnval.4 
|- ( ph -> X e. CC )
fwddifnval.5 
|- ( ( ph /\ k e. ( 0 ... N ) ) -> ( X + k ) e. A )
Assertion fwddifnval 
|- ( ph -> ( ( N _/_\^n F ) ` X ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fwddifnval.1 
 |-  ( ph -> N e. NN0 )
2 fwddifnval.2 
 |-  ( ph -> A C_ CC )
3 fwddifnval.3 
 |-  ( ph -> F : A --> CC )
4 fwddifnval.4 
 |-  ( ph -> X e. CC )
5 fwddifnval.5 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( X + k ) e. A )
6 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 ) ) ) ) ) )
7 6 a1i 
 |-  ( ph -> _/_\^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 ) ) ) ) ) ) )
8 oveq2 
 |-  ( n = N -> ( 0 ... n ) = ( 0 ... N ) )
9 8 adantr 
 |-  ( ( n = N /\ f = F ) -> ( 0 ... n ) = ( 0 ... N ) )
10 dmeq 
 |-  ( f = F -> dom f = dom F )
11 10 eleq2d 
 |-  ( f = F -> ( ( y + k ) e. dom f <-> ( y + k ) e. dom F ) )
12 11 adantl 
 |-  ( ( n = N /\ f = F ) -> ( ( y + k ) e. dom f <-> ( y + k ) e. dom F ) )
13 9 12 raleqbidv 
 |-  ( ( n = N /\ f = F ) -> ( A. k e. ( 0 ... n ) ( y + k ) e. dom f <-> A. k e. ( 0 ... N ) ( y + k ) e. dom F ) )
14 13 rabbidv 
 |-  ( ( n = N /\ f = F ) -> { y e. CC | A. k e. ( 0 ... n ) ( y + k ) e. dom f } = { y e. CC | A. k e. ( 0 ... N ) ( y + k ) e. dom F } )
15 oveq1 
 |-  ( n = N -> ( n _C k ) = ( N _C k ) )
16 15 adantr 
 |-  ( ( n = N /\ f = F ) -> ( n _C k ) = ( N _C k ) )
17 oveq1 
 |-  ( n = N -> ( n - k ) = ( N - k ) )
18 17 oveq2d 
 |-  ( n = N -> ( -u 1 ^ ( n - k ) ) = ( -u 1 ^ ( N - k ) ) )
19 fveq1 
 |-  ( f = F -> ( f ` ( x + k ) ) = ( F ` ( x + k ) ) )
20 18 19 oveqan12d 
 |-  ( ( n = N /\ f = F ) -> ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) = ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) )
21 16 20 oveq12d 
 |-  ( ( n = N /\ f = F ) -> ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) = ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) ) )
22 21 adantr 
 |-  ( ( ( n = N /\ f = F ) /\ k e. ( 0 ... n ) ) -> ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) = ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) ) )
23 9 22 sumeq12dv 
 |-  ( ( n = N /\ f = F ) -> sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( -u 1 ^ ( n - k ) ) x. ( f ` ( x + k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) ) )
24 14 23 mpteq12dv 
 |-  ( ( n = N /\ f = F ) -> ( 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 ) ) ) ) ) = ( 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 ) ) ) ) ) )
25 24 adantl 
 |-  ( ( ph /\ ( n = N /\ f = F ) ) -> ( 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 ) ) ) ) ) = ( 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 ) ) ) ) ) )
26 cnex 
 |-  CC e. _V
27 elpm2r 
 |-  ( ( ( CC e. _V /\ CC e. _V ) /\ ( F : A --> CC /\ A C_ CC ) ) -> F e. ( CC ^pm CC ) )
28 26 26 27 mpanl12 
 |-  ( ( F : A --> CC /\ A C_ CC ) -> F e. ( CC ^pm CC ) )
29 3 2 28 syl2anc 
 |-  ( ph -> F e. ( CC ^pm CC ) )
30 26 mptrabex 
 |-  ( 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 ) ) ) ) ) e. _V
31 30 a1i 
 |-  ( ph -> ( 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 ) ) ) ) ) e. _V )
32 7 25 1 29 31 ovmpod 
 |-  ( ph -> ( N _/_\^n F ) = ( 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 ) ) ) ) ) )
33 fvoveq1 
 |-  ( x = X -> ( F ` ( x + k ) ) = ( F ` ( X + k ) ) )
34 33 oveq2d 
 |-  ( x = X -> ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) = ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) )
35 34 oveq2d 
 |-  ( x = X -> ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) ) = ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
36 35 sumeq2sdv 
 |-  ( x = X -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
37 36 adantl 
 |-  ( ( ph /\ x = X ) -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( x + k ) ) ) ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )
38 3 fdmd 
 |-  ( ph -> dom F = A )
39 38 adantr 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> dom F = A )
40 5 39 eleqtrrd 
 |-  ( ( ph /\ k e. ( 0 ... N ) ) -> ( X + k ) e. dom F )
41 40 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... N ) ( X + k ) e. dom F )
42 oveq1 
 |-  ( y = X -> ( y + k ) = ( X + k ) )
43 42 eleq1d 
 |-  ( y = X -> ( ( y + k ) e. dom F <-> ( X + k ) e. dom F ) )
44 43 ralbidv 
 |-  ( y = X -> ( A. k e. ( 0 ... N ) ( y + k ) e. dom F <-> A. k e. ( 0 ... N ) ( X + k ) e. dom F ) )
45 44 elrab 
 |-  ( X e. { y e. CC | A. k e. ( 0 ... N ) ( y + k ) e. dom F } <-> ( X e. CC /\ A. k e. ( 0 ... N ) ( X + k ) e. dom F ) )
46 4 41 45 sylanbrc 
 |-  ( ph -> X e. { y e. CC | A. k e. ( 0 ... N ) ( y + k ) e. dom F } )
47 sumex 
 |-  sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) e. _V
48 47 a1i 
 |-  ( ph -> sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) e. _V )
49 32 37 46 48 fvmptd 
 |-  ( ph -> ( ( N _/_\^n F ) ` X ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( -u 1 ^ ( N - k ) ) x. ( F ` ( X + k ) ) ) ) )