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 φ A : 0
abelth.2 φ seq 0 + A dom
abelth.3 φ M
abelth.4 φ 0 M
abelth.5 S = z | 1 z M 1 z
abelth.6 F = x S n 0 A n x n
Assertion abelth φ F : S cn

Proof

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