| 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 26478 |
. . 3
⊢ (𝜑 → 𝐹:𝑆⟶ℂ) |
| 8 | 1, 2, 3, 4, 5, 6 | abelthlem9 26484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)) |
| 9 | 1, 2, 3, 4, 5 | abelthlem2 26476 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1))) |
| 10 | 9 | simpld 494 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 1 ∈ 𝑆) |
| 11 | 10 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 1 ∈ 𝑆) |
| 12 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
| 13 | 11, 12 | ovresd 7600 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) = (1(abs ∘ − )𝑦)) |
| 14 | | ax-1cn 11213 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℂ |
| 15 | 5 | ssrab3 4082 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑆 ⊆
ℂ |
| 16 | 15, 12 | sselid 3981 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ) |
| 17 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ (abs
∘ − ) = (abs ∘ − ) |
| 18 | 17 | cnmetdval 24791 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ 𝑦
∈ ℂ) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦))) |
| 19 | 14, 16, 18 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦))) |
| 20 | 13, 19 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) = (abs‘(1 − 𝑦))) |
| 21 | 20 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → ((1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) < 𝑤 ↔ (abs‘(1 − 𝑦)) < 𝑤)) |
| 22 | 7 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝐹:𝑆⟶ℂ) |
| 23 | 22, 11 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (𝐹‘1) ∈ ℂ) |
| 24 | 7 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑆⟶ℂ) |
| 25 | 24 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (𝐹‘𝑦) ∈ ℂ) |
| 26 | 17 | cnmetdval 24791 |
. . . . . . . . . . . . . . 15
⊢ (((𝐹‘1) ∈ ℂ ∧
(𝐹‘𝑦) ∈ ℂ) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦)))) |
| 27 | 23, 25, 26 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦)))) |
| 28 | 27 | breq1d 5153 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟 ↔ (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)) |
| 29 | 21, 28 | imbi12d 344 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (((1((abs ∘ − ) ↾
(𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))) |
| 30 | 29 | ralbidva 3176 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∀𝑦 ∈ 𝑆 ((1((abs ∘ − )
↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))) |
| 31 | 30 | rexbidv 3179 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
(∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))) |
| 32 | 8, 31 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) →
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)) |
| 33 | 32 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ ℝ+
∀𝑦 ∈ 𝑆 ((1((abs ∘ − )
↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)) |
| 34 | | cnxmet 24793 |
. . . . . . . . . 10
⊢ (abs
∘ − ) ∈ (∞Met‘ℂ) |
| 35 | | xmetres2 24371 |
. . . . . . . . . 10
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘
− ) ↾ (𝑆
× 𝑆)) ∈
(∞Met‘𝑆)) |
| 36 | 34, 15, 35 | mp2an 692 |
. . . . . . . . 9
⊢ ((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) |
| 37 | | eqid 2737 |
. . . . . . . . . . . 12
⊢ ((abs
∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆)) |
| 38 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) |
| 39 | 38 | cnfldtopn 24802 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) = (MetOpen‘(abs ∘
− )) |
| 40 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − )
↾ (𝑆 × 𝑆))) |
| 41 | 37, 39, 40 | metrest 24537 |
. . . . . . . . . . 11
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) →
((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − )
↾ (𝑆 × 𝑆)))) |
| 42 | 34, 15, 41 | mp2an 692 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘
− ) ↾ (𝑆
× 𝑆))) |
| 43 | 42, 39 | metcnp 24554 |
. . . . . . . . 9
⊢ ((((abs
∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ (abs ∘ − )
∈ (∞Met‘ℂ) ∧ 1 ∈ 𝑆) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)))) |
| 44 | 36, 34, 10, 43 | mp3an12i 1467 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+
∃𝑤 ∈
ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟)))) |
| 45 | 7, 33, 44 | mpbir2and 713 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1)) |
| 46 | 45 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1)) |
| 47 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝑦 = 1) |
| 48 | 47 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) →
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t 𝑆) CnP
(TopOpen‘ℂfld))‘1)) |
| 49 | 46, 48 | eleqtrrd 2844 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 50 | | eldifsn 4786 |
. . . . . . 7
⊢ (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) |
| 51 | 9 | simprd 495 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs
∘ − ))1)) |
| 52 | | abscl 15317 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ →
(abs‘𝑤) ∈
ℝ) |
| 53 | 52 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈
ℝ) |
| 54 | 53 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) ∈
ℝ)) |
| 55 | | absge0 15326 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ → 0 ≤
(abs‘𝑤)) |
| 56 | 55 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 0 ≤
(abs‘𝑤)) |
| 57 | 56 | a1d 25 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → 0 ≤
(abs‘𝑤))) |
| 58 | 1, 2 | abelthlem1 26475 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 59 | 58 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) |
| 60 | 53 | rexrd 11311 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈
ℝ*) |
| 61 | | 1re 11261 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 ∈
ℝ |
| 62 | | rexr 11307 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (1 ∈
ℝ → 1 ∈ ℝ*) |
| 63 | 61, 62 | mp1i 13 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ∈
ℝ*) |
| 64 | | iccssxr 13470 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(0[,]+∞) ⊆ ℝ* |
| 65 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛)))) = (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛)))) |
| 66 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) = sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) |
| 67 | 65, 1, 66 | radcnvcl 26460 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ (0[,]+∞)) |
| 68 | 64, 67 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
| 69 | 68 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) |
| 70 | | xrltletr 13199 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((abs‘𝑤)
∈ ℝ* ∧ 1 ∈ ℝ* ∧ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
| 71 | 60, 63, 69, 70 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
| 72 | 59, 71 | mpan2d 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
| 73 | 54, 57, 72 | 3jcad 1130 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 →
((abs‘𝑤) ∈
ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 74 | | 0cn 11253 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 0 ∈
ℂ |
| 75 | 17 | cnmetdval 24791 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℂ ∧ 𝑤
∈ ℂ) → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤))) |
| 76 | 74, 75 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ → (0(abs
∘ − )𝑤) =
(abs‘(0 − 𝑤))) |
| 77 | | abssub 15365 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((0
∈ ℂ ∧ 𝑤
∈ ℂ) → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0))) |
| 78 | 74, 77 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ →
(abs‘(0 − 𝑤)) =
(abs‘(𝑤 −
0))) |
| 79 | | subid1 11529 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑤 ∈ ℂ → (𝑤 − 0) = 𝑤) |
| 80 | 79 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑤 ∈ ℂ →
(abs‘(𝑤 − 0)) =
(abs‘𝑤)) |
| 81 | 76, 78, 80 | 3eqtrd 2781 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑤 ∈ ℂ → (0(abs
∘ − )𝑤) =
(abs‘𝑤)) |
| 82 | 81 | breq1d 5153 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 ∈ ℂ → ((0(abs
∘ − )𝑤) < 1
↔ (abs‘𝑤) <
1)) |
| 83 | 82 | adantl 481 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘
− )𝑤) < 1 ↔
(abs‘𝑤) <
1)) |
| 84 | | 0re 11263 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ∈
ℝ |
| 85 | | elico2 13451 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((0
∈ ℝ ∧ sup({𝑟
∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ) ∈ ℝ*) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤
(abs‘𝑤) ∧
(abs‘𝑤) <
sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 86 | 84, 69, 85 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤
(abs‘𝑤) ∧
(abs‘𝑤) <
sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 87 | 73, 83, 86 | 3imtr4d 294 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘
− )𝑤) < 1 →
(abs‘𝑤) ∈
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 88 | 87 | imdistanda 571 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑤 ∈ ℂ ∧ (0(abs ∘ −
)𝑤) < 1) → (𝑤 ∈ ℂ ∧
(abs‘𝑤) ∈
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))))) |
| 89 | | 1xr 11320 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ* |
| 90 | | elbl 24398 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((abs
∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ
∧ 1 ∈ ℝ*) → (𝑤 ∈ (0(ball‘(abs ∘ −
))1) ↔ (𝑤 ∈
ℂ ∧ (0(abs ∘ − )𝑤) < 1))) |
| 91 | 34, 74, 89, 90 | mp3an 1463 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (0(ball‘(abs
∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ −
)𝑤) <
1)) |
| 92 | | absf 15376 |
. . . . . . . . . . . . . . . . . . 19
⊢
abs:ℂ⟶ℝ |
| 93 | | ffn 6736 |
. . . . . . . . . . . . . . . . . . 19
⊢
(abs:ℂ⟶ℝ → abs Fn ℂ) |
| 94 | | elpreima 7078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (abs Fn
ℂ → (𝑤 ∈
(◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( +
, ((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↔ (𝑤 ∈
ℂ ∧ (abs‘𝑤)
∈ (0[,)sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))))) |
| 95 | 92, 93, 94 | mp2b 10 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↔ (𝑤 ∈
ℂ ∧ (abs‘𝑤)
∈ (0[,)sup({𝑟 ∈
ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 96 | 88, 91, 95 | 3imtr4g 296 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝑤 ∈ (0(ball‘(abs ∘ −
))1) → 𝑤 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))))) |
| 97 | 96 | ssrdv 3989 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (0(ball‘(abs ∘
− ))1) ⊆ (◡abs “
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 98 | 51, 97 | sstrd 3994 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))) |
| 99 | 98 | resmptd 6058 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛)))) |
| 100 | 6 | reseq1i 5993 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ↾ (𝑆 ∖ {1})) = ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) |
| 101 | | difss 4136 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∖ {1}) ⊆ 𝑆 |
| 102 | | resmpt 6055 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑆 ∖ {1}) ⊆ 𝑆 → ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛)))) |
| 103 | 101, 102 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛))) |
| 104 | 100, 103 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0
((𝐴‘𝑛) · (𝑥↑𝑛))) |
| 105 | 99, 104 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝐹 ↾ (𝑆 ∖ {1}))) |
| 106 | | cnvimass 6100 |
. . . . . . . . . . . . . . . . . . 19
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ⊆ dom abs |
| 107 | 92 | fdmi 6747 |
. . . . . . . . . . . . . . . . . . 19
⊢ dom abs =
ℂ |
| 108 | 106, 107 | sseqtri 4032 |
. . . . . . . . . . . . . . . . . 18
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ⊆ ℂ |
| 109 | 108 | sseli 3979 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) → 𝑥 ∈
ℂ) |
| 110 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗)) |
| 111 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑗 → (𝑥↑𝑛) = (𝑥↑𝑗)) |
| 112 | 110, 111 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑗 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑗) · (𝑥↑𝑗))) |
| 113 | 112 | cbvsumv 15732 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 ((𝐴‘𝑗) · (𝑥↑𝑗)) |
| 114 | 65 | pserval2 26454 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ0)
→ (((𝑡 ∈ ℂ
↦ (𝑛 ∈
ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = ((𝐴‘𝑗) · (𝑥↑𝑗))) |
| 115 | 114 | sumeq2dv 15738 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℂ →
Σ𝑗 ∈
ℕ0 (((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐴‘𝑗) · (𝑥↑𝑗))) |
| 116 | 113, 115 | eqtr4id 2796 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ →
Σ𝑛 ∈
ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗)) |
| 117 | 109, 116 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) → Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗)) |
| 118 | 117 | mpteq2ia 5245 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑗
∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗)) |
| 119 | | eqid 2737 |
. . . . . . . . . . . . . . 15
⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) = (◡abs “
(0[,)sup({𝑟 ∈ ℝ
∣ seq0( + , ((𝑡
∈ ℂ ↦ (𝑛
∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) |
| 120 | | eqid 2737 |
. . . . . . . . . . . . . . 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)) |
| 121 | 65, 118, 1, 66, 119, 120 | psercn 26470 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ ((◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< )))–cn→ℂ)) |
| 122 | | rescncf 24923 |
. . . . . . . . . . . . . 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→ℂ))) |
| 123 | 98, 121, 122 | sylc 65 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0
↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*,
< ))) ↦ Σ𝑛
∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)) |
| 124 | 105, 123 | eqeltrrd 2842 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)) |
| 125 | 124 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)) |
| 126 | 101, 15 | sstri 3993 |
. . . . . . . . . . . 12
⊢ (𝑆 ∖ {1}) ⊆
ℂ |
| 127 | | ssid 4006 |
. . . . . . . . . . . 12
⊢ ℂ
⊆ ℂ |
| 128 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) =
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) |
| 129 | 38 | cnfldtopon 24803 |
. . . . . . . . . . . . . 14
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) |
| 130 | 129 | toponrestid 22927 |
. . . . . . . . . . . . 13
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) |
| 131 | 38, 128, 130 | cncfcn 24936 |
. . . . . . . . . . . 12
⊢ (((𝑆 ∖ {1}) ⊆ ℂ
∧ ℂ ⊆ ℂ) → ((𝑆 ∖ {1})–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld))) |
| 132 | 126, 127,
131 | mp2an 692 |
. . . . . . . . . . 11
⊢ ((𝑆 ∖ {1})–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld)) |
| 133 | 125, 132 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld))) |
| 134 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ (𝑆 ∖ {1})) |
| 135 | | resttopon 23169 |
. . . . . . . . . . . . 13
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ (𝑆 ∖ {1})
⊆ ℂ) → ((TopOpen‘ℂfld)
↾t (𝑆
∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1}))) |
| 136 | 129, 126,
135 | mp2an 692 |
. . . . . . . . . . . 12
⊢
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈
(TopOn‘(𝑆 ∖
{1})) |
| 137 | 136 | toponunii 22922 |
. . . . . . . . . . 11
⊢ (𝑆 ∖ {1}) = ∪ ((TopOpen‘ℂfld)
↾t (𝑆
∖ {1})) |
| 138 | 137 | cncnpi 23286 |
. . . . . . . . . 10
⊢ (((𝐹 ↾ (𝑆 ∖ {1})) ∈
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn
(TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 139 | 133, 134,
138 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 140 | 38 | cnfldtop 24804 |
. . . . . . . . . . . 12
⊢
(TopOpen‘ℂfld) ∈ Top |
| 141 | | cnex 11236 |
. . . . . . . . . . . . 13
⊢ ℂ
∈ V |
| 142 | 141, 15 | ssexi 5322 |
. . . . . . . . . . . 12
⊢ 𝑆 ∈ V |
| 143 | | restabs 23173 |
. . . . . . . . . . . 12
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆 ∧ 𝑆 ∈ V) →
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) =
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))) |
| 144 | 140, 101,
142, 143 | mp3an 1463 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) =
((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) |
| 145 | 144 | oveq1i 7441 |
. . . . . . . . . 10
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld)) =
(((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld)) |
| 146 | 145 | fveq1i 6907 |
. . . . . . . . 9
⊢
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld)
↾t (𝑆
∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦) |
| 147 | 139, 146 | eleqtrrdi 2852 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 148 | | resttop 23168 |
. . . . . . . . . . 11
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
| 149 | 140, 142,
148 | mp2an 692 |
. . . . . . . . . 10
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top |
| 150 | 149 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) →
((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top) |
| 151 | 101 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝑆 ∖ {1}) ⊆ 𝑆) |
| 152 | 10 | snssd 4809 |
. . . . . . . . . . . . 13
⊢ (𝜑 → {1} ⊆ 𝑆) |
| 153 | 38 | cnfldhaus 24805 |
. . . . . . . . . . . . . . 15
⊢
(TopOpen‘ℂfld) ∈ Haus |
| 154 | | unicntop 24806 |
. . . . . . . . . . . . . . . 16
⊢ ℂ =
∪
(TopOpen‘ℂfld) |
| 155 | 154 | sncld 23379 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ Haus ∧ 1 ∈
ℂ) → {1} ∈
(Clsd‘(TopOpen‘ℂfld))) |
| 156 | 153, 14, 155 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ {1}
∈ (Clsd‘(TopOpen‘ℂfld)) |
| 157 | 154 | restcldi 23181 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ⊆ ℂ ∧ {1}
∈ (Clsd‘(TopOpen‘ℂfld)) ∧ {1} ⊆
𝑆) → {1} ∈
(Clsd‘((TopOpen‘ℂfld) ↾t 𝑆))) |
| 158 | 15, 156, 157 | mp3an12 1453 |
. . . . . . . . . . . . 13
⊢ ({1}
⊆ 𝑆 → {1} ∈
(Clsd‘((TopOpen‘ℂfld) ↾t 𝑆))) |
| 159 | 154 | restuni 23170 |
. . . . . . . . . . . . . . 15
⊢
(((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 160 | 140, 15, 159 | mp2an 692 |
. . . . . . . . . . . . . 14
⊢ 𝑆 = ∪
((TopOpen‘ℂfld) ↾t 𝑆) |
| 161 | 160 | cldopn 23039 |
. . . . . . . . . . . . 13
⊢ ({1}
∈ (Clsd‘((TopOpen‘ℂfld) ↾t
𝑆)) → (𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 162 | 152, 158,
161 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆)) |
| 163 | 160 | isopn3 23074 |
. . . . . . . . . . . . 13
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) → ((𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))) |
| 164 | 149, 101,
163 | mp2an 692 |
. . . . . . . . . . . 12
⊢ ((𝑆 ∖ {1}) ∈
((TopOpen‘ℂfld) ↾t 𝑆) ↔
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})) |
| 165 | 162, 164 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝜑 →
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})) |
| 166 | 165 | eleq2d 2827 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) ↔ 𝑦 ∈ (𝑆 ∖ {1}))) |
| 167 | 166 | biimpar 477 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈
((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1}))) |
| 168 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹:𝑆⟶ℂ) |
| 169 | 160, 154 | cnprest 23297 |
. . . . . . . . 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))‘𝑦))) |
| 170 | 150, 151,
167, 168, 169 | syl22anc 839 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈
(((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP
(TopOpen‘ℂfld))‘𝑦))) |
| 171 | 147, 170 | mpbird 257 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 172 | 50, 171 | sylan2br 595 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 173 | 172 | anassrs 467 |
. . . . 5
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ 1) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 174 | 49, 173 | pm2.61dane 3029 |
. . . 4
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 175 | 174 | ralrimiva 3146 |
. . 3
⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)) |
| 176 | | resttopon 23169 |
. . . . 5
⊢
(((TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
∧ 𝑆 ⊆ ℂ)
→ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)) |
| 177 | 129, 15, 176 | mp2an 692 |
. . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) |
| 178 | | cncnp 23288 |
. . . 4
⊢
((((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) ∧
(TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) →
(𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦)))) |
| 179 | 177, 129,
178 | mp2an 692 |
. . 3
⊢ (𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦 ∈ 𝑆 𝐹 ∈
((((TopOpen‘ℂfld) ↾t 𝑆) CnP
(TopOpen‘ℂfld))‘𝑦))) |
| 180 | 7, 175, 179 | sylanbrc 583 |
. 2
⊢ (𝜑 → 𝐹 ∈
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
| 181 | | eqid 2737 |
. . . 4
⊢
((TopOpen‘ℂfld) ↾t 𝑆) =
((TopOpen‘ℂfld) ↾t 𝑆) |
| 182 | 38, 181, 130 | cncfcn 24936 |
. . 3
⊢ ((𝑆 ⊆ ℂ ∧ ℂ
⊆ ℂ) → (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld))) |
| 183 | 15, 127, 182 | mp2an 692 |
. 2
⊢ (𝑆–cn→ℂ) =
(((TopOpen‘ℂfld) ↾t 𝑆) Cn
(TopOpen‘ℂfld)) |
| 184 | 180, 183 | eleqtrrdi 2852 |
1
⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ)) |