Metamath Proof Explorer

Theorem abelth

Description: Abel's theorem. If the power series sum_ n e. NN0 A ( n ) ( x ^ n ) is convergent at 1 , then it is equal to the limit from "below", along a Stolz angle S (note that the M = 1 case of a Stolz angle is the real line [ 0 , 1 ] ). (Continuity on S \ { 1 } follows more generally from psercn .) (Contributed by Mario Carneiro, 2-Apr-2015) (Revised by Mario Carneiro, 8-Sep-2015)

Ref Expression
Hypotheses abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
Assertion abelth ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )

Proof

Step Hyp Ref Expression
1 abelth.1 ⊢ ( 𝜑 → 𝐴 : ℕ0 ⟶ ℂ )
2 abelth.2 ⊢ ( 𝜑 → seq 0 ( + , 𝐴 ) ∈ dom ⇝ )
3 abelth.3 ⊢ ( 𝜑 → 𝑀 ∈ ℝ )
4 abelth.4 ⊢ ( 𝜑 → 0 ≤ 𝑀 )
5 abelth.5 ⊢ 𝑆 = { 𝑧 ∈ ℂ ∣ ( abs ‘ ( 1 − 𝑧 ) ) ≤ ( 𝑀 · ( 1 − ( abs ‘ 𝑧 ) ) ) }
6 abelth.6 ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
7 1 2 3 4 5 6 abelthlem4 ⊢ ( 𝜑 → 𝐹 : 𝑆 ⟶ ℂ )
8 1 2 3 4 5 6 abelthlem9 ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑟 ) )
9 1 2 3 4 5 abelthlem2 ⊢ ( 𝜑 → ( 1 ∈ 𝑆 ∧ ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ) )
10 9 simpld ⊢ ( 𝜑 → 1 ∈ 𝑆 )
11 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → 1 ∈ 𝑆 )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
13 11 12 ovresd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( 1 ( abs ∘ − ) 𝑦 ) )
14 ax-1cn ⊢ 1 ∈ ℂ
15 5 ssrab3 ⊢ 𝑆 ⊆ ℂ
16 15 12 sselid ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ℂ )
17 eqid ⊢ ( abs ∘ − ) = ( abs ∘ − )
18 17 cnmetdval ⊢ ( ( 1 ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( 1 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 1 − 𝑦 ) ) )
19 14 16 18 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( 1 ( abs ∘ − ) 𝑦 ) = ( abs ‘ ( 1 − 𝑦 ) ) )
20 13 19 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) = ( abs ‘ ( 1 − 𝑦 ) ) )
21 20 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 ↔ ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 ) )
22 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → 𝐹 : 𝑆 ⟶ ℂ )
23 22 11 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 1 ) ∈ ℂ )
24 7 adantr ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → 𝐹 : 𝑆 ⟶ ℂ )
25 24 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝐹 ‘ 𝑦 ) ∈ ℂ )
26 17 cnmetdval ⊢ ( ( ( 𝐹 ‘ 1 ) ∈ ℂ ∧ ( 𝐹 ‘ 𝑦 ) ∈ ℂ ) → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) )
27 23 25 26 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) )
28 27 breq1d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ↔ ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑟 ) )
29 21 28 imbi12d ⊢ ( ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) ↔ ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑟 ) ) )
30 29 ralbidva ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∀ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) ↔ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑟 ) ) )
31 30 rexbidv ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ( ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) ↔ ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( abs ‘ ( 1 − 𝑦 ) ) < 𝑤 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐹 ‘ 𝑦 ) ) ) < 𝑟 ) ) )
32 8 31 mpbird ⊢ ( ( 𝜑 ∧ 𝑟 ∈ ℝ+ ) → ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) )
33 32 ralrimiva ⊢ ( 𝜑 → ∀ 𝑟 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) )
34 cnxmet ⊢ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ )
35 xmetres2 ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) )
36 34 15 35 mp2an ⊢ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 )
37 eqid ⊢ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) = ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) )
38 eqid ⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
39 38 cnfldtopn ⊢ ( TopOpen ‘ ℂfld ) = ( MetOpen ‘ ( abs ∘ − ) )
40 eqid ⊢ ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) )
41 37 39 40 metrest ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ) )
42 34 15 41 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( MetOpen ‘ ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) )
43 42 39 metcnp ⊢ ( ( ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) ∈ ( ∞Met ‘ 𝑆 ) ∧ ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 1 ∈ 𝑆 ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 1 ) ↔ ( 𝐹 : 𝑆 ⟶ ℂ ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) ) ) )
44 36 34 10 43 mp3an12i ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 1 ) ↔ ( 𝐹 : 𝑆 ⟶ ℂ ∧ ∀ 𝑟 ∈ ℝ+ ∃ 𝑤 ∈ ℝ+ ∀ 𝑦 ∈ 𝑆 ( ( 1 ( ( abs ∘ − ) ↾ ( 𝑆 × 𝑆 ) ) 𝑦 ) < 𝑤 → ( ( 𝐹 ‘ 1 ) ( abs ∘ − ) ( 𝐹 ‘ 𝑦 ) ) < 𝑟 ) ) ) )
45 7 33 44 mpbir2and ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 1 ) )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 1 ) )
47 simpr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) → 𝑦 = 1 )
48 47 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) → ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 1 ) )
49 46 48 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 = 1 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
50 eldifsn ⊢ ( 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ↔ ( 𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1 ) )
51 9 simprd ⊢ ( 𝜑 → ( 𝑆 ∖ { 1 } ) ⊆ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) )
52 abscl ⊢ ( 𝑤 ∈ ℂ → ( abs ‘ 𝑤 ) ∈ ℝ )
53 52 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( abs ‘ 𝑤 ) ∈ ℝ )
54 53 a1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( abs ‘ 𝑤 ) < 1 → ( abs ‘ 𝑤 ) ∈ ℝ ) )
55 absge0 ⊢ ( 𝑤 ∈ ℂ → 0 ≤ ( abs ‘ 𝑤 ) )
56 55 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → 0 ≤ ( abs ‘ 𝑤 ) )
57 56 a1d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( abs ‘ 𝑤 ) < 1 → 0 ≤ ( abs ‘ 𝑤 ) ) )
58 1 2 abelthlem1 ⊢ ( 𝜑 → 1 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
59 58 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → 1 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) )
60 53 rexrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( abs ‘ 𝑤 ) ∈ ℝ* )
61 1re ⊢ 1 ∈ ℝ
62 rexr ⊢ ( 1 ∈ ℝ → 1 ∈ ℝ* )
63 61 62 mp1i ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → 1 ∈ ℝ* )
64 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
65 eqid ⊢ ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) = ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) )
66 eqid ⊢ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) = sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < )
67 65 1 66 radcnvcl ⊢ ( 𝜑 → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ( 0 [,] +∞ ) )
68 64 67 sselid ⊢ ( 𝜑 → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
69 68 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* )
70 xrltletr ⊢ ( ( ( abs ‘ 𝑤 ) ∈ ℝ* ∧ 1 ∈ ℝ* ∧ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* ) → ( ( ( abs ‘ 𝑤 ) < 1 ∧ 1 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) → ( abs ‘ 𝑤 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
71 60 63 69 70 syl3anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( ( abs ‘ 𝑤 ) < 1 ∧ 1 ≤ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) → ( abs ‘ 𝑤 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
72 59 71 mpan2d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( abs ‘ 𝑤 ) < 1 → ( abs ‘ 𝑤 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
73 54 57 72 3jcad ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( abs ‘ 𝑤 ) < 1 → ( ( abs ‘ 𝑤 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑤 ) ∧ ( abs ‘ 𝑤 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
74 0cn ⊢ 0 ∈ ℂ
75 17 cnmetdval ⊢ ( ( 0 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( 0 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 0 − 𝑤 ) ) )
76 74 75 mpan ⊢ ( 𝑤 ∈ ℂ → ( 0 ( abs ∘ − ) 𝑤 ) = ( abs ‘ ( 0 − 𝑤 ) ) )
77 abssub ⊢ ( ( 0 ∈ ℂ ∧ 𝑤 ∈ ℂ ) → ( abs ‘ ( 0 − 𝑤 ) ) = ( abs ‘ ( 𝑤 − 0 ) ) )
78 74 77 mpan ⊢ ( 𝑤 ∈ ℂ → ( abs ‘ ( 0 − 𝑤 ) ) = ( abs ‘ ( 𝑤 − 0 ) ) )
79 subid1 ⊢ ( 𝑤 ∈ ℂ → ( 𝑤 − 0 ) = 𝑤 )
80 79 fveq2d ⊢ ( 𝑤 ∈ ℂ → ( abs ‘ ( 𝑤 − 0 ) ) = ( abs ‘ 𝑤 ) )
81 76 78 80 3eqtrd ⊢ ( 𝑤 ∈ ℂ → ( 0 ( abs ∘ − ) 𝑤 ) = ( abs ‘ 𝑤 ) )
82 81 breq1d ⊢ ( 𝑤 ∈ ℂ → ( ( 0 ( abs ∘ − ) 𝑤 ) < 1 ↔ ( abs ‘ 𝑤 ) < 1 ) )
83 82 adantl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( 0 ( abs ∘ − ) 𝑤 ) < 1 ↔ ( abs ‘ 𝑤 ) < 1 ) )
84 0re ⊢ 0 ∈ ℝ
85 elico2 ⊢ ( ( 0 ∈ ℝ ∧ sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ* ) → ( ( abs ‘ 𝑤 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs ‘ 𝑤 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑤 ) ∧ ( abs ‘ 𝑤 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
86 84 69 85 sylancr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( abs ‘ 𝑤 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ↔ ( ( abs ‘ 𝑤 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝑤 ) ∧ ( abs ‘ 𝑤 ) < sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
87 73 83 86 3imtr4d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℂ ) → ( ( 0 ( abs ∘ − ) 𝑤 ) < 1 → ( abs ‘ 𝑤 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
88 87 imdistanda ⊢ ( 𝜑 → ( ( 𝑤 ∈ ℂ ∧ ( 0 ( abs ∘ − ) 𝑤 ) < 1 ) → ( 𝑤 ∈ ℂ ∧ ( abs ‘ 𝑤 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
89 1xr ⊢ 1 ∈ ℝ*
90 elbl ⊢ ( ( ( abs ∘ − ) ∈ ( ∞Met ‘ ℂ ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ* ) → ( 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑤 ∈ ℂ ∧ ( 0 ( abs ∘ − ) 𝑤 ) < 1 ) ) )
91 34 74 89 90 mp3an ⊢ ( 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ↔ ( 𝑤 ∈ ℂ ∧ ( 0 ( abs ∘ − ) 𝑤 ) < 1 ) )
92 absf ⊢ abs : ℂ ⟶ ℝ
93 ffn ⊢ ( abs : ℂ ⟶ ℝ → abs Fn ℂ )
94 elpreima ⊢ ( abs Fn ℂ → ( 𝑤 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑤 ∈ ℂ ∧ ( abs ‘ 𝑤 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
95 92 93 94 mp2b ⊢ ( 𝑤 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↔ ( 𝑤 ∈ ℂ ∧ ( abs ‘ 𝑤 ) ∈ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
96 88 91 95 3imtr4g ⊢ ( 𝜑 → ( 𝑤 ∈ ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) → 𝑤 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ) )
97 96 ssrdv ⊢ ( 𝜑 → ( 0 ( ball ‘ ( abs ∘ − ) ) 1 ) ⊆ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
98 51 97 sstrd ⊢ ( 𝜑 → ( 𝑆 ∖ { 1 } ) ⊆ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) )
99 98 resmptd ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) ) = ( 𝑥 ∈ ( 𝑆 ∖ { 1 } ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
100 6 reseq1i ⊢ ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) = ( ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) )
101 difss ⊢ ( 𝑆 ∖ { 1 } ) ⊆ 𝑆
102 resmpt ⊢ ( ( 𝑆 ∖ { 1 } ) ⊆ 𝑆 → ( ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) ) = ( 𝑥 ∈ ( 𝑆 ∖ { 1 } ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) )
103 101 102 ax-mp ⊢ ( ( 𝑥 ∈ 𝑆 ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) ) = ( 𝑥 ∈ ( 𝑆 ∖ { 1 } ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
104 100 103 eqtri ⊢ ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) = ( 𝑥 ∈ ( 𝑆 ∖ { 1 } ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) )
105 99 104 eqtr4di ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) ) = ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) )
106 cnvimass ⊢ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⊆ dom abs
107 92 fdmi ⊢ dom abs = ℂ
108 106 107 sseqtri ⊢ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ⊆ ℂ
109 108 sseli ⊢ ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) → 𝑥 ∈ ℂ )
110 fveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝐴 ‘ 𝑛 ) = ( 𝐴 ‘ 𝑗 ) )
111 oveq2 ⊢ ( 𝑛 = 𝑗 → ( 𝑥 ↑ 𝑛 ) = ( 𝑥 ↑ 𝑗 ) )
112 110 111 oveq12d ⊢ ( 𝑛 = 𝑗 → ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = ( ( 𝐴 ‘ 𝑗 ) · ( 𝑥 ↑ 𝑗 ) ) )
113 112 cbvsumv ⊢ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐴 ‘ 𝑗 ) · ( 𝑥 ↑ 𝑗 ) )
114 65 pserval2 ⊢ ( ( 𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ0 ) → ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑥 ) ‘ 𝑗 ) = ( ( 𝐴 ‘ 𝑗 ) · ( 𝑥 ↑ 𝑗 ) ) )
115 114 sumeq2dv ⊢ ( 𝑥 ∈ ℂ → Σ 𝑗 ∈ ℕ0 ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑥 ) ‘ 𝑗 ) = Σ 𝑗 ∈ ℕ0 ( ( 𝐴 ‘ 𝑗 ) · ( 𝑥 ↑ 𝑗 ) ) )
116 113 115 eqtr4id ⊢ ( 𝑥 ∈ ℂ → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = Σ 𝑗 ∈ ℕ0 ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑥 ) ‘ 𝑗 ) )
117 109 116 syl ⊢ ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) → Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) = Σ 𝑗 ∈ ℕ0 ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑥 ) ‘ 𝑗 ) )
118 117 mpteq2ia ⊢ ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) = ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑗 ∈ ℕ0 ( ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑥 ) ‘ 𝑗 ) )
119 eqid ⊢ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) = ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) )
120 eqid ⊢ if ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑣 ) + sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑣 ) + 1 ) ) = if ( sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ∈ ℝ , ( ( ( abs ‘ 𝑣 ) + sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) / 2 ) , ( ( abs ‘ 𝑣 ) + 1 ) )
121 65 118 1 66 119 120 psercn ⊢ ( 𝜑 → ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ ( ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cn→ ℂ ) )
122 rescncf ⊢ ( ( 𝑆 ∖ { 1 } ) ⊆ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) → ( ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ∈ ( ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) –cn→ ℂ ) → ( ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( 𝑆 ∖ { 1 } ) –cn→ ℂ ) ) )
123 98 121 122 sylc ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ◡ abs “ ( 0 [,) sup ( { 𝑟 ∈ ℝ ∣ seq 0 ( + , ( ( 𝑡 ∈ ℂ ↦ ( 𝑛 ∈ ℕ0 ↦ ( ( 𝐴 ‘ 𝑛 ) · ( 𝑡 ↑ 𝑛 ) ) ) ) ‘ 𝑟 ) ) ∈ dom ⇝ } , ℝ* , < ) ) ) ↦ Σ 𝑛 ∈ ℕ0 ( ( 𝐴 ‘ 𝑛 ) · ( 𝑥 ↑ 𝑛 ) ) ) ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( 𝑆 ∖ { 1 } ) –cn→ ℂ ) )
124 105 123 eqeltrrd ⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( 𝑆 ∖ { 1 } ) –cn→ ℂ ) )
125 124 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( 𝑆 ∖ { 1 } ) –cn→ ℂ ) )
126 101 15 sstri ⊢ ( 𝑆 ∖ { 1 } ) ⊆ ℂ
127 ssid ⊢ ℂ ⊆ ℂ
128 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) )
129 38 cnfldtopon ⊢ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
130 129 toponrestid ⊢ ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
131 38 128 130 cncfcn ⊢ ( ( ( 𝑆 ∖ { 1 } ) ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( ( 𝑆 ∖ { 1 } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
132 126 127 131 mp2an ⊢ ( ( 𝑆 ∖ { 1 } ) –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) Cn ( TopOpen ‘ ℂfld ) )
133 125 132 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) Cn ( TopOpen ‘ ℂfld ) ) )
134 simpr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → 𝑦 ∈ ( 𝑆 ∖ { 1 } ) )
135 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ ( 𝑆 ∖ { 1 } ) ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) ∈ ( TopOn ‘ ( 𝑆 ∖ { 1 } ) ) )
136 129 126 135 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) ∈ ( TopOn ‘ ( 𝑆 ∖ { 1 } ) )
137 136 toponunii ⊢ ( 𝑆 ∖ { 1 } ) = ∪ ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) )
138 137 cncnpi ⊢ ( ( ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) Cn ( TopOpen ‘ ℂfld ) ) ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
139 133 134 138 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
140 38 cnfldtop ⊢ ( TopOpen ‘ ℂfld ) ∈ Top
141 cnex ⊢ ℂ ∈ V
142 141 15 ssexi ⊢ 𝑆 ∈ V
143 restabs ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ ( 𝑆 ∖ { 1 } ) ⊆ 𝑆 ∧ 𝑆 ∈ V ) → ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 𝑆 ∖ { 1 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) )
144 140 101 142 143 mp3an ⊢ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 𝑆 ∖ { 1 } ) ) = ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) )
145 144 oveq1i ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) = ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) )
146 145 fveq1i ⊢ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) = ( ( ( ( TopOpen ‘ ℂfld ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 )
147 139 146 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
148 resttop ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ∈ V ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
149 140 142 148 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top
150 149 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top )
151 101 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝑆 ∖ { 1 } ) ⊆ 𝑆 )
152 10 snssd ⊢ ( 𝜑 → { 1 } ⊆ 𝑆 )
153 38 cnfldhaus ⊢ ( TopOpen ‘ ℂfld ) ∈ Haus
154 unicntop ⊢ ℂ = ∪ ( TopOpen ‘ ℂfld )
155 154 sncld ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Haus ∧ 1 ∈ ℂ ) → { 1 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) )
156 153 14 155 mp2an ⊢ { 1 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) )
157 154 restcldi ⊢ ( ( 𝑆 ⊆ ℂ ∧ { 1 } ∈ ( Clsd ‘ ( TopOpen ‘ ℂfld ) ) ∧ { 1 } ⊆ 𝑆 ) → { 1 } ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
158 15 156 157 mp3an12 ⊢ ( { 1 } ⊆ 𝑆 → { 1 } ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) )
159 154 restuni ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ Top ∧ 𝑆 ⊆ ℂ ) → 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
160 140 15 159 mp2an ⊢ 𝑆 = ∪ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
161 160 cldopn ⊢ ( { 1 } ∈ ( Clsd ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) → ( 𝑆 ∖ { 1 } ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
162 152 158 161 3syl ⊢ ( 𝜑 → ( 𝑆 ∖ { 1 } ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) )
163 160 isopn3 ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ Top ∧ ( 𝑆 ∖ { 1 } ) ⊆ 𝑆 ) → ( ( 𝑆 ∖ { 1 } ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 𝑆 ∖ { 1 } ) ) = ( 𝑆 ∖ { 1 } ) ) )
164 149 101 163 mp2an ⊢ ( ( 𝑆 ∖ { 1 } ) ∈ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↔ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 𝑆 ∖ { 1 } ) ) = ( 𝑆 ∖ { 1 } ) )
165 162 164 sylib ⊢ ( 𝜑 → ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 𝑆 ∖ { 1 } ) ) = ( 𝑆 ∖ { 1 } ) )
166 165 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 𝑆 ∖ { 1 } ) ) ↔ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) )
167 166 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → 𝑦 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ ( 𝑆 ∖ { 1 } ) ) )
168 7 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → 𝐹 : 𝑆 ⟶ ℂ )
169 160 154 cnprest ⊢ ( ( ( ( ( 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 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → ( 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ↔ ( 𝐹 ↾ ( 𝑆 ∖ { 1 } ) ) ∈ ( ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ↾t ( 𝑆 ∖ { 1 } ) ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
171 147 170 mpbird ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑆 ∖ { 1 } ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
172 50 171 sylan2br ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1 ) ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
173 172 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) ∧ 𝑦 ≠ 1 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
174 49 173 pm2.61dane ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
175 174 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) )
176 resttopon ⊢ ( ( ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
177 129 15 176 mp2an ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 )
178 cncnp ⊢ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) ∧ ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ ) ) → ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝑆 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) ) )
179 177 129 178 mp2an ⊢ ( 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) ↔ ( 𝐹 : 𝑆 ⟶ ℂ ∧ ∀ 𝑦 ∈ 𝑆 𝐹 ∈ ( ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) CnP ( TopOpen ‘ ℂfld ) ) ‘ 𝑦 ) ) )
180 7 175 179 sylanbrc ⊢ ( 𝜑 → 𝐹 ∈ ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) )
181 eqid ⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
182 38 181 130 cncfcn ⊢ ( ( 𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ ) → ( 𝑆 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) ) )
183 15 127 182 mp2an ⊢ ( 𝑆 –cn→ ℂ ) = ( ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) Cn ( TopOpen ‘ ℂfld ) )
184 180 183 eleqtrrdi ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 –cn→ ℂ ) )