Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
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 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 fwddifnp1.2 ⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
3 fwddifnp1.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
4 fwddifnp1.4 ⊢ ( 𝜑 → 𝑋 ∈ ℂ )
5 fwddifnp1.5 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + 𝑘 ) ∈ 𝐴 )
6 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → 𝑘 ∈ ℤ )
7 bcpasc ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( ( 𝑁 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 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑘 ∈ ℤ ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
11 1 6 10 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℕ0 )
12 11 nn0cnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C 𝑘 ) ∈ ℂ )
13 peano2zm ⊢ ( 𝑘 ∈ ℤ → ( 𝑘 − 1 ) ∈ ℤ )
14 6 13 syl ⊢ ( 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑘 − 1 ) ∈ ℤ )
15 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑘 − 1 ) ∈ ℤ ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
16 1 14 15 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑁 C ( 𝑘 − 1 ) ) ∈ ℕ0 )
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 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 + 1 ) ∈ ℕ0 )
21 1 20 syl ⊢ ( 𝜑 → ( 𝑁 + 1 ) ∈ ℕ0 )
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 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 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 ) ) ) → 𝑁 ∈ ℕ0 )
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 = ( ℤ≥ ‘ 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 ⊢ ( 𝑁 ∈ ℕ0 → ( 𝑁 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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + 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 addlidd ⊢ ( 𝜑 → ( 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 1zzd ⊢ ( 𝜑 → 1 ∈ ℤ )
140 0zd ⊢ ( 𝜑 → 0 ∈ ℤ )
141 elfzelz ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℤ )
142 bccl ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( 𝑁 C 𝑗 ) ∈ ℕ0 )
143 142 nn0cnd ⊢ ( ( 𝑁 ∈ ℕ0 ∧ 𝑗 ∈ ℤ ) → ( 𝑁 C 𝑗 ) ∈ ℂ )
144 1 141 143 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 C 𝑗 ) ∈ ℂ )
145 zsubcl ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ ) → ( 𝑁 − 𝑗 ) ∈ ℤ )
146 49 141 145 syl2an ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑁 − 𝑗 ) ∈ ℤ )
147 m1expcl ⊢ ( ( 𝑁 − 𝑗 ) ∈ ℤ → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) ∈ ℤ )
148 146 147 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) ∈ ℤ )
149 148 zcnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) ∈ ℂ )
150 3 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝐹 : 𝐴 ⟶ ℂ )
151 4 adantr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑋 ∈ ℂ )
152 1cnd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 1 ∈ ℂ )
153 141 zcnd ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → 𝑗 ∈ ℂ )
154 153 adantl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → 𝑗 ∈ ℂ )
155 151 152 154 addassd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑗 ) = ( 𝑋 + ( 1 + 𝑗 ) ) )
156 152 154 addcomd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 1 + 𝑗 ) = ( 𝑗 + 1 ) )
157 156 oveq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + ( 1 + 𝑗 ) ) = ( 𝑋 + ( 𝑗 + 1 ) ) )
158 155 157 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑗 ) = ( 𝑋 + ( 𝑗 + 1 ) ) )
159 fzp1elp1 ⊢ ( 𝑗 ∈ ( 0 ... 𝑁 ) → ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) )
160 oveq2 ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( 𝑋 + 𝑘 ) = ( 𝑋 + ( 𝑗 + 1 ) ) )
161 160 eleq1d ⊢ ( 𝑘 = ( 𝑗 + 1 ) → ( ( 𝑋 + 𝑘 ) ∈ 𝐴 ↔ ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) )
162 161 rspccv ⊢ ( ∀ 𝑘 ∈ ( 0 ... ( 𝑁 + 1 ) ) ( 𝑋 + 𝑘 ) ∈ 𝐴 → ( ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) )
163 110 162 syl ⊢ ( 𝜑 → ( ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 ) )
164 163 imp ⊢ ( ( 𝜑 ∧ ( 𝑗 + 1 ) ∈ ( 0 ... ( 𝑁 + 1 ) ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 )
165 159 164 sylan2 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝑋 + ( 𝑗 + 1 ) ) ∈ 𝐴 )
166 158 165 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑋 + 1 ) + 𝑗 ) ∈ 𝐴 )
167 150 166 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ∈ ℂ )
168 149 167 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ∈ ℂ )
169 144 168 mulcld ⊢ ( ( 𝜑 ∧ 𝑗 ∈ ( 0 ... 𝑁 ) ) → ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) ∈ ℂ )
170 oveq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑁 C 𝑗 ) = ( 𝑁 C ( 𝑘 − 1 ) ) )
171 oveq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝑁 − 𝑗 ) = ( 𝑁 − ( 𝑘 − 1 ) ) )
172 171 oveq2d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) = ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) )
173 oveq2 ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑋 + 1 ) + 𝑗 ) = ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) )
174 173 fveq2d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) = ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) )
175 172 174 oveq12d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) = ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) )
176 170 175 oveq12d ⊢ ( 𝑗 = ( 𝑘 − 1 ) → ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) )
177 139 140 49 169 176 fsumshft ⊢ ( 𝜑 → Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = Σ 𝑘 ∈ ( ( 0 + 1 ) ... ( 𝑁 + 1 ) ) ( ( 𝑁 C ( 𝑘 − 1 ) ) · ( ( - 1 ↑ ( 𝑁 − ( 𝑘 − 1 ) ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + ( 𝑘 − 1 ) ) ) ) ) )
178 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑁 C 𝑗 ) = ( 𝑁 C 𝑘 ) )
179 oveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝑁 − 𝑗 ) = ( 𝑁 − 𝑘 ) )
180 179 oveq2d ⊢ ( 𝑗 = 𝑘 → ( - 1 ↑ ( 𝑁 − 𝑗 ) ) = ( - 1 ↑ ( 𝑁 − 𝑘 ) ) )
181 oveq2 ⊢ ( 𝑗 = 𝑘 → ( ( 𝑋 + 1 ) + 𝑗 ) = ( ( 𝑋 + 1 ) + 𝑘 ) )
182 181 fveq2d ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) = ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) )
183 180 182 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) = ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) )
184 178 183 oveq12d ⊢ ( 𝑗 = 𝑘 → ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) ) )
185 184 cbvsumv ⊢ Σ 𝑗 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑗 ) · ( ( - 1 ↑ ( 𝑁 − 𝑗 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑗 ) ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( - 1 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐹 ‘ ( ( 𝑋 + 1 ) + 𝑘 ) ) ) )
186 177 185 eqtr3di ⊢ ( 𝜑 → Σ 𝑘 ∈ ( ( 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 ⊢ ( ( 𝑁 ∈ ℕ0 ∧ ( 𝑁 + 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 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝑋 + ( 𝑁 + 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 addridd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 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 164 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 𝐹 ) ‘ 𝑋 ) ) )