Proof of Theorem tayl0
Step | Hyp | Ref
| Expression |
1 | | taylfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
2 | | taylfval.s |
. . . . . 6
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
3 | | recnprss 23474 |
. . . . . 6
⊢ (𝑆 ∈ {ℝ, ℂ}
→ 𝑆 ⊆
ℂ) |
4 | 2, 3 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
5 | 1, 4 | sstrd 3578 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ ℂ) |
6 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑘 = 0 → ((𝑆 D𝑛 𝐹)‘𝑘) = ((𝑆 D𝑛 𝐹)‘0)) |
7 | 6 | dmeqd 5248 |
. . . . . . 7
⊢ (𝑘 = 0 → dom ((𝑆 D𝑛 𝐹)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘0)) |
8 | 7 | eleq2d 2673 |
. . . . . 6
⊢ (𝑘 = 0 → (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘0))) |
9 | | taylfval.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
10 | 9 | ralrimiva 2949 |
. . . . . 6
⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
11 | | taylfval.n |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
12 | | elxnn0 11242 |
. . . . . . . . 9
⊢ (𝑁 ∈
ℕ0* ↔ (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
13 | | 0xr 9965 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
14 | 13 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
ℕ0* → 0 ∈
ℝ*) |
15 | | xnn0xr 11245 |
. . . . . . . . . 10
⊢ (𝑁 ∈
ℕ0* → 𝑁 ∈
ℝ*) |
16 | | xnn0ge0 11843 |
. . . . . . . . . 10
⊢ (𝑁 ∈
ℕ0* → 0 ≤ 𝑁) |
17 | | lbicc2 12159 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑁 ∈ ℝ* ∧ 0 ≤
𝑁) → 0 ∈
(0[,]𝑁)) |
18 | 14, 15, 16, 17 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑁 ∈
ℕ0* → 0 ∈ (0[,]𝑁)) |
19 | 12, 18 | sylbir 224 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 = +∞) → 0
∈ (0[,]𝑁)) |
20 | 11, 19 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 0 ∈ (0[,]𝑁)) |
21 | | 0zd 11266 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
ℤ) |
22 | 20, 21 | elind 3760 |
. . . . . 6
⊢ (𝜑 → 0 ∈ ((0[,]𝑁) ∩
ℤ)) |
23 | 8, 10, 22 | rspcdva 3288 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘0)) |
24 | | cnex 9896 |
. . . . . . . . . 10
⊢ ℂ
∈ V |
25 | 24 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ℂ ∈
V) |
26 | | taylfval.f |
. . . . . . . . 9
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
27 | | elpm2r 7761 |
. . . . . . . . 9
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
28 | 25, 2, 26, 1, 27 | syl22anc 1319 |
. . . . . . . 8
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
29 | | dvn0 23493 |
. . . . . . . 8
⊢ ((𝑆 ⊆ ℂ ∧ 𝐹 ∈ (ℂ
↑pm 𝑆)) → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
30 | 4, 28, 29 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ((𝑆 D𝑛 𝐹)‘0) = 𝐹) |
31 | 30 | dmeqd 5248 |
. . . . . 6
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘0) = dom 𝐹) |
32 | | fdm 5964 |
. . . . . . 7
⊢ (𝐹:𝐴⟶ℂ → dom 𝐹 = 𝐴) |
33 | 26, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → dom 𝐹 = 𝐴) |
34 | 31, 33 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → dom ((𝑆 D𝑛 𝐹)‘0) = 𝐴) |
35 | 23, 34 | eleqtrd 2690 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ 𝐴) |
36 | 5, 35 | sseldd 3569 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ℂ) |
37 | | cnfldbas 19571 |
. . . . . . 7
⊢ ℂ =
(Base‘ℂfld) |
38 | | cnfld0 19589 |
. . . . . . 7
⊢ 0 =
(0g‘ℂfld) |
39 | | cnring 19587 |
. . . . . . . 8
⊢
ℂfld ∈ Ring |
40 | | ringmnd 18379 |
. . . . . . . 8
⊢
(ℂfld ∈ Ring → ℂfld ∈
Mnd) |
41 | 39, 40 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → ℂfld
∈ Mnd) |
42 | | ovex 6577 |
. . . . . . . . 9
⊢
(0[,]𝑁) ∈
V |
43 | 42 | inex1 4727 |
. . . . . . . 8
⊢
((0[,]𝑁) ∩
ℤ) ∈ V |
44 | 43 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ∈ V) |
45 | 2 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑆 ∈ {ℝ, ℂ}) |
46 | 28 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
47 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) |
48 | 47 | elin2d 3765 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℤ) |
49 | 47 | elin1d 3764 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ (0[,]𝑁)) |
50 | | nn0re 11178 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ) |
51 | 50 | rexrd 9968 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈
ℝ*) |
52 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑁 = +∞ → 𝑁 = +∞) |
53 | | pnfxr 9971 |
. . . . . . . . . . . . . . . . . . . 20
⊢ +∞
∈ ℝ* |
54 | 52, 53 | syl6eqel 2696 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑁 = +∞ → 𝑁 ∈
ℝ*) |
55 | 51, 54 | jaoi 393 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 = +∞) → 𝑁 ∈
ℝ*) |
56 | 11, 55 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝑁 ∈
ℝ*) |
57 | 56 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑁 ∈
ℝ*) |
58 | | elicc1 12090 |
. . . . . . . . . . . . . . . 16
⊢ ((0
∈ ℝ* ∧ 𝑁 ∈ ℝ*) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
59 | 13, 57, 58 | sylancr 694 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ (0[,]𝑁) ↔ (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁))) |
60 | 49, 59 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (𝑘 ∈ ℝ* ∧ 0 ≤
𝑘 ∧ 𝑘 ≤ 𝑁)) |
61 | 60 | simp2d 1067 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ≤ 𝑘) |
62 | | elnn0z 11267 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ0
↔ (𝑘 ∈ ℤ
∧ 0 ≤ 𝑘)) |
63 | 48, 61, 62 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝑘 ∈ ℕ0) |
64 | | dvnf 23496 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∈ {ℝ, ℂ} ∧
𝐹 ∈ (ℂ
↑pm 𝑆) ∧ 𝑘 ∈ ℕ0) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
65 | 45, 46, 63, 64 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((𝑆 D𝑛 𝐹)‘𝑘):dom ((𝑆 D𝑛 𝐹)‘𝑘)⟶ℂ) |
66 | 65, 9 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) ∈ ℂ) |
67 | 63 | faccld 12933 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℕ) |
68 | 67 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ∈
ℂ) |
69 | 67 | nnne0d 10942 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (!‘𝑘) ≠ 0) |
70 | 66, 68, 69 | divcld 10680 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) ∈ ℂ) |
71 | | 0cnd 9912 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 0 ∈
ℂ) |
72 | 71, 63 | expcld 12870 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (0↑𝑘) ∈
ℂ) |
73 | 70, 72 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) ∈ ℂ) |
74 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) |
75 | 73, 74 | fmptd 6292 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))):((0[,]𝑁) ∩
ℤ)⟶ℂ) |
76 | | eldifi 3694 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0}) → 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) |
77 | 76, 63 | sylan2 490 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ∈
ℕ0) |
78 | | eldifsni 4261 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0}) → 𝑘 ≠ 0) |
79 | 78 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ≠ 0) |
80 | | elnnne0 11183 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ ↔ (𝑘 ∈ ℕ0
∧ 𝑘 ≠
0)) |
81 | 77, 79, 80 | sylanbrc 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) → 𝑘 ∈
ℕ) |
82 | 81 | 0expd 12886 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(0↑𝑘) =
0) |
83 | 82 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0)) |
84 | 70 | mul01d 10114 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0) |
85 | 76, 84 | sylan2 490 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · 0) = 0) |
86 | 83, 85 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ (((0[,]𝑁) ∩ ℤ) ∖ {0})) →
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = 0) |
87 | | zex 11263 |
. . . . . . . . . 10
⊢ ℤ
∈ V |
88 | 87 | inex2 4728 |
. . . . . . . . 9
⊢
((0[,]𝑁) ∩
ℤ) ∈ V |
89 | 88 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ∈ V) |
90 | 86, 89 | suppss2 7216 |
. . . . . . 7
⊢ (𝜑 → ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) supp 0) ⊆ {0}) |
91 | 37, 38, 41, 44, 22, 75, 90 | gsumpt 18184 |
. . . . . 6
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) = ((𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))‘0)) |
92 | 6 | fveq1d 6105 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) = (((𝑆 D𝑛 𝐹)‘0)‘𝐵)) |
93 | | fveq2 6103 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (!‘𝑘) =
(!‘0)) |
94 | | fac0 12925 |
. . . . . . . . . . 11
⊢
(!‘0) = 1 |
95 | 93, 94 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (!‘𝑘) = 1) |
96 | 92, 95 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑘 = 0 → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1)) |
97 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑘 = 0 → (0↑𝑘) = (0↑0)) |
98 | | 0exp0e1 12727 |
. . . . . . . . . 10
⊢
(0↑0) = 1 |
99 | 97, 98 | syl6eq 2660 |
. . . . . . . . 9
⊢ (𝑘 = 0 → (0↑𝑘) = 1) |
100 | 96, 99 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝑘 = 0 → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1)) |
101 | | ovex 6577 |
. . . . . . . 8
⊢
(((((𝑆
D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) ∈ V |
102 | 100, 74, 101 | fvmpt 6191 |
. . . . . . 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 6105 |
. . . . . . . . . 10
⊢ (𝜑 → (((𝑆 D𝑛 𝐹)‘0)‘𝐵) = (𝐹‘𝐵)) |
105 | 104 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) = ((𝐹‘𝐵) / 1)) |
106 | 26, 35 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹‘𝐵) ∈ ℂ) |
107 | 106 | div1d 10672 |
. . . . . . . . 9
⊢ (𝜑 → ((𝐹‘𝐵) / 1) = (𝐹‘𝐵)) |
108 | 105, 107 | eqtrd 2644 |
. . . . . . . 8
⊢ (𝜑 → ((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) = (𝐹‘𝐵)) |
109 | 108 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) = ((𝐹‘𝐵) · 1)) |
110 | 106 | mulid1d 9936 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝐵) · 1) = (𝐹‘𝐵)) |
111 | 109, 110 | eqtrd 2644 |
. . . . . 6
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘0)‘𝐵) / 1) · 1) = (𝐹‘𝐵)) |
112 | 91, 103, 111 | 3eqtrd 2648 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) = (𝐹‘𝐵)) |
113 | | ringcmn 18404 |
. . . . . . 7
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
114 | 39, 113 | mp1i 13 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ CMnd) |
115 | | cnfldtps 22391 |
. . . . . . 7
⊢
ℂfld ∈ TopSp |
116 | 115 | a1i 11 |
. . . . . 6
⊢ (𝜑 → ℂfld
∈ TopSp) |
117 | | mptexg 6389 |
. . . . . . . 8
⊢
(((0[,]𝑁) ∩
ℤ) ∈ V → (𝑘
∈ ((0[,]𝑁) ∩
ℤ) ↦ (((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V) |
118 | 88, 117 | mp1i 13 |
. . . . . . 7
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) ∈ V) |
119 | | funmpt 5840 |
. . . . . . . 8
⊢ Fun
(𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) |
120 | 119 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → Fun (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) |
121 | | c0ex 9913 |
. . . . . . . 8
⊢ 0 ∈
V |
122 | 121 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 0 ∈
V) |
123 | | snfi 7923 |
. . . . . . . 8
⊢ {0}
∈ Fin |
124 | 123 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → {0} ∈
Fin) |
125 | | suppssfifsupp 8173 |
. . . . . . 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 1326 |
. . . . . 6
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) finSupp 0) |
127 | 37, 38, 114, 116, 44, 75, 126 | tsmsid 21753 |
. . . . 5
⊢ (𝜑 → (ℂfld
Σg (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) ∈ (ℂfld tsums
(𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))) |
128 | 112, 127 | eqeltrrd 2689 |
. . . 4
⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))) |
129 | 36 | subidd 10259 |
. . . . . . . 8
⊢ (𝜑 → (𝐵 − 𝐵) = 0) |
130 | 129 | oveq1d 6564 |
. . . . . . 7
⊢ (𝜑 → ((𝐵 − 𝐵)↑𝑘) = (0↑𝑘)) |
131 | 130 | oveq2d 6565 |
. . . . . 6
⊢ (𝜑 → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))) |
132 | 131 | mpteq2dv 4673 |
. . . . 5
⊢ (𝜑 → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘)))) |
133 | 132 | oveq2d 6565 |
. . . 4
⊢ (𝜑 → (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · (0↑𝑘))))) |
134 | 128, 133 | eleqtrrd 2691 |
. . 3
⊢ (𝜑 → (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))))) |
135 | | taylfval.t |
. . . 4
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
136 | 2, 26, 1, 11, 9, 135 | eltayl 23918 |
. . 3
⊢ (𝜑 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ ℂ ∧ (𝐹‘𝐵) ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝐵 − 𝐵)↑𝑘))))))) |
137 | 36, 134, 136 | mpbir2and 959 |
. 2
⊢ (𝜑 → 𝐵𝑇(𝐹‘𝐵)) |
138 | 2, 26, 1, 11, 9, 135 | taylf 23919 |
. . 3
⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ) |
139 | | ffun 5961 |
. . 3
⊢ (𝑇:dom 𝑇⟶ℂ → Fun 𝑇) |
140 | | funbrfv2b 6150 |
. . 3
⊢ (Fun
𝑇 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))) |
141 | 138, 139,
140 | 3syl 18 |
. 2
⊢ (𝜑 → (𝐵𝑇(𝐹‘𝐵) ↔ (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵)))) |
142 | 137, 141 | mpbid 221 |
1
⊢ (𝜑 → (𝐵 ∈ dom 𝑇 ∧ (𝑇‘𝐵) = (𝐹‘𝐵))) |