Step | Hyp | Ref
| Expression |
1 | | taylfval.t |
. 2
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
2 | | df-tayl 24550 |
. . . . 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 2779 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 ∪
{+∞}) = (ℕ0 ∪ {+∞})) |
5 | | oveq12 6933 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑓 = 𝐹) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
6 | 5 | ad2antlr 717 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
7 | 6 | fveq1d 6450 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((𝑠 D𝑛 𝑓)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘)) |
8 | 7 | dmeqd 5573 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → dom ((𝑠 D𝑛 𝑓)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
9 | 8 | iineq2dv 4778 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
10 | 7 | fveq1d 6450 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎)) |
11 | 10 | oveq1d 6939 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘))) |
12 | 11 | oveq1d 6939 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) |
13 | 12 | mpteq2dva 4981 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) |
14 | 13 | oveq2d 6940 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
15 | 14 | xpeq2d 5387 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
16 | 15 | iuneq2d 4782 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
17 | 4, 9, 16 | mpt2eq123dv 6996 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
18 | | simpr 479 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
19 | 18 | oveq2d 6940 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (ℂ ↑pm
𝑠) = (ℂ
↑pm 𝑆)) |
20 | | taylfval.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
21 | | cnex 10355 |
. . . . . 6
⊢ ℂ
∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ∈
V) |
23 | | taylfval.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
24 | | taylfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
25 | | elpm2r 8160 |
. . . . 5
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
26 | 22, 20, 23, 24, 25 | syl22anc 829 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm
𝑆)) |
27 | | nn0ex 11653 |
. . . . . . 7
⊢
ℕ0 ∈ V |
28 | | snex 5142 |
. . . . . . 7
⊢
{+∞} ∈ V |
29 | 27, 28 | unex 7235 |
. . . . . 6
⊢
(ℕ0 ∪ {+∞}) ∈ V |
30 | | 0xr 10425 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ* |
31 | 30 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ∈ ℝ*) |
32 | | nn0ssre 11650 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℝ |
33 | | ressxr 10422 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
34 | 32, 33 | sstri 3830 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℝ* |
35 | | pnfxr 10432 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
36 | | snssi 4572 |
. . . . . . . . . . . . 13
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
37 | 35, 36 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
{+∞} ⊆ ℝ* |
38 | 34, 37 | unssi 4011 |
. . . . . . . . . . 11
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
39 | 38 | sseli 3817 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 𝑛
∈ ℝ*) |
40 | | elun 3976 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) ↔ (𝑛
∈ ℕ0 ∨ 𝑛 ∈ {+∞})) |
41 | | nn0ge0 11673 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 0 ≤ 𝑛) |
42 | | 0lepnf 12281 |
. . . . . . . . . . . . 13
⊢ 0 ≤
+∞ |
43 | | elsni 4415 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {+∞} → 𝑛 = +∞) |
44 | 42, 43 | syl5breqr 4926 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {+∞} → 0 ≤
𝑛) |
45 | 41, 44 | jaoi 846 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0 ∨
𝑛 ∈ {+∞}) →
0 ≤ 𝑛) |
46 | 40, 45 | sylbi 209 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ≤ 𝑛) |
47 | | lbicc2 12606 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 0 ≤
𝑛) → 0 ∈
(0[,]𝑛)) |
48 | 31, 39, 46, 47 | syl3anc 1439 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ∈ (0[,]𝑛)) |
49 | | 0z 11743 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
50 | | inelcm 4257 |
. . . . . . . . 9
⊢ ((0
∈ (0[,]𝑛) ∧ 0
∈ ℤ) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
51 | 48, 49, 50 | sylancl 580 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
52 | | fvex 6461 |
. . . . . . . . . 10
⊢ ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
53 | 52 | dmex 7380 |
. . . . . . . . 9
⊢ dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
54 | 53 | rgenw 3106 |
. . . . . . . 8
⊢
∀𝑘 ∈
((0[,]𝑛) ∩ ℤ)dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
55 | | iinexg 5060 |
. . . . . . . 8
⊢
((((0[,]𝑛) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) |
56 | 51, 54, 55 | sylancl 580 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) |
57 | 56 | rgen 3104 |
. . . . . 6
⊢
∀𝑛 ∈
(ℕ0 ∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
58 | | eqid 2778 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
59 | 58 | mpt2exxg 7526 |
. . . . . 6
⊢
(((ℕ0 ∪ {+∞}) ∈ V ∧ ∀𝑛 ∈ (ℕ0
∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V) |
60 | 29, 57, 59 | mp2an 682 |
. . . . 5
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V |
61 | 60 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V) |
62 | 3, 17, 19, 20, 26, 61 | ovmpt2dx 7066 |
. . 3
⊢ (𝜑 → (𝑆 Tayl 𝐹) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
63 | | simprl 761 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑛 = 𝑁) |
64 | 63 | oveq2d 6940 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (0[,]𝑛) = (0[,]𝑁)) |
65 | 64 | ineq1d 4036 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
66 | | simprr 763 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑎 = 𝐵) |
67 | 66 | fveq2d 6452 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵)) |
68 | 67 | oveq1d 6939 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘))) |
69 | 66 | oveq2d 6940 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑥 − 𝑎) = (𝑥 − 𝐵)) |
70 | 69 | oveq1d 6939 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((𝑥 − 𝑎)↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
71 | 68, 70 | oveq12d 6942 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
72 | 65, 71 | mpteq12dv 4971 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
73 | 72 | oveq2d 6940 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
74 | 73 | xpeq2d 5387 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
75 | 74 | iuneq2d 4782 |
. . 3
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
76 | | simpr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
77 | 76 | oveq2d 6940 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → (0[,]𝑛) = (0[,]𝑁)) |
78 | 77 | ineq1d 4036 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
79 | | iineq1 4770 |
. . . 4
⊢
(((0[,]𝑛) ∩
ℤ) = ((0[,]𝑁) ∩
ℤ) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
80 | 78, 79 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ∩
𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
81 | | taylfval.n |
. . . . 5
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
82 | | pnfex 10431 |
. . . . . . 7
⊢ +∞
∈ V |
83 | 82 | elsn2 4433 |
. . . . . 6
⊢ (𝑁 ∈ {+∞} ↔ 𝑁 = +∞) |
84 | 83 | orbi2i 899 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 ∈ {+∞}) ↔
(𝑁 ∈
ℕ0 ∨ 𝑁
= +∞)) |
85 | 81, 84 | sylibr 226 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 ∈
{+∞})) |
86 | | elun 3976 |
. . . 4
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) ↔ (𝑁
∈ ℕ0 ∨ 𝑁 ∈ {+∞})) |
87 | 85, 86 | sylibr 226 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℕ0 ∪
{+∞})) |
88 | | taylfval.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
89 | 88 | ralrimiva 3148 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
90 | | oveq2 6932 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (0[,]𝑛) = (0[,]𝑁)) |
91 | 90 | ineq1d 4036 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
92 | 91 | neeq1d 3028 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (((0[,]𝑛) ∩ ℤ) ≠ ∅ ↔
((0[,]𝑁) ∩ ℤ)
≠ ∅)) |
93 | 92, 51 | vtoclga 3474 |
. . . . . . 7
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
94 | 87, 93 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
95 | | r19.2z 4283 |
. . . . . 6
⊢
((((0[,]𝑁) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
96 | 94, 89, 95 | syl2anc 579 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
97 | | elex 3414 |
. . . . . 6
⊢ (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) → 𝐵 ∈ V) |
98 | 97 | rexlimivw 3211 |
. . . . 5
⊢
(∃𝑘 ∈
((0[,]𝑁) ∩
ℤ)𝐵 ∈ dom
((𝑆 D𝑛
𝐹)‘𝑘) → 𝐵 ∈ V) |
99 | | eliin 4760 |
. . . . 5
⊢ (𝐵 ∈ V → (𝐵 ∈ ∩ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))) |
100 | 96, 98, 99 | 3syl 18 |
. . . 4
⊢ (𝜑 → (𝐵 ∈ ∩
𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↔ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘))) |
101 | 89, 100 | mpbird 249 |
. . 3
⊢ (𝜑 → 𝐵 ∈ ∩
𝑘 ∈ ((0[,]𝑁) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
102 | | snssi 4572 |
. . . . . . . 8
⊢ (𝑥 ∈ ℂ → {𝑥} ⊆
ℂ) |
103 | 102 | adantl 475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → {𝑥} ⊆ ℂ) |
104 | 20, 23, 24, 81, 88 | taylfvallem 24553 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) |
105 | | xpss12 5372 |
. . . . . . 7
⊢ (({𝑥} ⊆ ℂ ∧
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) → ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
106 | 103, 104,
105 | syl2anc 579 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
107 | 106 | ralrimiva 3148 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
108 | | iunss 4796 |
. . . . 5
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
↔ ∀𝑥 ∈
ℂ ({𝑥} ×
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
109 | 107, 108 | sylibr 226 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
110 | 21, 21 | xpex 7242 |
. . . . 5
⊢ (ℂ
× ℂ) ∈ V |
111 | 110 | ssex 5041 |
. . . 4
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
→ ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ∈ V) |
112 | 109, 111 | syl 17 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ∈ V) |
113 | 62, 75, 80, 87, 101, 112 | ovmpt2dx 7066 |
. 2
⊢ (𝜑 → (𝑁(𝑆 Tayl 𝐹)𝐵) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
114 | 1, 113 | syl5eq 2826 |
1
⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |