Step | Hyp | Ref
| Expression |
1 | | taylfval.t |
. 2
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
2 | | df-tayl 25094 |
. . . . 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 2739 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 ∪
{+∞}) = (ℕ0 ∪ {+∞})) |
5 | | oveq12 7173 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑓 = 𝐹) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
6 | 5 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
7 | 6 | fveq1d 6670 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((𝑠 D𝑛 𝑓)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘)) |
8 | 7 | dmeqd 5742 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → dom ((𝑠 D𝑛 𝑓)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
9 | 8 | iineq2dv 4903 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
10 | 7 | fveq1d 6670 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎)) |
11 | 10 | oveq1d 7179 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘))) |
12 | 11 | oveq1d 7179 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) |
13 | 12 | mpteq2dva 5122 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) |
14 | 13 | oveq2d 7180 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
15 | 14 | xpeq2d 5549 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
16 | 15 | iuneq2d 4907 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
17 | 4, 9, 16 | mpoeq123dv 7237 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
18 | | simpr 488 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
19 | 18 | oveq2d 7180 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (ℂ ↑pm 𝑠) = (ℂ ↑pm
𝑆)) |
20 | | taylfval.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
21 | | cnex 10689 |
. . . . . 6
⊢ ℂ
∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ∈
V) |
23 | | taylfval.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
24 | | taylfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
25 | | elpm2r 8448 |
. . . . 5
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
26 | 22, 20, 23, 24, 25 | syl22anc 838 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
27 | | nn0ex 11975 |
. . . . . . 7
⊢
ℕ0 ∈ V |
28 | | snex 5295 |
. . . . . . 7
⊢
{+∞} ∈ V |
29 | 27, 28 | unex 7481 |
. . . . . 6
⊢
(ℕ0 ∪ {+∞}) ∈ V |
30 | | 0xr 10759 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
31 | | nn0ssre 11973 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℝ |
32 | | ressxr 10756 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
33 | 31, 32 | sstri 3884 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℝ* |
34 | | pnfxr 10766 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
35 | | snssi 4693 |
. . . . . . . . . . . . 13
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
{+∞} ⊆ ℝ* |
37 | 33, 36 | unssi 4073 |
. . . . . . . . . . 11
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
38 | 37 | sseli 3871 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 𝑛
∈ ℝ*) |
39 | | elun 4037 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) ↔ (𝑛
∈ ℕ0 ∨ 𝑛 ∈ {+∞})) |
40 | | nn0ge0 11994 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 0 ≤ 𝑛) |
41 | | 0lepnf 12603 |
. . . . . . . . . . . . 13
⊢ 0 ≤
+∞ |
42 | | elsni 4530 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {+∞} → 𝑛 = +∞) |
43 | 41, 42 | breqtrrid 5065 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {+∞} → 0 ≤
𝑛) |
44 | 40, 43 | jaoi 856 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0 ∨
𝑛 ∈ {+∞}) →
0 ≤ 𝑛) |
45 | 39, 44 | sylbi 220 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ≤ 𝑛) |
46 | | lbicc2 12931 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 0 ≤
𝑛) → 0 ∈
(0[,]𝑛)) |
47 | 30, 38, 45, 46 | mp3an2i 1467 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ∈ (0[,]𝑛)) |
48 | | 0z 12066 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
49 | | inelcm 4351 |
. . . . . . . . 9
⊢ ((0
∈ (0[,]𝑛) ∧ 0
∈ ℤ) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
50 | 47, 48, 49 | sylancl 589 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
51 | | fvex 6681 |
. . . . . . . . . 10
⊢ ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
52 | 51 | dmex 7635 |
. . . . . . . . 9
⊢ dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
53 | 52 | rgenw 3065 |
. . . . . . . 8
⊢
∀𝑘 ∈
((0[,]𝑛) ∩ ℤ)dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
54 | | iinexg 5206 |
. . . . . . . 8
⊢
((((0[,]𝑛) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) |
55 | 50, 53, 54 | sylancl 589 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) |
56 | 55 | rgen 3063 |
. . . . . 6
⊢
∀𝑛 ∈
(ℕ0 ∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
57 | | eqid 2738 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
58 | 57 | mpoexxg 7792 |
. . . . . 6
⊢
(((ℕ0 ∪ {+∞}) ∈ V ∧ ∀𝑛 ∈ (ℕ0
∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V) |
59 | 29, 56, 58 | mp2an 692 |
. . . . 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 7310 |
. . 3
⊢ (𝜑 → (𝑆 Tayl 𝐹) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
62 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑛 = 𝑁) |
63 | 62 | oveq2d 7180 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (0[,]𝑛) = (0[,]𝑁)) |
64 | 63 | ineq1d 4100 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
65 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑎 = 𝐵) |
66 | 65 | fveq2d 6672 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵)) |
67 | 66 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘))) |
68 | 65 | oveq2d 7180 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑥 − 𝑎) = (𝑥 − 𝐵)) |
69 | 68 | oveq1d 7179 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((𝑥 − 𝑎)↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
70 | 67, 69 | oveq12d 7182 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
71 | 64, 70 | mpteq12dv 5112 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
72 | 71 | oveq2d 7180 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
73 | 72 | xpeq2d 5549 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
74 | 73 | iuneq2d 4907 |
. . 3
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
75 | | simpr 488 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
76 | 75 | oveq2d 7180 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → (0[,]𝑛) = (0[,]𝑁)) |
77 | 76 | ineq1d 4100 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
78 | | iineq1 4895 |
. . . 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 10765 |
. . . . . . 7
⊢ +∞
∈ V |
82 | 81 | elsn2 4552 |
. . . . . 6
⊢ (𝑁 ∈ {+∞} ↔ 𝑁 = +∞) |
83 | 82 | orbi2i 912 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 ∈ {+∞}) ↔
(𝑁 ∈
ℕ0 ∨ 𝑁
= +∞)) |
84 | 80, 83 | sylibr 237 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 ∈
{+∞})) |
85 | | elun 4037 |
. . . 4
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) ↔ (𝑁
∈ ℕ0 ∨ 𝑁 ∈ {+∞})) |
86 | 84, 85 | sylibr 237 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℕ0 ∪
{+∞})) |
87 | | taylfval.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
88 | 87 | ralrimiva 3096 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
89 | | oveq2 7172 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (0[,]𝑛) = (0[,]𝑁)) |
90 | 89 | ineq1d 4100 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
91 | 90 | neeq1d 2993 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (((0[,]𝑛) ∩ ℤ) ≠ ∅ ↔
((0[,]𝑁) ∩ ℤ)
≠ ∅)) |
92 | 91, 50 | vtoclga 3477 |
. . . . . . 7
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
93 | 86, 92 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
94 | | r19.2z 4378 |
. . . . . 6
⊢
((((0[,]𝑁) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
95 | 93, 88, 94 | syl2anc 587 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
96 | | elex 3415 |
. . . . . 6
⊢ (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) → 𝐵 ∈ V) |
97 | 96 | rexlimivw 3191 |
. . . . 5
⊢
(∃𝑘 ∈
((0[,]𝑁) ∩
ℤ)𝐵 ∈ dom
((𝑆 D𝑛
𝐹)‘𝑘) → 𝐵 ∈ V) |
98 | | eliin 4883 |
. . . . 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 260 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ∩
𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
101 | | snssi 4693 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → {𝑥} ⊆
ℂ) |
102 | 20, 23, 24, 80, 87 | taylfvallem 25097 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) |
103 | | xpss12 5534 |
. . . . . . 7
⊢ (({𝑥} ⊆ ℂ ∧
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) → ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
104 | 101, 102,
103 | syl2an2 686 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
105 | 104 | ralrimiva 3096 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
106 | | iunss 4928 |
. . . . 5
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
↔ ∀𝑥 ∈
ℂ ({𝑥} ×
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
107 | 105, 106 | sylibr 237 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
108 | 21, 21 | xpex 7488 |
. . . . 5
⊢ (ℂ
× ℂ) ∈ V |
109 | 108 | ssex 5186 |
. . . 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 7310 |
. 2
⊢ (𝜑 → (𝑁(𝑆 Tayl 𝐹)𝐵) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
112 | 1, 111 | syl5eq 2785 |
1
⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |