fwddifnp1

Description: The value of the n-iterated forward difference at a successor. (Contributed by Scott Fenton, 28-May-2020)

	Ref	Expression
Hypotheses	fwddifnp1.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
	fwddifnp1.2	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	fwddifnp1.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	fwddifnp1.4	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
	fwddifnp1.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
Assertion	fwddifnp1	⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) △n 𝐹 ) ‘ 𝑋 ) = ( ( ( 𝑁 △n 𝐹 ) ‘ ( 𝑋 + 1 ) ) − ( ( 𝑁 △n 𝐹 ) ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		fwddifnp1.1	⊢ ( 𝜑 → 𝑁 ∈ ℕ₀ )
2		fwddifnp1.2	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3		fwddifnp1.3	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
4		fwddifnp1.4	⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5		fwddifnp1.5	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
6		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
7		bcpasc	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
8	1 6 7	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 + 1 ) C 𝑘 ) )
9	8	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
10		bccl	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ₀ )
11	1 6 10	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ₀ )
12	11	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
13		peano2zm	⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
14	6 13	syl	⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
15		bccl	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ₀ )
16	1 14 15	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ₀ )
17	16	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℂ )
18	12 17	addcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) + ( 𝑁 C 𝑘 ) ) )
19	18	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) + ( 𝑁 C 𝑘 ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
20		peano2nn0	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑁 + 1 ) ∈ ℕ₀ )
21	1 20	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ₀ )
22	21	nn0zd	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℤ )
23		zsubcl	⊢ ( ( ( 𝑁 + 1 ) ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℤ )
24	22 6 23	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℤ )
25		m1expcl	⊢ ( ( ( 𝑁 + 1 ) − 𝑘 ) ∈ ℤ → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℤ )
26	24 25	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℤ )
27	26	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) ∈ ℂ )
28	3	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝐹 : 𝐴 ⟶ ℂ )
29	28 5	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ∈ ℂ )
30	27 29	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ∈ ℂ )
31	17 12 30	adddird	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) + ( 𝑁 C 𝑘 ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
32	19 31	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
33	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℕ₀ )
34	33	nn0cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑁 ∈ ℂ )
35	6	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℤ )
36	35	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
37		1cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
38	34 36 37	subsub3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 − ( 𝑘 − 1 ) ) = ( ( 𝑁 + 1 ) − 𝑘 ) )
39	38	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( 𝑁 − ( 𝑘 − 1 ) ) )
40	39	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) )
41	40	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) )
42	41	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
43	34 37 36	addsubd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 + 1 ) − 𝑘 ) = ( ( 𝑁 − 𝑘 ) + 1 ) )
44	43	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( - 1 ↑ ( ( 𝑁 − 𝑘 ) + 1 ) ) )
45		neg1cn	⊢ - 1 ∈ ℂ
46	45	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → - 1 ∈ ℂ )
47		neg1ne0	⊢ - 1 ≠ 0
48	47	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → - 1 ≠ 0 )
49	1	nn0zd	⊢ ( 𝜑 → 𝑁 ∈ ℤ )
50		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
51	49 6 50	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 − 𝑘 ) ∈ ℤ )
52	46 48 51	expp1zd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 − 𝑘 ) + 1 ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · - 1 ) )
53	44 52	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · - 1 ) )
54		m1expcl	⊢ ( ( 𝑁 − 𝑘 ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℤ )
55	51 54	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℤ )
56	55	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ∈ ℂ )
57	56 46	mulcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · - 1 ) = ( - 1 · ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ) )
58	56	mulm1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 · ( - 1 ↑ ( 𝑁 − 𝑘 ) ) ) = - ( - 1 ↑ ( 𝑁 − 𝑘 ) ) )
59	53 57 58	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) = - ( - 1 ↑ ( 𝑁 − 𝑘 ) ) )
60	59	oveq1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = ( - ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) )
61	56 29	mulneg1d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = - ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) )
62	60 61	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = - ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) )
63	62	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( 𝑁 C 𝑘 ) · - ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
64	56 29	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ∈ ℂ )
65	12 64	mulneg2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · - ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = - ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
66	63 65	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = - ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
67	42 66	oveq12d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + - ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
68		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 − ( 𝑘 − 1 ) ) ∈ ℤ )
69	49 14 68	syl2an	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 − ( 𝑘 − 1 ) ) ∈ ℤ )
70		m1expcl	⊢ ( ( 𝑁 − ( 𝑘 − 1 ) ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) ∈ ℤ )
71	69 70	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) ∈ ℤ )
72	71	zcnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) ∈ ℂ )
73	72 29	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ∈ ℂ )
74	17 73	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ ℂ )
75	12 64	mulcld	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ ℂ )
76	74 75	negsubd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + - ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
77	32 67 76	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 C 𝑘 ) + ( 𝑁 C ( 𝑘 − 1 ) ) ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
78	9 77	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
79	78	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
80		fzfid	⊢ ( 𝜑 → ( 0 ... ( 𝑁 + 1 ) ) ∈ Fin )
81	80 74 75	fsumsub	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
82		nn0uz	⊢ ℕ₀ = ( ℤ_≥ ‘ 0 )
83	21 82	eleqtrdi	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( ℤ_≥ ‘ 0 ) )
84		oveq1	⊢ ( 𝑘 = 0 → ( 𝑘 − 1 ) = ( 0 − 1 ) )
85	84	oveq2d	⊢ ( 𝑘 = 0 → ( 𝑁 C ( 𝑘 − 1 ) ) = ( 𝑁 C ( 0 − 1 ) ) )
86	84	oveq2d	⊢ ( 𝑘 = 0 → ( 𝑁 − ( 𝑘 − 1 ) ) = ( 𝑁 − ( 0 − 1 ) ) )
87	86	oveq2d	⊢ ( 𝑘 = 0 → ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) = ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) )
88		oveq2	⊢ ( 𝑘 = 0 → ( 𝑋 + 𝑘 ) = ( 𝑋 + 0 ) )
89	88	fveq2d	⊢ ( 𝑘 = 0 → ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) = ( 𝐹 ‘ ( 𝑋 + 0 ) ) )
90	87 89	oveq12d	⊢ ( 𝑘 = 0 → ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) )
91	85 90	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( 𝑁 C ( 0 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) )
92	83 74 91	fsum1p	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( ( 𝑁 C ( 0 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
93		df-neg	⊢ - 1 = ( 0 − 1 )
94	93	oveq2i	⊢ ( 𝑁 C - 1 ) = ( 𝑁 C ( 0 − 1 ) )
95		bcneg1	⊢ ( 𝑁 ∈ ℕ₀ → ( 𝑁 C - 1 ) = 0 )
96	1 95	syl	⊢ ( 𝜑 → ( 𝑁 C - 1 ) = 0 )
97	94 96	eqtr3id	⊢ ( 𝜑 → ( 𝑁 C ( 0 − 1 ) ) = 0 )
98	97	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) = ( 0 · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) )
99		0z	⊢ 0 ∈ ℤ
100		1z	⊢ 1 ∈ ℤ
101		zsubcl	⊢ ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ) → ( 0 − 1 ) ∈ ℤ )
102	99 100 101	mp2an	⊢ ( 0 − 1 ) ∈ ℤ
103	102	a1i	⊢ ( 𝜑 → ( 0 − 1 ) ∈ ℤ )
104	49 103	zsubcld	⊢ ( 𝜑 → ( 𝑁 − ( 0 − 1 ) ) ∈ ℤ )
105		m1expcl	⊢ ( ( 𝑁 − ( 0 − 1 ) ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) ∈ ℤ )
106	104 105	syl	⊢ ( 𝜑 → ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) ∈ ℤ )
107	106	zcnd	⊢ ( 𝜑 → ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) ∈ ℂ )
108		eluzfz1	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ_≥ ‘ 0 ) → 0 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
109	83 108	syl	⊢ ( 𝜑 → 0 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
110	5	ralrimiva	⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( 𝑋 + 𝑘 ) ∈ 𝐴 )
111	88	eleq1d	⊢ ( 𝑘 = 0 → ( ( 𝑋 + 𝑘 ) ∈ 𝐴 ↔ ( 𝑋 + 0 ) ∈ 𝐴 ) )
112	111	rspcva	⊢ ( ( 0 ∈ ( 0 ... ( 𝑁 + 1 ) ) ∧ ∀ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( 𝑋 + 𝑘 ) ∈ 𝐴 ) → ( 𝑋 + 0 ) ∈ 𝐴 )
113	109 110 112	syl2anc	⊢ ( 𝜑 → ( 𝑋 + 0 ) ∈ 𝐴 )
114	3 113	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + 0 ) ) ∈ ℂ )
115	107 114	mulcld	⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ∈ ℂ )
116	115	mul02d	⊢ ( 𝜑 → ( 0 · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) = 0 )
117	98 116	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 C ( 0 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) = 0 )
118	117	oveq1d	⊢ ( 𝜑 → ( ( ( 𝑁 C ( 0 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 0 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 0 ) ) ) ) + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) = ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
119		fzfid	⊢ ( 𝜑 → ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ∈ Fin )
120		olc	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) )
121		elfzp12	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ_≥ ‘ 0 ) → ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) )
122	83 121	syl	⊢ ( 𝜑 → ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) )
123	122	biimpar	⊢ ( ( 𝜑 ∧ ( 𝑘 = 0 ∨ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
124	120 123	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
125	124 74	syldan	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ ℂ )
126	119 125	fsumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ ℂ )
127	126	addid2d	⊢ ( 𝜑 → ( 0 + Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
128	92 118 127	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
129	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑋 ∈ ℂ )
130		1cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 1 ∈ ℂ )
131		elfzelz	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
132	131	zcnd	⊢ ( 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℂ )
133	132	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → 𝑘 ∈ ℂ )
134	129 130 133	ppncand	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) = ( 𝑋 + 𝑘 ) )
135	134	fveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) = ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) )
136	135	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) = ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) )
137	136	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ) → ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
138	137	sumeq2dv	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
139		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑁 C 𝑗 ) = ( 𝑁 C 𝑘 ) )
140		oveq2	⊢ ( 𝑗 = 𝑘 → ( 𝑁 − 𝑗 ) = ( 𝑁 − 𝑘 ) )
141	140	oveq2d	⊢ ( 𝑗 = 𝑘 → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) = ( - 1 ↑ ( 𝑁 − 𝑘 ) ) )
142		oveq2	⊢ ( 𝑗 = 𝑘 → ( ( 𝑋 + 1 ) + 𝑗 ) = ( ( 𝑋 + 1 ) + 𝑘 ) )
143	142	fveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) = ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) )
144	141 143	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) )
145	139 144	oveq12d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) )
146	145	cbvsumv	⊢ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) )
147		1zzd	⊢ ( 𝜑 → 1 ∈ ℤ )
148		0zd	⊢ ( 𝜑 → 0 ∈ ℤ )
149		elfzelz	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
150		bccl	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ 𝑗 ∈ ℤ ) → ( 𝑁 C 𝑗 ) ∈ ℕ₀ )
151	150	nn0cnd	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ 𝑗 ∈ ℤ ) → ( 𝑁 C 𝑗 ) ∈ ℂ )
152	1 149 151	syl2an	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑗 ) ∈ ℂ )
153		zsubcl	⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑁 − 𝑗 ) ∈ ℤ )
154	49 149 153	syl2an	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑗 ) ∈ ℤ )
155		m1expcl	⊢ ( ( 𝑁 − 𝑗 ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) ∈ ℤ )
156	154 155	syl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) ∈ ℤ )
157	156	zcnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) ∈ ℂ )
158	3	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
159	4	adantr	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
160		1cnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
161	149	zcnd	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℂ )
162	161	adantl	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ℂ )
163	159 160 162	addassd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑗 ) = ( 𝑋 + ( 1 + 𝑗 ) ) )
164	160 162	addcomd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 + 𝑗 ) = ( 𝑗 + 1 ) )
165	164	oveq2d	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + ( 1 + 𝑗 ) ) = ( 𝑋 + ( 𝑗 + 1 ) ) )
166	163 165	eqtrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑗 ) = ( 𝑋 + ( 𝑗 + 1 ) ) )
167		fzp1elp1	⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
168		oveq2	⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑋 + 𝑘 ) = ( 𝑋 + ( 𝑗 + 1 ) ) )
169	168	eleq1d	⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝑋 + 𝑘 ) ∈ 𝐴 ↔ ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) )
170	169	rspccv	⊢ ( ∀ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( 𝑋 + 𝑘 ) ∈ 𝐴 → ( ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) )
171	110 170	syl	⊢ ( 𝜑 → ( ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) )
172	171	imp	⊢ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 )
173	167 172	sylan2	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 )
174	166 173	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑗 ) ∈ 𝐴 )
175	158 174	ffvelrnd	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ∈ ℂ )
176	157 175	mulcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ∈ ℂ )
177	152 176	mulcld	⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) ∈ ℂ )
178		oveq2	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑁 C 𝑗 ) = ( 𝑁 C ( 𝑘 − 1 ) ) )
179		oveq2	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑁 − 𝑗 ) = ( 𝑁 − ( 𝑘 − 1 ) ) )
180	179	oveq2d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) = ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) )
181		oveq2	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑋 + 1 ) + 𝑗 ) = ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) )
182	181	fveq2d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) = ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) )
183	180 182	oveq12d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) = ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) )
184	178 183	oveq12d	⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) )
185	147 148 49 177 184	fsumshft	⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) )
186	146 185	syl5reqr	⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) )
187	128 138 186	3eqtr2d	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) )
188	1 82	eleqtrdi	⊢ ( 𝜑 → 𝑁 ∈ ( ℤ_≥ ‘ 0 ) )
189		oveq2	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑁 C 𝑘 ) = ( 𝑁 C ( 𝑁 + 1 ) ) )
190		oveq2	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑁 − 𝑘 ) = ( 𝑁 − ( 𝑁 + 1 ) ) )
191	190	oveq2d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( - 1 ↑ ( 𝑁 − 𝑘 ) ) = ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) )
192		oveq2	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝑋 + 𝑘 ) = ( 𝑋 + ( 𝑁 + 1 ) ) )
193	192	fveq2d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) = ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) )
194	191 193	oveq12d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) = ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) )
195	189 194	oveq12d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) )
196	188 75 195	fsump1	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) ) )
197		bcval	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ ( 𝑁 + 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) , 0 ) )
198	1 22 197	syl2anc	⊢ ( 𝜑 → ( 𝑁 C ( 𝑁 + 1 ) ) = if ( ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) , 0 ) )
199		fzp1nel	⊢ ¬ ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 )
200	199	iffalsei	⊢ if ( ( 𝑁 + 1 ) ∈ ( 0 ... 𝑁 ) , ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( ! ‘ ( 𝑁 + 1 ) ) ) ) , 0 ) = 0
201	198 200	eqtrdi	⊢ ( 𝜑 → ( 𝑁 C ( 𝑁 + 1 ) ) = 0 )
202	201	oveq1d	⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) = ( 0 · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) )
203	49 22	zsubcld	⊢ ( 𝜑 → ( 𝑁 − ( 𝑁 + 1 ) ) ∈ ℤ )
204		m1expcl	⊢ ( ( 𝑁 − ( 𝑁 + 1 ) ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) ∈ ℤ )
205	204	zcnd	⊢ ( ( 𝑁 − ( 𝑁 + 1 ) ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) ∈ ℂ )
206	203 205	syl	⊢ ( 𝜑 → ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) ∈ ℂ )
207		eluzfz2	⊢ ( ( 𝑁 + 1 ) ∈ ( ℤ_≥ ‘ 0 ) → ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
208	83 207	syl	⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
209	192	eleq1d	⊢ ( 𝑘 = ( 𝑁 + 1 ) → ( ( 𝑋 + 𝑘 ) ∈ 𝐴 ↔ ( 𝑋 + ( 𝑁 + 1 ) ) ∈ 𝐴 ) )
210	209	rspcv	⊢ ( ( 𝑁 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( ∀ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( 𝑋 + 𝑘 ) ∈ 𝐴 → ( 𝑋 + ( 𝑁 + 1 ) ) ∈ 𝐴 ) )
211	208 110 210	sylc	⊢ ( 𝜑 → ( 𝑋 + ( 𝑁 + 1 ) ) ∈ 𝐴 )
212	3 211	ffvelrnd	⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ∈ ℂ )
213	206 212	mulcld	⊢ ( 𝜑 → ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ∈ ℂ )
214	213	mul02d	⊢ ( 𝜑 → ( 0 · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) = 0 )
215	202 214	eqtrd	⊢ ( 𝜑 → ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) = 0 )
216	215	oveq2d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + ( ( 𝑁 C ( 𝑁 + 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑁 + 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 1 ) ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + 0 ) )
217		fzfid	⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ Fin )
218		fzelp1	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) )
219	218 75	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ ℂ )
220	217 219	fsumcl	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ∈ ℂ )
221	220	addid1d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) + 0 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
222	196 216 221	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
223	187 222	oveq12d	⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) − Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) − Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
224	79 81 223	3eqtrd	⊢ ( 𝜑 → Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) − Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
225	21 2 3 4 5	fwddifnval	⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) △n 𝐹 ) ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( ( ( 𝑁 + 1 ) C 𝑘 ) · ( ( - 1 ↑ ( ( 𝑁 + 1 ) − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
226		peano2cn	⊢ ( 𝑋 ∈ ℂ → ( 𝑋 + 1 ) ∈ ℂ )
227	4 226	syl	⊢ ( 𝜑 → ( 𝑋 + 1 ) ∈ ℂ )
228	4	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
229		1cnd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
230		elfzelz	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℤ )
231	230	zcnd	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → 𝑘 ∈ ℂ )
232	231	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → 𝑘 ∈ ℂ )
233	228 229 232	addassd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑘 ) = ( 𝑋 + ( 1 + 𝑘 ) ) )
234	229 232	addcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 1 + 𝑘 ) = ( 𝑘 + 1 ) )
235	234	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + ( 1 + 𝑘 ) ) = ( 𝑋 + ( 𝑘 + 1 ) ) )
236	233 235	eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑘 ) = ( 𝑋 + ( 𝑘 + 1 ) ) )
237		fzp1elp1	⊢ ( 𝑘 ∈ ( 0 ... 𝑁 ) → ( 𝑘 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
238		oveq1	⊢ ( 𝑗 = 𝑘 → ( 𝑗 + 1 ) = ( 𝑘 + 1 ) )
239	238	eleq1d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ↔ ( 𝑘 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) )
240	239	anbi2d	⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ↔ ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) ) )
241	238	oveq2d	⊢ ( 𝑗 = 𝑘 → ( 𝑋 + ( 𝑗 + 1 ) ) = ( 𝑋 + ( 𝑘 + 1 ) ) )
242	241	eleq1d	⊢ ( 𝑗 = 𝑘 → ( ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ↔ ( 𝑋 + ( 𝑘 + 1 ) ) ∈ 𝐴 ) )
243	240 242	imbi12d	⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) ↔ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + ( 𝑘 + 1 ) ) ∈ 𝐴 ) ) )
244	243 172	chvarvv	⊢ ( ( 𝜑 ∧ ( 𝑘 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + ( 𝑘 + 1 ) ) ∈ 𝐴 )
245	237 244	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + ( 𝑘 + 1 ) ) ∈ 𝐴 )
246	236 245	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑘 ) ∈ 𝐴 )
247	1 2 3 227 246	fwddifnval	⊢ ( 𝜑 → ( ( 𝑁 △n 𝐹 ) ‘ ( 𝑋 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) )
248	218 5	sylan2	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
249	1 2 3 4 248	fwddifnval	⊢ ( 𝜑 → ( ( 𝑁 △n 𝐹 ) ‘ 𝑋 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) )
250	247 249	oveq12d	⊢ ( 𝜑 → ( ( ( 𝑁 △n 𝐹 ) ‘ ( 𝑋 + 1 ) ) − ( ( 𝑁 △n 𝐹 ) ‘ 𝑋 ) ) = ( Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) − Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( 𝑋 + 𝑘 ) ) ) ) ) )
251	224 225 250	3eqtr4d	⊢ ( 𝜑 → ( ( ( 𝑁 + 1 ) △n 𝐹 ) ‘ 𝑋 ) = ( ( ( 𝑁 △n 𝐹 ) ‘ ( 𝑋 + 1 ) ) − ( ( 𝑁 △n 𝐹 ) ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem fwddifnp1

Proof