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	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	fwddifn0.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	fwddifn0.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
Assertion	fwddifn0	⊢ ( 𝜑 → ( ( 0 △n 𝐹 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		fwddifn0.1	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2		fwddifn0.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		fwddifn0.3	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		0nn0	⊢ 0 ∈ ℕ0
5	4	a1i	⊢ ( 𝜑 → 0 ∈ ℕ0 )
6	1 3	sseldd	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
7		0z	⊢ 0 ∈ ℤ
8		fzsn	⊢ ( 0 ∈ ℤ → ( 0 ... 0 ) = { 0 } )
9	7 8	ax-mp	⊢ ( 0 ... 0 ) = { 0 }
10	9	eleq2i	⊢ ( 𝑘 ∈ ( 0 ... 0 ) ↔ 𝑘 ∈ { 0 } )
11		velsn	⊢ ( 𝑘 ∈ { 0 } ↔ 𝑘 = 0 )
12	10 11	bitri	⊢ ( 𝑘 ∈ ( 0 ... 0 ) ↔ 𝑘 = 0 )
13		oveq2	⊢ ( 𝑘 = 0 → ( 𝑋 + 𝑘 ) = ( 𝑋 + 0 ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑋 + 𝑘 ) = ( 𝑋 + 0 ) )
15	6	addridd	⊢ ( 𝜑 → ( 𝑋 + 0 ) = 𝑋 )
16	15 3	eqeltrd	⊢ ( 𝜑 → ( 𝑋 + 0 ) ∈ 𝐴 )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑋 + 0 ) ∈ 𝐴 )
18	14 17	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 = 0 ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
19	12 18	sylan2b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 0 ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
20	5 1 2 6 19	fwddifnval	⊢ ( 𝜑 → ( ( 0 △n 𝐹 ) ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( - 1 ↑ ( 0 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
21	15	fveq2d	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + 0 ) ) = ( 𝐹 ‘ 𝑋 ) )
22	21	oveq2d	⊢ ( 𝜑 → ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) = ( 1 · ( 𝐹 ‘ 𝑋 ) ) )
23	2 3	ffvelcdmd	⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℂ )
24	23	mullidd	⊢ ( 𝜑 → ( 1 · ( 𝐹 ‘ 𝑋 ) ) = ( 𝐹 ‘ 𝑋 ) )
25	22 24	eqtrd	⊢ ( 𝜑 → ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) = ( 𝐹 ‘ 𝑋 ) )
26	25	oveq2d	⊢ ( 𝜑 → ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) = ( 1 · ( 𝐹 ‘ 𝑋 ) ) )
27	26 24	eqtrd	⊢ ( 𝜑 → ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) = ( 𝐹 ‘ 𝑋 ) )
28	27 23	eqeltrd	⊢ ( 𝜑 → ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) ∈ ℂ )
29		oveq2	⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = ( 0 C 0 ) )
30		bcnn	⊢ ( 0 ∈ ℕ0 → ( 0 C 0 ) = 1 )
31	4 30	ax-mp	⊢ ( 0 C 0 ) = 1
32	29 31	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = 1 )
33		oveq2	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = ( 0 − 0 ) )
34		0m0e0	⊢ ( 0 − 0 ) = 0
35	33 34	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = 0 )
36	35	oveq2d	⊢ ( 𝑘 = 0 → ( - 1 ↑ ( 0 − 𝑘 ) ) = ( - 1 ↑ 0 ) )
37		neg1cn	⊢ - 1 ∈ ℂ
38		exp0	⊢ ( - 1 ∈ ℂ → ( - 1 ↑ 0 ) = 1 )
39	37 38	ax-mp	⊢ ( - 1 ↑ 0 ) = 1
40	36 39	eqtrdi	⊢ ( 𝑘 = 0 → ( - 1 ↑ ( 0 − 𝑘 ) ) = 1 )
41	13	fveq2d	⊢ ( 𝑘 = 0 → ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) = ( 𝐹 ‘ ( 𝑋 + 0 ) ) )
42	40 41	oveq12d	⊢ ( 𝑘 = 0 → ( ( - 1 ↑ ( 0 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) )
43	32 42	oveq12d	⊢ ( 𝑘 = 0 → ( ( 0 C 𝑘 ) · ( ( - 1 ↑ ( 0 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) )
44	43	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( - 1 ↑ ( 0 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) )
45	7 28 44	sylancr	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( - 1 ↑ ( 0 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( 1 · ( 1 · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) )
46	45 27	eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( - 1 ↑ ( 0 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( 𝐹 ‘ 𝑋 ) )
47	20 46	eqtrd	⊢ ( 𝜑 → ( ( 0 △n 𝐹 ) ‘ 𝑋 ) = ( 𝐹 ‘ 𝑋 ) )