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∈ℕ0,f∈ℂ↑𝑝𝑚ℂ⟼x∈y∈ℂ|∀k∈0…ny+k∈dom⁡f⟼∑k=0n(nk)⁢−1n−k⁢f⁡x+k

Detailed syntax breakdown

Step Hyp Ref Expression
0 cfwddifn class△n
1 vn setvarn
2 cn0 classℕ0
3 vf setvarf
4 cc classℂ
5 cpm class↑𝑝𝑚
6 4 4 5 co classℂ↑𝑝𝑚ℂ
7 vx setvarx
8 vy setvary
9 vk setvark
10 cc0 class0
11 cfz class…
12 1 cv setvarn
13 10 12 11 co class0…n
14 8 cv setvary
15 caddc class+
16 9 cv setvark
17 14 16 15 co classy+k
18 3 cv setvarf
19 18 cdm classdom⁡f
20 17 19 wcel wffy+k∈dom⁡f
21 20 9 13 wral wff∀k∈0…ny+k∈dom⁡f
22 21 8 4 crab classy∈ℂ|∀k∈0…ny+k∈dom⁡f
23 cbc class(..)
24 12 16 23 co class(nk)
25 cmul class×
26 c1 class1
27 26 cneg class-1
28 cexp class^
29 cmin class−
30 12 16 29 co classn−k
31 27 30 28 co class−1n−k
32 7 cv setvarx
33 32 16 15 co classx+k
34 33 18 cfv classf⁡x+k
35 31 34 25 co class−1n−k⁢f⁡x+k
36 24 35 25 co class(nk)⁢−1n−k⁢f⁡x+k
37 13 36 9 csu class∑k=0n(nk)⁢−1n−k⁢f⁡x+k
38 7 22 37 cmpt classx∈y∈ℂ|∀k∈0…ny+k∈dom⁡f⟼∑k=0n(nk)⁢−1n−k⁢f⁡x+k
39 1 3 2 6 38 cmpo classn∈ℕ0,f∈ℂ↑𝑝𝑚ℂ⟼x∈y∈ℂ|∀k∈0…ny+k∈dom⁡f⟼∑k=0n(nk)⁢−1n−k⁢f⁡x+k
40 0 39 wceq wff△n=n∈ℕ0,f∈ℂ↑𝑝𝑚ℂ⟼x∈y∈ℂ|∀k∈0…ny+k∈dom⁡f⟼∑k=0n(nk)⁢−1n−k⁢f⁡x+k