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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
fwddifnval.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
fwddifnval.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
fwddifnval.4 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
fwddifnval.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
Assertion fwddifnval ( 𝜑 → ( ( 𝑁 △n 𝐹 ) ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fwddifnval.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 fwddifnval.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 fwddifnval.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
4 fwddifnval.4 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5 fwddifnval.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
6 df-fwddifn ⊢ △n = ( 𝑛 ∈ ℕ0 , 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )
7 6 a1i ⊢ ( 𝜑 → △n = ( 𝑛 ∈ ℕ0 , 𝑓 ∈ ( ℂ ↑pm ℂ ) ↦ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) ) )
8 oveq2 ⊢ ( 𝑛 = 𝑁 → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
9 8 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( 0 ... 𝑛 ) = ( 0 ... 𝑁 ) )
10 dmeq ⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
11 10 eleq2d ⊢ ( 𝑓 = 𝐹 → ( ( 𝑦 + 𝑘 ) ∈ dom 𝑓 ↔ ( 𝑦 + 𝑘 ) ∈ dom 𝐹 ) )
12 11 adantl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( ( 𝑦 + 𝑘 ) ∈ dom 𝑓 ↔ ( 𝑦 + 𝑘 ) ∈ dom 𝐹 ) )
13 9 12 raleqbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 ) )
14 13 rabbidv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } = { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } )
15 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 C 𝑘 ) = ( 𝑁 C 𝑘 ) )
16 15 adantr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( 𝑛 C 𝑘 ) = ( 𝑁 C 𝑘 ) )
17 oveq1 ⊢ ( 𝑛 = 𝑁 → ( 𝑛 − 𝑘 ) = ( 𝑁 − 𝑘 ) )
18 17 oveq2d ⊢ ( 𝑛 = 𝑁 → ( - 1 ↑ ( 𝑛 − 𝑘 ) ) = ( - 1 ↑ ( 𝑁 − 𝑘 ) ) )
19 fveq1 ⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) = ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) )
20 18 19 oveqan12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) )
21 16 20 oveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) )
22 21 adantr ⊢ ( ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) ∧ 𝑘 ∈ ( 0 ... 𝑛 ) ) → ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) )
23 9 22 sumeq12dv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) )
24 14 23 mpteq12dv ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) → ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )
25 24 adantl ⊢ ( ( 𝜑 ∧ ( 𝑛 = 𝑁 ∧ 𝑓 = 𝐹 ) ) → ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑛 ) ( 𝑦 + 𝑘 ) ∈ dom 𝑓 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( - 1 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝑓 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )
26 cnex ⊢ ℂ ∈ V
27 elpm2r ⊢ ( ( ( ℂ ∈ V ∧ ℂ ∈ V ) ∧ ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ) ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
28 26 26 27 mpanl12 ⊢ ( ( 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ ℂ ) → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
29 3 2 28 syl2anc ⊢ ( 𝜑 → 𝐹 ∈ ( ℂ ↑pm ℂ ) )
30 26 mptrabex ⊢ ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) ∈ V
31 30 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) ∈ V )
32 7 25 1 29 31 ovmpod ⊢ ( 𝜑 → ( 𝑁 △n 𝐹 ) = ( 𝑥 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } ↦ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) ) )
33 fvoveq1 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) )
34 33 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) )
35 34 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
36 35 sumeq2sdv ⊢ ( 𝑥 = 𝑋 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
37 36 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑥 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
38 3 fdmd ⊢ ( 𝜑 → dom 𝐹 = 𝐴 )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → dom 𝐹 = 𝐴 )
40 5 39 eleqtrrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + 𝑘 ) ∈ dom 𝐹 )
41 40 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑋 + 𝑘 ) ∈ dom 𝐹 )
42 oveq1 ⊢ ( 𝑦 = 𝑋 → ( 𝑦 + 𝑘 ) = ( 𝑋 + 𝑘 ) )
43 42 eleq1d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑦 + 𝑘 ) ∈ dom 𝐹 ↔ ( 𝑋 + 𝑘 ) ∈ dom 𝐹 ) )
44 43 ralbidv ⊢ ( 𝑦 = 𝑋 → ( ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 ↔ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑋 + 𝑘 ) ∈ dom 𝐹 ) )
45 44 elrab ⊢ ( 𝑋 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } ↔ ( 𝑋 ∈ ℂ ∧ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑋 + 𝑘 ) ∈ dom 𝐹 ) )
46 4 41 45 sylanbrc ⊢ ( 𝜑 → 𝑋 ∈ { 𝑦 ∈ ℂ ∣ ∀ 𝑘 ∈ ( 0 ... 𝑁 ) ( 𝑦 + 𝑘 ) ∈ dom 𝐹 } )
47 sumex ⊢ Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ V
48 47 a1i ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ V )
49 32 37 46 48 fvmptd ⊢ ( 𝜑 → ( ( 𝑁 △n 𝐹 ) ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )