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

Theorem abelth 24176
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 24161.) (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 24169 . . 3 (𝜑𝐹:𝑆⟶ℂ)
81, 2, 3, 4, 5, 6abelthlem9 24175 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟))
91, 2, 3, 4, 5abelthlem2 24167 . . . . . . . . . . . . . . . . . 18 (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
109simpld 475 . . . . . . . . . . . . . . . . 17 (𝜑 → 1 ∈ 𝑆)
1110ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 1 ∈ 𝑆)
12 simpr 477 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 𝑦𝑆)
1311, 12ovresd 6786 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (1(abs ∘ − )𝑦))
14 ax-1cn 9979 . . . . . . . . . . . . . . . 16 1 ∈ ℂ
15 ssrab2 3679 . . . . . . . . . . . . . . . . . 18 {𝑧 ∈ ℂ ∣ (abs‘(1 − 𝑧)) ≤ (𝑀 · (1 − (abs‘𝑧)))} ⊆ ℂ
165, 15eqsstri 3627 . . . . . . . . . . . . . . . . 17 𝑆 ⊆ ℂ
1716, 12sseldi 3593 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 𝑦 ∈ ℂ)
18 eqid 2620 . . . . . . . . . . . . . . . . 17 (abs ∘ − ) = (abs ∘ − )
1918cnmetdval 22555 . . . . . . . . . . . . . . . 16 ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
2014, 17, 19sylancr 694 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
2113, 20eqtrd 2654 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (abs‘(1 − 𝑦)))
2221breq1d 4654 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 ↔ (abs‘(1 − 𝑦)) < 𝑤))
237ad2antrr 761 . . . . . . . . . . . . . . . 16 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → 𝐹:𝑆⟶ℂ)
2423, 11ffvelrnd 6346 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (𝐹‘1) ∈ ℂ)
257adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑟 ∈ ℝ+) → 𝐹:𝑆⟶ℂ)
2625ffvelrnda 6345 . . . . . . . . . . . . . . 15 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (𝐹𝑦) ∈ ℂ)
2718cnmetdval 22555 . . . . . . . . . . . . . . 15 (((𝐹‘1) ∈ ℂ ∧ (𝐹𝑦) ∈ ℂ) → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) = (abs‘((𝐹‘1) − (𝐹𝑦))))
2824, 26, 27syl2anc 692 . . . . . . . . . . . . . 14 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) = (abs‘((𝐹‘1) − (𝐹𝑦))))
2928breq1d 4654 . . . . . . . . . . . . 13 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟 ↔ (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟))
3022, 29imbi12d 334 . . . . . . . . . . . 12 (((𝜑𝑟 ∈ ℝ+) ∧ 𝑦𝑆) → (((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟)))
3130ralbidva 2982 . . . . . . . . . . 11 ((𝜑𝑟 ∈ ℝ+) → (∀𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟) ↔ ∀𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟)))
3231rexbidv 3048 . . . . . . . . . 10 ((𝜑𝑟 ∈ ℝ+) → (∃𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟) ↔ ∃𝑤 ∈ ℝ+𝑦𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹𝑦))) < 𝑟)))
338, 32mpbird 247 . . . . . . . . 9 ((𝜑𝑟 ∈ ℝ+) → ∃𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))
3433ralrimiva 2963 . . . . . . . 8 (𝜑 → ∀𝑟 ∈ ℝ+𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))
35 cnxmet 22557 . . . . . . . . . . 11 (abs ∘ − ) ∈ (∞Met‘ℂ)
36 xmetres2 22147 . . . . . . . . . . 11 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
3735, 16, 36mp2an 707 . . . . . . . . . 10 ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆)
3837a1i 11 . . . . . . . . 9 (𝜑 → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
3935a1i 11 . . . . . . . . 9 (𝜑 → (abs ∘ − ) ∈ (∞Met‘ℂ))
40 eqid 2620 . . . . . . . . . . . 12 ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
41 eqid 2620 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
4241cnfldtopn 22566 . . . . . . . . . . . 12 (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
43 eqid 2620 . . . . . . . . . . . 12 (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
4440, 42, 43metrest 22310 . . . . . . . . . . 11 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
4535, 16, 44mp2an 707 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
4645, 42metcnp 22327 . . . . . . . . 9 ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ 𝑆) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))))
4738, 39, 10, 46syl3anc 1324 . . . . . . . 8 (𝜑 → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+𝑤 ∈ ℝ+𝑦𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹𝑦)) < 𝑟))))
487, 34, 47mpbir2and 956 . . . . . . 7 (𝜑𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
4948ad2antrr 761 . . . . . 6 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
50 simpr 477 . . . . . . 7 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → 𝑦 = 1)
5150fveq2d 6182 . . . . . 6 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
5249, 51eleqtrrd 2702 . . . . 5 (((𝜑𝑦𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
53 eldifsn 4308 . . . . . . 7 (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦𝑆𝑦 ≠ 1))
549simprd 479 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
55 abscl 13999 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (abs‘𝑤) ∈ ℝ)
5655adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ)
5756a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) ∈ ℝ))
58 absge0 14008 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → 0 ≤ (abs‘𝑤))
5958adantl 482 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → 0 ≤ (abs‘𝑤))
6059a1d 25 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → 0 ≤ (abs‘𝑤)))
611, 2abelthlem1 24166 . . . . . . . . . . . . . . . . . . . . . . 23 (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
6261adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
6356rexrd 10074 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ*)
64 1re 10024 . . . . . . . . . . . . . . . . . . . . . . . 24 1 ∈ ℝ
65 rexr 10070 . . . . . . . . . . . . . . . . . . . . . . . 24 (1 ∈ ℝ → 1 ∈ ℝ*)
6664, 65mp1i 13 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ ℂ) → 1 ∈ ℝ*)
67 iccssxr 12241 . . . . . . . . . . . . . . . . . . . . . . . . 25 (0[,]+∞) ⊆ ℝ*
68 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛)))) = (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))
69 eqid 2620 . . . . . . . . . . . . . . . . . . . . . . . . . 26 sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
7068, 1, 69radcnvcl 24152 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
7167, 70sseldi 3593 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
7271adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑤 ∈ ℂ) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
73 xrltletr 11973 . . . . . . . . . . . . . . . . . . . . . . 23 (((abs‘𝑤) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
7463, 66, 72, 73syl3anc 1324 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑤 ∈ ℂ) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
7562, 74mpan2d 709 . . . . . . . . . . . . . . . . . . . . 21 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
7657, 60, 753jcad 1241 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
77 0cn 10017 . . . . . . . . . . . . . . . . . . . . . . . 24 0 ∈ ℂ
7818cnmetdval 22555 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
7977, 78mpan 705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
80 abssub 14047 . . . . . . . . . . . . . . . . . . . . . . . 24 ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
8177, 80mpan 705 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
82 subid1 10286 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑤 ∈ ℂ → (𝑤 − 0) = 𝑤)
8382fveq2d 6182 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 ∈ ℂ → (abs‘(𝑤 − 0)) = (abs‘𝑤))
8479, 81, 833eqtrd 2658 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘𝑤))
8584breq1d 4654 . . . . . . . . . . . . . . . . . . . . 21 (𝑤 ∈ ℂ → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
8685adantl 482 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
87 0re 10025 . . . . . . . . . . . . . . . . . . . . 21 0 ∈ ℝ
88 elico2 12222 . . . . . . . . . . . . . . . . . . . . 21 ((0 ∈ ℝ ∧ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
8987, 72, 88sylancr 694 . . . . . . . . . . . . . . . . . . . 20 ((𝜑𝑤 ∈ ℂ) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
9076, 86, 893imtr4d 283 . . . . . . . . . . . . . . . . . . 19 ((𝜑𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 → (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
9190imdistanda 728 . . . . . . . . . . . . . . . . . 18 (𝜑 → ((𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1) → (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))))
9264rexri 10082 . . . . . . . . . . . . . . . . . . 19 1 ∈ ℝ*
93 elbl 22174 . . . . . . . . . . . . . . . . . . 19 (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1)))
9435, 77, 92, 93mp3an 1422 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1))
95 absf 14058 . . . . . . . . . . . . . . . . . . 19 abs:ℂ⟶ℝ
96 ffn 6032 . . . . . . . . . . . . . . . . . . 19 (abs:ℂ⟶ℝ → abs Fn ℂ)
97 elpreima 6323 . . . . . . . . . . . . . . . . . . 19 (abs Fn ℂ → (𝑤 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))))
9895, 96, 97mp2b 10 . . . . . . . . . . . . . . . . . 18 (𝑤 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↔ (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
9991, 94, 983imtr4g 285 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) → 𝑤 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))))
10099ssrdv 3601 . . . . . . . . . . . . . . . 16 (𝜑 → (0(ball‘(abs ∘ − ))1) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
10154, 100sstrd 3605 . . . . . . . . . . . . . . 15 (𝜑 → (𝑆 ∖ {1}) ⊆ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
102101resmptd 5440 . . . . . . . . . . . . . 14 (𝜑 → ((𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))))
1036reseq1i 5381 . . . . . . . . . . . . . . 15 (𝐹 ↾ (𝑆 ∖ {1})) = ((𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1}))
104 difss 3729 . . . . . . . . . . . . . . . 16 (𝑆 ∖ {1}) ⊆ 𝑆
105 resmpt 5437 . . . . . . . . . . . . . . . 16 ((𝑆 ∖ {1}) ⊆ 𝑆 → ((𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))))
106104, 105ax-mp 5 . . . . . . . . . . . . . . 15 ((𝑥𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
107103, 106eqtri 2642 . . . . . . . . . . . . . 14 (𝐹 ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)))
108102, 107syl6eqr 2672 . . . . . . . . . . . . 13 (𝜑 → ((𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) = (𝐹 ↾ (𝑆 ∖ {1})))
109 cnvimass 5473 . . . . . . . . . . . . . . . . . . 19 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
11095fdmi 6039 . . . . . . . . . . . . . . . . . . 19 dom abs = ℂ
111109, 110sseqtri 3629 . . . . . . . . . . . . . . . . . 18 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
112111sseli 3591 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) → 𝑥 ∈ ℂ)
11368pserval2 24146 . . . . . . . . . . . . . . . . . . 19 ((𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗) = ((𝐴𝑗) · (𝑥𝑗)))
114113sumeq2dv 14414 . . . . . . . . . . . . . . . . . 18 (𝑥 ∈ ℂ → Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) · (𝑥𝑗)))
115 fveq2 6178 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → (𝐴𝑛) = (𝐴𝑗))
116 oveq2 6643 . . . . . . . . . . . . . . . . . . . 20 (𝑛 = 𝑗 → (𝑥𝑛) = (𝑥𝑗))
117115, 116oveq12d 6653 . . . . . . . . . . . . . . . . . . 19 (𝑛 = 𝑗 → ((𝐴𝑛) · (𝑥𝑛)) = ((𝐴𝑗) · (𝑥𝑗)))
118117cbvsumv 14407 . . . . . . . . . . . . . . . . . 18 Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑗 ∈ ℕ0 ((𝐴𝑗) · (𝑥𝑗))
119114, 118syl6reqr 2673 . . . . . . . . . . . . . . . . 17 (𝑥 ∈ ℂ → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗))
120112, 119syl 17 . . . . . . . . . . . . . . . 16 (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗))
121120mpteq2ia 4731 . . . . . . . . . . . . . . 15 (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) = (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑥)‘𝑗))
122 eqid 2620 . . . . . . . . . . . . . . 15 (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) = (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
123 eqid 2620 . . . . . . . . . . . . . . 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))
12468, 121, 1, 69, 122, 123psercn 24161 . . . . . . . . . . . . . 14 (𝜑 → (𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ∈ ((abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))–cn→ℂ))
125 rescncf 22681 . . . . . . . . . . . . . 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→ℂ)))
126101, 124, 125sylc 65 . . . . . . . . . . . . 13 (𝜑 → ((𝑥 ∈ (abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴𝑛) · (𝑡𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴𝑛) · (𝑥𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
127108, 126eqeltrrd 2700 . . . . . . . . . . . 12 (𝜑 → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
128127adantr 481 . . . . . . . . . . 11 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
129104, 16sstri 3604 . . . . . . . . . . . 12 (𝑆 ∖ {1}) ⊆ ℂ
130 ssid 3616 . . . . . . . . . . . 12 ℂ ⊆ ℂ
131 eqid 2620 . . . . . . . . . . . . 13 ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
13241cnfldtop 22568 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ Top
13341cnfldtopon 22567 . . . . . . . . . . . . . . . . 17 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
134133toponunii 20702 . . . . . . . . . . . . . . . 16 ℂ = (TopOpen‘ℂfld)
135134restid 16075 . . . . . . . . . . . . . . 15 ((TopOpen‘ℂfld) ∈ Top → ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld))
136132, 135ax-mp 5 . . . . . . . . . . . . . 14 ((TopOpen‘ℂfld) ↾t ℂ) = (TopOpen‘ℂfld)
137136eqcomi 2629 . . . . . . . . . . . . 13 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
13841, 131, 137cncfcn 22693 . . . . . . . . . . . 12 (((𝑆 ∖ {1}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)))
139129, 130, 138mp2an 707 . . . . . . . . . . 11 ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld))
140128, 139syl6eleq 2709 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)))
141 simpr 477 . . . . . . . . . 10 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ (𝑆 ∖ {1}))
142 resttopon 20946 . . . . . . . . . . . . 13 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝑆 ∖ {1}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1})))
143133, 129, 142mp2an 707 . . . . . . . . . . . 12 ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1}))
144143toponunii 20702 . . . . . . . . . . 11 (𝑆 ∖ {1}) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
145144cncnpi 21063 . . . . . . . . . 10 (((𝐹 ↾ (𝑆 ∖ {1})) ∈ (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)) ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
146140, 141, 145syl2anc 692 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
147 cnex 10002 . . . . . . . . . . . . 13 ℂ ∈ V
148147, 16ssexi 4794 . . . . . . . . . . . 12 𝑆 ∈ V
149 restabs 20950 . . . . . . . . . . . 12 (((TopOpen‘ℂfld) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆𝑆 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})))
150132, 104, 148, 149mp3an 1422 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
151150oveq1i 6645 . . . . . . . . . 10 ((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))
152151fveq1i 6179 . . . . . . . . 9 (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦)
153146, 152syl6eleqr 2710 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
154 resttop 20945 . . . . . . . . . . 11 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
155132, 148, 154mp2an 707 . . . . . . . . . 10 ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top
156155a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
157104a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝑆 ∖ {1}) ⊆ 𝑆)
15810snssd 4331 . . . . . . . . . . . . 13 (𝜑 → {1} ⊆ 𝑆)
15941cnfldhaus 22569 . . . . . . . . . . . . . . 15 (TopOpen‘ℂfld) ∈ Haus
160134sncld 21156 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ Haus ∧ 1 ∈ ℂ) → {1} ∈ (Clsd‘(TopOpen‘ℂfld)))
161159, 14, 160mp2an 707 . . . . . . . . . . . . . 14 {1} ∈ (Clsd‘(TopOpen‘ℂfld))
162134restcldi 20958 . . . . . . . . . . . . . 14 ((𝑆 ⊆ ℂ ∧ {1} ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ {1} ⊆ 𝑆) → {1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)))
16316, 161, 162mp3an12 1412 . . . . . . . . . . . . 13 ({1} ⊆ 𝑆 → {1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)))
164134restuni 20947 . . . . . . . . . . . . . . 15 (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆))
165132, 16, 164mp2an 707 . . . . . . . . . . . . . 14 𝑆 = ((TopOpen‘ℂfld) ↾t 𝑆)
166165cldopn 20816 . . . . . . . . . . . . 13 ({1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)) → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
167158, 163, 1663syl 18 . . . . . . . . . . . 12 (𝜑 → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
168165isopn3 20851 . . . . . . . . . . . . 13 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) → ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})))
169155, 104, 168mp2an 707 . . . . . . . . . . . 12 ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))
170167, 169sylib 208 . . . . . . . . . . 11 (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))
171170eleq2d 2685 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) ↔ 𝑦 ∈ (𝑆 ∖ {1})))
172171biimpar 502 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})))
1737adantr 481 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝐹:𝑆⟶ℂ)
174165, 134cnprest 21074 . . . . . . . . 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))‘𝑦)))
175156, 157, 172, 173, 174syl22anc 1325 . . . . . . . 8 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦)))
176153, 175mpbird 247 . . . . . . 7 ((𝜑𝑦 ∈ (𝑆 ∖ {1})) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
17753, 176sylan2br 493 . . . . . 6 ((𝜑 ∧ (𝑦𝑆𝑦 ≠ 1)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
178177anassrs 679 . . . . 5 (((𝜑𝑦𝑆) ∧ 𝑦 ≠ 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
17952, 178pm2.61dane 2878 . . . 4 ((𝜑𝑦𝑆) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
180179ralrimiva 2963 . . 3 (𝜑 → ∀𝑦𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
181 resttopon 20946 . . . . 5 (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
182133, 16, 181mp2an 707 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)
183 cncnp 21065 . . . 4 ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆) ∧ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)) → (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))))
184182, 133, 183mp2an 707 . . 3 (𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦)))
1857, 180, 184sylanbrc 697 . 2 (𝜑𝐹 ∈ (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
186 eqid 2620 . . . 4 ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
18741, 186, 137cncfcn 22693 . . 3 ((𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑆cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
18816, 130, 187mp2an 707 . 2 (𝑆cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
189185, 188syl6eleqr 2710 1 (𝜑𝐹 ∈ (𝑆cn→ℂ))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1481  wcel 1988  wne 2791  wral 2909  wrex 2910  {crab 2913  Vcvv 3195  cdif 3564  wss 3567  ifcif 4077  {csn 4168   cuni 4427   class class class wbr 4644  cmpt 4720   × cxp 5102  ccnv 5103  dom cdm 5104  cres 5106  cima 5107  ccom 5108   Fn wfn 5871  wf 5872  cfv 5876  (class class class)co 6635  supcsup 8331  cc 9919  cr 9920  0cc0 9921  1c1 9922   + caddc 9924   · cmul 9926  +∞cpnf 10056  *cxr 10058   < clt 10059  cle 10060  cmin 10251   / cdiv 10669  2c2 11055  0cn0 11277  +crp 11817  [,)cico 12162  [,]cicc 12163  seqcseq 12784  cexp 12843  abscabs 13955  cli 14196  Σcsu 14397  t crest 16062  TopOpenctopn 16063  ∞Metcxmt 19712  ballcbl 19714  MetOpencmopn 19717  fldccnfld 19727  Topctop 20679  TopOnctopon 20696  Clsdccld 20801  intcnt 20802   Cn ccn 21009   CnP ccnp 21010  Hauscha 21093  cnccncf 22660
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-8 1990  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-rep 4762  ax-sep 4772  ax-nul 4780  ax-pow 4834  ax-pr 4897  ax-un 6934  ax-inf2 8523  ax-cnex 9977  ax-resscn 9978  ax-1cn 9979  ax-icn 9980  ax-addcl 9981  ax-addrcl 9982  ax-mulcl 9983  ax-mulrcl 9984  ax-mulcom 9985  ax-addass 9986  ax-mulass 9987  ax-distr 9988  ax-i2m1 9989  ax-1ne0 9990  ax-1rid 9991  ax-rnegex 9992  ax-rrecex 9993  ax-cnre 9994  ax-pre-lttri 9995  ax-pre-lttrn 9996  ax-pre-ltadd 9997  ax-pre-mulgt0 9998  ax-pre-sup 9999  ax-addf 10000  ax-mulf 10001
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1484  df-fal 1487  df-ex 1703  df-nf 1708  df-sb 1879  df-eu 2472  df-mo 2473  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-ne 2792  df-nel 2895  df-ral 2914  df-rex 2915  df-reu 2916  df-rmo 2917  df-rab 2918  df-v 3197  df-sbc 3430  df-csb 3527  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-pss 3583  df-nul 3908  df-if 4078  df-pw 4151  df-sn 4169  df-pr 4171  df-tp 4173  df-op 4175  df-uni 4428  df-int 4467  df-iun 4513  df-iin 4514  df-br 4645  df-opab 4704  df-mpt 4721  df-tr 4744  df-id 5014  df-eprel 5019  df-po 5025  df-so 5026  df-fr 5063  df-se 5064  df-we 5065  df-xp 5110  df-rel 5111  df-cnv 5112  df-co 5113  df-dm 5114  df-rn 5115  df-res 5116  df-ima 5117  df-pred 5668  df-ord 5714  df-on 5715  df-lim 5716  df-suc 5717  df-iota 5839  df-fun 5878  df-fn 5879  df-f 5880  df-f1 5881  df-fo 5882  df-f1o 5883  df-fv 5884  df-isom 5885  df-riota 6596  df-ov 6638  df-oprab 6639  df-mpt2 6640  df-of 6882  df-om 7051  df-1st 7153  df-2nd 7154  df-supp 7281  df-wrecs 7392  df-recs 7453  df-rdg 7491  df-1o 7545  df-2o 7546  df-oadd 7549  df-er 7727  df-map 7844  df-pm 7845  df-ixp 7894  df-en 7941  df-dom 7942  df-sdom 7943  df-fin 7944  df-fsupp 8261  df-fi 8302  df-sup 8333  df-inf 8334  df-oi 8400  df-card 8750  df-cda 8975  df-pnf 10061  df-mnf 10062  df-xr 10063  df-ltxr 10064  df-le 10065  df-sub 10253  df-neg 10254  df-div 10670  df-nn 11006  df-2 11064  df-3 11065  df-4 11066  df-5 11067  df-6 11068  df-7 11069  df-8 11070  df-9 11071  df-n0 11278  df-z 11363  df-dec 11479  df-uz 11673  df-q 11774  df-rp 11818  df-xneg 11931  df-xadd 11932  df-xmul 11933  df-ico 12166  df-icc 12167  df-fz 12312  df-fzo 12450  df-fl 12576  df-seq 12785  df-exp 12844  df-hash 13101  df-shft 13788  df-cj 13820  df-re 13821  df-im 13822  df-sqrt 13956  df-abs 13957  df-limsup 14183  df-clim 14200  df-rlim 14201  df-sum 14398  df-struct 15840  df-ndx 15841  df-slot 15842  df-base 15844  df-sets 15845  df-ress 15846  df-plusg 15935  df-mulr 15936  df-starv 15937  df-sca 15938  df-vsca 15939  df-ip 15940  df-tset 15941  df-ple 15942  df-ds 15945  df-unif 15946  df-hom 15947  df-cco 15948  df-rest 16064  df-topn 16065  df-0g 16083  df-gsum 16084  df-topgen 16085  df-pt 16086  df-prds 16089  df-xrs 16143  df-qtop 16148  df-imas 16149  df-xps 16151  df-mre 16227  df-mrc 16228  df-acs 16230  df-mgm 17223  df-sgrp 17265  df-mnd 17276  df-submnd 17317  df-mulg 17522  df-cntz 17731  df-cmn 18176  df-psmet 19719  df-xmet 19720  df-met 19721  df-bl 19722  df-mopn 19723  df-cnfld 19728  df-top 20680  df-topon 20697  df-topsp 20718  df-bases 20731  df-cld 20804  df-ntr 20805  df-cn 21012  df-cnp 21013  df-t1 21099  df-haus 21100  df-tx 21346  df-hmeo 21539  df-xms 22106  df-ms 22107  df-tms 22108  df-cncf 22662  df-ulm 24112
This theorem is referenced by:  abelth2  24177
  Copyright terms: Public domain W3C validator