Step | Hyp | Ref
| Expression |
1 | | taylfval.t |
. 2
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
2 | | df-tayl 25714 |
. . . . 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 2737 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℕ0 ∪
{+∞}) = (ℕ0 ∪ {+∞})) |
5 | | oveq12 7366 |
. . . . . . . . 9
⊢ ((𝑠 = 𝑆 ∧ 𝑓 = 𝐹) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
6 | 5 | ad2antlr 725 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (𝑠 D𝑛 𝑓) = (𝑆 D𝑛 𝐹)) |
7 | 6 | fveq1d 6844 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((𝑠 D𝑛 𝑓)‘𝑘) = ((𝑆 D𝑛 𝐹)‘𝑘)) |
8 | 7 | dmeqd 5861 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → dom ((𝑠 D𝑛 𝑓)‘𝑘) = dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
9 | 8 | iineq2dv 4979 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) = ∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
10 | 7 | fveq1d 6844 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎)) |
11 | 10 | oveq1d 7372 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → ((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘))) |
12 | 11 | oveq1d 7372 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) ∧ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)) → (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) |
13 | 12 | mpteq2dva 5205 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) |
14 | 13 | oveq2d 7373 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) |
15 | 14 | xpeq2d 5663 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
16 | 15 | iuneq2d 4983 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑠 D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
17 | 4, 9, 16 | mpoeq123dv 7432 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 = 𝑆 ∧ 𝑓 = 𝐹)) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑠 D𝑛 𝑓)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑠
D𝑛 𝑓)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
18 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑠 = 𝑆) |
19 | 18 | oveq2d 7373 |
. . . 4
⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (ℂ ↑pm 𝑠) = (ℂ ↑pm
𝑆)) |
20 | | taylfval.s |
. . . 4
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
21 | | cnex 11132 |
. . . . . 6
⊢ ℂ
∈ V |
22 | 21 | a1i 11 |
. . . . 5
⊢ (𝜑 → ℂ ∈
V) |
23 | | taylfval.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
24 | | taylfval.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
25 | | elpm2r 8783 |
. . . . 5
⊢
(((ℂ ∈ V ∧ 𝑆 ∈ {ℝ, ℂ}) ∧ (𝐹:𝐴⟶ℂ ∧ 𝐴 ⊆ 𝑆)) → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
26 | 22, 20, 23, 24, 25 | syl22anc 837 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (ℂ ↑pm 𝑆)) |
27 | | nn0ex 12419 |
. . . . . . 7
⊢
ℕ0 ∈ V |
28 | | snex 5388 |
. . . . . . 7
⊢
{+∞} ∈ V |
29 | 27, 28 | unex 7680 |
. . . . . 6
⊢
(ℕ0 ∪ {+∞}) ∈ V |
30 | | 0xr 11202 |
. . . . . . . . . 10
⊢ 0 ∈
ℝ* |
31 | | nn0ssre 12417 |
. . . . . . . . . . . . 13
⊢
ℕ0 ⊆ ℝ |
32 | | ressxr 11199 |
. . . . . . . . . . . . 13
⊢ ℝ
⊆ ℝ* |
33 | 31, 32 | sstri 3953 |
. . . . . . . . . . . 12
⊢
ℕ0 ⊆ ℝ* |
34 | | pnfxr 11209 |
. . . . . . . . . . . . 13
⊢ +∞
∈ ℝ* |
35 | | snssi 4768 |
. . . . . . . . . . . . 13
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
36 | 34, 35 | ax-mp 5 |
. . . . . . . . . . . 12
⊢
{+∞} ⊆ ℝ* |
37 | 33, 36 | unssi 4145 |
. . . . . . . . . . 11
⊢
(ℕ0 ∪ {+∞}) ⊆
ℝ* |
38 | 37 | sseli 3940 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 𝑛
∈ ℝ*) |
39 | | elun 4108 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) ↔ (𝑛
∈ ℕ0 ∨ 𝑛 ∈ {+∞})) |
40 | | nn0ge0 12438 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ ℕ0
→ 0 ≤ 𝑛) |
41 | | 0lepnf 13053 |
. . . . . . . . . . . . 13
⊢ 0 ≤
+∞ |
42 | | elsni 4603 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ {+∞} → 𝑛 = +∞) |
43 | 41, 42 | breqtrrid 5143 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ {+∞} → 0 ≤
𝑛) |
44 | 40, 43 | jaoi 855 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0 ∨
𝑛 ∈ {+∞}) →
0 ≤ 𝑛) |
45 | 39, 44 | sylbi 216 |
. . . . . . . . . 10
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ≤ 𝑛) |
46 | | lbicc2 13381 |
. . . . . . . . . 10
⊢ ((0
∈ ℝ* ∧ 𝑛 ∈ ℝ* ∧ 0 ≤
𝑛) → 0 ∈
(0[,]𝑛)) |
47 | 30, 38, 45, 46 | mp3an2i 1466 |
. . . . . . . . 9
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → 0 ∈ (0[,]𝑛)) |
48 | | 0z 12510 |
. . . . . . . . 9
⊢ 0 ∈
ℤ |
49 | | inelcm 4424 |
. . . . . . . . 9
⊢ ((0
∈ (0[,]𝑛) ∧ 0
∈ ℤ) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
50 | 47, 48, 49 | sylancl 586 |
. . . . . . . 8
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑛) ∩ ℤ) ≠
∅) |
51 | | fvex 6855 |
. . . . . . . . . 10
⊢ ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
52 | 51 | dmex 7848 |
. . . . . . . . 9
⊢ dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
53 | 52 | rgenw 3068 |
. . . . . . . 8
⊢
∀𝑘 ∈
((0[,]𝑛) ∩ ℤ)dom
((𝑆 D𝑛
𝐹)‘𝑘) ∈ V |
54 | | iinexg 5298 |
. . . . . . . 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 3066 |
. . . . . 6
⊢
∀𝑛 ∈
(ℕ0 ∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V |
57 | | eqid 2736 |
. . . . . . 7
⊢ (𝑛 ∈ (ℕ0
∪ {+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) |
58 | 57 | mpoexxg 8008 |
. . . . . 6
⊢
(((ℕ0 ∪ {+∞}) ∈ V ∧ ∀𝑛 ∈ (ℕ0
∪ {+∞})∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ∈ V) → (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))))) ∈ V) |
59 | 29, 56, 58 | mp2an 690 |
. . . . 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 7506 |
. . 3
⊢ (𝜑 → (𝑆 Tayl 𝐹) = (𝑛 ∈ (ℕ0 ∪
{+∞}), 𝑎 ∈
∩ 𝑘 ∈ ((0[,]𝑛) ∩ ℤ)dom ((𝑆 D𝑛 𝐹)‘𝑘) ↦ ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))))) |
62 | | simprl 769 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑛 = 𝑁) |
63 | 62 | oveq2d 7373 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (0[,]𝑛) = (0[,]𝑁)) |
64 | 63 | ineq1d 4171 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
65 | | simprr 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → 𝑎 = 𝐵) |
66 | 65 | fveq2d 6846 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) = (((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵)) |
67 | 66 | oveq1d 7372 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) = ((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘))) |
68 | 65 | oveq2d 7373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑥 − 𝑎) = (𝑥 − 𝐵)) |
69 | 68 | oveq1d 7372 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ((𝑥 − 𝑎)↑𝑘) = ((𝑥 − 𝐵)↑𝑘)) |
70 | 67, 69 | oveq12d 7375 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)) = (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
71 | 64, 70 | mpteq12dv 5196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) |
72 | 71 | oveq2d 7373 |
. . . . 5
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → (ℂfld tsums
(𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘)))) = (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
73 | 72 | xpeq2d 5663 |
. . . 4
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
74 | 73 | iuneq2d 4983 |
. . 3
⊢ ((𝜑 ∧ (𝑛 = 𝑁 ∧ 𝑎 = 𝐵)) → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑛) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝑎) / (!‘𝑘)) · ((𝑥 − 𝑎)↑𝑘))))) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
75 | | simpr 485 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → 𝑛 = 𝑁) |
76 | 75 | oveq2d 7373 |
. . . . 5
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → (0[,]𝑛) = (0[,]𝑁)) |
77 | 76 | ineq1d 4171 |
. . . 4
⊢ ((𝜑 ∧ 𝑛 = 𝑁) → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
78 | | iineq1 4971 |
. . . 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 11208 |
. . . . . . 7
⊢ +∞
∈ V |
82 | 81 | elsn2 4625 |
. . . . . 6
⊢ (𝑁 ∈ {+∞} ↔ 𝑁 = +∞) |
83 | 82 | orbi2i 911 |
. . . . 5
⊢ ((𝑁 ∈ ℕ0 ∨
𝑁 ∈ {+∞}) ↔
(𝑁 ∈
ℕ0 ∨ 𝑁
= +∞)) |
84 | 80, 83 | sylibr 233 |
. . . 4
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 ∈
{+∞})) |
85 | | elun 4108 |
. . . 4
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) ↔ (𝑁
∈ ℕ0 ∨ 𝑁 ∈ {+∞})) |
86 | 84, 85 | sylibr 233 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (ℕ0 ∪
{+∞})) |
87 | | taylfval.b |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
88 | 87 | ralrimiva 3143 |
. . . 4
⊢ (𝜑 → ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
89 | | oveq2 7365 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑁 → (0[,]𝑛) = (0[,]𝑁)) |
90 | 89 | ineq1d 4171 |
. . . . . . . . 9
⊢ (𝑛 = 𝑁 → ((0[,]𝑛) ∩ ℤ) = ((0[,]𝑁) ∩ ℤ)) |
91 | 90 | neeq1d 3003 |
. . . . . . . 8
⊢ (𝑛 = 𝑁 → (((0[,]𝑛) ∩ ℤ) ≠ ∅ ↔
((0[,]𝑁) ∩ ℤ)
≠ ∅)) |
92 | 91, 50 | vtoclga 3534 |
. . . . . . 7
⊢ (𝑁 ∈ (ℕ0
∪ {+∞}) → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
93 | 86, 92 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((0[,]𝑁) ∩ ℤ) ≠
∅) |
94 | | r19.2z 4452 |
. . . . . 6
⊢
((((0[,]𝑁) ∩
ℤ) ≠ ∅ ∧ ∀𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
95 | 93, 88, 94 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → ∃𝑘 ∈ ((0[,]𝑁) ∩ ℤ)𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
96 | | elex 3463 |
. . . . . 6
⊢ (𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘) → 𝐵 ∈ V) |
97 | 96 | rexlimivw 3148 |
. . . . 5
⊢
(∃𝑘 ∈
((0[,]𝑁) ∩
ℤ)𝐵 ∈ dom
((𝑆 D𝑛
𝐹)‘𝑘) → 𝐵 ∈ V) |
98 | | eliin 4959 |
. . . . 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 4768 |
. . . . . . 7
⊢ (𝑥 ∈ ℂ → {𝑥} ⊆
ℂ) |
102 | 20, 23, 24, 80, 87 | taylfvallem 25717 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) |
103 | | xpss12 5648 |
. . . . . . 7
⊢ (({𝑥} ⊆ ℂ ∧
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) → ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
104 | 101, 102,
103 | syl2an2 684 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
105 | 104 | ralrimiva 3143 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
106 | | iunss 5005 |
. . . . 5
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
↔ ∀𝑥 ∈
ℂ ({𝑥} ×
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
107 | 105, 106 | sylibr 233 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
108 | 21, 21 | xpex 7687 |
. . . . 5
⊢ (ℂ
× ℂ) ∈ V |
109 | 108 | ssex 5278 |
. . . 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 7506 |
. 2
⊢ (𝜑 → (𝑁(𝑆 Tayl 𝐹)𝐵) = ∪
𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
112 | 1, 111 | eqtrid 2788 |
1
⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |