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 23923 |
. . . 4
⊢ (𝜑 → 𝑇 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
8 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
9 | | cnex 9896 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ∈
V) |
11 | | elpm2r 7761 |
. . . . . . . . . . . 12
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
12 | 10, 1, 2, 3, 11 | syl22anc 1319 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
13 | | dvnbss 23497 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑁 ∈ ℕ0) → dom
((𝑆 D𝑛
𝐹)‘𝑁) ⊆ dom 𝐹) |
14 | 1, 12, 4, 13 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom 𝐹) |
15 | | fdm 5964 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
16 | 2, 15 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝐴) |
17 | 14, 16 | sseqtrd 3604 |
. . . . . . . . 9
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ 𝐴) |
18 | | recnprss 23474 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
19 | 1, 18 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
20 | 3, 19 | sstrd 3578 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
21 | 17, 20 | sstrd 3578 |
. . . . . . . 8
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ ℂ) |
22 | 21, 5 | sseldd 3569 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
24 | 8, 23 | subcld 10271 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥 − 𝐵) ∈ ℂ) |
25 | | df-idp 23749 |
. . . . . . . 8
⊢
Xp = ( I ↾ ℂ) |
26 | | mptresid 5375 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ ↦ 𝑥) = ( I ↾
ℂ) |
27 | 25, 26 | eqtr4i 2635 |
. . . . . . 7
⊢
Xp = (𝑥 ∈ ℂ ↦ 𝑥) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Xp =
(𝑥 ∈ ℂ ↦
𝑥)) |
29 | | fconstmpt 5085 |
. . . . . . 7
⊢ (ℂ
× {𝐵}) = (𝑥 ∈ ℂ ↦ 𝐵) |
30 | 29 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (ℂ × {𝐵}) = (𝑥 ∈ ℂ ↦ 𝐵)) |
31 | 10, 8, 23, 28, 30 | offval2 6812 |
. . . . 5
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐵})) = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐵))) |
32 | | eqidd 2611 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) |
33 | | oveq1 6556 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝐵) → (𝑦↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
34 | 33 | oveq2d 6565 |
. . . . . 6
⊢ (𝑦 = (𝑥 − 𝐵) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
35 | 34 | sumeq2sdv 14282 |
. . . . 5
⊢ (𝑦 = (𝑥 − 𝐵) → Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
36 | 24, 31, 32, 35 | fmptco 6303 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘𝑓 − (ℂ × {𝐵}))) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
37 | 7, 36 | eqtr4d 2647 |
. . 3
⊢ (𝜑 → 𝑇 = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘𝑓 − (ℂ × {𝐵})))) |
38 | | taylply2.1 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
(SubRing‘ℂfld)) |
39 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
40 | 39 | subrgss 18604 |
. . . . . 6
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 𝐷 ⊆ ℂ) |
41 | 38, 40 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
42 | | taylply2.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ 𝐷) |
43 | 41, 4, 42 | elplyd 23762 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∈ (Poly‘𝐷)) |
44 | | cnfld1 19590 |
. . . . . . . 8
⊢ 1 =
(1r‘ℂfld) |
45 | 44 | subrg1cl 18611 |
. . . . . . 7
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 1 ∈ 𝐷) |
46 | 38, 45 | syl 17 |
. . . . . 6
⊢ (𝜑 → 1 ∈ 𝐷) |
47 | | plyid 23769 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ 1 ∈
𝐷) →
Xp ∈ (Poly‘𝐷)) |
48 | 41, 46, 47 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → Xp
∈ (Poly‘𝐷)) |
49 | | taylply2.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
50 | | plyconst 23766 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ 𝐵 ∈ 𝐷) → (ℂ × {𝐵}) ∈ (Poly‘𝐷)) |
51 | 41, 49, 50 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (ℂ × {𝐵}) ∈ (Poly‘𝐷)) |
52 | | subrgsubg 18609 |
. . . . . . 7
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 𝐷 ∈
(SubGrp‘ℂfld)) |
53 | 38, 52 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
(SubGrp‘ℂfld)) |
54 | | cnfldadd 19572 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
55 | 54 | subgcl 17427 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢 + 𝑣) ∈ 𝐷) |
56 | 55 | 3expb 1258 |
. . . . . 6
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 + 𝑣) ∈ 𝐷) |
57 | 53, 56 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 + 𝑣) ∈ 𝐷) |
58 | | cnfldmul 19573 |
. . . . . . . 8
⊢ ·
= (.r‘ℂfld) |
59 | 58 | subrgmcl 18615 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢 · 𝑣) ∈ 𝐷) |
60 | 59 | 3expb 1258 |
. . . . . 6
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 · 𝑣) ∈ 𝐷) |
61 | 38, 60 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 · 𝑣) ∈ 𝐷) |
62 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
63 | | cnfldneg 19591 |
. . . . . . 7
⊢ (1 ∈
ℂ → ((invg‘ℂfld)‘1) =
-1) |
64 | 62, 63 | ax-mp 5 |
. . . . . 6
⊢
((invg‘ℂfld)‘1) =
-1 |
65 | | eqid 2610 |
. . . . . . . 8
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
66 | 65 | subginvcl 17426 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ 1 ∈ 𝐷) →
((invg‘ℂfld)‘1) ∈ 𝐷) |
67 | 53, 46, 66 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 →
((invg‘ℂfld)‘1) ∈ 𝐷) |
68 | 64, 67 | syl5eqelr 2693 |
. . . . 5
⊢ (𝜑 → -1 ∈ 𝐷) |
69 | 48, 51, 57, 61, 68 | plysub 23779 |
. . . 4
⊢ (𝜑 → (Xp
∘𝑓 − (ℂ × {𝐵})) ∈ (Poly‘𝐷)) |
70 | 43, 69, 57, 61 | plyco 23801 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘𝑓 − (ℂ × {𝐵}))) ∈ (Poly‘𝐷)) |
71 | 37, 70 | eqeltrd 2688 |
. 2
⊢ (𝜑 → 𝑇 ∈ (Poly‘𝐷)) |
72 | 37 | fveq2d 6107 |
. . . 4
⊢ (𝜑 → (deg‘𝑇) = (deg‘((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘𝑓 − (ℂ × {𝐵}))))) |
73 | | eqid 2610 |
. . . . 5
⊢
(deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) = (deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) |
74 | | eqid 2610 |
. . . . 5
⊢
(deg‘(Xp ∘𝑓 −
(ℂ × {𝐵}))) =
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐵}))) |
75 | 73, 74, 43, 69 | dgrco 23835 |
. . . 4
⊢ (𝜑 → (deg‘((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘𝑓 − (ℂ × {𝐵})))) = ((deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐵}))))) |
76 | | eqid 2610 |
. . . . . . . . 9
⊢
(Xp ∘𝑓 − (ℂ
× {𝐵})) =
(Xp ∘𝑓 − (ℂ ×
{𝐵})) |
77 | 76 | plyremlem 23863 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
((Xp ∘𝑓 − (ℂ ×
{𝐵})) ∈
(Poly‘ℂ) ∧ (deg‘(Xp
∘𝑓 − (ℂ × {𝐵}))) = 1 ∧ (◡(Xp
∘𝑓 − (ℂ × {𝐵})) “ {0}) = {𝐵})) |
78 | 22, 77 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((Xp
∘𝑓 − (ℂ × {𝐵})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐵}))) = 1 ∧
(◡(Xp
∘𝑓 − (ℂ × {𝐵})) “ {0}) = {𝐵})) |
79 | 78 | simp2d 1067 |
. . . . . 6
⊢ (𝜑 →
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐵}))) =
1) |
80 | 79 | oveq2d 6565 |
. . . . 5
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐵})))) =
((deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) · 1)) |
81 | | dgrcl 23793 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∈ (Poly‘𝐷) → (deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈
ℕ0) |
82 | 43, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈
ℕ0) |
83 | 82 | nn0cnd 11230 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈ ℂ) |
84 | 83 | mulid1d 9936 |
. . . . 5
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) · 1) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
85 | 80, 84 | eqtrd 2644 |
. . . 4
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘𝑓 − (ℂ
× {𝐵})))) =
(deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
86 | 72, 75, 85 | 3eqtrd 2648 |
. . 3
⊢ (𝜑 → (deg‘𝑇) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
87 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ}) |
88 | 12 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
89 | | elfznn0 12302 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
90 | 89 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
91 | | dvnf 23496 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
92 | 87, 88, 90, 91 | syl3anc 1318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
93 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁)) |
94 | | dvn2bss 23499 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
95 | 87, 88, 93, 94 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
96 | 5 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
97 | 95, 96 | sseldd 3569 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
98 | 92, 97 | ffvelrnd 6268 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
99 | | faccl 12932 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ0
→ (!‘𝑘) ∈
ℕ) |
100 | 90, 99 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
101 | 100 | nncnd 10913 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ) |
102 | 100 | nnne0d 10942 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0) |
103 | 98, 101, 102 | divcld 10680 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
104 | 43, 4, 103, 32 | dgrle 23803 |
. . 3
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ≤ 𝑁) |
105 | 86, 104 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (deg‘𝑇) ≤ 𝑁) |
106 | 71, 105 | jca 553 |
1
⊢ (𝜑 → (𝑇 ∈ (Poly‘𝐷) ∧ (deg‘𝑇) ≤ 𝑁)) |