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 25516 |
. . . . . 6
⊢ (𝜑 → 𝑇 = ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
8 | | simpr 485 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ) |
9 | 8 | snssd 4748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → {𝑥} ⊆ ℂ) |
10 | 1, 2, 3, 4, 5 | taylfvallem 25515 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) |
11 | | xpss12 5605 |
. . . . . . . . 9
⊢ (({𝑥} ⊆ ℂ ∧
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))) ⊆ ℂ) → ({𝑥} × (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
12 | 9, 10, 11 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
13 | 12 | ralrimiva 3110 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
14 | | iunss 4980 |
. . . . . . 7
⊢ (∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ × ℂ)
↔ ∀𝑥 ∈
ℂ ({𝑥} ×
(ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
15 | 13, 14 | sylibr 233 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑥 ∈ ℂ ({𝑥} × (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ⊆ (ℂ ×
ℂ)) |
16 | 7, 15 | eqsstrd 3964 |
. . . . 5
⊢ (𝜑 → 𝑇 ⊆ (ℂ ×
ℂ)) |
17 | | relxp 5608 |
. . . . 5
⊢ Rel
(ℂ × ℂ) |
18 | | relss 5692 |
. . . . 5
⊢ (𝑇 ⊆ (ℂ ×
ℂ) → (Rel (ℂ × ℂ) → Rel 𝑇)) |
19 | 16, 17, 18 | mpisyl 21 |
. . . 4
⊢ (𝜑 → Rel 𝑇) |
20 | 1, 2, 3, 4, 5, 6 | eltayl 25517 |
. . . . . . . 8
⊢ (𝜑 → (𝑥𝑇𝑦 ↔ (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))) |
21 | 20 | biimpd 228 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝑇𝑦 → (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))) |
22 | 21 | alrimiv 1934 |
. . . . . 6
⊢ (𝜑 → ∀𝑦(𝑥𝑇𝑦 → (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))))) |
23 | | cnfldbas 20599 |
. . . . . . . . 9
⊢ ℂ =
(Base‘ℂfld) |
24 | | cnring 20618 |
. . . . . . . . . 10
⊢
ℂfld ∈ Ring |
25 | | ringcmn 19818 |
. . . . . . . . . 10
⊢
(ℂfld ∈ Ring → ℂfld ∈
CMnd) |
26 | 24, 25 | mp1i 13 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ℂfld
∈ CMnd) |
27 | | cnfldtps 23939 |
. . . . . . . . . 10
⊢
ℂfld ∈ TopSp |
28 | 27 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ℂfld
∈ TopSp) |
29 | | ovex 7304 |
. . . . . . . . . . 11
⊢
(0[,]𝑁) ∈
V |
30 | 29 | inex1 5245 |
. . . . . . . . . 10
⊢
((0[,]𝑁) ∩
ℤ) ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ((0[,]𝑁) ∩ ℤ) ∈
V) |
32 | 1, 2, 3, 4, 5 | taylfvallem1 25514 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℂ) ∧ 𝑘 ∈ ((0[,]𝑁) ∩ ℤ)) → (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)) ∈ ℂ) |
33 | 32 | fmpttd 6986 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))):((0[,]𝑁) ∩
ℤ)⟶ℂ) |
34 | | eqid 2740 |
. . . . . . . . 9
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
35 | 34 | cnfldhaus 23946 |
. . . . . . . . . 10
⊢
(TopOpen‘ℂfld) ∈ Haus |
36 | 35 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) →
(TopOpen‘ℂfld) ∈ Haus) |
37 | 23, 26, 28, 31, 33, 34, 36 | haustsms 23285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℂ) → ∃*𝑦 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) |
38 | 37 | ex 413 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℂ → ∃*𝑦 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
39 | | moanimv 2623 |
. . . . . . 7
⊢
(∃*𝑦(𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld
tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦
(((((𝑆
D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) ↔ (𝑥 ∈ ℂ → ∃*𝑦 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
40 | 38, 39 | sylibr 233 |
. . . . . 6
⊢ (𝜑 → ∃*𝑦(𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) |
41 | | moim 2546 |
. . . . . 6
⊢
(∀𝑦(𝑥𝑇𝑦 → (𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘)))))) → (∃*𝑦(𝑥 ∈ ℂ ∧ 𝑦 ∈ (ℂfld tsums (𝑘 ∈ ((0[,]𝑁) ∩ ℤ) ↦ (((((𝑆 D𝑛 𝐹)‘𝑘)‘𝐵) / (!‘𝑘)) · ((𝑥 − 𝐵)↑𝑘))))) → ∃*𝑦 𝑥𝑇𝑦)) |
42 | 22, 40, 41 | sylc 65 |
. . . . 5
⊢ (𝜑 → ∃*𝑦 𝑥𝑇𝑦) |
43 | 42 | alrimiv 1934 |
. . . 4
⊢ (𝜑 → ∀𝑥∃*𝑦 𝑥𝑇𝑦) |
44 | | dffun6 6447 |
. . . 4
⊢ (Fun
𝑇 ↔ (Rel 𝑇 ∧ ∀𝑥∃*𝑦 𝑥𝑇𝑦)) |
45 | 19, 43, 44 | sylanbrc 583 |
. . 3
⊢ (𝜑 → Fun 𝑇) |
46 | 45 | funfnd 6463 |
. 2
⊢ (𝜑 → 𝑇 Fn dom 𝑇) |
47 | | rnss 5847 |
. . . 4
⊢ (𝑇 ⊆ (ℂ ×
ℂ) → ran 𝑇
⊆ ran (ℂ × ℂ)) |
48 | 16, 47 | syl 17 |
. . 3
⊢ (𝜑 → ran 𝑇 ⊆ ran (ℂ ×
ℂ)) |
49 | | rnxpss 6074 |
. . 3
⊢ ran
(ℂ × ℂ) ⊆ ℂ |
50 | 48, 49 | sstrdi 3938 |
. 2
⊢ (𝜑 → ran 𝑇 ⊆ ℂ) |
51 | | df-f 6436 |
. 2
⊢ (𝑇:dom 𝑇⟶ℂ ↔ (𝑇 Fn dom 𝑇 ∧ ran 𝑇 ⊆ ℂ)) |
52 | 46, 50, 51 | sylanbrc 583 |
1
⊢ (𝜑 → 𝑇:dom 𝑇⟶ℂ) |