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 … n y + k ∈ dom ⁡ f ⟼ ∑ k = 0 n ( n k) ⁢ − 1 n − k ⁢ f ⁡ x + k

Detailed syntax breakdown

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