Step | Hyp | Ref
| Expression |
1 | | taylfval.t |
. 2
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
2 | | df-tayl 25523 |
. . . . 5
⊢ Tayl =
(𝑠 ∈ {ℝ,
ℂ}, 𝑓 ∈ (ℂ
↑pm 𝑠)
↦ (𝑛 ∈
(ℕ0 ∪ {+∞}), 𝑎 ∈ ∩
𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
3 | 2 | a1i 11 |
. . . 4
⊢ (𝜑 → Tayl = (𝑠 ∈ {ℝ, ℂ}, 𝑓 ∈ (ℂ
↑pm 𝑠)
↦ (𝑛 ∈
(ℕ0 ∪ {+∞}), 𝑎 ∈ ∩
𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))))) |
4 | | eqidd 2740 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 ∪
{+∞}) = (ℕ0 ∪ {+∞})) |
5 | | oveq12 7293 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑓 = 𝐹) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
6 | 5 | ad2antlr 724 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
7 | 6 | fveq1d 6785 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((𝑠 D𝑛 𝑓)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘)) |
8 | 7 | dmeqd 5817 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → dom ((𝑠 D𝑛 𝑓)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
9 | 8 | iineq2dv 4950 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
10 | 7 | fveq1d 6785 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎)) |
11 | 10 | oveq1d 7299 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘))) |
12 | 11 | oveq1d 7299 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) |
13 | 12 | mpteq2dva 5175 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) |
14 | 13 | oveq2d 7300 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
15 | 14 | xpeq2d 5620 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
16 | 15 | iuneq2d 4954 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
17 | 4, 9, 16 | mpoeq123dv 7359 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
18 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
19 | 18 | oveq2d 7300 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (ℂ ↑pm 𝑠) = (ℂ ↑pm
𝑆)) |
20 | | taylfval.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
21 | | cnex 10961 |
. . . . . 6
⊢ ℂ
∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ∈
V) |
23 | | taylfval.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
24 | | taylfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
25 | | elpm2r 8642 |
. . . . 5
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
26 | 22, 20, 23, 24, 25 | syl22anc 836 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
27 | | nn0ex 12248 |
. . . . . . 7
⊢
ℕ0 ∈ V |
28 | | snex 5355 |
. . . . . . 7
⊢
{+∞} ∈ V |
29 | 27, 28 | unex 7605 |
. . . . . 6
⊢
(ℕ0 ∪ {+∞}) ∈ V |
30 | | 0xr 11031 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
31 | | nn0ssre 12246 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℝ |
32 | | ressxr 11028 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
33 | 31, 32 | sstri 3931 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℝ* |
34 | | pnfxr 11038 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
35 | | snssi 4742 |
. . . . . . . . . . . . 13
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
{+∞} ⊆ ℝ* |
37 | 33, 36 | unssi 4120 |
. . . . . . . . . . 11
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
38 | 37 | sseli 3918 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 𝑛
∈ ℝ*) |
39 | | elun 4084 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) ↔ (𝑛
∈ ℕ0 ∨ 𝑛 ∈ {+∞})) |
40 | | nn0ge0 12267 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 0 ≤ 𝑛) |
41 | | 0lepnf 12877 |
. . . . . . . . . . . . 13
⊢ 0 ≤
+∞ |
42 | | elsni 4579 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {+∞} → 𝑛 = +∞) |
43 | 41, 42 | breqtrrid 5113 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {+∞} → 0 ≤
𝑛) |
44 | 40, 43 | jaoi 854 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0 ∨
𝑛 ∈ {+∞}) →
0 ≤ 𝑛) |
45 | 39, 44 | sylbi 216 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ≤ 𝑛) |
46 | | lbicc2 13205 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 0 ≤
𝑛) → 0 ∈
(0[,]𝑛)) |
47 | 30, 38, 45, 46 | mp3an2i 1465 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ∈ (0[,]𝑛)) |
48 | | 0z 12339 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
49 | | inelcm 4399 |
. . . . . . . . 9
⊢ ((0
∈ (0[,]𝑛) ∧ 0
∈ ℤ) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
50 | 47, 48, 49 | sylancl 586 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
51 | | fvex 6796 |
. . . . . . . . . 10
⊢ ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
52 | 51 | dmex 7767 |
. . . . . . . . 9
⊢ dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
53 | 52 | rgenw 3077 |
. . . . . . . 8
⊢
∀𝑘 ∈
((0[,]𝑛) ∩ ℤ)dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
54 | | iinexg 5266 |
. . . . . . . 8
⊢
((((0[,]𝑛) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) |
55 | 50, 53, 54 | sylancl 586 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) |
56 | 55 | rgen 3075 |
. . . . . 6
⊢
∀𝑛 ∈
(ℕ0 ∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
57 | | eqid 2739 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
58 | 57 | mpoexxg 7925 |
. . . . . 6
⊢
(((ℕ0 ∪ {+∞}) ∈ V ∧ ∀𝑛 ∈ (ℕ0
∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V) |
59 | 29, 56, 58 | mp2an 689 |
. . . . 5
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V |
60 | 59 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V) |
61 | 3, 17, 19, 20, 26, 60 | ovmpodx 7433 |
. . 3
⊢ (𝜑 → (𝑆 Tayl 𝐹) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
62 | | simprl 768 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑛 = 𝑁) |
63 | 62 | oveq2d 7300 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (0[,]𝑛) = (0[,]𝑁)) |
64 | 63 | ineq1d 4146 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
65 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑎 = 𝐵) |
66 | 65 | fveq2d 6787 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵)) |
67 | 66 | oveq1d 7299 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘))) |
68 | 65 | oveq2d 7300 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑥 − 𝑎) = (𝑥 − 𝐵)) |
69 | 68 | oveq1d 7299 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((𝑥 − 𝑎)↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
70 | 67, 69 | oveq12d 7302 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
71 | 64, 70 | mpteq12dv 5166 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
72 | 71 | oveq2d 7300 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
73 | 72 | xpeq2d 5620 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
74 | 73 | iuneq2d 4954 |
. . 3
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
75 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
76 | 75 | oveq2d 7300 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → (0[,]𝑛) = (0[,]𝑁)) |
77 | 76 | ineq1d 4146 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
78 | | iineq1 4942 |
. . . 4
⊢
(((0[,]𝑛) ∩
ℤ) = ((0[,]𝑁) ∩
ℤ) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
79 | 77, 78 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ∩
𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
80 | | taylfval.n |
. . . . 5
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
81 | | pnfex 11037 |
. . . . . . 7
⊢ +∞
∈ V |
82 | 81 | elsn2 4601 |
. . . . . 6
⊢ (𝑁 ∈ {+∞} ↔ 𝑁 = +∞) |
83 | 82 | orbi2i 910 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 ∈ {+∞}) ↔
(𝑁 ∈
ℕ0 ∨ 𝑁
= +∞)) |
84 | 80, 83 | sylibr 233 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 ∈
{+∞})) |
85 | | elun 4084 |
. . . 4
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) ↔ (𝑁
∈ ℕ0 ∨ 𝑁 ∈ {+∞})) |
86 | 84, 85 | sylibr 233 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℕ0 ∪
{+∞})) |
87 | | taylfval.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
88 | 87 | ralrimiva 3104 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
89 | | oveq2 7292 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (0[,]𝑛) = (0[,]𝑁)) |
90 | 89 | ineq1d 4146 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
91 | 90 | neeq1d 3004 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (((0[,]𝑛) ∩ ℤ) ≠ ∅ ↔
((0[,]𝑁) ∩ ℤ)
≠ ∅)) |
92 | 91, 50 | vtoclga 3514 |
. . . . . . 7
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
93 | 86, 92 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
94 | | r19.2z 4426 |
. . . . . 6
⊢
((((0[,]𝑁) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
95 | 93, 88, 94 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
96 | | elex 3451 |
. . . . . 6
⊢ (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) → 𝐵 ∈ V) |
97 | 96 | rexlimivw 3212 |
. . . . 5
⊢
(∃𝑘 ∈
((0[,]𝑁) ∩
ℤ)𝐵 ∈ dom
((𝑆 D𝑛
𝐹)‘𝑘) → 𝐵 ∈ V) |
98 | | eliin 4930 |
. . . . 5
⊢ (𝐵 ∈ V → (𝐵 ∈ ∩ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))) |
99 | 95, 97, 98 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝐵 ∈ ∩
𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))) |
100 | 88, 99 | mpbird 256 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ∩
𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
101 | | snssi 4742 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → {𝑥} ⊆
ℂ) |
102 | 20, 23, 24, 80, 87 | taylfvallem 25526 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) |
103 | | xpss12 5605 |
. . . . . . 7
⊢ (({𝑥} ⊆ ℂ ∧
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) → ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
104 | 101, 102,
103 | syl2an2 683 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
105 | 104 | ralrimiva 3104 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
106 | | iunss 4976 |
. . . . 5
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
↔ ∀𝑥 ∈
ℂ ({𝑥} ×
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
107 | 105, 106 | sylibr 233 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
108 | 21, 21 | xpex 7612 |
. . . . 5
⊢ (ℂ
× ℂ) ∈ V |
109 | 108 | ssex 5246 |
. . . 4
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
→ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ∈ V) |
110 | 107, 109 | syl 17 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ∈ V) |
111 | 61, 74, 79, 86, 100, 110 | ovmpodx 7433 |
. 2
⊢ (𝜑 → (𝑁(𝑆 Tayl 𝐹)𝐵) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
112 | 1, 111 | eqtrid 2791 |
1
⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |