| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6905 | . . 3
⊢ (𝑛 = 0 → ((𝑆 D𝑛 𝐹)‘𝑛) = ((𝑆 D𝑛 𝐹)‘0)) | 
| 2 |  | breq2 5146 | . . . . 5
⊢ (𝑛 = 0 → (𝐾 < 𝑛 ↔ 𝐾 < 0)) | 
| 3 |  | eqidd 2737 | . . . . 5
⊢ (𝑛 = 0 → 0 =
0) | 
| 4 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑛 = 0 → (𝐾 − 𝑛) = (𝐾 − 0)) | 
| 5 | 4 | fveq2d 6909 | . . . . . . 7
⊢ (𝑛 = 0 → (!‘(𝐾 − 𝑛)) = (!‘(𝐾 − 0))) | 
| 6 | 5 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 0 → ((!‘𝐾) / (!‘(𝐾 − 𝑛))) = ((!‘𝐾) / (!‘(𝐾 − 0)))) | 
| 7 | 4 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 0 → ((𝑥 + 𝐴)↑(𝐾 − 𝑛)) = ((𝑥 + 𝐴)↑(𝐾 − 0))) | 
| 8 | 6, 7 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 0 → (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))) = (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))) | 
| 9 | 2, 3, 8 | ifbieq12d 4553 | . . . 4
⊢ (𝑛 = 0 → if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛)))) = if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0))))) | 
| 10 | 9 | mpteq2dv 5243 | . . 3
⊢ (𝑛 = 0 → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))))) | 
| 11 | 1, 10 | eqeq12d 2752 | . 2
⊢ (𝑛 = 0 → (((𝑆 D𝑛 𝐹)‘𝑛) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) ↔ ((𝑆 D𝑛 𝐹)‘0) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0))))))) | 
| 12 |  | fveq2 6905 | . . 3
⊢ (𝑛 = 𝑚 → ((𝑆 D𝑛 𝐹)‘𝑛) = ((𝑆 D𝑛 𝐹)‘𝑚)) | 
| 13 |  | breq2 5146 | . . . . 5
⊢ (𝑛 = 𝑚 → (𝐾 < 𝑛 ↔ 𝐾 < 𝑚)) | 
| 14 |  | eqidd 2737 | . . . . 5
⊢ (𝑛 = 𝑚 → 0 = 0) | 
| 15 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑛 = 𝑚 → (𝐾 − 𝑛) = (𝐾 − 𝑚)) | 
| 16 | 15 | fveq2d 6909 | . . . . . . 7
⊢ (𝑛 = 𝑚 → (!‘(𝐾 − 𝑛)) = (!‘(𝐾 − 𝑚))) | 
| 17 | 16 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑚 → ((!‘𝐾) / (!‘(𝐾 − 𝑛))) = ((!‘𝐾) / (!‘(𝐾 − 𝑚)))) | 
| 18 | 15 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑚 → ((𝑥 + 𝐴)↑(𝐾 − 𝑛)) = ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) | 
| 19 | 17, 18 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑚 → (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))) = (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) | 
| 20 | 13, 14, 19 | ifbieq12d 4553 | . . . 4
⊢ (𝑛 = 𝑚 → if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛)))) = if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) | 
| 21 | 20 | mpteq2dv 5243 | . . 3
⊢ (𝑛 = 𝑚 → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) | 
| 22 | 12, 21 | eqeq12d 2752 | . 2
⊢ (𝑛 = 𝑚 → (((𝑆 D𝑛 𝐹)‘𝑛) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) ↔ ((𝑆 D𝑛 𝐹)‘𝑚) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))))) | 
| 23 |  | fveq2 6905 | . . 3
⊢ (𝑛 = (𝑚 + 1) → ((𝑆 D𝑛 𝐹)‘𝑛) = ((𝑆 D𝑛 𝐹)‘(𝑚 + 1))) | 
| 24 |  | breq2 5146 | . . . . 5
⊢ (𝑛 = (𝑚 + 1) → (𝐾 < 𝑛 ↔ 𝐾 < (𝑚 + 1))) | 
| 25 |  | eqidd 2737 | . . . . 5
⊢ (𝑛 = (𝑚 + 1) → 0 = 0) | 
| 26 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑛 = (𝑚 + 1) → (𝐾 − 𝑛) = (𝐾 − (𝑚 + 1))) | 
| 27 | 26 | fveq2d 6909 | . . . . . . 7
⊢ (𝑛 = (𝑚 + 1) → (!‘(𝐾 − 𝑛)) = (!‘(𝐾 − (𝑚 + 1)))) | 
| 28 | 27 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = (𝑚 + 1) → ((!‘𝐾) / (!‘(𝐾 − 𝑛))) = ((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1))))) | 
| 29 | 26 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = (𝑚 + 1) → ((𝑥 + 𝐴)↑(𝐾 − 𝑛)) = ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))) | 
| 30 | 28, 29 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = (𝑚 + 1) → (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))) = (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) | 
| 31 | 24, 25, 30 | ifbieq12d 4553 | . . . 4
⊢ (𝑛 = (𝑚 + 1) → if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛)))) = if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))))) | 
| 32 | 31 | mpteq2dv 5243 | . . 3
⊢ (𝑛 = (𝑚 + 1) → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 33 | 23, 32 | eqeq12d 2752 | . 2
⊢ (𝑛 = (𝑚 + 1) → (((𝑆 D𝑛 𝐹)‘𝑛) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) ↔ ((𝑆 D𝑛 𝐹)‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))))))) | 
| 34 |  | fveq2 6905 | . . 3
⊢ (𝑛 = 𝑁 → ((𝑆 D𝑛 𝐹)‘𝑛) = ((𝑆 D𝑛 𝐹)‘𝑁)) | 
| 35 |  | breq2 5146 | . . . . 5
⊢ (𝑛 = 𝑁 → (𝐾 < 𝑛 ↔ 𝐾 < 𝑁)) | 
| 36 |  | eqidd 2737 | . . . . 5
⊢ (𝑛 = 𝑁 → 0 = 0) | 
| 37 |  | oveq2 7440 | . . . . . . . 8
⊢ (𝑛 = 𝑁 → (𝐾 − 𝑛) = (𝐾 − 𝑁)) | 
| 38 | 37 | fveq2d 6909 | . . . . . . 7
⊢ (𝑛 = 𝑁 → (!‘(𝐾 − 𝑛)) = (!‘(𝐾 − 𝑁))) | 
| 39 | 38 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑁 → ((!‘𝐾) / (!‘(𝐾 − 𝑛))) = ((!‘𝐾) / (!‘(𝐾 − 𝑁)))) | 
| 40 | 37 | oveq2d 7448 | . . . . . 6
⊢ (𝑛 = 𝑁 → ((𝑥 + 𝐴)↑(𝐾 − 𝑛)) = ((𝑥 + 𝐴)↑(𝐾 − 𝑁))) | 
| 41 | 39, 40 | oveq12d 7450 | . . . . 5
⊢ (𝑛 = 𝑁 → (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))) = (((!‘𝐾) / (!‘(𝐾 − 𝑁))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑁)))) | 
| 42 | 35, 36, 41 | ifbieq12d 4553 | . . . 4
⊢ (𝑛 = 𝑁 → if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛)))) = if(𝐾 < 𝑁, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑁))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑁))))) | 
| 43 | 42 | mpteq2dv 5243 | . . 3
⊢ (𝑛 = 𝑁 → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑁, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑁))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑁)))))) | 
| 44 | 34, 43 | eqeq12d 2752 | . 2
⊢ (𝑛 = 𝑁 → (((𝑆 D𝑛 𝐹)‘𝑛) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑛, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑛))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑛))))) ↔ ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑁, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑁))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑁))))))) | 
| 45 |  | dvnxpaek.s | . . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) | 
| 46 |  | recnprss 25940 | . . . . 5
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) | 
| 47 | 45, 46 | syl 17 | . . . 4
⊢ (𝜑 → 𝑆 ⊆ ℂ) | 
| 48 |  | cnex 11237 | . . . . . 6
⊢ ℂ
∈ V | 
| 49 | 48 | a1i 11 | . . . . 5
⊢ (𝜑 → ℂ ∈
V) | 
| 50 |  | dvnxpaek.x | . . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 51 |  | restsspw 17477 | . . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ⊆ 𝒫 𝑆 | 
| 52 |  | id 22 | . . . . . . . . . . . . . 14
⊢ (𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆) → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 53 | 51, 52 | sselid 3980 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆) → 𝑋 ∈ 𝒫 𝑆) | 
| 54 |  | elpwi 4606 | . . . . . . . . . . . . 13
⊢ (𝑋 ∈ 𝒫 𝑆 → 𝑋 ⊆ 𝑆) | 
| 55 | 53, 54 | syl 17 | . . . . . . . . . . . 12
⊢ (𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆) → 𝑋 ⊆ 𝑆) | 
| 56 | 50, 55 | syl 17 | . . . . . . . . . . 11
⊢ (𝜑 → 𝑋 ⊆ 𝑆) | 
| 57 | 56, 47 | sstrd 3993 | . . . . . . . . . 10
⊢ (𝜑 → 𝑋 ⊆ ℂ) | 
| 58 | 57 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑋 ⊆ ℂ) | 
| 59 |  | simpr 484 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 60 | 58, 59 | sseldd 3983 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ ℂ) | 
| 61 |  | dvnxpaek.a | . . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ ℂ) | 
| 62 | 61 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ ℂ) | 
| 63 | 60, 62 | addcld 11281 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝑥 + 𝐴) ∈ ℂ) | 
| 64 |  | dvnxpaek.k | . . . . . . . 8
⊢ (𝜑 → 𝐾 ∈
ℕ0) | 
| 65 | 64 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐾 ∈
ℕ0) | 
| 66 | 63, 65 | expcld 14187 | . . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑𝐾) ∈ ℂ) | 
| 67 |  | dvnxpaek.f | . . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥 + 𝐴)↑𝐾)) | 
| 68 | 66, 67 | fmptd 7133 | . . . . 5
⊢ (𝜑 → 𝐹:𝑋⟶ℂ) | 
| 69 |  | elpm2r 8886 | . . . . 5
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝑋⟶ℂ ∧ 𝑋 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) | 
| 70 | 49, 45, 68, 56, 69 | syl22anc 838 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) | 
| 71 |  | dvn0 25961 | . . . 4
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆))
→ ((𝑆
D𝑛 𝐹)‘0) = 𝐹) | 
| 72 | 47, 70, 71 | syl2anc 584 | . . 3
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) | 
| 73 | 67 | a1i 11 | . . 3
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝑋 ↦ ((𝑥 + 𝐴)↑𝐾))) | 
| 74 | 64 | nn0ge0d 12592 | . . . . . . . 8
⊢ (𝜑 → 0 ≤ 𝐾) | 
| 75 |  | 0red 11265 | . . . . . . . . 9
⊢ (𝜑 → 0 ∈
ℝ) | 
| 76 | 64 | nn0red 12590 | . . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) | 
| 77 | 75, 76 | lenltd 11408 | . . . . . . . 8
⊢ (𝜑 → (0 ≤ 𝐾 ↔ ¬ 𝐾 < 0)) | 
| 78 | 74, 77 | mpbid 232 | . . . . . . 7
⊢ (𝜑 → ¬ 𝐾 < 0) | 
| 79 | 78 | iffalsed 4535 | . . . . . 6
⊢ (𝜑 → if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))) = (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))) | 
| 80 | 79 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))) = (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))) | 
| 81 | 64 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ (𝜑 → 𝐾 ∈ ℂ) | 
| 82 | 81 | subid1d 11610 | . . . . . . . . . 10
⊢ (𝜑 → (𝐾 − 0) = 𝐾) | 
| 83 | 82 | fveq2d 6909 | . . . . . . . . 9
⊢ (𝜑 → (!‘(𝐾 − 0)) = (!‘𝐾)) | 
| 84 | 83 | oveq2d 7448 | . . . . . . . 8
⊢ (𝜑 → ((!‘𝐾) / (!‘(𝐾 − 0))) = ((!‘𝐾) / (!‘𝐾))) | 
| 85 |  | faccl 14323 | . . . . . . . . . . 11
⊢ (𝐾 ∈ ℕ0
→ (!‘𝐾) ∈
ℕ) | 
| 86 | 64, 85 | syl 17 | . . . . . . . . . 10
⊢ (𝜑 → (!‘𝐾) ∈ ℕ) | 
| 87 | 86 | nncnd 12283 | . . . . . . . . 9
⊢ (𝜑 → (!‘𝐾) ∈ ℂ) | 
| 88 | 86 | nnne0d 12317 | . . . . . . . . 9
⊢ (𝜑 → (!‘𝐾) ≠ 0) | 
| 89 | 87, 88 | dividd 12042 | . . . . . . . 8
⊢ (𝜑 → ((!‘𝐾) / (!‘𝐾)) = 1) | 
| 90 | 84, 89 | eqtrd 2776 | . . . . . . 7
⊢ (𝜑 → ((!‘𝐾) / (!‘(𝐾 − 0))) = 1) | 
| 91 | 82 | oveq2d 7448 | . . . . . . 7
⊢ (𝜑 → ((𝑥 + 𝐴)↑(𝐾 − 0)) = ((𝑥 + 𝐴)↑𝐾)) | 
| 92 | 90, 91 | oveq12d 7450 | . . . . . 6
⊢ (𝜑 → (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0))) = (1 · ((𝑥 + 𝐴)↑𝐾))) | 
| 93 | 92 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0))) = (1 · ((𝑥 + 𝐴)↑𝐾))) | 
| 94 | 66 | mullidd 11280 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (1 · ((𝑥 + 𝐴)↑𝐾)) = ((𝑥 + 𝐴)↑𝐾)) | 
| 95 | 80, 93, 94 | 3eqtrrd 2781 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑𝐾) = if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0))))) | 
| 96 | 95 | mpteq2dva 5241 | . . 3
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ ((𝑥 + 𝐴)↑𝐾)) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))))) | 
| 97 | 72, 73, 96 | 3eqtrd 2780 | . 2
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 0, 0, (((!‘𝐾) / (!‘(𝐾 − 0))) · ((𝑥 + 𝐴)↑(𝐾 − 0)))))) | 
| 98 | 47 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑆 ⊆
ℂ) | 
| 99 | 70 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝐹 ∈ (ℂ
↑pm 𝑆)) | 
| 100 |  | simpr 484 | . . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℕ0) | 
| 101 |  | dvnp1 25962 | . . . . 5
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑚 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑚))) | 
| 102 | 98, 99, 100, 101 | syl3anc 1372 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑚))) | 
| 103 | 102 | adantr 480 | . . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑆 D𝑛 𝐹)‘𝑚) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) → ((𝑆 D𝑛 𝐹)‘(𝑚 + 1)) = (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑚))) | 
| 104 |  | oveq2 7440 | . . . 4
⊢ (((𝑆 D𝑛 𝐹)‘𝑚) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) → (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑚)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))))) | 
| 105 | 104 | adantl 481 | . . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑆 D𝑛 𝐹)‘𝑚) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) → (𝑆 D ((𝑆 D𝑛 𝐹)‘𝑚)) = (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))))) | 
| 106 |  | iftrue 4530 | . . . . . . . . 9
⊢ (𝐾 < 𝑚 → if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) = 0) | 
| 107 | 106 | mpteq2dv 5243 | . . . . . . . 8
⊢ (𝐾 < 𝑚 → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 108 | 107 | oveq2d 7448 | . . . . . . 7
⊢ (𝐾 < 𝑚 → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 0))) | 
| 109 | 108 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ 0))) | 
| 110 |  | 0cnd 11255 | . . . . . . . 8
⊢ (𝜑 → 0 ∈
ℂ) | 
| 111 | 45, 50, 110 | dvmptconst 45935 | . . . . . . 7
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ 0)) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 112 | 111 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → (𝑆 D (𝑥 ∈ 𝑋 ↦ 0)) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 113 | 76 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → 𝐾 ∈ ℝ) | 
| 114 |  | nn0re 12537 | . . . . . . . . . . . 12
⊢ (𝑚 ∈ ℕ0
→ 𝑚 ∈
ℝ) | 
| 115 | 114 | ad2antlr 727 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → 𝑚 ∈ ℝ) | 
| 116 |  | simpr 484 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → 𝐾 < 𝑚) | 
| 117 | 113, 115,
116 | ltled 11410 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → 𝐾 ≤ 𝑚) | 
| 118 | 64 | nn0zd 12641 | . . . . . . . . . . . . 13
⊢ (𝜑 → 𝐾 ∈ ℤ) | 
| 119 | 118 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝐾 ∈
ℤ) | 
| 120 | 100 | nn0zd 12641 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℤ) | 
| 121 |  | zleltp1 12670 | . . . . . . . . . . . 12
⊢ ((𝐾 ∈ ℤ ∧ 𝑚 ∈ ℤ) → (𝐾 ≤ 𝑚 ↔ 𝐾 < (𝑚 + 1))) | 
| 122 | 119, 120,
121 | syl2anc 584 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝐾 ≤ 𝑚 ↔ 𝐾 < (𝑚 + 1))) | 
| 123 | 122 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → (𝐾 ≤ 𝑚 ↔ 𝐾 < (𝑚 + 1))) | 
| 124 | 117, 123 | mpbid 232 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → 𝐾 < (𝑚 + 1)) | 
| 125 | 124 | iftrued 4532 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) = 0) | 
| 126 | 125 | mpteq2dv 5243 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 127 | 126 | eqcomd 2742 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → (𝑥 ∈ 𝑋 ↦ 0) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 128 | 109, 112,
127 | 3eqtrd 2780 | . . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝐾 < 𝑚) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 129 |  | simpl 482 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → (𝜑 ∧ 𝑚 ∈
ℕ0)) | 
| 130 |  | simpr 484 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → ¬ 𝐾 < 𝑚) | 
| 131 | 129, 100,
114 | 3syl 18 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → 𝑚 ∈ ℝ) | 
| 132 | 76 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → 𝐾 ∈ ℝ) | 
| 133 | 131, 132 | lenltd 11408 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → (𝑚 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑚)) | 
| 134 | 130, 133 | mpbird 257 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → 𝑚 ≤ 𝐾) | 
| 135 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → 𝑚 = 𝐾) | 
| 136 | 114 | ad2antlr 727 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → 𝑚 ∈ ℝ) | 
| 137 | 76 | ad2antrr 726 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → 𝐾 ∈ ℝ) | 
| 138 | 136, 137 | lttri3d 11402 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝑚 = 𝐾 ↔ (¬ 𝑚 < 𝐾 ∧ ¬ 𝐾 < 𝑚))) | 
| 139 | 135, 138 | mpbid 232 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (¬ 𝑚 < 𝐾 ∧ ¬ 𝐾 < 𝑚)) | 
| 140 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((¬
𝑚 < 𝐾 ∧ ¬ 𝐾 < 𝑚) → ¬ 𝐾 < 𝑚) | 
| 141 | 139, 140 | syl 17 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → ¬ 𝐾 < 𝑚) | 
| 142 | 141 | iffalsed 4535 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) = (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) | 
| 143 | 142 | mpteq2dv 5243 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) | 
| 144 | 143 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) | 
| 145 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 = 𝐾 → (𝐾 − 𝑚) = (𝐾 − 𝐾)) | 
| 146 | 145 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 = 𝐾 → (!‘(𝐾 − 𝑚)) = (!‘(𝐾 − 𝐾))) | 
| 147 | 146 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (!‘(𝐾 − 𝑚)) = (!‘(𝐾 − 𝐾))) | 
| 148 | 81 | subidd 11609 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → (𝐾 − 𝐾) = 0) | 
| 149 | 148 | fveq2d 6909 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (!‘(𝐾 − 𝐾)) = (!‘0)) | 
| 150 |  | fac0 14316 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(!‘0) = 1 | 
| 151 | 150 | a1i 11 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (!‘0) =
1) | 
| 152 | 149, 151 | eqtrd 2776 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (!‘(𝐾 − 𝐾)) = 1) | 
| 153 | 152 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (!‘(𝐾 − 𝐾)) = 1) | 
| 154 | 147, 153 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (!‘(𝐾 − 𝑚)) = 1) | 
| 155 | 154 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → ((!‘𝐾) / (!‘(𝐾 − 𝑚))) = ((!‘𝐾) / 1)) | 
| 156 | 87 | div1d 12036 | . . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((!‘𝐾) / 1) = (!‘𝐾)) | 
| 157 | 156 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → ((!‘𝐾) / 1) = (!‘𝐾)) | 
| 158 | 155, 157 | eqtrd 2776 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → ((!‘𝐾) / (!‘(𝐾 − 𝑚))) = (!‘𝐾)) | 
| 159 | 158 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → ((!‘𝐾) / (!‘(𝐾 − 𝑚))) = (!‘𝐾)) | 
| 160 | 145 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝐾 − 𝑚) = (𝐾 − 𝐾)) | 
| 161 | 148 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝐾 − 𝐾) = 0) | 
| 162 | 160, 161 | eqtrd 2776 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝐾 − 𝑚) = 0) | 
| 163 | 162 | oveq2d 7448 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → ((𝑥 + 𝐴)↑(𝐾 − 𝑚)) = ((𝑥 + 𝐴)↑0)) | 
| 164 | 163 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑(𝐾 − 𝑚)) = ((𝑥 + 𝐴)↑0)) | 
| 165 | 63 | exp0d 14181 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑0) = 1) | 
| 166 | 165 | adantlr 715 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑0) = 1) | 
| 167 | 164, 166 | eqtrd 2776 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑(𝐾 − 𝑚)) = 1) | 
| 168 | 159, 167 | oveq12d 7450 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) = ((!‘𝐾) · 1)) | 
| 169 | 87 | mulridd 11279 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → ((!‘𝐾) · 1) = (!‘𝐾)) | 
| 170 | 169 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → ((!‘𝐾) · 1) = (!‘𝐾)) | 
| 171 | 168, 170 | eqtrd 2776 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 = 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) = (!‘𝐾)) | 
| 172 | 171 | mpteq2dva 5241 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) = (𝑥 ∈ 𝑋 ↦ (!‘𝐾))) | 
| 173 | 172 | oveq2d 7448 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (!‘𝐾)))) | 
| 174 | 45, 50, 87 | dvmptconst 45935 | . . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 D (𝑥 ∈ 𝑋 ↦ (!‘𝐾))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 175 | 174 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (!‘𝐾))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 176 | 173, 175 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 177 | 176 | adantlr 715 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 178 | 137 | ltp1d 12199 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → 𝐾 < (𝐾 + 1)) | 
| 179 |  | oveq1 7439 | . . . . . . . . . . . . . . 15
⊢ (𝑚 = 𝐾 → (𝑚 + 1) = (𝐾 + 1)) | 
| 180 | 179 | eqcomd 2742 | . . . . . . . . . . . . . 14
⊢ (𝑚 = 𝐾 → (𝐾 + 1) = (𝑚 + 1)) | 
| 181 | 180 | adantl 481 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝐾 + 1) = (𝑚 + 1)) | 
| 182 | 178, 181 | breqtrd 5168 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → 𝐾 < (𝑚 + 1)) | 
| 183 | 182 | iftrued 4532 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) = 0) | 
| 184 | 183 | eqcomd 2742 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → 0 = if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))))) | 
| 185 | 184 | mpteq2dv 5243 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝑥 ∈ 𝑋 ↦ 0) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 186 | 144, 177,
185 | 3eqtrd 2780 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 187 | 186 | adantlr 715 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 188 |  | simpll 766 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → (𝜑 ∧ 𝑚 ∈
ℕ0)) | 
| 189 | 188, 100,
114 | 3syl 18 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → 𝑚 ∈ ℝ) | 
| 190 | 76 | ad3antrrr 730 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → 𝐾 ∈ ℝ) | 
| 191 |  | simplr 768 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → 𝑚 ≤ 𝐾) | 
| 192 |  | neqne 2947 | . . . . . . . . . . 11
⊢ (¬
𝑚 = 𝐾 → 𝑚 ≠ 𝐾) | 
| 193 | 192 | necomd 2995 | . . . . . . . . . 10
⊢ (¬
𝑚 = 𝐾 → 𝐾 ≠ 𝑚) | 
| 194 | 193 | adantl 481 | . . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → 𝐾 ≠ 𝑚) | 
| 195 | 189, 190,
191, 194 | leneltd 11416 | . . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → 𝑚 < 𝐾) | 
| 196 | 114 | ad2antlr 727 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑚 ∈ ℝ) | 
| 197 | 76 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝐾 ∈ ℝ) | 
| 198 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑚 < 𝐾) | 
| 199 | 196, 197,
198 | ltled 11410 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑚 ≤ 𝐾) | 
| 200 | 196, 197 | lenltd 11408 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑚 ≤ 𝐾 ↔ ¬ 𝐾 < 𝑚)) | 
| 201 | 199, 200 | mpbid 232 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ¬ 𝐾 < 𝑚) | 
| 202 | 201 | iffalsed 4535 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) = (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) | 
| 203 | 202 | mpteq2dv 5243 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) | 
| 204 | 203 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑆 D (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) | 
| 205 | 45 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑆 ∈ {ℝ,
ℂ}) | 
| 206 | 205 | adantr 480 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑆 ∈ {ℝ, ℂ}) | 
| 207 | 87 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘𝐾) ∈ ℂ) | 
| 208 | 100 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑚 ∈ ℕ0) | 
| 209 | 64 | ad2antrr 726 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝐾 ∈
ℕ0) | 
| 210 |  | nn0sub 12578 | . . . . . . . . . . . . . . . 16
⊢ ((𝑚 ∈ ℕ0
∧ 𝐾 ∈
ℕ0) → (𝑚 ≤ 𝐾 ↔ (𝐾 − 𝑚) ∈
ℕ0)) | 
| 211 | 208, 209,
210 | syl2anc 584 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑚 ≤ 𝐾 ↔ (𝐾 − 𝑚) ∈
ℕ0)) | 
| 212 | 199, 211 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝐾 − 𝑚) ∈
ℕ0) | 
| 213 |  | faccl 14323 | . . . . . . . . . . . . . 14
⊢ ((𝐾 − 𝑚) ∈ ℕ0 →
(!‘(𝐾 − 𝑚)) ∈
ℕ) | 
| 214 | 212, 213 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘(𝐾 − 𝑚)) ∈ ℕ) | 
| 215 | 214 | nncnd 12283 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘(𝐾 − 𝑚)) ∈ ℂ) | 
| 216 | 214 | nnne0d 12317 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘(𝐾 − 𝑚)) ≠ 0) | 
| 217 | 207, 215,
216 | divcld 12044 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((!‘𝐾) / (!‘(𝐾 − 𝑚))) ∈ ℂ) | 
| 218 | 217 | adantr 480 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((!‘𝐾) / (!‘(𝐾 − 𝑚))) ∈ ℂ) | 
| 219 | 75 | ad3antrrr 730 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → 0 ∈ ℝ) | 
| 220 | 50 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 221 | 220 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑋 ∈
((TopOpen‘ℂfld) ↾t 𝑆)) | 
| 222 | 206, 221,
217 | dvmptconst 45935 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ((!‘𝐾) / (!‘(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ 0)) | 
| 223 | 63 | adantlr 715 | . . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑥 ∈ 𝑋) → (𝑥 + 𝐴) ∈ ℂ) | 
| 224 | 223 | adantlr 715 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (𝑥 + 𝐴) ∈ ℂ) | 
| 225 | 212 | adantr 480 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (𝐾 − 𝑚) ∈
ℕ0) | 
| 226 | 224, 225 | expcld 14187 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑(𝐾 − 𝑚)) ∈ ℂ) | 
| 227 | 225 | nn0cnd 12591 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (𝐾 − 𝑚) ∈ ℂ) | 
| 228 | 212 | nn0zd 12641 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝐾 − 𝑚) ∈ ℤ) | 
| 229 | 196, 197 | posdifd 11851 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑚 < 𝐾 ↔ 0 < (𝐾 − 𝑚))) | 
| 230 | 198, 229 | mpbid 232 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 0 < (𝐾 − 𝑚)) | 
| 231 | 228, 230 | jca 511 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝐾 − 𝑚) ∈ ℤ ∧ 0 < (𝐾 − 𝑚))) | 
| 232 |  | elnnz 12625 | . . . . . . . . . . . . . . 15
⊢ ((𝐾 − 𝑚) ∈ ℕ ↔ ((𝐾 − 𝑚) ∈ ℤ ∧ 0 < (𝐾 − 𝑚))) | 
| 233 | 231, 232 | sylibr 234 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝐾 − 𝑚) ∈ ℕ) | 
| 234 |  | nnm1nn0 12569 | . . . . . . . . . . . . . 14
⊢ ((𝐾 − 𝑚) ∈ ℕ → ((𝐾 − 𝑚) − 1) ∈
ℕ0) | 
| 235 | 233, 234 | syl 17 | . . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝐾 − 𝑚) − 1) ∈
ℕ0) | 
| 236 | 235 | adantr 480 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝐾 − 𝑚) − 1) ∈
ℕ0) | 
| 237 | 224, 236 | expcld 14187 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1)) ∈
ℂ) | 
| 238 | 227, 237 | mulcld 11282 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) ∈
ℂ) | 
| 239 | 61 | ad2antrr 726 | . . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝐴 ∈ ℂ) | 
| 240 | 206, 221,
239, 233 | dvxpaek 45960 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))) = (𝑥 ∈ 𝑋 ↦ ((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))))) | 
| 241 | 206, 218,
219, 222, 226, 238, 240 | dvmptmul 26000 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))))) = (𝑥 ∈ 𝑋 ↦ ((0 · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) + (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚))))))) | 
| 242 | 226 | mul02d 11460 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (0 · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) = 0) | 
| 243 | 242 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((0 · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) + (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚))))) = (0 + (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚)))))) | 
| 244 | 238, 218 | mulcld 11282 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚)))) ∈ ℂ) | 
| 245 | 244 | addlidd 11463 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (0 + (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚))))) = (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚))))) | 
| 246 | 120 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝑚 ∈ ℤ) | 
| 247 | 119 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → 𝐾 ∈ ℤ) | 
| 248 |  | zltp1le 12669 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝑚 < 𝐾 ↔ (𝑚 + 1) ≤ 𝐾)) | 
| 249 | 246, 247,
248 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑚 < 𝐾 ↔ (𝑚 + 1) ≤ 𝐾)) | 
| 250 | 198, 249 | mpbid 232 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑚 + 1) ≤ 𝐾) | 
| 251 |  | peano2re 11435 | . . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℝ → (𝑚 + 1) ∈
ℝ) | 
| 252 | 196, 251 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑚 + 1) ∈ ℝ) | 
| 253 | 252, 197 | lenltd 11408 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝑚 + 1) ≤ 𝐾 ↔ ¬ 𝐾 < (𝑚 + 1))) | 
| 254 | 250, 253 | mpbid 232 | . . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ¬ 𝐾 < (𝑚 + 1)) | 
| 255 | 254 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ¬ 𝐾 < (𝑚 + 1)) | 
| 256 | 255 | iffalsed 4535 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) = (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) | 
| 257 | 218, 227,
237 | mulassd 11285 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((((!‘𝐾) / (!‘(𝐾 − 𝑚))) · (𝐾 − 𝑚)) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) = (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))))) | 
| 258 | 257 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1)))) = ((((!‘𝐾) / (!‘(𝐾 − 𝑚))) · (𝐾 − 𝑚)) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1)))) | 
| 259 | 233 | nncnd 12283 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝐾 − 𝑚) ∈ ℂ) | 
| 260 | 207, 215,
259, 216 | div32d 12067 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · (𝐾 − 𝑚)) = ((!‘𝐾) · ((𝐾 − 𝑚) / (!‘(𝐾 − 𝑚))))) | 
| 261 |  | facnn2 14322 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 − 𝑚) ∈ ℕ → (!‘(𝐾 − 𝑚)) = ((!‘((𝐾 − 𝑚) − 1)) · (𝐾 − 𝑚))) | 
| 262 | 233, 261 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘(𝐾 − 𝑚)) = ((!‘((𝐾 − 𝑚) − 1)) · (𝐾 − 𝑚))) | 
| 263 | 262 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝐾 − 𝑚) / (!‘(𝐾 − 𝑚))) = ((𝐾 − 𝑚) / ((!‘((𝐾 − 𝑚) − 1)) · (𝐾 − 𝑚)))) | 
| 264 |  | faccl 14323 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐾 − 𝑚) − 1) ∈ ℕ0
→ (!‘((𝐾 −
𝑚) − 1)) ∈
ℕ) | 
| 265 | 234, 264 | syl 17 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐾 − 𝑚) ∈ ℕ → (!‘((𝐾 − 𝑚) − 1)) ∈
ℕ) | 
| 266 | 265 | nncnd 12283 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 − 𝑚) ∈ ℕ → (!‘((𝐾 − 𝑚) − 1)) ∈
ℂ) | 
| 267 | 233, 266 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘((𝐾 − 𝑚) − 1)) ∈
ℂ) | 
| 268 | 235, 264 | syl 17 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘((𝐾 − 𝑚) − 1)) ∈
ℕ) | 
| 269 |  | nnne0 12301 | . . . . . . . . . . . . . . . . . . . 20
⊢
((!‘((𝐾
− 𝑚) − 1))
∈ ℕ → (!‘((𝐾 − 𝑚) − 1)) ≠ 0) | 
| 270 | 268, 269 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘((𝐾 − 𝑚) − 1)) ≠ 0) | 
| 271 |  | nnne0 12301 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐾 − 𝑚) ∈ ℕ → (𝐾 − 𝑚) ≠ 0) | 
| 272 | 233, 271 | syl 17 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝐾 − 𝑚) ≠ 0) | 
| 273 | 267, 259,
270, 272 | divcan8d 45329 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝐾 − 𝑚) / ((!‘((𝐾 − 𝑚) − 1)) · (𝐾 − 𝑚))) = (1 / (!‘((𝐾 − 𝑚) − 1)))) | 
| 274 | 263, 273 | eqtrd 2776 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝐾 − 𝑚) / (!‘(𝐾 − 𝑚))) = (1 / (!‘((𝐾 − 𝑚) − 1)))) | 
| 275 | 274 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((!‘𝐾) · ((𝐾 − 𝑚) / (!‘(𝐾 − 𝑚)))) = ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1))))) | 
| 276 |  | eqidd 2737 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1)))) = ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1))))) | 
| 277 | 260, 275,
276 | 3eqtrd 2780 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · (𝐾 − 𝑚)) = ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1))))) | 
| 278 | 277 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · (𝐾 − 𝑚)) = ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1))))) | 
| 279 | 81 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝐾 ∈
ℂ) | 
| 280 | 100 | nn0cnd 12591 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 𝑚 ∈
ℂ) | 
| 281 |  | 1cnd 11257 | . . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → 1 ∈
ℂ) | 
| 282 | 279, 280,
281 | subsub4d 11652 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝐾 − 𝑚) − 1) = (𝐾 − (𝑚 + 1))) | 
| 283 | 282 | oveq2d 7448 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1)) = ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))) | 
| 284 | 283 | ad2antrr 726 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1)) = ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))) | 
| 285 | 278, 284 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((((!‘𝐾) / (!‘(𝐾 − 𝑚))) · (𝐾 − 𝑚)) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) = (((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) | 
| 286 | 282 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((𝐾 − 𝑚) − 1) = (𝐾 − (𝑚 + 1))) | 
| 287 | 286 | eqcomd 2742 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝐾 − (𝑚 + 1)) = ((𝐾 − 𝑚) − 1)) | 
| 288 | 287 | fveq2d 6909 | . . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (!‘(𝐾 − (𝑚 + 1))) = (!‘((𝐾 − 𝑚) − 1))) | 
| 289 | 288 | oveq2d 7448 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) = ((!‘𝐾) / (!‘((𝐾 − 𝑚) − 1)))) | 
| 290 | 207, 267,
270 | divrecd 12047 | . . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((!‘𝐾) / (!‘((𝐾 − 𝑚) − 1))) = ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1))))) | 
| 291 | 289, 290 | eqtr2d 2777 | . . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1)))) = ((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1))))) | 
| 292 | 291 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1)))) = ((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1))))) | 
| 293 | 292 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) · (1 / (!‘((𝐾 − 𝑚) − 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))) = (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))) | 
| 294 | 258, 285,
293 | 3eqtrrd 2781 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))) = (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))))) | 
| 295 | 218, 238 | mulcomd 11283 | . . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1)))) = (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚))))) | 
| 296 | 256, 294,
295 | 3eqtrrd 2781 | . . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚)))) = if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))))) | 
| 297 | 243, 245,
296 | 3eqtrd 2780 | . . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) ∧ 𝑥 ∈ 𝑋) → ((0 · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) + (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚))))) = if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1)))))) | 
| 298 | 297 | mpteq2dva 5241 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑥 ∈ 𝑋 ↦ ((0 · ((𝑥 + 𝐴)↑(𝐾 − 𝑚))) + (((𝐾 − 𝑚) · ((𝑥 + 𝐴)↑((𝐾 − 𝑚) − 1))) · ((!‘𝐾) / (!‘(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 299 | 204, 241,
298 | 3eqtrd 2780 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 < 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 300 | 188, 195,
299 | syl2anc 584 | . . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) ∧ ¬ 𝑚 = 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 301 | 187, 300 | pm2.61dan 812 | . . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ 𝑚 ≤ 𝐾) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 302 | 129, 134,
301 | syl2anc 584 | . . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ¬
𝐾 < 𝑚) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 303 | 128, 302 | pm2.61dan 812 | . . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ ℕ0) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 304 | 303 | adantr 480 | . . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑆 D𝑛 𝐹)‘𝑚) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) → (𝑆 D (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 305 | 103, 105,
304 | 3eqtrd 2780 | . 2
⊢ (((𝜑 ∧ 𝑚 ∈ ℕ0) ∧ ((𝑆 D𝑛 𝐹)‘𝑚) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑚, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑚))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑚)))))) → ((𝑆 D𝑛 𝐹)‘(𝑚 + 1)) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < (𝑚 + 1), 0, (((!‘𝐾) / (!‘(𝐾 − (𝑚 + 1)))) · ((𝑥 + 𝐴)↑(𝐾 − (𝑚 + 1))))))) | 
| 306 | 11, 22, 33, 44, 97, 305 | nn0indd 12717 | 1
⊢ ((𝜑 ∧ 𝑁 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑁) = (𝑥 ∈ 𝑋 ↦ if(𝐾 < 𝑁, 0, (((!‘𝐾) / (!‘(𝐾 − 𝑁))) · ((𝑥 + 𝐴)↑(𝐾 − 𝑁)))))) |