abelth - Metamath Proof Explorer

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

Theorem abelth 25945

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 25930.) (Contributed by Mario Carneiro, 2-Apr-2015.) (Revised by Mario Carneiro, 8-Sep-2015.)

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

**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 ⊢ (𝜑 → 𝐴:ℕ₀⟶ℂ)
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 ⊢ 𝐹 = (𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)))
7	1, 2, 3, 4, 5, 6	abelthlem4 25938	. . 3 ⊢ (𝜑 → 𝐹:𝑆⟶ℂ)
8	1, 2, 3, 4, 5, 6	abelthlem9 25944	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))
9	1, 2, 3, 4, 5	abelthlem2 25936	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (1 ∈ 𝑆 ∧ (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1)))
10	9	simpld 496	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 1 ∈ 𝑆)
11	10	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → 1 ∈ 𝑆)
12		simpr 486	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆)
13	11, 12	ovresd 7571	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (1(abs ∘ − )𝑦))
14		ax-1cn 11165	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ ℂ
15	5	ssrab3 4080	. . . . . . . . . . . . . . . . 17 ⊢ 𝑆 ⊆ ℂ
16	15, 12	sselid 3980	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ ℂ)
17		eqid 2733	. . . . . . . . . . . . . . . . 17 ⊢ (abs ∘ − ) = (abs ∘ − )
18	17	cnmetdval 24279	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
19	14, 16, 18	sylancr 588	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (1(abs ∘ − )𝑦) = (abs‘(1 − 𝑦)))
20	13, 19	eqtrd 2773	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) = (abs‘(1 − 𝑦)))
21	20	breq1d 5158	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 ↔ (abs‘(1 − 𝑦)) < 𝑤))
22	7	ad2antrr 725	. . . . . . . . . . . . . . . 16 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → 𝐹:𝑆⟶ℂ)
23	22, 11	ffvelcdmd 7085	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (𝐹‘1) ∈ ℂ)
24	7	adantr 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ⁺) → 𝐹:𝑆⟶ℂ)
25	24	ffvelcdmda 7084	. . . . . . . . . . . . . . 15 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (𝐹‘𝑦) ∈ ℂ)
26	17	cnmetdval 24279	. . . . . . . . . . . . . . 15 ⊢ (((𝐹‘1) ∈ ℂ ∧ (𝐹‘𝑦) ∈ ℂ) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦))))
27	23, 25, 26	syl2anc 585	. . . . . . . . . . . . . 14 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) = (abs‘((𝐹‘1) − (𝐹‘𝑦))))
28	27	breq1d 5158	. . . . . . . . . . . . 13 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟 ↔ (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟))
29	21, 28	imbi12d 345	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑟 ∈ ℝ⁺) ∧ 𝑦 ∈ 𝑆) → (((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)))
30	29	ralbidva 3176	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ⁺) → (∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)))
31	30	rexbidv 3179	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ⁺) → (∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟) ↔ ∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((abs‘(1 − 𝑦)) < 𝑤 → (abs‘((𝐹‘1) − (𝐹‘𝑦))) < 𝑟)))
32	8, 31	mpbird 257	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ℝ⁺) → ∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))
33	32	ralrimiva 3147	. . . . . . . 8 ⊢ (𝜑 → ∀𝑟 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))
34		cnxmet 24281	. . . . . . . . . 10 ⊢ (abs ∘ − ) ∈ (∞Met‘ℂ)
35		xmetres2 23859	. . . . . . . . . 10 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆))
36	34, 15, 35	mp2an 691	. . . . . . . . 9 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆)
37		eqid 2733	. . . . . . . . . . . 12 ⊢ ((abs ∘ − ) ↾ (𝑆 × 𝑆)) = ((abs ∘ − ) ↾ (𝑆 × 𝑆))
38		eqid 2733	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = (TopOpen‘ℂ_fld)
39	38	cnfldtopn 24290	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) = (MetOpen‘(abs ∘ − ))
40		eqid 2733	. . . . . . . . . . . 12 ⊢ (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
41	37, 39, 40	metrest 24025	. . . . . . . . . . 11 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆))))
42	34, 15, 41	mp2an 691	. . . . . . . . . 10 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = (MetOpen‘((abs ∘ − ) ↾ (𝑆 × 𝑆)))
43	42, 39	metcnp 24042	. . . . . . . . 9 ⊢ ((((abs ∘ − ) ↾ (𝑆 × 𝑆)) ∈ (∞Met‘𝑆) ∧ (abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 1 ∈ 𝑆) → (𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))))
44	36, 34, 10, 43	mp3an12i 1466	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘1) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑟 ∈ ℝ⁺ ∃𝑤 ∈ ℝ⁺ ∀𝑦 ∈ 𝑆 ((1((abs ∘ − ) ↾ (𝑆 × 𝑆))𝑦) < 𝑤 → ((𝐹‘1)(abs ∘ − )(𝐹‘𝑦)) < 𝑟))))
45	7, 33, 44	mpbir2and 712	. . . . . . 7 ⊢ (𝜑 → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘1))
46	45	ad2antrr 725	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘1))
47		simpr 486	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝑦 = 1)
48	47	fveq2d 6893	. . . . . 6 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘1))
49	46, 48	eleqtrrd 2837	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 = 1) → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦))
50		eldifsn 4790	. . . . . . 7 ⊢ (𝑦 ∈ (𝑆 ∖ {1}) ↔ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1))
51	9	simprd 497	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (0(ball‘(abs ∘ − ))1))
52		abscl 15222	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (abs‘𝑤) ∈ ℝ)
53	52	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ)
54	53	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) ∈ ℝ))
55		absge0 15231	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → 0 ≤ (abs‘𝑤))
56	55	adantl 483	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 0 ≤ (abs‘𝑤))
57	56	a1d 25	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → 0 ≤ (abs‘𝑤)))
58	1, 2	abelthlem1 25935	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝜑 → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))
59	58	adantr 482	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))
60	53	rexrd 11261	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (abs‘𝑤) ∈ ℝ^*)
61		1re 11211	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 1 ∈ ℝ
62		rexr 11257	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (1 ∈ ℝ → 1 ∈ ℝ^*)
63	61, 62	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → 1 ∈ ℝ^*)
64		iccssxr 13404	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (0[,]+∞) ⊆ ℝ^*
65		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛)))) = (𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))
66		eqid 2733	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) = sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )
67	65, 1, 66	radcnvcl 25921	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ) ∈ (0[,]+∞))
68	64, 67	sselid 3980	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝜑 → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) ∈ ℝ^)
69	68	adantr 482	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) ∈ ℝ^)
70		xrltletr 13133	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((abs‘𝑤) ∈ ℝ^* ∧ 1 ∈ ℝ^* ∧ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) ∈ ℝ^) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )))
71	60, 63, 69, 70	syl3anc 1372	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → (((abs‘𝑤) < 1 ∧ 1 ≤ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )) → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )))
72	59, 71	mpan2d 693	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )))
73	54, 57, 72	3jcad 1130	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) < 1 → ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))))
74		0cn 11203	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 0 ∈ ℂ
75	17	cnmetdval 24279	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
76	74, 75	mpan 689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘(0 − 𝑤)))
77		abssub 15270	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((0 ∈ ℂ ∧ 𝑤 ∈ ℂ) → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
78	74, 77	mpan 689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (abs‘(0 − 𝑤)) = (abs‘(𝑤 − 0)))
79		subid1 11477	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑤 ∈ ℂ → (𝑤 − 0) = 𝑤)
80	79	fveq2d 6893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑤 ∈ ℂ → (abs‘(𝑤 − 0)) = (abs‘𝑤))
81	76, 78, 80	3eqtrd 2777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑤 ∈ ℂ → (0(abs ∘ − )𝑤) = (abs‘𝑤))
82	81	breq1d 5158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑤 ∈ ℂ → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
83	82	adantl 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 ↔ (abs‘𝑤) < 1))
84		0re 11213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 0 ∈ ℝ
85		elico2 13385	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((0 ∈ ℝ ∧ sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) ∈ ℝ^) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))))
86	84, 69, 85	sylancr 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )) ↔ ((abs‘𝑤) ∈ ℝ ∧ 0 ≤ (abs‘𝑤) ∧ (abs‘𝑤) < sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))))
87	73, 83, 86	3imtr4d 294	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝜑 ∧ 𝑤 ∈ ℂ) → ((0(abs ∘ − )𝑤) < 1 → (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))))
88	87	imdistanda 573	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → ((𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1) → (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )))))
89		1xr 11270	. . . . . . . . . . . . . . . . . . 19 ⊢ 1 ∈ ℝ^*
90		elbl 23886	. . . . . . . . . . . . . . . . . . 19 ⊢ (((abs ∘ − ) ∈ (∞Met‘ℂ) ∧ 0 ∈ ℂ ∧ 1 ∈ ℝ^*) → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1)))
91	34, 74, 89, 90	mp3an 1462	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (0(ball‘(abs ∘ − ))1) ↔ (𝑤 ∈ ℂ ∧ (0(abs ∘ − )𝑤) < 1))
92		absf 15281	. . . . . . . . . . . . . . . . . . 19 ⊢ abs:ℂ⟶ℝ
93		ffn 6715	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs:ℂ⟶ℝ → abs Fn ℂ)
94		elpreima 7057	. . . . . . . . . . . . . . . . . . 19 ⊢ (abs Fn ℂ → (𝑤 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↔ (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )))))
95	92, 93, 94	mp2b 10	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑤 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↔ (𝑤 ∈ ℂ ∧ (abs‘𝑤) ∈ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))))
96	88, 91, 95	3imtr4g 296	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝑤 ∈ (0(ball‘(abs ∘ − ))1) → 𝑤 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < )))))
97	96	ssrdv 3988	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (0(ball‘(abs ∘ − ))1) ⊆ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))))
98	51, 97	sstrd 3992	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝑆 ∖ {1}) ⊆ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))))
99	98	resmptd 6039	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))))
100	6	reseq1i 5976	. . . . . . . . . . . . . . 15 ⊢ (𝐹 ↾ (𝑆 ∖ {1})) = ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1}))
101		difss 4131	. . . . . . . . . . . . . . . 16 ⊢ (𝑆 ∖ {1}) ⊆ 𝑆
102		resmpt 6036	. . . . . . . . . . . . . . . 16 ⊢ ((𝑆 ∖ {1}) ⊆ 𝑆 → ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))))
103	101, 102	ax-mp 5	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 ∈ 𝑆 ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)))
104	100, 103	eqtri 2761	. . . . . . . . . . . . . 14 ⊢ (𝐹 ↾ (𝑆 ∖ {1})) = (𝑥 ∈ (𝑆 ∖ {1}) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)))
105	99, 104	eqtr4di 2791	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) = (𝐹 ↾ (𝑆 ∖ {1})))
106		cnvimass 6078	. . . . . . . . . . . . . . . . . . 19 ⊢ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) ⊆ dom abs
107	92	fdmi 6727	. . . . . . . . . . . . . . . . . . 19 ⊢ dom abs = ℂ
108	106, 107	sseqtri 4018	. . . . . . . . . . . . . . . . . 18 ⊢ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) ⊆ ℂ
109	108	sseli 3978	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) → 𝑥 ∈ ℂ)
110		fveq2 6889	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → (𝐴‘𝑛) = (𝐴‘𝑗))
111		oveq2 7414	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑛 = 𝑗 → (𝑥↑𝑛) = (𝑥↑𝑗))
112	110, 111	oveq12d 7424	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑛 = 𝑗 → ((𝐴‘𝑛) · (𝑥↑𝑛)) = ((𝐴‘𝑗) · (𝑥↑𝑗)))
113	112	cbvsumv 15639	. . . . . . . . . . . . . . . . . 18 ⊢ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ₀ ((𝐴‘𝑗) · (𝑥↑𝑗))
114	65	pserval2 25915	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑥 ∈ ℂ ∧ 𝑗 ∈ ℕ₀) → (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = ((𝐴‘𝑗) · (𝑥↑𝑗)))
115	114	sumeq2dv 15646	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℂ → Σ𝑗 ∈ ℕ₀ (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗) = Σ𝑗 ∈ ℕ₀ ((𝐴‘𝑗) · (𝑥↑𝑗)))
116	113, 115	eqtr4id 2792	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ₀ (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗))
117	109, 116	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) → Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛)) = Σ𝑗 ∈ ℕ₀ (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗))
118	117	mpteq2ia 5251	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) = (𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↦ Σ𝑗 ∈ ℕ₀ (((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑥)‘𝑗))
119		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) = (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )))
120		eqid 2733	. . . . . . . . . . . . . . 15 ⊢ if(sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) ∈ ℝ, (((abs‘𝑣) + sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )) / 2), ((abs‘𝑣) + 1)) = if(sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ) ∈ ℝ, (((abs‘𝑣) + sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )) / 2), ((abs‘𝑣) + 1))
121	65, 118, 1, 66, 119, 120	psercn 25930	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ ((^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )))–cn→ℂ))
122		rescncf 24405	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ∖ {1}) ⊆ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) → ((𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ∈ ((^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < )))–cn→ℂ) → ((𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ)))
123	98, 121, 122	sylc 65	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝑥 ∈ (^◡abs “ (0[,)sup({𝑟 ∈ ℝ ∣ seq0( + , ((𝑡 ∈ ℂ ↦ (𝑛 ∈ ℕ₀ ↦ ((𝐴‘𝑛) · (𝑡↑𝑛))))‘𝑟)) ∈ dom ⇝ }, ℝ^*, < ))) ↦ Σ𝑛 ∈ ℕ₀ ((𝐴‘𝑛) · (𝑥↑𝑛))) ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
124	105, 123	eqeltrrd 2835	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
125	124	adantr 482	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((𝑆 ∖ {1})–cn→ℂ))
126	101, 15	sstri 3991	. . . . . . . . . . . 12 ⊢ (𝑆 ∖ {1}) ⊆ ℂ
127		ssid 4004	. . . . . . . . . . . 12 ⊢ ℂ ⊆ ℂ
128		eqid 2733	. . . . . . . . . . . . 13 ⊢ ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) = ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1}))
129	38	cnfldtopon 24291	. . . . . . . . . . . . . 14 ⊢ (TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ)
130	129	toponrestid 22415	. . . . . . . . . . . . 13 ⊢ (TopOpen‘ℂ_fld) = ((TopOpen‘ℂ_fld) ↾_t ℂ)
131	38, 128, 130	cncfcn 24418	. . . . . . . . . . . 12 ⊢ (((𝑆 ∖ {1}) ⊆ ℂ ∧ ℂ ⊆ ℂ) → ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) Cn (TopOpen‘ℂ_fld)))
132	126, 127, 131	mp2an 691	. . . . . . . . . . 11 ⊢ ((𝑆 ∖ {1})–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) Cn (TopOpen‘ℂ_fld))
133	125, 132	eleqtrdi 2844	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) Cn (TopOpen‘ℂ_fld)))
134		simpr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ (𝑆 ∖ {1}))
135		resttopon 22657	. . . . . . . . . . . . 13 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ (𝑆 ∖ {1}) ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1})))
136	129, 126, 135	mp2an 691	. . . . . . . . . . . 12 ⊢ ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) ∈ (TopOn‘(𝑆 ∖ {1}))
137	136	toponunii 22410	. . . . . . . . . . 11 ⊢ (𝑆 ∖ {1}) = ∪ ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1}))
138	137	cncnpi 22774	. . . . . . . . . 10 ⊢ (((𝐹 ↾ (𝑆 ∖ {1})) ∈ (((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) Cn (TopOpen‘ℂ_fld)) ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))‘𝑦))
139	133, 134, 138	syl2anc 585	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ ((((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))‘𝑦))
140	38	cnfldtop 24292	. . . . . . . . . . . 12 ⊢ (TopOpen‘ℂ_fld) ∈ Top
141		cnex 11188	. . . . . . . . . . . . 13 ⊢ ℂ ∈ V
142	141, 15	ssexi 5322	. . . . . . . . . . . 12 ⊢ 𝑆 ∈ V
143		restabs 22661	. . . . . . . . . . . 12 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆 ∧ 𝑆 ∈ V) → (((TopOpen‘ℂ_fld) ↾_t 𝑆) ↾_t (𝑆 ∖ {1})) = ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})))
144	140, 101, 142, 143	mp3an 1462	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂ_fld) ↾_t 𝑆) ↾_t (𝑆 ∖ {1})) = ((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1}))
145	144	oveq1i 7416	. . . . . . . . . 10 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld)) = (((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))
146	145	fveq1i 6890	. . . . . . . . 9 ⊢ (((((TopOpen‘ℂ_fld) ↾_t 𝑆) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))‘𝑦) = ((((TopOpen‘ℂ_fld) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))‘𝑦)
147	139, 146	eleqtrrdi 2845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂ_fld) ↾_t 𝑆) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))‘𝑦))
148		resttop 22656	. . . . . . . . . . 11 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝑆 ∈ V) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top)
149	140, 142, 148	mp2an 691	. . . . . . . . . 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 4812	. . . . . . . . . . . . 13 ⊢ (𝜑 → {1} ⊆ 𝑆)
153	38	cnfldhaus 24293	. . . . . . . . . . . . . . 15 ⊢ (TopOpen‘ℂ_fld) ∈ Haus
154		unicntop 24294	. . . . . . . . . . . . . . . 16 ⊢ ℂ = ∪ (TopOpen‘ℂ_fld)
155	154	sncld 22867	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂ_fld) ∈ Haus ∧ 1 ∈ ℂ) → {1} ∈ (Clsd‘(TopOpen‘ℂ_fld)))
156	153, 14, 155	mp2an 691	. . . . . . . . . . . . . 14 ⊢ {1} ∈ (Clsd‘(TopOpen‘ℂ_fld))
157	154	restcldi 22669	. . . . . . . . . . . . . 14 ⊢ ((𝑆 ⊆ ℂ ∧ {1} ∈ (Clsd‘(TopOpen‘ℂ_fld)) ∧ {1} ⊆ 𝑆) → {1} ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t 𝑆)))
158	15, 156, 157	mp3an12 1452	. . . . . . . . . . . . 13 ⊢ ({1} ⊆ 𝑆 → {1} ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t 𝑆)))
159	154	restuni 22658	. . . . . . . . . . . . . . 15 ⊢ (((TopOpen‘ℂ_fld) ∈ Top ∧ 𝑆 ⊆ ℂ) → 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
160	140, 15, 159	mp2an 691	. . . . . . . . . . . . . 14 ⊢ 𝑆 = ∪ ((TopOpen‘ℂ_fld) ↾_t 𝑆)
161	160	cldopn 22527	. . . . . . . . . . . . 13 ⊢ ({1} ∈ (Clsd‘((TopOpen‘ℂ_fld) ↾_t 𝑆)) → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
162	152, 158, 161	3syl 18	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆 ∖ {1}) ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆))
163	160	isopn3 22562	. . . . . . . . . . . . 13 ⊢ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ Top ∧ (𝑆 ∖ {1}) ⊆ 𝑆) → ((𝑆 ∖ {1}) ∈ ((TopOpen‘ℂ_fld) ↾_t 𝑆) ↔ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘(𝑆 ∖ {1})) = (𝑆 ∖ {1})))
164	149, 101, 163	mp2an 691	. . . . . . . . . . . 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 2820	. . . . . . . . . 10 ⊢ (𝜑 → (𝑦 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘(𝑆 ∖ {1})) ↔ 𝑦 ∈ (𝑆 ∖ {1})))
167	166	biimpar 479	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝑦 ∈ ((int‘((TopOpen‘ℂ_fld) ↾_t 𝑆))‘(𝑆 ∖ {1})))
168	7	adantr 482	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹:𝑆⟶ℂ)
169	160, 154	cnprest 22785	. . . . . . . . 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 838	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → (𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦) ↔ (𝐹 ↾ (𝑆 ∖ {1})) ∈ (((((TopOpen‘ℂ_fld) ↾_t 𝑆) ↾_t (𝑆 ∖ {1})) CnP (TopOpen‘ℂ_fld))‘𝑦)))
171	147, 170	mpbird 257	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑦 ∈ (𝑆 ∖ {1})) → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦))
172	50, 171	sylan2br 596	. . . . . 6 ⊢ ((𝜑 ∧ (𝑦 ∈ 𝑆 ∧ 𝑦 ≠ 1)) → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦))
173	172	anassrs 469	. . . . 5 ⊢ (((𝜑 ∧ 𝑦 ∈ 𝑆) ∧ 𝑦 ≠ 1) → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦))
174	49, 173	pm2.61dane 3030	. . . 4 ⊢ ((𝜑 ∧ 𝑦 ∈ 𝑆) → 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦))
175	174	ralrimiva 3147	. . 3 ⊢ (𝜑 → ∀𝑦 ∈ 𝑆 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦))
176		resttopon 22657	. . . . 5 ⊢ (((TopOpen‘ℂ_fld) ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆))
177	129, 15, 176	mp2an 691	. . . 4 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) ∈ (TopOn‘𝑆)
178		cncnp 22776	. . . 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 691	. . 3 ⊢ (𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn (TopOpen‘ℂ_fld)) ↔ (𝐹:𝑆⟶ℂ ∧ ∀𝑦 ∈ 𝑆 𝐹 ∈ ((((TopOpen‘ℂ_fld) ↾_t 𝑆) CnP (TopOpen‘ℂ_fld))‘𝑦)))
180	7, 175, 179	sylanbrc 584	. 2 ⊢ (𝜑 → 𝐹 ∈ (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn (TopOpen‘ℂ_fld)))
181		eqid 2733	. . . 4 ⊢ ((TopOpen‘ℂ_fld) ↾_t 𝑆) = ((TopOpen‘ℂ_fld) ↾_t 𝑆)
182	38, 181, 130	cncfcn 24418	. . 3 ⊢ ((𝑆 ⊆ ℂ ∧ ℂ ⊆ ℂ) → (𝑆–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn (TopOpen‘ℂ_fld)))
183	15, 127, 182	mp2an 691	. 2 ⊢ (𝑆–cn→ℂ) = (((TopOpen‘ℂ_fld) ↾_t 𝑆) Cn (TopOpen‘ℂ_fld))
184	180, 183	eleqtrrdi 2845	1 ⊢ (𝜑 → 𝐹 ∈ (𝑆–cn→ℂ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ≠ wne 2941 ∀wral 3062 ∃wrex 3071 {crab 3433 Vcvv 3475 ∖ cdif 3945 ⊆ wss 3948 ifcif 4528 {csn 4628 ∪ cuni 4908 class class class wbr 5148 ↦ cmpt 5231 × cxp 5674 ^◡ccnv 5675 dom cdm 5676 ↾ cres 5678 “ cima 5679 ∘ ccom 5680 Fn wfn 6536 ⟶wf 6537 ‘cfv 6541 (class class class)co 7406 supcsup 9432 ℂcc 11105 ℝcr 11106 0cc0 11107 1c1 11108 + caddc 11110 · cmul 11112 +∞cpnf 11242 ℝ^*cxr 11244 < clt 11245 ≤ cle 11246 − cmin 11441 / cdiv 11868 2c2 12264 ℕ₀cn0 12469 ℝ⁺crp 12971 [,)cico 13323 [,]cicc 13324 seqcseq 13963 ↑cexp 14024 abscabs 15178 ⇝ cli 15425 Σcsu 15629 ↾_t crest 17363 TopOpenctopn 17364 ∞Metcxmet 20922 ballcbl 20924 MetOpencmopn 20927 ℂ_fldccnfld 20937 Topctop 22387 TopOnctopon 22404 Clsdccld 22512 intcnt 22513 Cn ccn 22720 CnP ccnp 22721 Hauscha 22804 –cn→ccncf 24384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7722 ax-inf2 9633 ax-cnex 11163 ax-resscn 11164 ax-1cn 11165 ax-icn 11166 ax-addcl 11167 ax-addrcl 11168 ax-mulcl 11169 ax-mulrcl 11170 ax-mulcom 11171 ax-addass 11172 ax-mulass 11173 ax-distr 11174 ax-i2m1 11175 ax-1ne0 11176 ax-1rid 11177 ax-rnegex 11178 ax-rrecex 11179 ax-cnre 11180 ax-pre-lttri 11181 ax-pre-lttrn 11182 ax-pre-ltadd 11183 ax-pre-mulgt0 11184 ax-pre-sup 11185 ax-addf 11186 ax-mulf 11187

This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3or 1089 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3377 df-reu 3378 df-rab 3434 df-v 3477 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-tp 4633 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-iin 5000 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-se 5632 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-pred 6298 df-ord 6365 df-on 6366 df-lim 6367 df-suc 6368 df-iota 6493 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-isom 6550 df-riota 7362 df-ov 7409 df-oprab 7410 df-mpo 7411 df-of 7667 df-om 7853 df-1st 7972 df-2nd 7973 df-supp 8144 df-frecs 8263 df-wrecs 8294 df-recs 8368 df-rdg 8407 df-1o 8463 df-2o 8464 df-er 8700 df-map 8819 df-pm 8820 df-ixp 8889 df-en 8937 df-dom 8938 df-sdom 8939 df-fin 8940 df-fsupp 9359 df-fi 9403 df-sup 9434 df-inf 9435 df-oi 9502 df-card 9931 df-pnf 11247 df-mnf 11248 df-xr 11249 df-ltxr 11250 df-le 11251 df-sub 11443 df-neg 11444 df-div 11869 df-nn 12210 df-2 12272 df-3 12273 df-4 12274 df-5 12275 df-6 12276 df-7 12277 df-8 12278 df-9 12279 df-n0 12470 df-z 12556 df-dec 12675 df-uz 12820 df-q 12930 df-rp 12972 df-xneg 13089 df-xadd 13090 df-xmul 13091 df-ico 13327 df-icc 13328 df-fz 13482 df-fzo 13625 df-fl 13754 df-seq 13964 df-exp 14025 df-hash 14288 df-shft 15011 df-cj 15043 df-re 15044 df-im 15045 df-sqrt 15179 df-abs 15180 df-limsup 15412 df-clim 15429 df-rlim 15430 df-sum 15630 df-struct 17077 df-sets 17094 df-slot 17112 df-ndx 17124 df-base 17142 df-ress 17171 df-plusg 17207 df-mulr 17208 df-starv 17209 df-sca 17210 df-vsca 17211 df-ip 17212 df-tset 17213 df-ple 17214 df-ds 17216 df-unif 17217 df-hom 17218 df-cco 17219 df-rest 17365 df-topn 17366 df-0g 17384 df-gsum 17385 df-topgen 17386 df-pt 17387 df-prds 17390 df-xrs 17445 df-qtop 17450 df-imas 17451 df-xps 17453 df-mre 17527 df-mrc 17528 df-acs 17530 df-mgm 18558 df-sgrp 18607 df-mnd 18623 df-submnd 18669 df-mulg 18946 df-cntz 19176 df-cmn 19645 df-psmet 20929 df-xmet 20930 df-met 20931 df-bl 20932 df-mopn 20933 df-cnfld 20938 df-top 22388 df-topon 22405 df-topsp 22427 df-bases 22441 df-cld 22515 df-ntr 22516 df-cn 22723 df-cnp 22724 df-t1 22810 df-haus 22811 df-tx 23058 df-hmeo 23251 df-xms 23818 df-ms 23819 df-tms 23820 df-cncf 24386 df-ulm 25881

This theorem is referenced by: abelth2 25946

W3C validator