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 25257 |
. . . 4
⊢ (𝜑 → 𝑇 = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
8 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
9 | | cnex 10810 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
10 | 9 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → ℂ ∈
V) |
11 | | elpm2r 8526 |
. . . . . . . . . . . 12
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
12 | 10, 1, 2, 3, 11 | syl22anc 839 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
13 | | dvnbss 24825 |
. . . . . . . . . . 11
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑁 ∈
ℕ0) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom 𝐹) |
14 | 1, 12, 4, 13 | syl3anc 1373 |
. . . . . . . . . 10
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom 𝐹) |
15 | 2, 14 | fssdmd 6564 |
. . . . . . . . 9
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ 𝐴) |
16 | | recnprss 24801 |
. . . . . . . . . . 11
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
17 | 1, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
18 | 3, 17 | sstrd 3911 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
19 | 15, 18 | sstrd 3911 |
. . . . . . . 8
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ ℂ) |
20 | 19, 5 | sseldd 3902 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ ℂ) |
21 | 20 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝐵 ∈ ℂ) |
22 | 8, 21 | subcld 11189 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑥 − 𝐵) ∈ ℂ) |
23 | | df-idp 25083 |
. . . . . . . 8
⊢
Xp = ( I ↾ ℂ) |
24 | | mptresid 5918 |
. . . . . . . 8
⊢ ( I
↾ ℂ) = (𝑥
∈ ℂ ↦ 𝑥) |
25 | 23, 24 | eqtri 2765 |
. . . . . . 7
⊢
Xp = (𝑥 ∈ ℂ ↦ 𝑥) |
26 | 25 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Xp =
(𝑥 ∈ ℂ ↦
𝑥)) |
27 | | fconstmpt 5611 |
. . . . . . 7
⊢ (ℂ
× {𝐵}) = (𝑥 ∈ ℂ ↦ 𝐵) |
28 | 27 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (ℂ × {𝐵}) = (𝑥 ∈ ℂ ↦ 𝐵)) |
29 | 10, 8, 21, 26, 28 | offval2 7488 |
. . . . 5
⊢ (𝜑 → (Xp
∘f − (ℂ × {𝐵})) = (𝑥 ∈ ℂ ↦ (𝑥 − 𝐵))) |
30 | | eqidd 2738 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) = (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) |
31 | | oveq1 7220 |
. . . . . . 7
⊢ (𝑦 = (𝑥 − 𝐵) → (𝑦↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
32 | 31 | oveq2d 7229 |
. . . . . 6
⊢ (𝑦 = (𝑥 − 𝐵) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
33 | 32 | sumeq2sdv 15268 |
. . . . 5
⊢ (𝑦 = (𝑥 − 𝐵) → Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)) = Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
34 | 22, 29, 30, 33 | fmptco 6944 |
. . . 4
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵}))) = (𝑥 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
35 | 7, 34 | eqtr4d 2780 |
. . 3
⊢ (𝜑 → 𝑇 = ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵})))) |
36 | | taylply2.1 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
(SubRing‘ℂfld)) |
37 | | cnfldbas 20367 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
38 | 37 | subrgss 19801 |
. . . . . 6
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 𝐷 ⊆ ℂ) |
39 | 36, 38 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷 ⊆ ℂ) |
40 | | taylply2.3 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ 𝐷) |
41 | 39, 4, 40 | elplyd 25096 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∈ (Poly‘𝐷)) |
42 | | cnfld1 20388 |
. . . . . . . 8
⊢ 1 =
(1r‘ℂfld) |
43 | 42 | subrg1cl 19808 |
. . . . . . 7
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 1 ∈ 𝐷) |
44 | 36, 43 | syl 17 |
. . . . . 6
⊢ (𝜑 → 1 ∈ 𝐷) |
45 | | plyid 25103 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ 1 ∈
𝐷) →
Xp ∈ (Poly‘𝐷)) |
46 | 39, 44, 45 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → Xp
∈ (Poly‘𝐷)) |
47 | | taylply2.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝐷) |
48 | | plyconst 25100 |
. . . . . 6
⊢ ((𝐷 ⊆ ℂ ∧ 𝐵 ∈ 𝐷) → (ℂ × {𝐵}) ∈ (Poly‘𝐷)) |
49 | 39, 47, 48 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → (ℂ × {𝐵}) ∈ (Poly‘𝐷)) |
50 | | subrgsubg 19806 |
. . . . . . 7
⊢ (𝐷 ∈
(SubRing‘ℂfld) → 𝐷 ∈
(SubGrp‘ℂfld)) |
51 | 36, 50 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈
(SubGrp‘ℂfld)) |
52 | | cnfldadd 20368 |
. . . . . . . 8
⊢ + =
(+g‘ℂfld) |
53 | 52 | subgcl 18553 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢 + 𝑣) ∈ 𝐷) |
54 | 53 | 3expb 1122 |
. . . . . 6
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 + 𝑣) ∈ 𝐷) |
55 | 51, 54 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 + 𝑣) ∈ 𝐷) |
56 | | cnfldmul 20369 |
. . . . . . . 8
⊢ ·
= (.r‘ℂfld) |
57 | 56 | subrgmcl 19812 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ 𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷) → (𝑢 · 𝑣) ∈ 𝐷) |
58 | 57 | 3expb 1122 |
. . . . . 6
⊢ ((𝐷 ∈
(SubRing‘ℂfld) ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 · 𝑣) ∈ 𝐷) |
59 | 36, 58 | sylan 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐷 ∧ 𝑣 ∈ 𝐷)) → (𝑢 · 𝑣) ∈ 𝐷) |
60 | | ax-1cn 10787 |
. . . . . . 7
⊢ 1 ∈
ℂ |
61 | | cnfldneg 20389 |
. . . . . . 7
⊢ (1 ∈
ℂ → ((invg‘ℂfld)‘1) =
-1) |
62 | 60, 61 | ax-mp 5 |
. . . . . 6
⊢
((invg‘ℂfld)‘1) =
-1 |
63 | | eqid 2737 |
. . . . . . . 8
⊢
(invg‘ℂfld) =
(invg‘ℂfld) |
64 | 63 | subginvcl 18552 |
. . . . . . 7
⊢ ((𝐷 ∈
(SubGrp‘ℂfld) ∧ 1 ∈ 𝐷) →
((invg‘ℂfld)‘1) ∈ 𝐷) |
65 | 51, 44, 64 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 →
((invg‘ℂfld)‘1) ∈ 𝐷) |
66 | 62, 65 | eqeltrrid 2843 |
. . . . 5
⊢ (𝜑 → -1 ∈ 𝐷) |
67 | 46, 49, 55, 59, 66 | plysub 25113 |
. . . 4
⊢ (𝜑 → (Xp
∘f − (ℂ × {𝐵})) ∈ (Poly‘𝐷)) |
68 | 41, 67, 55, 59 | plyco 25135 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵}))) ∈ (Poly‘𝐷)) |
69 | 35, 68 | eqeltrd 2838 |
. 2
⊢ (𝜑 → 𝑇 ∈ (Poly‘𝐷)) |
70 | 35 | fveq2d 6721 |
. . . 4
⊢ (𝜑 → (deg‘𝑇) = (deg‘((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵}))))) |
71 | | eqid 2737 |
. . . . 5
⊢
(deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) = (deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) |
72 | | eqid 2737 |
. . . . 5
⊢
(deg‘(Xp ∘f − (ℂ
× {𝐵}))) =
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))) |
73 | 71, 72, 41, 67 | dgrco 25169 |
. . . 4
⊢ (𝜑 → (deg‘((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∘ (Xp
∘f − (ℂ × {𝐵})))) = ((deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))))) |
74 | | eqid 2737 |
. . . . . . . . 9
⊢
(Xp ∘f − (ℂ ×
{𝐵})) =
(Xp ∘f − (ℂ × {𝐵})) |
75 | 74 | plyremlem 25197 |
. . . . . . . 8
⊢ (𝐵 ∈ ℂ →
((Xp ∘f − (ℂ × {𝐵})) ∈ (Poly‘ℂ)
∧ (deg‘(Xp ∘f − (ℂ
× {𝐵}))) = 1 ∧
(◡(Xp
∘f − (ℂ × {𝐵})) “ {0}) = {𝐵})) |
76 | 20, 75 | syl 17 |
. . . . . . 7
⊢ (𝜑 → ((Xp
∘f − (ℂ × {𝐵})) ∈ (Poly‘ℂ) ∧
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))) = 1 ∧ (◡(Xp ∘f
− (ℂ × {𝐵})) “ {0}) = {𝐵})) |
77 | 76 | simp2d 1145 |
. . . . . 6
⊢ (𝜑 →
(deg‘(Xp ∘f − (ℂ ×
{𝐵}))) =
1) |
78 | 77 | oveq2d 7229 |
. . . . 5
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘f − (ℂ ×
{𝐵})))) =
((deg‘(𝑦 ∈
ℂ ↦ Σ𝑘
∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) · 1)) |
79 | | dgrcl 25127 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))) ∈ (Poly‘𝐷) → (deg‘(𝑦 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈
ℕ0) |
80 | 41, 79 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈
ℕ0) |
81 | 80 | nn0cnd 12152 |
. . . . . 6
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ∈ ℂ) |
82 | 81 | mulid1d 10850 |
. . . . 5
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) · 1) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
83 | 78, 82 | eqtrd 2777 |
. . . 4
⊢ (𝜑 → ((deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ·
(deg‘(Xp ∘f − (ℂ ×
{𝐵})))) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
84 | 70, 73, 83 | 3eqtrd 2781 |
. . 3
⊢ (𝜑 → (deg‘𝑇) = (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘))))) |
85 | 1 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑆 ∈ {ℝ, ℂ}) |
86 | 12 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
87 | | elfznn0 13205 |
. . . . . . . 8
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
88 | 87 | adantl 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℕ0) |
89 | | dvnf 24824 |
. . . . . . 7
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑘 ∈
ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
90 | 85, 86, 88, 89 | syl3anc 1373 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
91 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ (0...𝑁)) |
92 | | dvn2bss 24827 |
. . . . . . . 8
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆)
∧ 𝑘 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
93 | 85, 86, 91, 92 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → dom ((𝑆 D𝑛 𝐹)‘𝑁) ⊆ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
94 | 5 | adantr 484 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑁)) |
95 | 93, 94 | sseldd 3902 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
96 | 90, 95 | ffvelrnd 6905 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
97 | 88 | faccld 13850 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℕ) |
98 | 97 | nncnd 11846 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ∈ ℂ) |
99 | 97 | nnne0d 11880 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (!‘𝑘) ≠ 0) |
100 | 96, 98, 99 | divcld 11608 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
101 | 41, 4, 100, 30 | dgrle 25137 |
. . 3
⊢ (𝜑 → (deg‘(𝑦 ∈ ℂ ↦
Σ𝑘 ∈ (0...𝑁)(((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (𝑦↑𝑘)))) ≤ 𝑁) |
102 | 84, 101 | eqbrtrd 5075 |
. 2
⊢ (𝜑 → (deg‘𝑇) ≤ 𝑁) |
103 | 69, 102 | jca 515 |
1
⊢ (𝜑 → (𝑇 ∈ (Poly‘𝐷) ∧ (deg‘𝑇) ≤ 𝑁)) |