Step | Hyp | Ref
| Expression |
1 | | taylpfval.s |
. . . . 5
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | | taylpfval.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
3 | | taylpfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
4 | | taylpfval.n |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
5 | | taylpfval.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
6 | | taylpfval.t |
. . . . 5
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
7 | 1, 2, 3, 4, 5, 6 | taylpfval 26312 |
. . . 4
⊢ (𝜑 → 𝑇 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
8 | | simpr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
9 | | cnex 11220 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ∈
V) |
11 | | elpm2r 8864 |
. . . . . . . . . . . 12
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
12 | 10, 1, 2, 3, 11 | syl22anc 838 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
13 | | dvnbss 25871 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑁 ∈
ℕ0) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom 𝐹) |
14 | 1, 12, 4, 13 | syl3anc 1369 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom 𝐹) |
15 | 2, 14 | fssdmd 6741 |
. . . . . . . . 9
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ 𝐴) |
16 | | recnprss 25846 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
17 | 1, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
18 | 3, 17 | sstrd 3990 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
19 | 15, 18 | sstrd 3990 |
. . . . . . . 8
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ ℂ) |
20 | 19, 5 | sseldd 3981 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
21 | 20 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
22 | 8, 21 | subcld 11602 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥 − 𝐵) ∈ ℂ) |
23 | | df-idp 26136 |
. . . . . . . 8
⊢
Xp = ( I ↾ ℂ) |
24 | | mptresid 6054 |
. . . . . . . 8
⊢ ( I
↾ ℂ) = (𝑥
∈ ℂ ↦ 𝑥) |
25 | 23, 24 | eqtri 2756 |
. . . . . . 7
⊢
Xp = (𝑥 ∈ ℂ ↦ 𝑥) |
26 | 25 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Xp =
(𝑥 ∈ ℂ ↦
𝑥)) |
27 | | fconstmpt 5740 |
. . . . . . 7
⊢ (ℂ
× {𝐵}) = (𝑥 ∈ ℂ ↦ 𝐵) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (ℂ × {𝐵}) = (𝑥 ∈ ℂ ↦ 𝐵)) |
29 | 10, 8, 21, 26, 28 | offval2 7705 |
. . . . 5
⊢ (𝜑 → (Xp
∘f − (ℂ × {𝐵})) = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐵))) |
30 | | eqidd 2729 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) |
31 | | oveq1 7427 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝐵) → (𝑦↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
32 | 31 | oveq2d 7436 |
. . . . . 6
⊢ (𝑦 = (𝑥 − 𝐵) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
33 | 32 | sumeq2sdv 15683 |
. . . . 5
⊢ (𝑦 = (𝑥 − 𝐵) → Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
34 | 22, 29, 30, 33 | fmptco 7138 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵}))) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
35 | 7, 34 | eqtr4d 2771 |
. . 3
⊢ (𝜑 → 𝑇 = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵})))) |
36 | | taylply2.1 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
(SubRing‘ℂfld)) |
37 | | cnfldbas 21283 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
38 | 37 | subrgss 20511 |
. . . . . 6
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 𝐷 ⊆ ℂ) |
39 | 36, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
40 | | taylply2.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ 𝐷) |
41 | 39, 4, 40 | elplyd 26149 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∈ (Poly‘𝐷)) |
42 | | cnfld1 21321 |
. . . . . . . 8
⊢ 1 =
(1r‘ℂfld) |
43 | 42 | subrg1cl 20519 |
. . . . . . 7
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 1 ∈ 𝐷) |
44 | 36, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 1 ∈ 𝐷) |
45 | | plyid 26156 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ 1 ∈
𝐷) →
Xp ∈ (Poly‘𝐷)) |
46 | 39, 44, 45 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → Xp
∈ (Poly‘𝐷)) |
47 | | taylply2.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
48 | | plyconst 26153 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ 𝐵 ∈ 𝐷) → (ℂ × {𝐵}) ∈ (Poly‘𝐷)) |
49 | 39, 47, 48 | syl2anc 583 |
. . . . 5
⊢ (𝜑 → (ℂ × {𝐵}) ∈ (Poly‘𝐷)) |
50 | | subrgsubg 20516 |
. . . . . . 7
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 𝐷 ∈
(SubGrp‘ℂfld)) |
51 | 36, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
(SubGrp‘ℂfld)) |
52 | | cnfldadd 21285 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
53 | 52 | subgcl 19091 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢 + 𝑣) ∈ 𝐷) |
54 | 53 | 3expb 1118 |
. . . . . 6
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 + 𝑣) ∈ 𝐷) |
55 | 51, 54 | sylan 579 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 + 𝑣) ∈ 𝐷) |
56 | 38 | sseld 3979 |
. . . . . . . . . . 11
⊢ (𝐷 ∈
(SubRing‘ℂfld) → (𝑢 ∈ 𝐷 → 𝑢 ∈ ℂ)) |
57 | 56 | a1dd 50 |
. . . . . . . . . 10
⊢ (𝐷 ∈
(SubRing‘ℂfld) → (𝑢 ∈ 𝐷 → (𝑣 ∈ 𝐷 → 𝑢 ∈ ℂ))) |
58 | 57 | 3imp 1109 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → 𝑢 ∈ ℂ) |
59 | 38 | sseld 3979 |
. . . . . . . . . . 11
⊢ (𝐷 ∈
(SubRing‘ℂfld) → (𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ)) |
60 | 59 | a1d 25 |
. . . . . . . . . 10
⊢ (𝐷 ∈
(SubRing‘ℂfld) → (𝑢 ∈ 𝐷 → (𝑣 ∈ 𝐷 → 𝑣 ∈ ℂ))) |
61 | 60 | 3imp 1109 |
. . . . . . . . 9
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → 𝑣 ∈ ℂ) |
62 | | ovmpot 7582 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ℂ ∧ 𝑣 ∈ ℂ) → (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) = (𝑢 · 𝑣)) |
63 | 58, 61, 62 | syl2anc 583 |
. . . . . . . 8
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) = (𝑢 · 𝑣)) |
64 | | mpocnfldmul 21286 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦)) =
(.r‘ℂfld) |
65 | 64 | subrgmcl 20523 |
. . . . . . . 8
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢(𝑥 ∈ ℂ, 𝑦 ∈ ℂ ↦ (𝑥 · 𝑦))𝑣) ∈ 𝐷) |
66 | 63, 65 | eqeltrrd 2830 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢 · 𝑣) ∈ 𝐷) |
67 | 66 | 3expb 1118 |
. . . . . 6
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 · 𝑣) ∈ 𝐷) |
68 | 36, 67 | sylan 579 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 · 𝑣) ∈ 𝐷) |
69 | | ax-1cn 11197 |
. . . . . . 7
⊢ 1 ∈
ℂ |
70 | | cnfldneg 21323 |
. . . . . . 7
⊢ (1 ∈
ℂ → ((invg‘ℂfld)‘1) =
-1) |
71 | 69, 70 | ax-mp 5 |
. . . . . 6
⊢
((invg‘ℂfld)‘1) =
-1 |
72 | | eqid 2728 |
. . . . . . . 8
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
73 | 72 | subginvcl 19090 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ 1 ∈ 𝐷) →
((invg‘ℂfld)‘1) ∈ 𝐷) |
74 | 51, 44, 73 | syl2anc 583 |
. . . . . 6
⊢ (𝜑 →
((invg‘ℂfld)‘1) ∈ 𝐷) |
75 | 71, 74 | eqeltrrid 2834 |
. . . . 5
⊢ (𝜑 → -1 ∈ 𝐷) |
76 | 46, 49, 55, 68, 75 | plysub 26166 |
. . . 4
⊢ (𝜑 → (Xp
∘f − (ℂ × {𝐵})) ∈ (Poly‘𝐷)) |
77 | 41, 76, 55, 68 | plyco 26188 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵}))) ∈ (Poly‘𝐷)) |
78 | 35, 77 | eqeltrd 2829 |
. 2
⊢ (𝜑 → 𝑇 ∈ (Poly‘𝐷)) |
79 | 35 | fveq2d 6901 |
. . . 4
⊢ (𝜑 → (deg‘𝑇) = (deg‘((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵}))))) |
80 | | eqid 2728 |
. . . . 5
⊢
(deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) = (deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) |
81 | | eqid 2728 |
. . . . 5
⊢
(deg‘(Xp ∘f − (ℂ
× {𝐵}))) =
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))) |
82 | 80, 81, 41, 76 | dgrco 26223 |
. . . 4
⊢ (𝜑 → (deg‘((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵})))) = ((deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))))) |
83 | | eqid 2728 |
. . . . . . . . 9
⊢
(Xp ∘f − (ℂ ×
{𝐵})) =
(Xp ∘f − (ℂ × {𝐵})) |
84 | 83 | plyremlem 26252 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
((Xp ∘f − (ℂ × {𝐵})) ∈ (Poly‘ℂ)
∧ (deg‘(Xp ∘f − (ℂ
× {𝐵}))) = 1 ∧
(◡(Xp
∘f − (ℂ × {𝐵})) “ {0}) = {𝐵})) |
85 | 20, 84 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((Xp
∘f − (ℂ × {𝐵})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))) = 1 ∧ (◡(Xp ∘f
− (ℂ × {𝐵})) “ {0}) = {𝐵})) |
86 | 85 | simp2d 1141 |
. . . . . 6
⊢ (𝜑 →
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))) =
1) |
87 | 86 | oveq2d 7436 |
. . . . 5
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘f − (ℂ ×
{𝐵})))) =
((deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) · 1)) |
88 | | dgrcl 26180 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∈ (Poly‘𝐷) → (deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈
ℕ0) |
89 | 41, 88 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈
ℕ0) |
90 | 89 | nn0cnd 12565 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈ ℂ) |
91 | 90 | mulridd 11262 |
. . . . 5
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) · 1) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
92 | 87, 91 | eqtrd 2768 |
. . . 4
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘f − (ℂ ×
{𝐵})))) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
93 | 79, 82, 92 | 3eqtrd 2772 |
. . 3
⊢ (𝜑 → (deg‘𝑇) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
94 | | elfznn0 13627 |
. . . . . . 7
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
95 | | dvnf 25870 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑘 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
96 | 1, 12, 94, 95 | syl2an3an 1420 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
97 | | id 22 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ (0...𝑁)) |
98 | | dvn2bss 25873 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑘 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
99 | 1, 12, 97, 98 | syl2an3an 1420 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
100 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
101 | 99, 100 | sseldd 3981 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
102 | 96, 101 | ffvelcdmd 7095 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
103 | 94 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
104 | 103 | faccld 14276 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
105 | 104 | nncnd 12259 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ) |
106 | 104 | nnne0d 12293 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0) |
107 | 102, 105,
106 | divcld 12021 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
108 | 41, 4, 107, 30 | dgrle 26190 |
. . 3
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ≤ 𝑁) |
109 | 93, 108 | eqbrtrd 5170 |
. 2
⊢ (𝜑 → (deg‘𝑇) ≤ 𝑁) |
110 | 78, 109 | jca 511 |
1
⊢ (𝜑 → (𝑇 ∈ (Poly‘𝐷) ∧ (deg‘𝑇) ≤ 𝑁)) |