Proof of Theorem tayl0
Step | Hyp | Ref
| Expression |
1 | | taylfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
2 | | taylfval.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
3 | | recnprss 23887 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
5 | 1, 4 | sstrd 3754 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
6 | | fveq2 6353 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘0)) |
7 | 6 | dmeqd 5481 |
. . . . . . 7
⊢ (𝑘 = 0 → dom ((𝑆 D𝑛 𝐹)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘0)) |
8 | 7 | eleq2d 2825 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘0))) |
9 | | taylfval.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
10 | 9 | ralrimiva 3104 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
11 | | taylfval.n |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
12 | | elxnn0 11577 |
. . . . . . . . 9
⊢ (𝑁 ∈
ℕ0* ↔ (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
13 | | 0xr 10298 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
ℕ0* → 0 ∈
ℝ*) |
15 | | xnn0xr 11580 |
. . . . . . . . . 10
⊢ (𝑁 ∈
ℕ0* → 𝑁 ∈
ℝ*) |
16 | | xnn0ge0 12180 |
. . . . . . . . . 10
⊢ (𝑁 ∈
ℕ0* → 0 ≤ 𝑁) |
17 | | lbicc2 12501 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 0 ≤
𝑁) → 0 ∈
(0[,]𝑁)) |
18 | 14, 15, 16, 17 | syl3anc 1477 |
. . . . . . . . 9
⊢ (𝑁 ∈
ℕ0* → 0 ∈ (0[,]𝑁)) |
19 | 12, 18 | sylbir 225 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 = +∞) → 0
∈ (0[,]𝑁)) |
20 | 11, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0[,]𝑁)) |
21 | | 0zd 11601 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
22 | 20, 21 | elind 3941 |
. . . . . 6
⊢ (𝜑 → 0 ∈ ((0[,]𝑁) ∩
ℤ)) |
23 | 8, 10, 22 | rspcdva 3455 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘0)) |
24 | | cnex 10229 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈
V) |
26 | | taylfval.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
27 | | elpm2r 8043 |
. . . . . . . . 9
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
28 | 25, 2, 26, 1, 27 | syl22anc 1478 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
29 | | dvn0 23906 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
30 | 4, 28, 29 | syl2anc 696 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
31 | 30 | dmeqd 5481 |
. . . . . 6
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘0) = dom 𝐹) |
32 | | fdm 6212 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
33 | 26, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
34 | 31, 33 | eqtrd 2794 |
. . . . 5
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘0) = 𝐴) |
35 | 23, 34 | eleqtrd 2841 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
36 | 5, 35 | sseldd 3745 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) |
37 | | cnfldbas 19972 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
38 | | cnfld0 19992 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
39 | | cnring 19990 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
40 | | ringmnd 18776 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
41 | 39, 40 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℂfld
∈ Mnd) |
42 | | ovex 6842 |
. . . . . . . . 9
⊢
(0[,]𝑁) ∈
V |
43 | 42 | inex1 4951 |
. . . . . . . 8
⊢
((0[,]𝑁) ∩
ℤ) ∈ V |
44 | 43 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ∈ V) |
45 | 2 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑆 ∈ {ℝ, ℂ}) |
46 | 28 | adantr 472 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
47 | | simpr 479 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) |
48 | 47 | elin2d 3946 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℤ) |
49 | 47 | elin1d 3945 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ (0[,]𝑁)) |
50 | | nn0re 11513 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
51 | 50 | rexrd 10301 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ*) |
52 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = +∞ → 𝑁 = +∞) |
53 | | pnfxr 10304 |
. . . . . . . . . . . . . . . . . . . 20
⊢ +∞
∈ ℝ* |
54 | 52, 53 | syl6eqel 2847 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = +∞ → 𝑁 ∈
ℝ*) |
55 | 51, 54 | jaoi 393 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 = +∞) → 𝑁 ∈
ℝ*) |
56 | 11, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
57 | 56 | adantr 472 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑁 ∈
ℝ*) |
58 | | elicc1 12432 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
59 | 13, 57, 58 | sylancr 698 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
60 | 49, 59 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁)) |
61 | 60 | simp2d 1138 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ≤ 𝑘) |
62 | | elnn0z 11602 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℤ
∧ 0 ≤ 𝑘)) |
63 | 48, 61, 62 | sylanbrc 701 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℕ0) |
64 | | dvnf 23909 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
65 | 45, 46, 63, 64 | syl3anc 1477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
66 | 65, 9 | ffvelrnd 6524 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
67 | 63 | faccld 13285 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℕ) |
68 | 67 | nncnd 11248 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℂ) |
69 | 67 | nnne0d 11277 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ≠ 0) |
70 | 66, 68, 69 | divcld 11013 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
71 | | 0cnd 10245 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ∈
ℂ) |
72 | 71, 63 | expcld 13222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (0↑𝑘) ∈
ℂ) |
73 | 70, 72 | mulcld 10272 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) ∈ ℂ) |
74 | | eqid 2760 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) |
75 | 73, 74 | fmptd 6549 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))):((0[,]𝑁) ∩
ℤ)⟶ℂ) |
76 | | eldifi 3875 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0}) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) |
77 | 76, 63 | sylan2 492 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ∈
ℕ0) |
78 | | eldifsni 4466 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0}) → 𝑘 ≠ 0) |
79 | 78 | adantl 473 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ≠ 0) |
80 | | elnnne0 11518 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0
∧ 𝑘 ≠
0)) |
81 | 77, 79, 80 | sylanbrc 701 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ∈
ℕ) |
82 | 81 | 0expd 13238 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(0↑𝑘) =
0) |
83 | 82 | oveq2d 6830 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0)) |
84 | 70 | mul01d 10447 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0) |
85 | 76, 84 | sylan2 492 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0) |
86 | 83, 85 | eqtrd 2794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = 0) |
87 | | zex 11598 |
. . . . . . . . . 10
⊢ ℤ
∈ V |
88 | 87 | inex2 4952 |
. . . . . . . . 9
⊢
((0[,]𝑁) ∩
ℤ) ∈ V |
89 | 88 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ∈ V) |
90 | 86, 89 | suppss2 7499 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) supp 0) ⊆ {0}) |
91 | 37, 38, 41, 44, 22, 75, 90 | gsumpt 18581 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) = ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0)) |
92 | 6 | fveq1d 6355 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) = (((𝑆 D𝑛 𝐹)‘0)‘𝐵)) |
93 | | fveq2 6353 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
94 | | fac0 13277 |
. . . . . . . . . . 11
⊢
(!‘0) = 1 |
95 | 93, 94 | syl6eq 2810 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
96 | 92, 95 | oveq12d 6832 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1)) |
97 | | oveq2 6822 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0)) |
98 | | 0exp0e1 13079 |
. . . . . . . . . 10
⊢
(0↑0) = 1 |
99 | 97, 98 | syl6eq 2810 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (0↑𝑘) = 1) |
100 | 96, 99 | oveq12d 6832 |
. . . . . . . 8
⊢ (𝑘 = 0 → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1)) |
101 | | ovex 6842 |
. . . . . . . 8
⊢
(((((𝑆
D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) ∈ V |
102 | 100, 74, 101 | fvmpt 6445 |
. . . . . . 7
⊢ (0 ∈
((0[,]𝑁) ∩ ℤ)
→ ((𝑘 ∈
((0[,]𝑁) ∩ ℤ)
↦ (((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1)) |
103 | 22, 102 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1)) |
104 | 30 | fveq1d 6355 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘0)‘𝐵) = (𝐹‘𝐵)) |
105 | 104 | oveq1d 6829 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) = ((𝐹‘𝐵) / 1)) |
106 | 26, 35 | ffvelrnd 6524 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
107 | 106 | div1d 11005 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝐵) / 1) = (𝐹‘𝐵)) |
108 | 105, 107 | eqtrd 2794 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) = (𝐹‘𝐵)) |
109 | 108 | oveq1d 6829 |
. . . . . . 7
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) = ((𝐹‘𝐵) · 1)) |
110 | 106 | mulid1d 10269 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵) · 1) = (𝐹‘𝐵)) |
111 | 109, 110 | eqtrd 2794 |
. . . . . 6
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) = (𝐹‘𝐵)) |
112 | 91, 103, 111 | 3eqtrd 2798 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) = (𝐹‘𝐵)) |
113 | | ringcmn 18801 |
. . . . . . 7
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
114 | 39, 113 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ CMnd) |
115 | | cnfldtps 22802 |
. . . . . . 7
⊢
ℂfld ∈ TopSp |
116 | 115 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ TopSp) |
117 | | mptexg 6649 |
. . . . . . . 8
⊢
(((0[,]𝑁) ∩
ℤ) ∈ V → (𝑘
∈ ((0[,]𝑁) ∩
ℤ) ↦ (((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V) |
118 | 88, 117 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V) |
119 | | funmpt 6087 |
. . . . . . . 8
⊢ Fun
(𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) |
120 | 119 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → Fun (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) |
121 | | c0ex 10246 |
. . . . . . . 8
⊢ 0 ∈
V |
122 | 121 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
V) |
123 | | snfi 8205 |
. . . . . . . 8
⊢ {0}
∈ Fin |
124 | 123 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → {0} ∈
Fin) |
125 | | suppssfifsupp 8457 |
. . . . . . 7
⊢ ((((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V ∧ Fun (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∧ 0 ∈ V) ∧ ({0} ∈ Fin
∧ ((𝑘 ∈
((0[,]𝑁) ∩ ℤ)
↦ (((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) supp 0) ⊆ {0})) → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) finSupp 0) |
126 | 118, 120,
122, 124, 90, 125 | syl32anc 1485 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) finSupp 0) |
127 | 37, 38, 114, 116, 44, 75, 126 | tsmsid 22164 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) ∈ (ℂfld tsums
(𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))) |
128 | 112, 127 | eqeltrrd 2840 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))) |
129 | 36 | subidd 10592 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐵) = 0) |
130 | 129 | oveq1d 6829 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 − 𝐵)↑𝑘) = (0↑𝑘)) |
131 | 130 | oveq2d 6830 |
. . . . . 6
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) |
132 | 131 | mpteq2dv 4897 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) |
133 | 132 | oveq2d 6830 |
. . . 4
⊢ (𝜑 → (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))) |
134 | 128, 133 | eleqtrrd 2842 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))))) |
135 | | taylfval.t |
. . . 4
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
136 | 2, 26, 1, 11, 9, 135 | eltayl 24333 |
. . 3
⊢ (𝜑 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ ℂ ∧ (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))))))) |
137 | 36, 134, 136 | mpbir2and 995 |
. 2
⊢ (𝜑 → 𝐵𝑇(𝐹‘𝐵)) |
138 | 2, 26, 1, 11, 9, 135 | taylf 24334 |
. . 3
⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ) |
139 | | ffun 6209 |
. . 3
⊢ (𝑇:dom 𝑇⟶ℂ → Fun 𝑇) |
140 | | funbrfv2b 6403 |
. . 3
⊢ (Fun
𝑇 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))) |
141 | 138, 139,
140 | 3syl 18 |
. 2
⊢ (𝜑 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))) |
142 | 137, 141 | mpbid 222 |
1
⊢ (𝜑 → (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵))) |