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	$⊢ φ \to A : ℕ_{0} ⟶ ℂ$
	abelth.2	$⊢ φ \to seq 0 (+ A) \in dom ⇝$
	abelth.3	$⊢ φ \to M \in ℝ$
	abelth.4	$⊢ φ \to 0 \leq M$
	abelth.5	$⊢ S = \{z \in ℂ \| \|1 - z\| \leq M (1 - \|z\|)\}$
	abelth.6	$⊢ F = (x \in S ⟼ \sum_{n \in ℕ_{0}} A (n) x^{n})$
Assertion	abelth	$⊢ φ \to F : S \underset{cn}{⟶} ℂ$

Proof

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

Metamath Proof Explorer

Theorem abelth

Proof