| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fwddifnp1.1 | . . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 2 |  | elfzelz 13564 | . . . . . . 7
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ) | 
| 3 |  | bcpasc 14360 | . . . . . . 7
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) | 
| 4 | 1, 2, 3 | syl2an 596 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘)) | 
| 5 | 4 | oveq1d 7446 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 6 |  | bccl 14361 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ 𝑘 ∈ ℤ)
→ (𝑁C𝑘) ∈
ℕ0) | 
| 7 | 1, 2, 6 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈
ℕ0) | 
| 8 | 7 | nn0cnd 12589 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈ ℂ) | 
| 9 |  | peano2zm 12660 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈
ℤ) | 
| 10 | 2, 9 | syl 17 | . . . . . . . . . . 11
⊢ (𝑘 ∈ (0...(𝑁 + 1)) → (𝑘 − 1) ∈ ℤ) | 
| 11 |  | bccl 14361 | . . . . . . . . . . 11
⊢ ((𝑁 ∈ ℕ0
∧ (𝑘 − 1) ∈
ℤ) → (𝑁C(𝑘 − 1)) ∈
ℕ0) | 
| 12 | 1, 10, 11 | syl2an 596 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈
ℕ0) | 
| 13 | 12 | nn0cnd 12589 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ) | 
| 14 | 8, 13 | addcomd 11463 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁C(𝑘 − 1)) + (𝑁C𝑘))) | 
| 15 | 14 | oveq1d 7446 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) + (𝑁C𝑘)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 16 |  | peano2nn0 12566 | . . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℕ0
→ (𝑁 + 1) ∈
ℕ0) | 
| 17 | 1, 16 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → (𝑁 + 1) ∈
ℕ0) | 
| 18 | 17 | nn0zd 12639 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 + 1) ∈ ℤ) | 
| 19 |  | zsubcl 12659 | . . . . . . . . . . . 12
⊢ (((𝑁 + 1) ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑁 + 1) − 𝑘) ∈ ℤ) | 
| 20 | 18, 2, 19 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) ∈ ℤ) | 
| 21 |  | m1expcl 14127 | . . . . . . . . . . 11
⊢ (((𝑁 + 1) − 𝑘) ∈ ℤ → (-1↑((𝑁 + 1) − 𝑘)) ∈ ℤ) | 
| 22 | 20, 21 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) ∈ ℤ) | 
| 23 | 22 | zcnd 12723 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) ∈ ℂ) | 
| 24 |  | fwddifnp1.3 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 25 | 24 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝐹:𝐴⟶ℂ) | 
| 26 |  | fwddifnp1.5 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑋 + 𝑘) ∈ 𝐴) | 
| 27 | 25, 26 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐹‘(𝑋 + 𝑘)) ∈ ℂ) | 
| 28 | 23, 27 | mulcld 11281 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) ∈ ℂ) | 
| 29 | 13, 8, 28 | adddird 11286 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) + (𝑁C𝑘)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 30 | 15, 29 | eqtrd 2777 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 31 | 1 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑁 ∈
ℕ0) | 
| 32 | 31 | nn0cnd 12589 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑁 ∈ ℂ) | 
| 33 | 2 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℤ) | 
| 34 | 33 | zcnd 12723 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℂ) | 
| 35 |  | 1cnd 11256 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 1 ∈
ℂ) | 
| 36 | 32, 34, 35 | subsub3d 11650 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) = ((𝑁 + 1) − 𝑘)) | 
| 37 | 36 | eqcomd 2743 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) = (𝑁 − (𝑘 − 1))) | 
| 38 | 37 | oveq2d 7447 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = (-1↑(𝑁 − (𝑘 − 1)))) | 
| 39 | 38 | oveq1d 7446 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) | 
| 40 | 39 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) | 
| 41 | 32, 35, 34 | addsubd 11641 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1)) | 
| 42 | 41 | oveq2d 7447 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = (-1↑((𝑁 − 𝑘) + 1))) | 
| 43 |  | neg1cn 12380 | . . . . . . . . . . . . . . 15
⊢ -1 ∈
ℂ | 
| 44 | 43 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → -1 ∈
ℂ) | 
| 45 |  | neg1ne0 12382 | . . . . . . . . . . . . . . 15
⊢ -1 ≠
0 | 
| 46 | 45 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → -1 ≠ 0) | 
| 47 | 1 | nn0zd 12639 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈ ℤ) | 
| 48 |  | zsubcl 12659 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (𝑁 − 𝑘) ∈ ℤ) | 
| 49 | 47, 2, 48 | syl2an 596 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁 − 𝑘) ∈ ℤ) | 
| 50 | 44, 46, 49 | expp1zd 14195 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 − 𝑘) + 1)) = ((-1↑(𝑁 − 𝑘)) · -1)) | 
| 51 | 42, 50 | eqtrd 2777 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = ((-1↑(𝑁 − 𝑘)) · -1)) | 
| 52 |  | m1expcl 14127 | . . . . . . . . . . . . . . 15
⊢ ((𝑁 − 𝑘) ∈ ℤ → (-1↑(𝑁 − 𝑘)) ∈ ℤ) | 
| 53 | 49, 52 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − 𝑘)) ∈ ℤ) | 
| 54 | 53 | zcnd 12723 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − 𝑘)) ∈ ℂ) | 
| 55 | 54, 44 | mulcomd 11282 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑(𝑁 − 𝑘)) · -1) = (-1 ·
(-1↑(𝑁 − 𝑘)))) | 
| 56 | 54 | mulm1d 11715 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1 · (-1↑(𝑁 − 𝑘))) = -(-1↑(𝑁 − 𝑘))) | 
| 57 | 51, 55, 56 | 3eqtrd 2781 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑((𝑁 + 1) − 𝑘)) = -(-1↑(𝑁 − 𝑘))) | 
| 58 | 57 | oveq1d 7446 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = (-(-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) | 
| 59 | 54, 27 | mulneg1d 11716 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-(-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) | 
| 60 | 58, 59 | eqtrd 2777 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) | 
| 61 | 60 | oveq2d 7447 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C𝑘) · -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 62 | 54, 27 | mulcld 11281 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) ∈ ℂ) | 
| 63 | 8, 62 | mulneg2d 11717 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · -((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 64 | 61, 63 | eqtrd 2777 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 65 | 40, 64 | oveq12d 7449 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) + -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 66 |  | zsubcl 12659 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ (𝑘 − 1) ∈ ℤ)
→ (𝑁 − (𝑘 − 1)) ∈
ℤ) | 
| 67 | 47, 10, 66 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) ∈ ℤ) | 
| 68 |  | m1expcl 14127 | . . . . . . . . . . 11
⊢ ((𝑁 − (𝑘 − 1)) ∈ ℤ →
(-1↑(𝑁 − (𝑘 − 1))) ∈
ℤ) | 
| 69 | 67, 68 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − (𝑘 − 1))) ∈
ℤ) | 
| 70 | 69 | zcnd 12723 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (-1↑(𝑁 − (𝑘 − 1))) ∈
ℂ) | 
| 71 | 70, 27 | mulcld 11281 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))) ∈ ℂ) | 
| 72 | 13, 71 | mulcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) | 
| 73 | 8, 62 | mulcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) | 
| 74 | 72, 73 | negsubd 11626 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) + -((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 75 | 30, 65, 74 | 3eqtrd 2781 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 76 | 5, 75 | eqtr3d 2779 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 77 | 76 | sumeq2dv 15738 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 78 |  | fzfid 14014 | . . . 4
⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin) | 
| 79 | 78, 72, 73 | fsumsub 15824 | . . 3
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 80 |  | nn0uz 12920 | . . . . . . . 8
⊢
ℕ0 = (ℤ≥‘0) | 
| 81 | 17, 80 | eleqtrdi 2851 | . . . . . . 7
⊢ (𝜑 → (𝑁 + 1) ∈
(ℤ≥‘0)) | 
| 82 |  | oveq1 7438 | . . . . . . . . 9
⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1)) | 
| 83 | 82 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑘 = 0 → (𝑁C(𝑘 − 1)) = (𝑁C(0 − 1))) | 
| 84 | 82 | oveq2d 7447 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑁 − (𝑘 − 1)) = (𝑁 − (0 − 1))) | 
| 85 | 84 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑘 = 0 → (-1↑(𝑁 − (𝑘 − 1))) = (-1↑(𝑁 − (0 − 1)))) | 
| 86 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑘 = 0 → (𝑋 + 𝑘) = (𝑋 + 0)) | 
| 87 | 86 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑘 = 0 → (𝐹‘(𝑋 + 𝑘)) = (𝐹‘(𝑋 + 0))) | 
| 88 | 85, 87 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑘 = 0 → ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))) = ((-1↑(𝑁 − (0 − 1))) · (𝐹‘(𝑋 + 0)))) | 
| 89 | 83, 88 | oveq12d 7449 | . . . . . . 7
⊢ (𝑘 = 0 → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0))))) | 
| 90 | 81, 72, 89 | fsum1p 15789 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = (((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 91 |  | df-neg 11495 | . . . . . . . . . . 11
⊢ -1 = (0
− 1) | 
| 92 | 91 | oveq2i 7442 | . . . . . . . . . 10
⊢ (𝑁C-1) = (𝑁C(0 − 1)) | 
| 93 |  | bcneg1 35736 | . . . . . . . . . . 11
⊢ (𝑁 ∈ ℕ0
→ (𝑁C-1) =
0) | 
| 94 | 1, 93 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁C-1) = 0) | 
| 95 | 92, 94 | eqtr3id 2791 | . . . . . . . . 9
⊢ (𝜑 → (𝑁C(0 − 1)) = 0) | 
| 96 | 95 | oveq1d 7446 | . . . . . . . 8
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) = (0 ·
((-1↑(𝑁 − (0
− 1))) · (𝐹‘(𝑋 + 0))))) | 
| 97 |  | 0z 12624 | . . . . . . . . . . . . . . 15
⊢ 0 ∈
ℤ | 
| 98 |  | 1z 12647 | . . . . . . . . . . . . . . 15
⊢ 1 ∈
ℤ | 
| 99 |  | zsubcl 12659 | . . . . . . . . . . . . . . 15
⊢ ((0
∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈
ℤ) | 
| 100 | 97, 98, 99 | mp2an 692 | . . . . . . . . . . . . . 14
⊢ (0
− 1) ∈ ℤ | 
| 101 | 100 | a1i 11 | . . . . . . . . . . . . 13
⊢ (𝜑 → (0 − 1) ∈
ℤ) | 
| 102 | 47, 101 | zsubcld 12727 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑁 − (0 − 1)) ∈
ℤ) | 
| 103 |  | m1expcl 14127 | . . . . . . . . . . . 12
⊢ ((𝑁 − (0 − 1)) ∈
ℤ → (-1↑(𝑁
− (0 − 1))) ∈ ℤ) | 
| 104 | 102, 103 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (-1↑(𝑁 − (0 − 1))) ∈
ℤ) | 
| 105 | 104 | zcnd 12723 | . . . . . . . . . 10
⊢ (𝜑 → (-1↑(𝑁 − (0 − 1))) ∈
ℂ) | 
| 106 |  | eluzfz1 13571 | . . . . . . . . . . . . 13
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → 0 ∈ (0...(𝑁 + 1))) | 
| 107 | 81, 106 | syl 17 | . . . . . . . . . . . 12
⊢ (𝜑 → 0 ∈ (0...(𝑁 + 1))) | 
| 108 | 26 | ralrimiva 3146 | . . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑘 ∈ (0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴) | 
| 109 | 86 | eleq1d 2826 | . . . . . . . . . . . . 13
⊢ (𝑘 = 0 → ((𝑋 + 𝑘) ∈ 𝐴 ↔ (𝑋 + 0) ∈ 𝐴)) | 
| 110 | 109 | rspcva 3620 | . . . . . . . . . . . 12
⊢ ((0
∈ (0...(𝑁 + 1)) ∧
∀𝑘 ∈
(0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴) → (𝑋 + 0) ∈ 𝐴) | 
| 111 | 107, 108,
110 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑋 + 0) ∈ 𝐴) | 
| 112 | 24, 111 | ffvelcdmd 7105 | . . . . . . . . . 10
⊢ (𝜑 → (𝐹‘(𝑋 + 0)) ∈ ℂ) | 
| 113 | 105, 112 | mulcld 11281 | . . . . . . . . 9
⊢ (𝜑 → ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0))) ∈
ℂ) | 
| 114 | 113 | mul02d 11459 | . . . . . . . 8
⊢ (𝜑 → (0 ·
((-1↑(𝑁 − (0
− 1))) · (𝐹‘(𝑋 + 0)))) = 0) | 
| 115 | 96, 114 | eqtrd 2777 | . . . . . . 7
⊢ (𝜑 → ((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) = 0) | 
| 116 | 115 | oveq1d 7446 | . . . . . 6
⊢ (𝜑 → (((𝑁C(0 − 1)) · ((-1↑(𝑁 − (0 − 1)))
· (𝐹‘(𝑋 + 0)))) + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) = (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 117 |  | fzfid 14014 | . . . . . . . 8
⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) ∈
Fin) | 
| 118 |  | olc 869 | . . . . . . . . . 10
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1)))) | 
| 119 |  | elfzp12 13643 | . . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (𝑘 ∈ (0...(𝑁 + 1)) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))))) | 
| 120 | 81, 119 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ (0...(𝑁 + 1)) ↔ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))))) | 
| 121 | 120 | biimpar 477 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑘 = 0 ∨ 𝑘 ∈ ((0 + 1)...(𝑁 + 1)))) → 𝑘 ∈ (0...(𝑁 + 1))) | 
| 122 | 118, 121 | sylan2 593 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1))) | 
| 123 | 122, 72 | syldan 591 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) | 
| 124 | 117, 123 | fsumcl 15769 | . . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) | 
| 125 | 124 | addlidd 11462 | . . . . . 6
⊢ (𝜑 → (0 + Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) | 
| 126 | 90, 116, 125 | 3eqtrd 2781 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) | 
| 127 |  | fwddifnp1.4 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 128 | 127 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑋 ∈ ℂ) | 
| 129 |  | 1cnd 11256 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈
ℂ) | 
| 130 |  | elfzelz 13564 | . . . . . . . . . . . 12
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℤ) | 
| 131 | 130 | zcnd 12723 | . . . . . . . . . . 11
⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℂ) | 
| 132 | 131 | adantl 481 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℂ) | 
| 133 | 128, 129,
132 | ppncand 11660 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑋 + 1) + (𝑘 − 1)) = (𝑋 + 𝑘)) | 
| 134 | 133 | fveq2d 6910 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐹‘((𝑋 + 1) + (𝑘 − 1))) = (𝐹‘(𝑋 + 𝑘))) | 
| 135 | 134 | oveq2d 7447 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1)))) = ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) | 
| 136 | 135 | oveq2d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) = ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) | 
| 137 | 136 | sumeq2dv 15738 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘))))) | 
| 138 |  | 1zzd 12648 | . . . . . . 7
⊢ (𝜑 → 1 ∈
ℤ) | 
| 139 |  | 0zd 12625 | . . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) | 
| 140 |  | elfzelz 13564 | . . . . . . . . 9
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℤ) | 
| 141 |  | bccl 14361 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ 𝑗 ∈ ℤ)
→ (𝑁C𝑗) ∈
ℕ0) | 
| 142 | 141 | nn0cnd 12589 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑗 ∈ ℤ)
→ (𝑁C𝑗) ∈
ℂ) | 
| 143 | 1, 140, 142 | syl2an 596 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑁C𝑗) ∈ ℂ) | 
| 144 |  | zsubcl 12659 | . . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℤ ∧ 𝑗 ∈ ℤ) → (𝑁 − 𝑗) ∈ ℤ) | 
| 145 | 47, 140, 144 | syl2an 596 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑁 − 𝑗) ∈ ℤ) | 
| 146 |  | m1expcl 14127 | . . . . . . . . . . 11
⊢ ((𝑁 − 𝑗) ∈ ℤ → (-1↑(𝑁 − 𝑗)) ∈ ℤ) | 
| 147 | 145, 146 | syl 17 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (-1↑(𝑁 − 𝑗)) ∈ ℤ) | 
| 148 | 147 | zcnd 12723 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (-1↑(𝑁 − 𝑗)) ∈ ℂ) | 
| 149 | 24 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝐹:𝐴⟶ℂ) | 
| 150 | 127 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑋 ∈ ℂ) | 
| 151 |  | 1cnd 11256 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 1 ∈ ℂ) | 
| 152 | 140 | zcnd 12723 | . . . . . . . . . . . . . 14
⊢ (𝑗 ∈ (0...𝑁) → 𝑗 ∈ ℂ) | 
| 153 | 152 | adantl 481 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → 𝑗 ∈ ℂ) | 
| 154 | 150, 151,
153 | addassd 11283 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑗) = (𝑋 + (1 + 𝑗))) | 
| 155 | 151, 153 | addcomd 11463 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (1 + 𝑗) = (𝑗 + 1)) | 
| 156 | 155 | oveq2d 7447 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋 + (1 + 𝑗)) = (𝑋 + (𝑗 + 1))) | 
| 157 | 154, 156 | eqtrd 2777 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑗) = (𝑋 + (𝑗 + 1))) | 
| 158 |  | fzp1elp1 13617 | . . . . . . . . . . . 12
⊢ (𝑗 ∈ (0...𝑁) → (𝑗 + 1) ∈ (0...(𝑁 + 1))) | 
| 159 |  | oveq2 7439 | . . . . . . . . . . . . . . . 16
⊢ (𝑘 = (𝑗 + 1) → (𝑋 + 𝑘) = (𝑋 + (𝑗 + 1))) | 
| 160 | 159 | eleq1d 2826 | . . . . . . . . . . . . . . 15
⊢ (𝑘 = (𝑗 + 1) → ((𝑋 + 𝑘) ∈ 𝐴 ↔ (𝑋 + (𝑗 + 1)) ∈ 𝐴)) | 
| 161 | 160 | rspccv 3619 | . . . . . . . . . . . . . 14
⊢
(∀𝑘 ∈
(0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴 → ((𝑗 + 1) ∈ (0...(𝑁 + 1)) → (𝑋 + (𝑗 + 1)) ∈ 𝐴)) | 
| 162 | 108, 161 | syl 17 | . . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑗 + 1) ∈ (0...(𝑁 + 1)) → (𝑋 + (𝑗 + 1)) ∈ 𝐴)) | 
| 163 | 162 | imp 406 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑗 + 1)) ∈ 𝐴) | 
| 164 | 158, 163 | sylan2 593 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝑋 + (𝑗 + 1)) ∈ 𝐴) | 
| 165 | 157, 164 | eqeltrd 2841 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑗) ∈ 𝐴) | 
| 166 | 149, 165 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → (𝐹‘((𝑋 + 1) + 𝑗)) ∈ ℂ) | 
| 167 | 148, 166 | mulcld 11281 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗))) ∈ ℂ) | 
| 168 | 143, 167 | mulcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ (0...𝑁)) → ((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) ∈ ℂ) | 
| 169 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑗 = (𝑘 − 1) → (𝑁C𝑗) = (𝑁C(𝑘 − 1))) | 
| 170 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑗 = (𝑘 − 1) → (𝑁 − 𝑗) = (𝑁 − (𝑘 − 1))) | 
| 171 | 170 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 − 1) → (-1↑(𝑁 − 𝑗)) = (-1↑(𝑁 − (𝑘 − 1)))) | 
| 172 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑗 = (𝑘 − 1) → ((𝑋 + 1) + 𝑗) = ((𝑋 + 1) + (𝑘 − 1))) | 
| 173 | 172 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑗 = (𝑘 − 1) → (𝐹‘((𝑋 + 1) + 𝑗)) = (𝐹‘((𝑋 + 1) + (𝑘 − 1)))) | 
| 174 | 171, 173 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑗 = (𝑘 − 1) → ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗))) = ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) | 
| 175 | 169, 174 | oveq12d 7449 | . . . . . . 7
⊢ (𝑗 = (𝑘 − 1) → ((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = ((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1)))))) | 
| 176 | 138, 139,
47, 168, 175 | fsumshft 15816 | . . . . . 6
⊢ (𝜑 → Σ𝑗 ∈ (0...𝑁)((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1)))))) | 
| 177 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → (𝑁C𝑗) = (𝑁C𝑘)) | 
| 178 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑁 − 𝑗) = (𝑁 − 𝑘)) | 
| 179 | 178 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → (-1↑(𝑁 − 𝑗)) = (-1↑(𝑁 − 𝑘))) | 
| 180 |  | oveq2 7439 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → ((𝑋 + 1) + 𝑗) = ((𝑋 + 1) + 𝑘)) | 
| 181 | 180 | fveq2d 6910 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝐹‘((𝑋 + 1) + 𝑗)) = (𝐹‘((𝑋 + 1) + 𝑘))) | 
| 182 | 179, 181 | oveq12d 7449 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗))) = ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) | 
| 183 | 177, 182 | oveq12d 7449 | . . . . . . 7
⊢ (𝑗 = 𝑘 → ((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) | 
| 184 | 183 | cbvsumv 15732 | . . . . . 6
⊢
Σ𝑗 ∈
(0...𝑁)((𝑁C𝑗) · ((-1↑(𝑁 − 𝑗)) · (𝐹‘((𝑋 + 1) + 𝑗)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) | 
| 185 | 176, 184 | eqtr3di 2792 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘((𝑋 + 1) + (𝑘 − 1))))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) | 
| 186 | 126, 137,
185 | 3eqtr2d 2783 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) | 
| 187 | 1, 80 | eleqtrdi 2851 | . . . . . 6
⊢ (𝜑 → 𝑁 ∈
(ℤ≥‘0)) | 
| 188 |  | oveq2 7439 | . . . . . . 7
⊢ (𝑘 = (𝑁 + 1) → (𝑁C𝑘) = (𝑁C(𝑁 + 1))) | 
| 189 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑁 − 𝑘) = (𝑁 − (𝑁 + 1))) | 
| 190 | 189 | oveq2d 7447 | . . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → (-1↑(𝑁 − 𝑘)) = (-1↑(𝑁 − (𝑁 + 1)))) | 
| 191 |  | oveq2 7439 | . . . . . . . . 9
⊢ (𝑘 = (𝑁 + 1) → (𝑋 + 𝑘) = (𝑋 + (𝑁 + 1))) | 
| 192 | 191 | fveq2d 6910 | . . . . . . . 8
⊢ (𝑘 = (𝑁 + 1) → (𝐹‘(𝑋 + 𝑘)) = (𝐹‘(𝑋 + (𝑁 + 1)))) | 
| 193 | 190, 192 | oveq12d 7449 | . . . . . . 7
⊢ (𝑘 = (𝑁 + 1) → ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))) = ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) | 
| 194 | 188, 193 | oveq12d 7449 | . . . . . 6
⊢ (𝑘 = (𝑁 + 1) → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))))) | 
| 195 | 187, 73, 194 | fsump1 15792 | . . . . 5
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))))) | 
| 196 |  | bcval 14343 | . . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ0
∧ (𝑁 + 1) ∈
ℤ) → (𝑁C(𝑁 + 1)) = if((𝑁 + 1) ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − (𝑁 + 1))) · (!‘(𝑁 + 1)))), 0)) | 
| 197 | 1, 18, 196 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = if((𝑁 + 1) ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − (𝑁 + 1))) · (!‘(𝑁 + 1)))), 0)) | 
| 198 |  | fzp1nel 13651 | . . . . . . . . . 10
⊢  ¬
(𝑁 + 1) ∈ (0...𝑁) | 
| 199 | 198 | iffalsei 4535 | . . . . . . . . 9
⊢ if((𝑁 + 1) ∈ (0...𝑁), ((!‘𝑁) / ((!‘(𝑁 − (𝑁 + 1))) · (!‘(𝑁 + 1)))), 0) = 0 | 
| 200 | 197, 199 | eqtrdi 2793 | . . . . . . . 8
⊢ (𝜑 → (𝑁C(𝑁 + 1)) = 0) | 
| 201 | 200 | oveq1d 7446 | . . . . . . 7
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) = (0 · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))))) | 
| 202 | 47, 18 | zsubcld 12727 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁 − (𝑁 + 1)) ∈ ℤ) | 
| 203 |  | m1expcl 14127 | . . . . . . . . . . 11
⊢ ((𝑁 − (𝑁 + 1)) ∈ ℤ → (-1↑(𝑁 − (𝑁 + 1))) ∈ ℤ) | 
| 204 | 203 | zcnd 12723 | . . . . . . . . . 10
⊢ ((𝑁 − (𝑁 + 1)) ∈ ℤ → (-1↑(𝑁 − (𝑁 + 1))) ∈ ℂ) | 
| 205 | 202, 204 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (-1↑(𝑁 − (𝑁 + 1))) ∈ ℂ) | 
| 206 |  | eluzfz2 13572 | . . . . . . . . . . . 12
⊢ ((𝑁 + 1) ∈
(ℤ≥‘0) → (𝑁 + 1) ∈ (0...(𝑁 + 1))) | 
| 207 | 81, 206 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁 + 1) ∈ (0...(𝑁 + 1))) | 
| 208 | 191 | eleq1d 2826 | . . . . . . . . . . . 12
⊢ (𝑘 = (𝑁 + 1) → ((𝑋 + 𝑘) ∈ 𝐴 ↔ (𝑋 + (𝑁 + 1)) ∈ 𝐴)) | 
| 209 | 208 | rspcv 3618 | . . . . . . . . . . 11
⊢ ((𝑁 + 1) ∈ (0...(𝑁 + 1)) → (∀𝑘 ∈ (0...(𝑁 + 1))(𝑋 + 𝑘) ∈ 𝐴 → (𝑋 + (𝑁 + 1)) ∈ 𝐴)) | 
| 210 | 207, 108,
209 | sylc 65 | . . . . . . . . . 10
⊢ (𝜑 → (𝑋 + (𝑁 + 1)) ∈ 𝐴) | 
| 211 | 24, 210 | ffvelcdmd 7105 | . . . . . . . . 9
⊢ (𝜑 → (𝐹‘(𝑋 + (𝑁 + 1))) ∈ ℂ) | 
| 212 | 205, 211 | mulcld 11281 | . . . . . . . 8
⊢ (𝜑 → ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))) ∈ ℂ) | 
| 213 | 212 | mul02d 11459 | . . . . . . 7
⊢ (𝜑 → (0 ·
((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) = 0) | 
| 214 | 201, 213 | eqtrd 2777 | . . . . . 6
⊢ (𝜑 → ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1))))) = 0) | 
| 215 | 214 | oveq2d 7447 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + ((𝑁C(𝑁 + 1)) · ((-1↑(𝑁 − (𝑁 + 1))) · (𝐹‘(𝑋 + (𝑁 + 1)))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + 0)) | 
| 216 |  | fzfid 14014 | . . . . . . 7
⊢ (𝜑 → (0...𝑁) ∈ Fin) | 
| 217 |  | fzelp1 13616 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ (0...(𝑁 + 1))) | 
| 218 | 217, 73 | sylan2 593 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) | 
| 219 | 216, 218 | fsumcl 15769 | . . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ ℂ) | 
| 220 | 219 | addridd 11461 | . . . . 5
⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) + 0) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 221 | 195, 215,
220 | 3eqtrd 2781 | . . . 4
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 222 | 186, 221 | oveq12d 7449 | . . 3
⊢ (𝜑 → (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((-1↑(𝑁 − (𝑘 − 1))) · (𝐹‘(𝑋 + 𝑘)))) − Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) − Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 223 | 77, 79, 222 | 3eqtrd 2781 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) − Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 224 |  | fwddifnp1.2 | . . 3
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 225 | 17, 224, 24, 127, 26 | fwddifnval 36164 | . 2
⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((-1↑((𝑁 + 1) − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 226 |  | peano2cn 11433 | . . . . 5
⊢ (𝑋 ∈ ℂ → (𝑋 + 1) ∈
ℂ) | 
| 227 | 127, 226 | syl 17 | . . . 4
⊢ (𝜑 → (𝑋 + 1) ∈ ℂ) | 
| 228 | 127 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑋 ∈ ℂ) | 
| 229 |  | 1cnd 11256 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ) | 
| 230 |  | elfzelz 13564 | . . . . . . . . 9
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ) | 
| 231 | 230 | zcnd 12723 | . . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℂ) | 
| 232 | 231 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ) | 
| 233 | 228, 229,
232 | addassd 11283 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑘) = (𝑋 + (1 + 𝑘))) | 
| 234 | 229, 232 | addcomd 11463 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (1 + 𝑘) = (𝑘 + 1)) | 
| 235 | 234 | oveq2d 7447 | . . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + (1 + 𝑘)) = (𝑋 + (𝑘 + 1))) | 
| 236 | 233, 235 | eqtrd 2777 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑘) = (𝑋 + (𝑘 + 1))) | 
| 237 |  | fzp1elp1 13617 | . . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → (𝑘 + 1) ∈ (0...(𝑁 + 1))) | 
| 238 |  | oveq1 7438 | . . . . . . . . . 10
⊢ (𝑗 = 𝑘 → (𝑗 + 1) = (𝑘 + 1)) | 
| 239 | 238 | eleq1d 2826 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → ((𝑗 + 1) ∈ (0...(𝑁 + 1)) ↔ (𝑘 + 1) ∈ (0...(𝑁 + 1)))) | 
| 240 | 239 | anbi2d 630 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → ((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 + 1))) ↔ (𝜑 ∧ (𝑘 + 1) ∈ (0...(𝑁 + 1))))) | 
| 241 | 238 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝑗 = 𝑘 → (𝑋 + (𝑗 + 1)) = (𝑋 + (𝑘 + 1))) | 
| 242 | 241 | eleq1d 2826 | . . . . . . . 8
⊢ (𝑗 = 𝑘 → ((𝑋 + (𝑗 + 1)) ∈ 𝐴 ↔ (𝑋 + (𝑘 + 1)) ∈ 𝐴)) | 
| 243 | 240, 242 | imbi12d 344 | . . . . . . 7
⊢ (𝑗 = 𝑘 → (((𝜑 ∧ (𝑗 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑗 + 1)) ∈ 𝐴) ↔ ((𝜑 ∧ (𝑘 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑘 + 1)) ∈ 𝐴))) | 
| 244 | 243, 163 | chvarvv 1998 | . . . . . 6
⊢ ((𝜑 ∧ (𝑘 + 1) ∈ (0...(𝑁 + 1))) → (𝑋 + (𝑘 + 1)) ∈ 𝐴) | 
| 245 | 237, 244 | sylan2 593 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + (𝑘 + 1)) ∈ 𝐴) | 
| 246 | 236, 245 | eqeltrd 2841 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑋 + 1) + 𝑘) ∈ 𝐴) | 
| 247 | 1, 224, 24, 227, 246 | fwddifnval 36164 | . . 3
⊢ (𝜑 → ((𝑁 △n 𝐹)‘(𝑋 + 1)) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘))))) | 
| 248 | 217, 26 | sylan2 593 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴) | 
| 249 | 1, 224, 24, 127, 248 | fwddifnval 36164 | . . 3
⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 250 | 247, 249 | oveq12d 7449 | . 2
⊢ (𝜑 → (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋)) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘((𝑋 + 1) + 𝑘)))) − Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))))) | 
| 251 | 223, 225,
250 | 3eqtr4d 2787 | 1
⊢ (𝜑 → (((𝑁 + 1) △n 𝐹)‘𝑋) = (((𝑁 △n 𝐹)‘(𝑋 + 1)) − ((𝑁 △n 𝐹)‘𝑋))) |