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 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )