MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  abelth Structured version   Visualization version   GIF version

Theorem abelth 26485
Description: Abel's theorem. If the power series Σ𝑛 ∈ ℕ0𝐴(𝑛)(𝑥𝑛) is convergent at 1, then it is equal to the limit from "below", along a Stolz angle 𝑆 (note that the 𝑀 = 1 case of a Stolz angle is the real line [0, 1]). (Continuity on 𝑆 ∖ {1} follows more generally from psercn 26470.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)
Hypotheses
Ref Expression
abelth.1 (𝜑𝐴:ℕ0⟶ℂ)
abelth.2 (𝜑 → seq0( + , 𝐴) ∈ dom ⇝ )
abelth.3 (𝜑𝑀 ∈ ℝ)
abelth.4 (𝜑 → 0 ≤ 𝑀)
abelth.5 𝑆 = {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))}
abelth.6 𝐹 = (𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
Assertion
Ref Expression
abelth (𝜑𝐹 ∈ (𝑆cn→ℂ))
Distinct variable groups:   𝑥,𝑛,𝑧,𝑀   𝐴,𝑛,𝑥,𝑧   𝜑,𝑛,𝑥   𝑆,𝑛,𝑥
Allowed substitution hints:   𝜑(𝑧)   𝑆(𝑧)   𝐹(𝑥,𝑧,𝑛)

Proof of Theorem abelth
Dummy variables 𝑗 𝑤 𝑦 𝑟 𝑡 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef 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 ((𝐴𝑛) · (𝑥𝑛)))
71, 2, 3, 4, 5, 6abelthlem4 26478 . . 3 (𝜑𝐹:𝑆⟶ℂ)
81, 2, 3, 4, 5, 6abelthlem9 26484 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟))
91, 2, 3, 4, 5abelthlem2 26476 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
109simpld 494 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ 𝑆)
1110ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 1 ∈ 𝑆)
12 simpr 484 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 𝑦𝑆)
1311, 12ovresd 7600 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (1(abs ∘ − )𝑦))
14 ax-1cn 11213 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
155ssrab3 4082 . . . . . . . . . . . . . . . . 17 𝑆 ⊆ ℂ
1615, 12sselid 3981 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 𝑦 ∈ ℂ)
17 eqid 2737 . . . . . . . . . . . . . . . . 17 (abs ∘ − ) = (abs ∘ − )
1817cnmetdval 24791 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
1914, 16, 18sylancr 587 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
2013, 19eqtrd 2777 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (abs‘(1 − 𝑦)))
2120breq1d 5153 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 ↔ (abs‘(1 − 𝑦)) < 𝑤))
227ad2antrr 726 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 𝐹:𝑆⟶ℂ)
2322, 11ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (𝐹‘1) ∈ ℂ)
247adantr 480 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ ℝ+) → 𝐹:𝑆⟶ℂ)
2524ffvelcdmda 7104 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (𝐹𝑦) ∈ ℂ)
2617cnmetdval 24791 . . . . . . . . . . . . . . 15 (((𝐹‘1) ∈ ℂ ∧ (𝐹𝑦) ∈ ℂ) → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) = (abs‘((𝐹‘1) − (𝐹𝑦))))
2723, 25, 26syl2anc 584 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) = (abs‘((𝐹‘1) − (𝐹𝑦))))
2827breq1d 5153 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟 ↔ (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟))
2921, 28imbi12d 344 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟)))
3029ralbidva 3176 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → (∀𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟) ↔ ∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟)))
3130rexbidv 3179 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → (∃𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟) ↔ ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟)))
328, 31mpbird 257 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))
3332ralrimiva 3146 . . . . . . . 8 (𝜑 → ∀𝑟 ∈ ℝ+𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))
34 cnxmet 24793 . . . . . . . . . 10 (abs ∘ − ) ∈ (∞Met‘ℂ)
35 xmetres2 24371 . . . . . . . . . 10 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
3634, 15, 35mp2an 692 . . . . . . . . 9 ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆)
37 eqid 2737 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
38 eqid 2737 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
3938cnfldtopn 24802 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
40 eqid 2737 . . . . . . . . . . . 12 (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
4137, 39, 40metrest 24537 . . . . . . . . . . 11 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
4234, 15, 41mp2an 692 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
4342, 39metcnp 24554 . . . . . . . . 9 ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ 𝑆) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))))
4436, 34, 10, 43mp3an12i 1467 . . . . . . . 8 (𝜑 → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))))
457, 33, 44mpbir2and 713 . . . . . . 7 (𝜑𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
4645ad2antrr 726 . . . . . 6 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
47 simpr 484 . . . . . . 7 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → 𝑦 = 1)
4847fveq2d 6910 . . . . . 6 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
4946, 48eleqtrrd 2844 . . . . 5 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
50 eldifsn 4786 . . . . . . 7 (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦𝑆𝑦 ≠ 1))
519simprd 495 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
52 abscl 15317 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (abs‘𝑤) ∈ ℝ)
5352adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ)
5453a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) ∈ ℝ))
55 absge0 15326 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → 0 ≤ (abs‘𝑤))
5655adantl 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → 0 ≤ (abs‘𝑤))
5756a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → 0 ≤ (abs‘𝑤)))
581, 2abelthlem1 26475 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
5958adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
6053rexrd 11311 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ*)
61 1re 11261 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℝ
62 rexr 11307 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℝ → 1 ∈ ℝ*)
6361, 62mp1i 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 ⇝ }, ℝ*, < )
6765, 1, 66radcnvcl 26460 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
6864, 67sselid 3981 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
6968adantr 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 ⇝ }, ℝ*, < )))
7160, 63, 69, 70syl3anc 1373 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
7259, 71mpan2d 694 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
7354, 57, 723jcad 1130 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
74 0cn 11253 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℂ
7517cnmetdval 24791 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
7674, 75mpan 690 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
77 abssub 15365 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
7874, 77mpan 690 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
79 subid1 11529 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℂ → (𝑤 − 0) = 𝑤)
8079fveq2d 6910 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (abs‘(𝑤 − 0)) = (abs‘𝑤))
8176, 78, 803eqtrd 2781 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘𝑤))
8281breq1d 5153 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℂ → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
8382adantl 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 ⇝ }, ℝ*, < ))))
8684, 69, 85sylancr 587 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
8773, 83, 863imtr4d 294 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 → (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
8887imdistanda 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)))
9134, 74, 89, 90mp3an 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 ⇝ }, ℝ*, < )))))
9592, 93, 94mp2b 10 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
9688, 91, 953imtr4g 296 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) → 𝑤 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))))
9796ssrdv 3989 . . . . . . . . . . . . . . . 16 (𝜑 → (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
9851, 97sstrd 3994 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 ∖ {1}) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
9998resmptd 6058 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))))
1006reseq1i 5993 . . . . . . . . . . . . . . 15 (𝐹 ↾ (𝑆 ∖ {1})) = ((𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1}))
101 difss 4136 . . . . . . . . . . . . . . . 16 (𝑆 ∖ {1}) ⊆ 𝑆
102 resmpt 6055 . . . . . . . . . . . . . . . 16 ((𝑆 ∖ {1}) ⊆ 𝑆 → ((𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))))
103101, 102ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
104100, 103eqtri 2765 . . . . . . . . . . . . . 14 (𝐹 ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
10599, 104eqtr4di 2795 . . . . . . . . . . . . 13 (𝜑 → ((𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝐹 ↾ (𝑆 ∖ {1})))
106 cnvimass 6100 . . . . . . . . . . . . . . . . . . 19 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
10792fdmi 6747 . . . . . . . . . . . . . . . . . . 19 dom abs = ℂ
108106, 107sseqtri 4032 . . . . . . . . . . . . . . . . . 18 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
109108sseli 3979 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) → 𝑥 ∈ ℂ)
110 fveq2 6906 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
111 oveq2 7439 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → (𝑥𝑛) = (𝑥𝑗))
112110, 111oveq12d 7449 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑗) · (𝑥𝑗)))
113112cbvsumv 15732 . . . . . . . . . . . . . . . . . 18 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) · (𝑥𝑗))
11465pserval2 26454 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗) = ((𝐴𝑗) · (𝑥𝑗)))
115114sumeq2dv 15738 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) · (𝑥𝑗)))
116113, 115eqtr4id 2796 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗))
117109, 116syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗))
118117mpteq2ia 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))
12165, 118, 1, 66, 119, 120psercn 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→ℂ)))
12398, 121, 122sylc 65 . . . . . . . . . . . . 13 (𝜑 → ((𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
124105, 123eqeltrrd 2842 . . . . . . . . . . . 12 (𝜑 → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
125124adantr 480 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
126101, 15sstri 3993 . . . . . . . . . . . 12 (𝑆 ∖ {1}) ⊆ ℂ
127 ssid 4006 . . . . . . . . . . . 12 ℂ ⊆ ℂ
128 eqid 2737 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
12938cnfldtopon 24803 . . . . . . . . . . . . . 14 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
130129toponrestid 22927 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
13138, 128, 130cncfcn 24936 . . . . . . . . . . . 12 (((𝑆 ∖ {1}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)))
132126, 127, 131mp2an 692 . . . . . . . . . . 11 ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld))
133125, 132eleqtrdi 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})))
136129, 126, 135mp2an 692 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1}))
137136toponunii 22922 . . . . . . . . . . 11 (𝑆 ∖ {1}) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
138137cncnpi 23286 . . . . . . . . . 10 (((𝐹 ↾ (𝑆 ∖ {1})) ∈ (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
139133, 134, 138syl2anc 584 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
14038cnfldtop 24804 . . . . . . . . . . . 12 (TopOpen‘ℂfld) ∈ Top
141 cnex 11236 . . . . . . . . . . . . 13 ℂ ∈ V
142141, 15ssexi 5322 . . . . . . . . . . . 12 𝑆 ∈ V
143 restabs 23173 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆𝑆 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})))
144140, 101, 142, 143mp3an 1463 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
145144oveq1i 7441 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))
146145fveq1i 6907 . . . . . . . . 9 (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦)
147139, 146eleqtrrdi 2852 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
148 resttop 23168 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
149140, 142, 148mp2an 692 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top
150149a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
151101a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝑆 ∖ {1}) ⊆ 𝑆)
15210snssd 4809 . . . . . . . . . . . . 13 (𝜑 → {1} ⊆ 𝑆)
15338cnfldhaus 24805 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ Haus
154 unicntop 24806 . . . . . . . . . . . . . . . 16 ℂ = (TopOpen‘ℂfld)
155154sncld 23379 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ Haus ∧ 1 ∈ ℂ) → {1} ∈ (Clsd‘(TopOpen‘ℂfld)))
156153, 14, 155mp2an 692 . . . . . . . . . . . . . 14 {1} ∈ (Clsd‘(TopOpen‘ℂfld))
157154restcldi 23181 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ {1} ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ {1} ⊆ 𝑆) → {1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)))
15815, 156, 157mp3an12 1453 . . . . . . . . . . . . 13 ({1} ⊆ 𝑆 → {1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)))
159154restuni 23170 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
160140, 15, 159mp2an 692 . . . . . . . . . . . . . 14 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆)
161160cldopn 23039 . . . . . . . . . . . . 13 ({1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)) → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
162152, 158, 1613syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
163160isopn3 23074 . . . . . . . . . . . . 13 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) → ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})))
164149, 101, 163mp2an 692 . . . . . . . . . . . 12 ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))
165162, 164sylib 218 . . . . . . . . . . 11 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))
166165eleq2d 2827 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) ↔ 𝑦 ∈ (𝑆 ∖ {1})))
167166biimpar 477 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})))
1687adantr 480 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝐹:𝑆⟶ℂ)
169160, 154cnprest 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))‘𝑦)))
170150, 151, 167, 168, 169syl22anc 839 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦)))
171147, 170mpbird 257 . . . . . . 7 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
17250, 171sylan2br 595 . . . . . 6 ((𝜑 ∧ (𝑦𝑆𝑦 ≠ 1)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
173172anassrs 467 . . . . 5 (((𝜑𝑦𝑆) ∧ 𝑦 ≠ 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
17449, 173pm2.61dane 3029 . . . 4 ((𝜑𝑦𝑆) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
175174ralrimiva 3146 . . 3 (𝜑 → ∀𝑦𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
176 resttopon 23169 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
177129, 15, 176mp2an 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))‘𝑦))))
179177, 129, 178mp2an 692 . . 3 (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦)))
1807, 175, 179sylanbrc 583 . 2 (𝜑𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
181 eqid 2737 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
18238, 181, 130cncfcn 24936 . . 3 ((𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑆cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
18315, 127, 182mp2an 692 . 2 (𝑆cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
184180, 183eleqtrrdi 2852 1 (𝜑𝐹 ∈ (𝑆cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087   = wceq 1540  wcel 2108  wne 2940  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  wss 3951  ifcif 4525  {csn 4626   cuni 4907   class class class wbr 5143  cmpt 5225   × cxp 5683  ccnv 5684  dom cdm 5685  cres 5687  cima 5688  ccom 5689   Fn wfn 6556  wf 6557  cfv 6561  (class class class)co 7431  supcsup 9480  cc 11153  cr 11154  0cc0 11155  1c1 11156   + caddc 11158   · cmul 11160  +∞cpnf 11292  *cxr 11294   < clt 11295  cle 11296  cmin 11492   / cdiv 11920  2c2 12321  0cn0 12526  +crp 13034  [,)cico 13389  [,]cicc 13390  seqcseq 14042  cexp 14102  abscabs 15273  cli 15520  Σcsu 15722  t crest 17465  TopOpenctopn 17466  ∞Metcxmet 21349  ballcbl 21351  MetOpencmopn 21354  fldccnfld 21364  Topctop 22899  TopOnctopon 22916  Clsdccld 23024  intcnt 23025   Cn ccn 23232   CnP ccnp 23233  Hauscha 23316  cnccncf 24902
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-inf2 9681  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233  ax-addf 11234
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-tp 4631  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-iin 4994  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-of 7697  df-om 7888  df-1st 8014  df-2nd 8015  df-supp 8186  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-2o 8507  df-er 8745  df-map 8868  df-pm 8869  df-ixp 8938  df-en 8986  df-dom 8987  df-sdom 8988  df-fin 8989  df-fsupp 9402  df-fi 9451  df-sup 9482  df-inf 9483  df-oi 9550  df-card 9979  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-nn 12267  df-2 12329  df-3 12330  df-4 12331  df-5 12332  df-6 12333  df-7 12334  df-8 12335  df-9 12336  df-n0 12527  df-z 12614  df-dec 12734  df-uz 12879  df-q 12991  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-ico 13393  df-icc 13394  df-fz 13548  df-fzo 13695  df-fl 13832  df-seq 14043  df-exp 14103  df-hash 14370  df-shft 15106  df-cj 15138  df-re 15139  df-im 15140  df-sqrt 15274  df-abs 15275  df-limsup 15507  df-clim 15524  df-rlim 15525  df-sum 15723  df-struct 17184  df-sets 17201  df-slot 17219  df-ndx 17231  df-base 17248  df-ress 17275  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-hom 17321  df-cco 17322  df-rest 17467  df-topn 17468  df-0g 17486  df-gsum 17487  df-topgen 17488  df-pt 17489  df-prds 17492  df-xrs 17547  df-qtop 17552  df-imas 17553  df-xps 17555  df-mre 17629  df-mrc 17630  df-acs 17632  df-mgm 18653  df-sgrp 18732  df-mnd 18748  df-submnd 18797  df-mulg 19086  df-cntz 19335  df-cmn 19800  df-psmet 21356  df-xmet 21357  df-met 21358  df-bl 21359  df-mopn 21360  df-cnfld 21365  df-top 22900  df-topon 22917  df-topsp 22939  df-bases 22953  df-cld 23027  df-ntr 23028  df-cn 23235  df-cnp 23236  df-t1 23322  df-haus 23323  df-tx 23570  df-hmeo 23763  df-xms 24330  df-ms 24331  df-tms 24332  df-cncf 24904  df-ulm 26420
This theorem is referenced by:  abelth2  26486
  Copyright terms: Public domain W3C validator