Theorem abelth 25800

Description: Abel's theorem. If the power series Σ𝑛 ∈ ℕ₀𝐴(𝑛)(𝑥↑𝑛) 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 25785.) (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.

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 25793	. . 3 ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
8	1, 2, 3, 4, 5, 6	abelthlem9 25799	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))
9	1, 2, 3, 4, 5	abelthlem2 25791	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
10	9	simpld 495	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ 𝑆)
11	10	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 1 ∈ 𝑆)
12		simpr 485	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆)
13	11, 12	ovresd 7521	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (1(abs ∘ − )𝑦))
14		ax-1cn 11109	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
15	5	ssrab3 4040	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ ℂ
16	15, 12	sselid 3942	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
17		eqid 2736	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) = (abs ∘ − )
18	17	cnmetdval 24134	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
19	14, 16, 18	sylancr 587	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
20	13, 19	eqtrd 2776	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (abs‘(1 − 𝑦)))
21	20	breq1d 5115	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 ↔ (abs‘(1 − 𝑦)) < 𝑤))
22	7	ad2antrr 724	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → 𝐹:𝑆⟶ℂ)
23	22, 11	ffvelcdmd 7036	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (𝐹‘1) ∈ ℂ)
24	7	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → 𝐹:𝑆⟶ℂ)
25	24	ffvelcdmda 7035	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (𝐹‘𝑦) ∈ ℂ)
26	17	cnmetdval 24134	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘1) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦))))
27	23, 25, 26	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦))))
28	27	breq1d 5115	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟 ↔ (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))
29	21, 28	imbi12d 344	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ+) ∧ 𝑦 ∈ 𝑆) → (((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)))
30	29	ralbidva 3172	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)))
31	30	rexbidv 3175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → (∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)))
32	8, 31	mpbird 256	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ+) → ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))
33	32	ralrimiva 3143	. . . . . . . 8 ⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))
34		cnxmet 24136	. . . . . . . . . 10 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
35		xmetres2 23714	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
36	34, 15, 35	mp2an 690	. . . . . . . . 9 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆)
37		eqid 2736	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
38		eqid 2736	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
39	38	cnfldtopn 24145	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂfld) = (MetOpen‘(abs ∘ − ))
40		eqid 2736	. . . . . . . . . . . 12 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
41	37, 39, 40	metrest 23880	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
42	34, 15, 41	mp2an 690	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂfld) ↾t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
43	42, 39	metcnp 23897	. . . . . . . . 9 ⊢ ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ 𝑆) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))))
44	36, 34, 10, 43	mp3an12i 1465	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ+ ∃𝑤 ∈ ℝ+ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))))
45	7, 33, 44	mpbir2and 711	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
46	45	ad2antrr 724	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
47		simpr 485	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝑦 = 1)
48	47	fveq2d 6846	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘1))
49	46, 48	eleqtrrd 2841	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
50		eldifsn 4747	. . . . . . 7 ⊢ (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1))
51	9	simprd 496	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
52		abscl 15163	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (abs‘𝑤) ∈ ℝ)
53	52	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ)
54	53	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) ∈ ℝ))
55		absge0 15172	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → 0 ≤ (abs‘𝑤))
56	55	adantl 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 0 ≤ (abs‘𝑤))
57	56	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → 0 ≤ (abs‘𝑤)))
58	1, 2	abelthlem1 25790	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
59	58	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))
60	53	rexrd 11205	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ*)
61		1re 11155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
62		rexr 11201	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℝ → 1 ∈ ℝ*)
63	61, 62	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ∈ ℝ*)
64		iccssxr 13347	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0[,]+∞) ⊆ ℝ*
65		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛)))) = (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))
66		eqid 2736	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )
67	65, 1, 66	radcnvcl 25776	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ (0[,]+∞))
68	64, 67	sselid 3942	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
69	68	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ) ∈ ℝ*)
70		xrltletr 13076	. . . . . . . . . . . . . . . . . . . . . . 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 1371	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
72	59, 71	mpan2d 692	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
73	54, 57, 72	3jcad 1129	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
74		0cn 11147	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℂ
75	17	cnmetdval 24134	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
76	74, 75	mpan 688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
77		abssub 15211	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
78	74, 77	mpan 688	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
79		subid1 11421	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℂ → (𝑤 − 0) = 𝑤)
80	79	fveq2d 6846	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (abs‘(𝑤 − 0)) = (abs‘𝑤))
81	76, 78, 80	3eqtrd 2780	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘𝑤))
82	81	breq1d 5115	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℂ → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
83	82	adantl 482	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
84		0re 11157	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℝ
85		elico2 13328	. . . . . . . . . . . . . . . . . . . . 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 293	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 → (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
88	87	imdistanda 572	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1) → (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))))
89		1xr 11214	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ*
90		elbl 23741	. . . . . . . . . . . . . . . . . . 19 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ*) → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1)))
91	34, 74, 89, 90	mp3an 1461	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1))
92		absf 15222	. . . . . . . . . . . . . . . . . . 19 ⊢ abs:ℂ⟶ℝ
93		ffn 6668	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
94		elpreima 7008	. . . . . . . . . . . . . . . . . . 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 295	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) → 𝑤 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))))
97	96	ssrdv 3950	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0(ball‘(abs ∘ − ))1) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
98	51, 97	sstrd 3954	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))))
99	98	resmptd 5994	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))))
100	6	reseq1i 5933	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ (𝑆 ∖ {1})) = ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1}))
101		difss 4091	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∖ {1}) ⊆ 𝑆
102		resmpt 5991	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∖ {1}) ⊆ 𝑆 → ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))))
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))
104	100, 103	eqtri 2764	. . . . . . . . . . . . . 14 ⊢ (𝐹 ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)))
105	99, 104	eqtr4di 2794	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝐹 ↾ (𝑆 ∖ {1})))
106		cnvimass 6033	. . . . . . . . . . . . . . . . . . 19 ⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ⊆ dom abs
107	92	fdmi 6680	. . . . . . . . . . . . . . . . . . 19 ⊢ dom abs = ℂ
108	106, 107	sseqtri 3980	. . . . . . . . . . . . . . . . . 18 ⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ⊆ ℂ
109	108	sseli 3940	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) → 𝑥 ∈ ℂ)
110		fveq2 6842	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗))
111		oveq2 7365	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → (𝑥↑𝑛) = (𝑥↑𝑗))
112	110, 111	oveq12d 7375	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑗) · (𝑥↑𝑗)))
113	112	cbvsumv 15581	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 ((𝐴‘𝑗) · (𝑥↑𝑗))
114	65	pserval2 25770	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ0) → (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = ((𝐴‘𝑗) · (𝑥↑𝑗)))
115	114	sumeq2dv 15588	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = Σ𝑗 ∈ ℕ0 ((𝐴‘𝑗) · (𝑥↑𝑗)))
116	113, 115	eqtr4id 2795	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗))
117	109, 116	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) → Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗))
118	117	mpteq2ia 5208	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑗 ∈ ℕ0 (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗))
119		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) = (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))
120		eqid 2736	. . . . . . . . . . . . . . 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 25785	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < ))) ↦ Σ𝑛 ∈ ℕ0 ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ ((◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ0 ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ*, < )))–cn→ℂ))
122		rescncf 24260	. . . . . . . . . . . . . 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 2839	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
125	124	adantr 481	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
126	101, 15	sstri 3953	. . . . . . . . . . . 12 ⊢ (𝑆 ∖ {1}) ⊆ ℂ
127		ssid 3966	. . . . . . . . . . . 12 ⊢ ℂ ⊆ ℂ
128		eqid 2736	. . . . . . . . . . . . 13 ⊢ ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
129	38	cnfldtopon 24146	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
130	129	toponrestid 22270	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
131	38, 128, 130	cncfcn 24273	. . . . . . . . . . . 12 ⊢ (((𝑆 ∖ {1}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)))
132	126, 127, 131	mp2an 690	. . . . . . . . . . 11 ⊢ ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld))
133	125, 132	eleqtrdi 2848	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) Cn (TopOpen‘ℂfld)))
134		simpr 485	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ (𝑆 ∖ {1}))
135		resttopon 22512	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ (𝑆 ∖ {1}) ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1})))
136	129, 126, 135	mp2an 690	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1}))
137	136	toponunii 22265	. . . . . . . . . . 11 ⊢ (𝑆 ∖ {1}) = ∪ ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
138	137	cncnpi 22629	. . . . . . . . . 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 24147	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂfld) ∈ Top
141		cnex 11132	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
142	141, 15	ssexi 5279	. . . . . . . . . . . 12 ⊢ 𝑆 ∈ V
143		restabs 22516	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆 ∧ 𝑆 ∈ V) → (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})))
144	140, 101, 142, 143	mp3an 1461	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) = ((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1}))
145	144	oveq1i 7367	. . . . . . . . . 10 ⊢ ((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld)) = (((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))
146	145	fveq1i 6843	. . . . . . . . 9 ⊢ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦) = ((((TopOpen‘ℂfld) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦)
147	139, 146	eleqtrrdi 2849	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦))
148		resttop 22511	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ∈ V) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top)
149	140, 142, 148	mp2an 690	. . . . . . . . . 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 4769	. . . . . . . . . . . . 13 ⊢ (𝜑 → {1} ⊆ 𝑆)
153	38	cnfldhaus 24148	. . . . . . . . . . . . . . 15 ⊢ (TopOpen‘ℂfld) ∈ Haus
154		unicntop 24149	. . . . . . . . . . . . . . . 16 ⊢ ℂ = ∪ (TopOpen‘ℂfld)
155	154	sncld 22722	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂfld) ∈ Haus ∧ 1 ∈ ℂ) → {1} ∈ (Clsd‘(TopOpen‘ℂfld)))
156	153, 14, 155	mp2an 690	. . . . . . . . . . . . . 14 ⊢ {1} ∈ (Clsd‘(TopOpen‘ℂfld))
157	154	restcldi 22524	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ {1} ∈ (Clsd‘(TopOpen‘ℂfld)) ∧ {1} ⊆ 𝑆) → {1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)))
158	15, 156, 157	mp3an12 1451	. . . . . . . . . . . . 13 ⊢ ({1} ⊆ 𝑆 → {1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)))
159	154	restuni 22513	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂfld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ∪ ((TopOpen‘ℂfld) ↾t 𝑆))
160	140, 15, 159	mp2an 690	. . . . . . . . . . . . . 14 ⊢ 𝑆 = ∪ ((TopOpen‘ℂfld) ↾t 𝑆)
161	160	cldopn 22382	. . . . . . . . . . . . 13 ⊢ ({1} ∈ (Clsd‘((TopOpen‘ℂfld) ↾t 𝑆)) → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
162	152, 158, 161	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆))
163	160	isopn3 22417	. . . . . . . . . . . . 13 ⊢ ((((TopOpen‘ℂfld) ↾t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) → ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})))
164	149, 101, 163	mp2an 690	. . . . . . . . . . . 12 ⊢ ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂfld) ↾t 𝑆) ↔ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))
165	162, 164	sylib 217	. . . . . . . . . . 11 ⊢ (𝜑 → ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1}))
166	165	eleq2d 2823	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})) ↔ 𝑦 ∈ (𝑆 ∖ {1})))
167	166	biimpar 478	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ ((int‘((TopOpen‘ℂfld) ↾t 𝑆))‘(𝑆 ∖ {1})))
168	7	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹:𝑆⟶ℂ)
169	160, 154	cnprest 22640	. . . . . . . . 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 837	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂfld) ↾t 𝑆) ↾t (𝑆 ∖ {1})) CnP (TopOpen‘ℂfld))‘𝑦)))
171	147, 170	mpbird 256	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
172	50, 171	sylan2br 595	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
173	172	anassrs 468	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ 1) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
174	49, 173	pm2.61dane 3032	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
175	174	ralrimiva 3143	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝐹 ∈ ((((TopOpen‘ℂfld) ↾t 𝑆) CnP (TopOpen‘ℂfld))‘𝑦))
176		resttopon 22512	. . . . 5 ⊢ (((TopOpen‘ℂfld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆))
177	129, 15, 176	mp2an 690	. . . 4 ⊢ ((TopOpen‘ℂfld) ↾t 𝑆) ∈ (TopOn‘𝑆)
178		cncnp 22631	. . . 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 690	. . 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 2736	. . . 4 ⊢ ((TopOpen‘ℂfld) ↾t 𝑆) = ((TopOpen‘ℂfld) ↾t 𝑆)
182	38, 181, 130	cncfcn 24273	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑆–cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld)))
183	15, 127, 182	mp2an 690	. 2 ⊢ (𝑆–cn→ℂ) = (((TopOpen‘ℂfld) ↾t 𝑆) Cn (TopOpen‘ℂfld))
184	180, 183	eleqtrrdi 2849	1 ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ≠ wne 2943  ∀wral 3064  ∃wrex 3073  {crab 3407  Vcvv 3445   ∖ cdif 3907   ⊆ wss 3910  ifcif 4486  {csn 4586  ∪ cuni 4865   class class class wbr 5105   ↦ cmpt 5188   × cxp 5631  ^◡ccnv 5632  dom cdm 5633   ↾ cres 5635   “ cima 5636   ∘ ccom 5637   Fn wfn 6491  ⟶wf 6492  ‘cfv 6496  (class class class)co 7357  supcsup 9376  ℂcc 11049  ℝcr 11050  0cc0 11051  1c1 11052   + caddc 11054   · cmul 11056  +∞cpnf 11186  ℝ^*cxr 11188   < clt 11189   ≤ cle 11190   − cmin 11385   / cdiv 11812  2c2 12208  ℕ₀cn0 12413  ℝ⁺crp 12915  [,)cico 13266  [,]cicc 13267  seqcseq 13906  ↑cexp 13967  abscabs 15119   ⇝ cli 15366  Σcsu 15570   ↾_t crest 17302  TopOpenctopn 17303  ∞Metcxmet 20781  ballcbl 20783  MetOpencmopn 20786  ℂ_fldccnfld 20796  Topctop 22242  TopOnctopon 22259  Clsdccld 22367  intcnt 22368   Cn ccn 22575   CnP ccnp 22576  Hauscha 22659  –cn→ccncf 24239

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129  ax-addf 11130  ax-mulf 11131

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-of 7617  df-om 7803  df-1st 7921  df-2nd 7922  df-supp 8093  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-2o 8413  df-er 8648  df-map 8767  df-pm 8768  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9306  df-fi 9347  df-sup 9378  df-inf 9379  df-oi 9446  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-4 12218  df-5 12219  df-6 12220  df-7 12221  df-8 12222  df-9 12223  df-n0 12414  df-z 12500  df-dec 12619  df-uz 12764  df-q 12874  df-rp 12916  df-xneg 13033  df-xadd 13034  df-xmul 13035  df-ico 13270  df-icc 13271  df-fz 13425  df-fzo 13568  df-fl 13697  df-seq 13907  df-exp 13968  df-hash 14231  df-shft 14952  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-limsup 15353  df-clim 15370  df-rlim 15371  df-sum 15571  df-struct 17019  df-sets 17036  df-slot 17054  df-ndx 17066  df-base 17084  df-ress 17113  df-plusg 17146  df-mulr 17147  df-starv 17148  df-sca 17149  df-vsca 17150  df-ip 17151  df-tset 17152  df-ple 17153  df-ds 17155  df-unif 17156  df-hom 17157  df-cco 17158  df-rest 17304  df-topn 17305  df-0g 17323  df-gsum 17324  df-topgen 17325  df-pt 17326  df-prds 17329  df-xrs 17384  df-qtop 17389  df-imas 17390  df-xps 17392  df-mre 17466  df-mrc 17467  df-acs 17469  df-mgm 18497  df-sgrp 18546  df-mnd 18557  df-submnd 18602  df-mulg 18873  df-cntz 19097  df-cmn 19564  df-psmet 20788  df-xmet 20789  df-met 20790  df-bl 20791  df-mopn 20792  df-cnfld 20797  df-top 22243  df-topon 22260  df-topsp 22282  df-bases 22296  df-cld 22370  df-ntr 22371  df-cn 22578  df-cnp 22579  df-t1 22665  df-haus 22666  df-tx 22913  df-hmeo 23106  df-xms 23673  df-ms 23674  df-tms 23675  df-cncf 24241  df-ulm 25736

This theorem is referenced by:  abelth2  25801