| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-fwddifn 36163 | . . . 4
⊢ 
△n = (𝑛
∈ ℕ0, 𝑓 ∈ (ℂ ↑pm ℂ)
↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣
∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))))) | 
| 2 | 1 | a1i 11 | . . 3
⊢ (𝜑 → △n =
(𝑛 ∈
ℕ0, 𝑓
∈ (ℂ ↑pm ℂ) ↦ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))))) | 
| 3 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑛 = 𝑁 → (0...𝑛) = (0...𝑁)) | 
| 4 | 3 | adantr 480 | . . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → (0...𝑛) = (0...𝑁)) | 
| 5 |  | dmeq 5913 | . . . . . . . . 9
⊢ (𝑓 = 𝐹 → dom 𝑓 = dom 𝐹) | 
| 6 | 5 | eleq2d 2826 | . . . . . . . 8
⊢ (𝑓 = 𝐹 → ((𝑦 + 𝑘) ∈ dom 𝑓 ↔ (𝑦 + 𝑘) ∈ dom 𝐹)) | 
| 7 | 6 | adantl 481 | . . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → ((𝑦 + 𝑘) ∈ dom 𝑓 ↔ (𝑦 + 𝑘) ∈ dom 𝐹)) | 
| 8 | 4, 7 | raleqbidv 3345 | . . . . . 6
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → (∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓 ↔ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹)) | 
| 9 | 8 | rabbidv 3443 | . . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} = {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹}) | 
| 10 |  | oveq1 7439 | . . . . . . . . 9
⊢ (𝑛 = 𝑁 → (𝑛C𝑘) = (𝑁C𝑘)) | 
| 11 | 10 | adantr 480 | . . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → (𝑛C𝑘) = (𝑁C𝑘)) | 
| 12 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (𝑛 − 𝑘) = (𝑁 − 𝑘)) | 
| 13 | 12 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑛 = 𝑁 → (-1↑(𝑛 − 𝑘)) = (-1↑(𝑁 − 𝑘))) | 
| 14 |  | fveq1 6904 | . . . . . . . . 9
⊢ (𝑓 = 𝐹 → (𝑓‘(𝑥 + 𝑘)) = (𝐹‘(𝑥 + 𝑘))) | 
| 15 | 13, 14 | oveqan12d 7451 | . . . . . . . 8
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))) = ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))) | 
| 16 | 11, 15 | oveq12d 7450 | . . . . . . 7
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → ((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))) = ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘))))) | 
| 17 | 16 | adantr 480 | . . . . . 6
⊢ (((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) ∧ 𝑘 ∈ (0...𝑛)) → ((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))) = ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘))))) | 
| 18 | 4, 17 | sumeq12dv 15743 | . . . . 5
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘))))) | 
| 19 | 9, 18 | mpteq12dv 5232 | . . . 4
⊢ ((𝑛 = 𝑁 ∧ 𝑓 = 𝐹) → (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹} ↦ Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))))) | 
| 20 | 19 | adantl 481 | . . 3
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑓 = 𝐹)) → (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑛)(𝑦 + 𝑘) ∈ dom 𝑓} ↦ Σ𝑘 ∈ (0...𝑛)((𝑛C𝑘) · ((-1↑(𝑛 − 𝑘)) · (𝑓‘(𝑥 + 𝑘))))) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹} ↦ Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))))) | 
| 21 |  | fwddifnval.1 | . . 3
⊢ (𝜑 → 𝑁 ∈
ℕ0) | 
| 22 |  | fwddifnval.3 | . . . 4
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) | 
| 23 |  | fwddifnval.2 | . . . 4
⊢ (𝜑 → 𝐴 ⊆ ℂ) | 
| 24 |  | cnex 11237 | . . . . 5
⊢ ℂ
∈ V | 
| 25 |  | elpm2r 8886 | . . . . 5
⊢
(((ℂ ∈ V ∧ ℂ ∈ V) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ)) → 𝐹 ∈ (ℂ ↑pm
ℂ)) | 
| 26 | 24, 24, 25 | mpanl12 702 | . . . 4
⊢ ((𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ ℂ) → 𝐹 ∈ (ℂ ↑pm
ℂ)) | 
| 27 | 22, 23, 26 | syl2anc 584 | . . 3
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
ℂ)) | 
| 28 | 24 | mptrabex 7246 | . . . 4
⊢ (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹} ↦ Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘))))) ∈ V | 
| 29 | 28 | a1i 11 | . . 3
⊢ (𝜑 → (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹} ↦ Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘))))) ∈ V) | 
| 30 | 2, 20, 21, 27, 29 | ovmpod 7586 | . 2
⊢ (𝜑 → (𝑁 △n 𝐹) = (𝑥 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹} ↦ Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))))) | 
| 31 |  | fvoveq1 7455 | . . . . . 6
⊢ (𝑥 = 𝑋 → (𝐹‘(𝑥 + 𝑘)) = (𝐹‘(𝑋 + 𝑘))) | 
| 32 | 31 | oveq2d 7448 | . . . . 5
⊢ (𝑥 = 𝑋 → ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘))) = ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) | 
| 33 | 32 | oveq2d 7448 | . . . 4
⊢ (𝑥 = 𝑋 → ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))) = ((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 34 | 33 | sumeq2sdv 15740 | . . 3
⊢ (𝑥 = 𝑋 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 35 | 34 | adantl 481 | . 2
⊢ ((𝜑 ∧ 𝑥 = 𝑋) → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑥 + 𝑘)))) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) | 
| 36 |  | fwddifnval.4 | . . 3
⊢ (𝜑 → 𝑋 ∈ ℂ) | 
| 37 |  | fwddifnval.5 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ 𝐴) | 
| 38 | 22 | fdmd 6745 | . . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) | 
| 39 | 38 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom 𝐹 = 𝐴) | 
| 40 | 37, 39 | eleqtrrd 2843 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑋 + 𝑘) ∈ dom 𝐹) | 
| 41 | 40 | ralrimiva 3145 | . . 3
⊢ (𝜑 → ∀𝑘 ∈ (0...𝑁)(𝑋 + 𝑘) ∈ dom 𝐹) | 
| 42 |  | oveq1 7439 | . . . . . 6
⊢ (𝑦 = 𝑋 → (𝑦 + 𝑘) = (𝑋 + 𝑘)) | 
| 43 | 42 | eleq1d 2825 | . . . . 5
⊢ (𝑦 = 𝑋 → ((𝑦 + 𝑘) ∈ dom 𝐹 ↔ (𝑋 + 𝑘) ∈ dom 𝐹)) | 
| 44 | 43 | ralbidv 3177 | . . . 4
⊢ (𝑦 = 𝑋 → (∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹 ↔ ∀𝑘 ∈ (0...𝑁)(𝑋 + 𝑘) ∈ dom 𝐹)) | 
| 45 | 44 | elrab 3691 | . . 3
⊢ (𝑋 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹} ↔ (𝑋 ∈ ℂ ∧ ∀𝑘 ∈ (0...𝑁)(𝑋 + 𝑘) ∈ dom 𝐹)) | 
| 46 | 36, 41, 45 | sylanbrc 583 | . 2
⊢ (𝜑 → 𝑋 ∈ {𝑦 ∈ ℂ ∣ ∀𝑘 ∈ (0...𝑁)(𝑦 + 𝑘) ∈ dom 𝐹}) | 
| 47 |  | sumex 15725 | . . 3
⊢
Σ𝑘 ∈
(0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ V | 
| 48 | 47 | a1i 11 | . 2
⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘)))) ∈ V) | 
| 49 | 30, 35, 46, 48 | fvmptd 7022 | 1
⊢ (𝜑 → ((𝑁 △n 𝐹)‘𝑋) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((-1↑(𝑁 − 𝑘)) · (𝐹‘(𝑋 + 𝑘))))) |