Metamath Proof Explorer

Theorem 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 
|- ( ph -> A C_ CC )
fwddifn0.2 
|- ( ph -> F : A --> CC )
fwddifn0.3 
|- ( ph -> X e. A )
Assertion fwddifn0 
|- ( ph -> ( ( 0 _/_\^n F ) ` X ) = ( F ` X ) )

Proof

Step Hyp Ref Expression
1 fwddifn0.1 
 |-  ( ph -> A C_ CC )
2 fwddifn0.2 
 |-  ( ph -> F : A --> CC )
3 fwddifn0.3 
 |-  ( ph -> X e. A )
4 0nn0 
 |-  0 e. NN0
5 4 a1i 
 |-  ( ph -> 0 e. NN0 )
6 1 3 sseldd 
 |-  ( ph -> X e. CC )
7 0z 
 |-  0 e. ZZ
8 fzsn 
 |-  ( 0 e. ZZ -> ( 0 ... 0 ) = { 0 } )
9 7 8 ax-mp 
 |-  ( 0 ... 0 ) = { 0 }
10 9 eleq2i 
 |-  ( k e. ( 0 ... 0 ) <-> k e. { 0 } )
11 velsn 
 |-  ( k e. { 0 } <-> k = 0 )
12 10 11 bitri 
 |-  ( k e. ( 0 ... 0 ) <-> k = 0 )
13 oveq2 
 |-  ( k = 0 -> ( X + k ) = ( X + 0 ) )
14 13 adantl 
 |-  ( ( ph /\ k = 0 ) -> ( X + k ) = ( X + 0 ) )
15 6 addid1d 
 |-  ( ph -> ( X + 0 ) = X )
16 15 3 eqeltrd 
 |-  ( ph -> ( X + 0 ) e. A )
17 16 adantr 
 |-  ( ( ph /\ k = 0 ) -> ( X + 0 ) e. A )
18 14 17 eqeltrd 
 |-  ( ( ph /\ k = 0 ) -> ( X + k ) e. A )
19 12 18 sylan2b 
 |-  ( ( ph /\ k e. ( 0 ... 0 ) ) -> ( X + k ) e. A )
20 5 1 2 6 19 fwddifnval 
 |-  ( ph -> ( ( 0 _/_\^n F ) ` X ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( -u 1 ^ ( 0 - k ) ) x. ( F ` ( X + k ) ) ) ) )
21 15 fveq2d 
 |-  ( ph -> ( F ` ( X + 0 ) ) = ( F ` X ) )
22 21 oveq2d 
 |-  ( ph -> ( 1 x. ( F ` ( X + 0 ) ) ) = ( 1 x. ( F ` X ) ) )
23 2 3 ffvelrnd 
 |-  ( ph -> ( F ` X ) e. CC )
24 23 mulid2d 
 |-  ( ph -> ( 1 x. ( F ` X ) ) = ( F ` X ) )
25 22 24 eqtrd 
 |-  ( ph -> ( 1 x. ( F ` ( X + 0 ) ) ) = ( F ` X ) )
26 25 oveq2d 
 |-  ( ph -> ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) = ( 1 x. ( F ` X ) ) )
27 26 24 eqtrd 
 |-  ( ph -> ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) = ( F ` X ) )
28 27 23 eqeltrd 
 |-  ( ph -> ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) e. CC )
29 oveq2 
 |-  ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
30 bcnn 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
31 4 30 ax-mp 
 |-  ( 0 _C 0 ) = 1
32 29 31 eqtrdi 
 |-  ( k = 0 -> ( 0 _C k ) = 1 )
33 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
34 0m0e0 
 |-  ( 0 - 0 ) = 0
35 33 34 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
36 35 oveq2d 
 |-  ( k = 0 -> ( -u 1 ^ ( 0 - k ) ) = ( -u 1 ^ 0 ) )
37 neg1cn 
 |-  -u 1 e. CC
38 exp0 
 |-  ( -u 1 e. CC -> ( -u 1 ^ 0 ) = 1 )
39 37 38 ax-mp 
 |-  ( -u 1 ^ 0 ) = 1
40 36 39 eqtrdi 
 |-  ( k = 0 -> ( -u 1 ^ ( 0 - k ) ) = 1 )
41 13 fveq2d 
 |-  ( k = 0 -> ( F ` ( X + k ) ) = ( F ` ( X + 0 ) ) )
42 40 41 oveq12d 
 |-  ( k = 0 -> ( ( -u 1 ^ ( 0 - k ) ) x. ( F ` ( X + k ) ) ) = ( 1 x. ( F ` ( X + 0 ) ) ) )
43 32 42 oveq12d 
 |-  ( k = 0 -> ( ( 0 _C k ) x. ( ( -u 1 ^ ( 0 - k ) ) x. ( F ` ( X + k ) ) ) ) = ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) )
44 43 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( -u 1 ^ ( 0 - k ) ) x. ( F ` ( X + k ) ) ) ) = ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) )
45 7 28 44 sylancr 
 |-  ( ph -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( -u 1 ^ ( 0 - k ) ) x. ( F ` ( X + k ) ) ) ) = ( 1 x. ( 1 x. ( F ` ( X + 0 ) ) ) ) )
46 45 27 eqtrd 
 |-  ( ph -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( -u 1 ^ ( 0 - k ) ) x. ( F ` ( X + k ) ) ) ) = ( F ` X ) )
47 20 46 eqtrd 
 |-  ( ph -> ( ( 0 _/_\^n F ) ` X ) = ( F ` X ) )