Step | Hyp | Ref
| Expression |
1 | | abelth.1 |
. . . 4
⊢ (𝜑 → 𝐴:ℕ0⟶ℂ) |
2 | | abelth.2 |
. . . 4
⊢ (𝜑 → seq0( + , 𝐴) ∈ dom ⇝
) |
3 | | abelth.3 |
. . . 4
⊢ (𝜑 → 𝑀 ∈ ℝ) |
4 | | abelth.4 |
. . . 4
⊢ (𝜑 → 0 ≤ 𝑀) |
5 | | abelth.5 |
. . . 4
⊢ 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 −
𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} |
6 | | abelth.6 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) |
7 | 1, 2, 3, 4, 5, 6 | abelthlem4 24188 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
8 | 1, 2, 3, 4, 5, 6 | abelthlem9 24194 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)) |
9 | 1, 2, 3, 4, 5 | abelthlem2 24186 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
10 | 9 | simpld 475 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈ 𝑆) |
11 | 10 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 1 ∈ 𝑆) |
12 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
13 | 11, 12 | ovresd 6801 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) = (1(abs ∘ − )𝑦)) |
14 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
15 | | ssrab2 3687 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑧 ∈ ℂ ∣
(abs‘(1 − 𝑧))
≤ (𝑀 · (1 −
(abs‘𝑧)))} ⊆
ℂ |
16 | 5, 15 | eqsstri 3635 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 ⊆
ℂ |
17 | 16, 12 | sseldi 3601 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
18 | | eqid 2622 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) = (abs ∘ − ) |
19 | 18 | cnmetdval 22574 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦))) |
20 | 14, 17, 19 | sylancr 695 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦))) |
21 | 13, 20 | eqtrd 2656 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) = (abs‘(1 − 𝑦))) |
22 | 21 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → ((1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) < 𝑤 ↔ (abs‘(1 − 𝑦)) < 𝑤)) |
23 | 7 | ad2antrr 762 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
24 | 23, 11 | ffvelrnd 6360 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (𝐹‘1) ∈ ℂ) |
25 | 7 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑆⟶ℂ) |
26 | 25 | ffvelrnda 6359 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (𝐹‘𝑦) ∈ ℂ) |
27 | 18 | cnmetdval 22574 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘1) ∈ ℂ ∧
(𝐹‘𝑦) ∈ ℂ) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦)))) |
28 | 24, 26, 27 | syl2anc 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦)))) |
29 | 28 | breq1d 4663 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟 ↔ (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)) |
30 | 22, 29 | imbi12d 334 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (((1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))) |
31 | 30 | ralbidva 2985 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑦 ∈ 𝑆 ((1((abs ∘ − )
↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))) |
32 | 31 | rexbidv 3052 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))) |
33 | 8, 32 | mpbird 247 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)) |
34 | 33 | ralrimiva 2966 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑦 ∈ 𝑆 ((1((abs ∘ − )
↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)) |
35 | | cnxmet 22576 |
. . . . . . . . . . 11
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
36 | | xmetres2 22166 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑆
× 𝑆)) ∈
(∞Met‘𝑆)) |
37 | 35, 16, 36 | mp2an 708 |
. . . . . . . . . 10
⊢ ((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) |
38 | 37 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → ((abs ∘ − )
↾ (𝑆 × 𝑆)) ∈
(∞Met‘𝑆)) |
39 | 35 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (abs ∘ − )
∈ (∞Met‘ℂ)) |
40 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) |
41 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
42 | 41 | cnfldtopn 22585 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
43 | | eqid 2622 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − )
↾ (𝑆 × 𝑆))) |
44 | 40, 42, 43 | metrest 22329 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − )
↾ (𝑆 × 𝑆)))) |
45 | 35, 16, 44 | mp2an 708 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘
− ) ↾ (𝑆
× 𝑆))) |
46 | 45, 42 | metcnp 22346 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ (abs ∘ − )
∈ (∞Met‘ℂ) ∧ 1 ∈ 𝑆) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)))) |
47 | 38, 39, 10, 46 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)))) |
48 | 7, 34, 47 | mpbir2and 957 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1)) |
49 | 48 | ad2antrr 762 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1)) |
50 | | simpr 477 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝑦 = 1) |
51 | 50 | fveq2d 6195 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) →
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1)) |
52 | 49, 51 | eleqtrrd 2704 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
53 | | eldifsn 4317 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) |
54 | 9 | simprd 479 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) |
55 | | abscl 14018 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ →
(abs‘𝑤) ∈
ℝ) |
56 | 55 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈
ℝ) |
57 | 56 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) ∈
ℝ)) |
58 | | absge0 14027 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ → 0 ≤
(abs‘𝑤)) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 0 ≤
(abs‘𝑤)) |
60 | 59 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → 0 ≤
(abs‘𝑤))) |
61 | 1, 2 | abelthlem1 24185 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
63 | 56 | rexrd 10089 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈
ℝ*) |
64 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℝ |
65 | | rexr 10085 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) |
66 | 64, 65 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ∈
ℝ*) |
67 | | iccssxr 12256 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0[,]+∞) ⊆ ℝ* |
68 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛)))) = (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛)))) |
69 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
70 | 68, 1, 69 | radcnvcl 24171 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ (0[,]+∞)) |
71 | 67, 70 | sseldi 3601 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
72 | 71 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
73 | | xrltletr 11988 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((abs‘𝑤)
∈ ℝ* ∧ 1 ∈ ℝ* ∧ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
74 | 63, 66, 72, 73 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
75 | 62, 74 | mpan2d 710 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
76 | 57, 60, 75 | 3jcad 1243 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 →
((abs‘𝑤) ∈
ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
77 | | 0cn 10032 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℂ |
78 | 18 | cnmetdval 22574 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℂ ∧ 𝑤
∈ ℂ) → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤))) |
79 | 77, 78 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ → (0(abs
∘ − )𝑤) =
(abs‘(0 − 𝑤))) |
80 | | abssub 14066 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℂ ∧ 𝑤
∈ ℂ) → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0))) |
81 | 77, 80 | mpan 706 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ →
(abs‘(0 − 𝑤)) =
(abs‘(𝑤 −
0))) |
82 | | subid1 10301 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ∈ ℂ → (𝑤 − 0) = 𝑤) |
83 | 82 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ →
(abs‘(𝑤 − 0)) =
(abs‘𝑤)) |
84 | 79, 81, 83 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℂ → (0(abs
∘ − )𝑤) =
(abs‘𝑤)) |
85 | 84 | breq1d 4663 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℂ → ((0(abs
∘ − )𝑤) < 1
↔ (abs‘𝑤) <
1)) |
86 | 85 | adantl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘
− )𝑤) < 1 ↔
(abs‘𝑤) <
1)) |
87 | | 0re 10040 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ |
88 | | elico2 12237 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ sup({𝑟
∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤
(abs‘𝑤) ∧
(abs‘𝑤) <
sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
89 | 87, 72, 88 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤
(abs‘𝑤) ∧
(abs‘𝑤) <
sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
90 | 76, 86, 89 | 3imtr4d 283 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘
− )𝑤) < 1 →
(abs‘𝑤) ∈
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
91 | 90 | imdistanda 729 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑤 ∈ ℂ ∧ (0(abs ∘ −
)𝑤) < 1) → (𝑤 ∈ ℂ ∧
(abs‘𝑤) ∈
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))))) |
92 | 64 | rexri 10097 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
93 | | elbl 22193 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ*) → (𝑤 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑤 ∈
ℂ ∧ (0(abs ∘ − )𝑤) < 1))) |
94 | 35, 77, 92, 93 | mp3an 1424 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (0(ball‘(abs
∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ −
)𝑤) <
1)) |
95 | | absf 14077 |
. . . . . . . . . . . . . . . . . . 19
⊢
abs:ℂ⟶ℝ |
96 | | ffn 6045 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
97 | | elpreima 6337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (abs Fn
ℂ → (𝑤 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↔ (𝑤 ∈
ℂ ∧ (abs‘𝑤)
∈ (0[,)sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))))) |
98 | 95, 96, 97 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↔ (𝑤 ∈
ℂ ∧ (abs‘𝑤)
∈ (0[,)sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
99 | 91, 94, 98 | 3imtr4g 285 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (0(ball‘(abs ∘ −
))1) → 𝑤 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))))) |
100 | 99 | ssrdv 3609 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0(ball‘(abs ∘
− ))1) ⊆ (◡abs “
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
101 | 54, 100 | sstrd 3613 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
102 | 101 | resmptd 5452 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛)))) |
103 | 6 | reseq1i 5392 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ↾ (𝑆 ∖ {1})) = ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) |
104 | | difss 3737 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∖ {1}) ⊆ 𝑆 |
105 | | resmpt 5449 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∖ {1}) ⊆ 𝑆 → ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛)))) |
106 | 104, 105 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛))) |
107 | 103, 106 | eqtri 2644 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛))) |
108 | 102, 107 | syl6eqr 2674 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝐹 ↾ (𝑆 ∖ {1}))) |
109 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ⊆ dom abs |
110 | 95 | fdmi 6052 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom abs =
ℂ |
111 | 109, 110 | sseqtri 3637 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ⊆ ℂ |
112 | 111 | sseli 3599 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) → 𝑥 ∈
ℂ) |
113 | 68 | pserval2 24165 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = ((𝐴‘𝑗) · (𝑥↑𝑗))) |
114 | 113 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
Σ𝑗 ∈
ℕ0 (((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐴‘𝑗) · (𝑥↑𝑗))) |
115 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗)) |
116 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑗 → (𝑥↑𝑛) = (𝑥↑𝑗)) |
117 | 115, 116 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑗 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑗) · (𝑥↑𝑗))) |
118 | 117 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 ((𝐴‘𝑗) · (𝑥↑𝑗)) |
119 | 114, 118 | syl6reqr 2675 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗)) |
120 | 112, 119 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) → Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗)) |
121 | 120 | mpteq2ia 4740 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑗
∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗)) |
122 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) = (◡abs “
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
123 | | eqid 2622 |
. . . . . . . . . . . . . . 15
⊢
if(sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑣) + sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑣) + 1)) = if(sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ, (((abs‘𝑣) + sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) / 2), ((abs‘𝑣) + 1)) |
124 | 68, 121, 1, 69, 122, 123 | psercn 24180 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ ((◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))–cn→ℂ)) |
125 | | rescncf 22700 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∖ {1}) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) → ((𝑥 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ ((◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))–cn→ℂ) →
((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))) |
126 | 101, 124,
125 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)) |
127 | 108, 126 | eqeltrrd 2702 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)) |
128 | 127 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)) |
129 | 104, 16 | sstri 3612 |
. . . . . . . . . . . 12
⊢ (𝑆 ∖ {1}) ⊆
ℂ |
130 | | ssid 3624 |
. . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ |
131 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) =
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) |
132 | 41 | cnfldtop 22587 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈ Top |
133 | 41 | cnfldtopon 22586 |
. . . . . . . . . . . . . . . . 17
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
134 | 133 | toponunii 20721 |
. . . . . . . . . . . . . . . 16
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
135 | 134 | restid 16094 |
. . . . . . . . . . . . . . 15
⊢
((TopOpen‘ℂfld) ∈ Top →
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld)) |
136 | 132, 135 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
((TopOpen‘ℂfld) ↾t ℂ) =
(TopOpen‘ℂfld) |
137 | 136 | eqcomi 2631 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
138 | 41, 131, 137 | cncfcn 22712 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∖ {1}) ⊆ ℂ
∧ ℂ ⊆ ℂ) → ((𝑆 ∖ {1})–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld))) |
139 | 129, 130,
138 | mp2an 708 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ {1})–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld)) |
140 | 128, 139 | syl6eleq 2711 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld))) |
141 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ (𝑆 ∖ {1})) |
142 | | resttopon 20965 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝑆 ∖ {1})
⊆ ℂ) → ((TopOpen‘ℂfld)
↾t (𝑆
∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1}))) |
143 | 133, 129,
142 | mp2an 708 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈
(TopOn‘(𝑆 ∖
{1})) |
144 | 143 | toponunii 20721 |
. . . . . . . . . . 11
⊢ (𝑆 ∖ {1}) = ∪ ((TopOpen‘ℂfld)
↾t (𝑆
∖ {1})) |
145 | 144 | cncnpi 21082 |
. . . . . . . . . 10
⊢ (((𝐹 ↾ (𝑆 ∖ {1})) ∈
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦)) |
146 | 140, 141,
145 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦)) |
147 | | cnex 10017 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
148 | 147, 16 | ssexi 4803 |
. . . . . . . . . . . 12
⊢ 𝑆 ∈ V |
149 | | restabs 20969 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆 ∧ 𝑆 ∈ V) →
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) =
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))) |
150 | 132, 104,
148, 149 | mp3an 1424 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) =
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) |
151 | 150 | oveq1i 6660 |
. . . . . . . . . 10
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld)) |
152 | 151 | fveq1i 6192 |
. . . . . . . . 9
⊢
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝑆
∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦) |
153 | 146, 152 | syl6eleqr 2712 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦)) |
154 | | resttop 20964 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
155 | 132, 148,
154 | mp2an 708 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top |
156 | 155 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
157 | 104 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝑆 ∖ {1}) ⊆ 𝑆) |
158 | 10 | snssd 4340 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {1} ⊆ 𝑆) |
159 | 41 | cnfldhaus 22588 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈ Haus |
160 | 134 | sncld 21175 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧ 1 ∈
ℂ) → {1} ∈
(Clsd‘(TopOpen‘ℂfld))) |
161 | 159, 14, 160 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢ {1}
∈ (Clsd‘(TopOpen‘ℂfld)) |
162 | 134 | restcldi 20977 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ {1}
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ {1} ⊆
𝑆) → {1} ∈
(Clsd‘((TopOpen‘ℂfld) ↾t 𝑆))) |
163 | 16, 161, 162 | mp3an12 1414 |
. . . . . . . . . . . . 13
⊢ ({1}
⊆ 𝑆 → {1} ∈
(Clsd‘((TopOpen‘ℂfld) ↾t 𝑆))) |
164 | 134 | restuni 20966 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
165 | 132, 16, 164 | mp2an 708 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆) |
166 | 165 | cldopn 20835 |
. . . . . . . . . . . . 13
⊢ ({1}
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
𝑆)) → (𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
167 | 158, 163,
166 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
168 | 165 | isopn3 20870 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) → ((𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))) |
169 | 155, 104,
168 | mp2an 708 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})) |
170 | 167, 169 | sylib 208 |
. . . . . . . . . . 11
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})) |
171 | 170 | eleq2d 2687 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) ↔ 𝑦 ∈ (𝑆 ∖ {1}))) |
172 | 171 | biimpar 502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1}))) |
173 | 7 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹:𝑆⟶ℂ) |
174 | 165, 134 | cnprest 21093 |
. . . . . . . . 9
⊢
(((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) ∧ (𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) ∧ 𝐹:𝑆⟶ℂ)) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦))) |
175 | 156, 157,
172, 173, 174 | syl22anc 1327 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦))) |
176 | 153, 175 | mpbird 247 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
177 | 53, 176 | sylan2br 493 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
178 | 177 | anassrs 680 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ 1) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
179 | 52, 178 | pm2.61dane 2881 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
180 | 179 | ralrimiva 2966 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
181 | | resttopon 20965 |
. . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
182 | 133, 16, 181 | mp2an 708 |
. . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) |
183 | | cncnp 21084 |
. . . 4
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
184 | 182, 133,
183 | mp2an 708 |
. . 3
⊢ (𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦))) |
185 | 7, 180, 184 | sylanbrc 698 |
. 2
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
186 | | eqid 2622 |
. . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
187 | 41, 186, 137 | cncfcn 22712 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
188 | 16, 130, 187 | mp2an 708 |
. 2
⊢ (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld)) |
189 | 185, 188 | syl6eleqr 2712 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |