Step | Hyp | Ref
| Expression |
1 | | taylfval.s |
. . . . . . 7
⊢ (𝜑 → 𝑆 ∈ {ℝ, ℂ}) |
2 | | taylfval.f |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴⟶ℂ) |
3 | | taylfval.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
4 | | taylfval.n |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ ℕ0 ∨ 𝑁 = +∞)) |
5 | | taylfval.b |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → 𝐵 ∈ dom ((𝑆 D𝑛 𝐹)‘𝑘)) |
6 | | taylfval.t |
. . . . . . 7
⊢ 𝑇 = (𝑁(𝑆 Tayl 𝐹)𝐵) |
7 | 1, 2, 3, 4, 5, 6 | taylfval 23917 |
. . . . . 6
⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
8 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
9 | 8 | snssd 4281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → {𝑥} ⊆ ℂ) |
10 | 1, 2, 3, 4, 5 | taylfvallem 23916 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) |
11 | | xpss12 5148 |
. . . . . . . . 9
⊢ (({𝑥} ⊆ ℂ ∧
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) → ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
12 | 9, 10, 11 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
13 | 12 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
14 | | iunss 4497 |
. . . . . . 7
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
↔ ∀𝑥 ∈
ℂ ({𝑥} ×
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
15 | 13, 14 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
16 | 7, 15 | eqsstrd 3602 |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ (ℂ ×
ℂ)) |
17 | | relxp 5150 |
. . . . 5
⊢ Rel
(ℂ × ℂ) |
18 | | relss 5129 |
. . . . 5
⊢ (𝑇 ⊆ (ℂ ×
ℂ) → (Rel (ℂ × ℂ) → Rel 𝑇)) |
19 | 16, 17, 18 | mpisyl 21 |
. . . 4
⊢ (𝜑 → Rel 𝑇) |
20 | 1, 2, 3, 4, 5, 6 | eltayl 23918 |
. . . . . . . 8
⊢ (𝜑 → (𝑥𝑇𝑦 ↔ (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))) |
21 | 20 | biimpd 218 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝑇𝑦 → (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))) |
22 | 21 | alrimiv 1842 |
. . . . . 6
⊢ (𝜑 → ∀𝑦(𝑥𝑇𝑦 → (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))) |
23 | | cnfldbas 19571 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
24 | | cnring 19587 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
25 | | ringcmn 18404 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ℂfld
∈ CMnd) |
27 | | cnfldtps 22391 |
. . . . . . . . . 10
⊢
ℂfld ∈ TopSp |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ℂfld
∈ TopSp) |
29 | | ovex 6577 |
. . . . . . . . . . 11
⊢
(0[,]𝑁) ∈
V |
30 | 29 | inex1 4727 |
. . . . . . . . . 10
⊢
((0[,]𝑁) ∩
ℤ) ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((0[,]𝑁) ∩ ℤ) ∈
V) |
32 | 1, 2, 3, 4, 5 | taylfvallem1 23915 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)) ∈ ℂ) |
33 | | eqid 2610 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) = (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))) |
34 | 32, 33 | fmptd 6292 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))):((0[,]𝑁) ∩
ℤ)⟶ℂ) |
35 | | eqid 2610 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
36 | 35 | cnfldhaus 22398 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Haus |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(TopOpen‘ℂfld) ∈ Haus) |
38 | 23, 26, 28, 31, 34, 35, 37 | haustsms 21749 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ∃*𝑦 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
39 | 38 | ex 449 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ → ∃*𝑦 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
40 | | moanimv 2519 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ↔ (𝑥 ∈ ℂ → ∃*𝑦 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
41 | 39, 40 | sylibr 223 |
. . . . . 6
⊢ (𝜑 → ∃*𝑦(𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
42 | | moim 2507 |
. . . . . 6
⊢
(∀𝑦(𝑥𝑇𝑦 → (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) → (∃*𝑦(𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) → ∃*𝑦 𝑥𝑇𝑦)) |
43 | 22, 41, 42 | sylc 63 |
. . . . 5
⊢ (𝜑 → ∃*𝑦 𝑥𝑇𝑦) |
44 | 43 | alrimiv 1842 |
. . . 4
⊢ (𝜑 → ∀𝑥∃*𝑦 𝑥𝑇𝑦) |
45 | | dffun6 5819 |
. . . 4
⊢ (Fun
𝑇 ↔ (Rel 𝑇 ∧ ∀𝑥∃*𝑦 𝑥𝑇𝑦)) |
46 | 19, 44, 45 | sylanbrc 695 |
. . 3
⊢ (𝜑 → Fun 𝑇) |
47 | | funfn 5833 |
. . 3
⊢ (Fun
𝑇 ↔ 𝑇 Fn dom 𝑇) |
48 | 46, 47 | sylib 207 |
. 2
⊢ (𝜑 → 𝑇 Fn dom 𝑇) |
49 | | rnss 5275 |
. . . 4
⊢ (𝑇 ⊆ (ℂ ×
ℂ) → ran 𝑇
⊆ ran (ℂ × ℂ)) |
50 | 16, 49 | syl 17 |
. . 3
⊢ (𝜑 → ran 𝑇 ⊆ ran (ℂ ×
ℂ)) |
51 | | rnxpss 5485 |
. . 3
⊢ ran
(ℂ × ℂ) ⊆ ℂ |
52 | 50, 51 | syl6ss 3580 |
. 2
⊢ (𝜑 → ran 𝑇 ⊆ ℂ) |
53 | | df-f 5808 |
. 2
⊢ (𝑇:dom 𝑇⟶ℂ ↔ (𝑇 Fn dom 𝑇 ∧ ran 𝑇 ⊆ ℂ)) |
54 | 48, 52, 53 | sylanbrc 695 |
1
⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ) |