Metamath Proof Explorer


Theorem efrlim

Description: The limit of the sequence ( 1 + A / k ) ^ k is the exponential function. This is often taken as an alternate definition of the exponential function (see also dfef2 ). (Contributed by Mario Carneiro, 1-Mar-2015)

Ref Expression
Hypothesis efrlim.1 S = 0 ball abs 1 A + 1
Assertion efrlim A k + 1 + A k k e A

Proof

Step Hyp Ref Expression
1 efrlim.1 S = 0 ball abs 1 A + 1
2 rge0ssre 0 +∞
3 ax-resscn
4 2 3 sstri 0 +∞
5 4 sseli x 0 +∞ x
6 simpll A x ¬ x = 0 A
7 1cnd A x ¬ x = 0 1
8 simplr A x ¬ x = 0 x
9 ax-1ne0 1 0
10 9 a1i A x ¬ x = 0 1 0
11 simpr A x ¬ x = 0 ¬ x = 0
12 11 neqned A x ¬ x = 0 x 0
13 6 7 8 10 12 divdiv2d A x ¬ x = 0 A 1 x = A x 1
14 mulcl A x A x
15 14 adantr A x ¬ x = 0 A x
16 15 div1d A x ¬ x = 0 A x 1 = A x
17 13 16 eqtrd A x ¬ x = 0 A 1 x = A x
18 17 oveq2d A x ¬ x = 0 1 + A 1 x = 1 + A x
19 18 oveq1d A x ¬ x = 0 1 + A 1 x 1 x = 1 + A x 1 x
20 19 ifeq2da A x if x = 0 e A 1 + A 1 x 1 x = if x = 0 e A 1 + A x 1 x
21 5 20 sylan2 A x 0 +∞ if x = 0 e A 1 + A 1 x 1 x = if x = 0 e A 1 + A x 1 x
22 21 mpteq2dva A x 0 +∞ if x = 0 e A 1 + A 1 x 1 x = x 0 +∞ if x = 0 e A 1 + A x 1 x
23 resmpt 0 +∞ x if x = 0 e A 1 + A x 1 x 0 +∞ = x 0 +∞ if x = 0 e A 1 + A x 1 x
24 4 23 ax-mp x if x = 0 e A 1 + A x 1 x 0 +∞ = x 0 +∞ if x = 0 e A 1 + A x 1 x
25 22 24 eqtr4di A x 0 +∞ if x = 0 e A 1 + A 1 x 1 x = x if x = 0 e A 1 + A x 1 x 0 +∞
26 0e0icopnf 0 0 +∞
27 26 a1i A 0 0 +∞
28 eqeq2 e A 1 = if A x = 0 e A 1 e A log 1 + A x A x if x = 0 e A 1 + A x 1 x = e A 1 if x = 0 e A 1 + A x 1 x = if A x = 0 e A 1 e A log 1 + A x A x
29 eqeq2 e A log 1 + A x A x = if A x = 0 e A 1 e A log 1 + A x A x if x = 0 e A 1 + A x 1 x = e A log 1 + A x A x if x = 0 e A 1 + A x 1 x = if A x = 0 e A 1 e A log 1 + A x A x
30 cnxmet abs ∞Met
31 0cnd A 0
32 abscl A A
33 peano2re A A + 1
34 32 33 syl A A + 1
35 0red A 0
36 absge0 A 0 A
37 32 ltp1d A A < A + 1
38 35 32 34 36 37 lelttrd A 0 < A + 1
39 34 38 elrpd A A + 1 +
40 39 rpreccld A 1 A + 1 +
41 40 rpxrd A 1 A + 1 *
42 blssm abs ∞Met 0 1 A + 1 * 0 ball abs 1 A + 1
43 30 31 41 42 mp3an2i A 0 ball abs 1 A + 1
44 1 43 eqsstrid A S
45 44 sselda A x S x
46 mul0or A x A x = 0 A = 0 x = 0
47 45 46 syldan A x S A x = 0 A = 0 x = 0
48 47 biimpa A x S A x = 0 A = 0 x = 0
49 8 12 reccld A x ¬ x = 0 1 x
50 45 49 syldanl A x S ¬ x = 0 1 x
51 50 adantlr A x S A = 0 ¬ x = 0 1 x
52 51 1cxpd A x S A = 0 ¬ x = 0 1 1 x = 1
53 simplr A x S A = 0 ¬ x = 0 A = 0
54 53 oveq1d A x S A = 0 ¬ x = 0 A x = 0 x
55 45 ad2antrr A x S A = 0 ¬ x = 0 x
56 55 mul02d A x S A = 0 ¬ x = 0 0 x = 0
57 54 56 eqtrd A x S A = 0 ¬ x = 0 A x = 0
58 57 oveq2d A x S A = 0 ¬ x = 0 1 + A x = 1 + 0
59 1p0e1 1 + 0 = 1
60 58 59 eqtrdi A x S A = 0 ¬ x = 0 1 + A x = 1
61 60 oveq1d A x S A = 0 ¬ x = 0 1 + A x 1 x = 1 1 x
62 53 fveq2d A x S A = 0 ¬ x = 0 e A = e 0
63 ef0 e 0 = 1
64 62 63 eqtrdi A x S A = 0 ¬ x = 0 e A = 1
65 52 61 64 3eqtr4d A x S A = 0 ¬ x = 0 1 + A x 1 x = e A
66 65 ifeq2da A x S A = 0 if x = 0 e A 1 + A x 1 x = if x = 0 e A e A
67 ifid if x = 0 e A e A = e A
68 66 67 eqtrdi A x S A = 0 if x = 0 e A 1 + A x 1 x = e A
69 iftrue x = 0 if x = 0 e A 1 + A x 1 x = e A
70 69 adantl A x S x = 0 if x = 0 e A 1 + A x 1 x = e A
71 68 70 jaodan A x S A = 0 x = 0 if x = 0 e A 1 + A x 1 x = e A
72 mulid1 A A 1 = A
73 72 ad2antrr A x S A = 0 x = 0 A 1 = A
74 73 fveq2d A x S A = 0 x = 0 e A 1 = e A
75 71 74 eqtr4d A x S A = 0 x = 0 if x = 0 e A 1 + A x 1 x = e A 1
76 48 75 syldan A x S A x = 0 if x = 0 e A 1 + A x 1 x = e A 1
77 mulne0b A x A 0 x 0 A x 0
78 45 77 syldan A x S A 0 x 0 A x 0
79 df-ne A x 0 ¬ A x = 0
80 78 79 bitrdi A x S A 0 x 0 ¬ A x = 0
81 simprr A x S A 0 x 0 x 0
82 81 neneqd A x S A 0 x 0 ¬ x = 0
83 82 iffalsed A x S A 0 x 0 if x = 0 e A 1 + A x 1 x = 1 + A x 1 x
84 ax-1cn 1
85 45 14 syldan A x S A x
86 addcl 1 A x 1 + A x
87 84 85 86 sylancr A x S 1 + A x
88 87 adantr A x S A 0 x 0 1 + A x
89 eqid 1 ball abs 1 = 1 ball abs 1
90 89 dvlog2lem 1 ball abs 1 −∞ 0
91 eqid −∞ 0 = −∞ 0
92 91 logdmss −∞ 0 0
93 90 92 sstri 1 ball abs 1 0
94 eqid abs = abs
95 94 cnmetdval 1 + A x 1 1 + A x abs 1 = 1 + A x - 1
96 87 84 95 sylancl A x S 1 + A x abs 1 = 1 + A x - 1
97 pncan2 1 A x 1 + A x - 1 = A x
98 84 85 97 sylancr A x S 1 + A x - 1 = A x
99 98 fveq2d A x S 1 + A x - 1 = A x
100 96 99 eqtrd A x S 1 + A x abs 1 = A x
101 85 abscld A x S A x
102 34 adantr A x S A + 1
103 45 abscld A x S x
104 102 103 remulcld A x S A + 1 x
105 1red A x S 1
106 absmul A x A x = A x
107 45 106 syldan A x S A x = A x
108 32 adantr A x S A
109 108 33 syl A x S A + 1
110 45 absge0d A x S 0 x
111 108 lep1d A x S A A + 1
112 108 109 103 110 111 lemul1ad A x S A x A + 1 x
113 107 112 eqbrtrd A x S A x A + 1 x
114 0cn 0
115 94 cnmetdval x 0 x abs 0 = x 0
116 45 114 115 sylancl A x S x abs 0 = x 0
117 45 subid1d A x S x 0 = x
118 117 fveq2d A x S x 0 = x
119 116 118 eqtrd A x S x abs 0 = x
120 simpr A x S x S
121 120 1 eleqtrdi A x S x 0 ball abs 1 A + 1
122 30 a1i A x S abs ∞Met
123 41 adantr A x S 1 A + 1 *
124 0cnd A x S 0
125 elbl3 abs ∞Met 1 A + 1 * 0 x x 0 ball abs 1 A + 1 x abs 0 < 1 A + 1
126 122 123 124 45 125 syl22anc A x S x 0 ball abs 1 A + 1 x abs 0 < 1 A + 1
127 121 126 mpbid A x S x abs 0 < 1 A + 1
128 119 127 eqbrtrrd A x S x < 1 A + 1
129 38 adantr A x S 0 < A + 1
130 ltmuldiv2 x 1 A + 1 0 < A + 1 A + 1 x < 1 x < 1 A + 1
131 103 105 109 129 130 syl112anc A x S A + 1 x < 1 x < 1 A + 1
132 128 131 mpbird A x S A + 1 x < 1
133 101 104 105 113 132 lelttrd A x S A x < 1
134 100 133 eqbrtrd A x S 1 + A x abs 1 < 1
135 1rp 1 +
136 rpxr 1 + 1 *
137 135 136 mp1i A x S 1 *
138 1cnd A x S 1
139 elbl3 abs ∞Met 1 * 1 1 + A x 1 + A x 1 ball abs 1 1 + A x abs 1 < 1
140 122 137 138 87 139 syl22anc A x S 1 + A x 1 ball abs 1 1 + A x abs 1 < 1
141 134 140 mpbird A x S 1 + A x 1 ball abs 1
142 93 141 sselid A x S 1 + A x 0
143 eldifsni 1 + A x 0 1 + A x 0
144 142 143 syl A x S 1 + A x 0
145 144 adantr A x S A 0 x 0 1 + A x 0
146 45 adantr A x S A 0 x 0 x
147 146 81 reccld A x S A 0 x 0 1 x
148 88 145 147 cxpefd A x S A 0 x 0 1 + A x 1 x = e 1 x log 1 + A x
149 87 144 logcld A x S log 1 + A x
150 149 adantr A x S A 0 x 0 log 1 + A x
151 147 150 mulcomd A x S A 0 x 0 1 x log 1 + A x = log 1 + A x 1 x
152 simpll A x S A 0 x 0 A
153 simprl A x S A 0 x 0 A 0
154 152 153 dividd A x S A 0 x 0 A A = 1
155 154 oveq1d A x S A 0 x 0 A A x = 1 x
156 152 152 146 153 81 divdiv1d A x S A 0 x 0 A A x = A A x
157 155 156 eqtr3d A x S A 0 x 0 1 x = A A x
158 157 oveq2d A x S A 0 x 0 log 1 + A x 1 x = log 1 + A x A A x
159 85 adantr A x S A 0 x 0 A x
160 78 biimpa A x S A 0 x 0 A x 0
161 150 152 159 160 div12d A x S A 0 x 0 log 1 + A x A A x = A log 1 + A x A x
162 151 158 161 3eqtrd A x S A 0 x 0 1 x log 1 + A x = A log 1 + A x A x
163 162 fveq2d A x S A 0 x 0 e 1 x log 1 + A x = e A log 1 + A x A x
164 83 148 163 3eqtrd A x S A 0 x 0 if x = 0 e A 1 + A x 1 x = e A log 1 + A x A x
165 164 ex A x S A 0 x 0 if x = 0 e A 1 + A x 1 x = e A log 1 + A x A x
166 80 165 sylbird A x S ¬ A x = 0 if x = 0 e A 1 + A x 1 x = e A log 1 + A x A x
167 166 imp A x S ¬ A x = 0 if x = 0 e A 1 + A x 1 x = e A log 1 + A x A x
168 28 29 76 167 ifbothda A x S if x = 0 e A 1 + A x 1 x = if A x = 0 e A 1 e A log 1 + A x A x
169 168 mpteq2dva A x S if x = 0 e A 1 + A x 1 x = x S if A x = 0 e A 1 e A log 1 + A x A x
170 44 resmptd A x if x = 0 e A 1 + A x 1 x S = x S if x = 0 e A 1 + A x 1 x
171 1cnd A x S A x = 0 1
172 149 adantr A x S ¬ A x = 0 log 1 + A x
173 85 adantr A x S ¬ A x = 0 A x
174 simpr A x S ¬ A x = 0 ¬ A x = 0
175 174 neqned A x S ¬ A x = 0 A x 0
176 172 173 175 divcld A x S ¬ A x = 0 log 1 + A x A x
177 171 176 ifclda A x S if A x = 0 1 log 1 + A x A x
178 eqidd A x S if A x = 0 1 log 1 + A x A x = x S if A x = 0 1 log 1 + A x A x
179 eqidd A y e A y = y e A y
180 oveq2 y = if A x = 0 1 log 1 + A x A x A y = A if A x = 0 1 log 1 + A x A x
181 180 fveq2d y = if A x = 0 1 log 1 + A x A x e A y = e A if A x = 0 1 log 1 + A x A x
182 oveq2 if A x = 0 1 log 1 + A x A x = 1 A if A x = 0 1 log 1 + A x A x = A 1
183 182 fveq2d if A x = 0 1 log 1 + A x A x = 1 e A if A x = 0 1 log 1 + A x A x = e A 1
184 oveq2 if A x = 0 1 log 1 + A x A x = log 1 + A x A x A if A x = 0 1 log 1 + A x A x = A log 1 + A x A x
185 184 fveq2d if A x = 0 1 log 1 + A x A x = log 1 + A x A x e A if A x = 0 1 log 1 + A x A x = e A log 1 + A x A x
186 183 185 ifsb e A if A x = 0 1 log 1 + A x A x = if A x = 0 e A 1 e A log 1 + A x A x
187 181 186 eqtrdi y = if A x = 0 1 log 1 + A x A x e A y = if A x = 0 e A 1 e A log 1 + A x A x
188 177 178 179 187 fmptco A y e A y x S if A x = 0 1 log 1 + A x A x = x S if A x = 0 e A 1 e A log 1 + A x A x
189 169 170 188 3eqtr4d A x if x = 0 e A 1 + A x 1 x S = y e A y x S if A x = 0 1 log 1 + A x A x
190 eqidd A x S 1 + A x = x S 1 + A x
191 eqidd A y 1 ball abs 1 if y = 1 1 log y y 1 = y 1 ball abs 1 if y = 1 1 log y y 1
192 eqeq1 y = 1 + A x y = 1 1 + A x = 1
193 fveq2 y = 1 + A x log y = log 1 + A x
194 oveq1 y = 1 + A x y 1 = 1 + A x - 1
195 193 194 oveq12d y = 1 + A x log y y 1 = log 1 + A x 1 + A x - 1
196 192 195 ifbieq2d y = 1 + A x if y = 1 1 log y y 1 = if 1 + A x = 1 1 log 1 + A x 1 + A x - 1
197 141 190 191 196 fmptco A y 1 ball abs 1 if y = 1 1 log y y 1 x S 1 + A x = x S if 1 + A x = 1 1 log 1 + A x 1 + A x - 1
198 59 eqeq2i 1 + A x = 1 + 0 1 + A x = 1
199 138 85 124 addcand A x S 1 + A x = 1 + 0 A x = 0
200 198 199 bitr3id A x S 1 + A x = 1 A x = 0
201 98 oveq2d A x S log 1 + A x 1 + A x - 1 = log 1 + A x A x
202 200 201 ifbieq2d A x S if 1 + A x = 1 1 log 1 + A x 1 + A x - 1 = if A x = 0 1 log 1 + A x A x
203 202 mpteq2dva A x S if 1 + A x = 1 1 log 1 + A x 1 + A x - 1 = x S if A x = 0 1 log 1 + A x A x
204 197 203 eqtrd A y 1 ball abs 1 if y = 1 1 log y y 1 x S 1 + A x = x S if A x = 0 1 log 1 + A x A x
205 eqid TopOpen fld 𝑡 S = TopOpen fld 𝑡 S
206 eqid TopOpen fld = TopOpen fld
207 206 cnfldtopon TopOpen fld TopOn
208 207 a1i A TopOpen fld TopOn
209 1cnd A 1
210 208 208 209 cnmptc A x 1 TopOpen fld Cn TopOpen fld
211 id A A
212 208 208 211 cnmptc A x A TopOpen fld Cn TopOpen fld
213 208 cnmptid A x x TopOpen fld Cn TopOpen fld
214 206 mulcn × TopOpen fld × t TopOpen fld Cn TopOpen fld
215 214 a1i A × TopOpen fld × t TopOpen fld Cn TopOpen fld
216 208 212 213 215 cnmpt12f A x A x TopOpen fld Cn TopOpen fld
217 206 addcn + TopOpen fld × t TopOpen fld Cn TopOpen fld
218 217 a1i A + TopOpen fld × t TopOpen fld Cn TopOpen fld
219 208 210 216 218 cnmpt12f A x 1 + A x TopOpen fld Cn TopOpen fld
220 205 208 44 219 cnmpt1res A x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld
221 141 fmpttd A x S 1 + A x : S 1 ball abs 1
222 221 frnd A ran x S 1 + A x 1 ball abs 1
223 difss 0
224 93 223 sstri 1 ball abs 1
225 224 a1i A 1 ball abs 1
226 cnrest2 TopOpen fld TopOn ran x S 1 + A x 1 ball abs 1 1 ball abs 1 x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld 𝑡 1 ball abs 1
227 207 222 225 226 mp3an2i A x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld 𝑡 1 ball abs 1
228 220 227 mpbid A x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld 𝑡 1 ball abs 1
229 blcntr abs ∞Met 0 1 A + 1 + 0 0 ball abs 1 A + 1
230 30 31 40 229 mp3an2i A 0 0 ball abs 1 A + 1
231 230 1 eleqtrrdi A 0 S
232 resttopon TopOpen fld TopOn S TopOpen fld 𝑡 S TopOn S
233 207 44 232 sylancr A TopOpen fld 𝑡 S TopOn S
234 toponuni TopOpen fld 𝑡 S TopOn S S = TopOpen fld 𝑡 S
235 233 234 syl A S = TopOpen fld 𝑡 S
236 231 235 eleqtrd A 0 TopOpen fld 𝑡 S
237 eqid TopOpen fld 𝑡 S = TopOpen fld 𝑡 S
238 237 cncnpi x S 1 + A x TopOpen fld 𝑡 S Cn TopOpen fld 𝑡 1 ball abs 1 0 TopOpen fld 𝑡 S x S 1 + A x TopOpen fld 𝑡 S CnP TopOpen fld 𝑡 1 ball abs 1 0
239 228 236 238 syl2anc A x S 1 + A x TopOpen fld 𝑡 S CnP TopOpen fld 𝑡 1 ball abs 1 0
240 cnelprrecn
241 logf1o log : 0 1-1 onto ran log
242 f1of log : 0 1-1 onto ran log log : 0 ran log
243 241 242 ax-mp log : 0 ran log
244 logrncn x ran log x
245 244 ssriv ran log
246 fss log : 0 ran log ran log log : 0
247 243 245 246 mp2an log : 0
248 fssres log : 0 1 ball abs 1 0 log 1 ball abs 1 : 1 ball abs 1
249 247 93 248 mp2an log 1 ball abs 1 : 1 ball abs 1
250 blcntr abs ∞Met 1 1 + 1 1 ball abs 1
251 30 84 135 250 mp3an 1 1 ball abs 1
252 ovex 1 y V
253 89 dvlog2 D log 1 ball abs 1 = y 1 ball abs 1 1 y
254 252 253 dmmpti dom log 1 ball abs 1 = 1 ball abs 1
255 251 254 eleqtrri 1 dom log 1 ball abs 1
256 eqid TopOpen fld 𝑡 1 ball abs 1 = TopOpen fld 𝑡 1 ball abs 1
257 253 fveq1i log 1 ball abs 1 1 = y 1 ball abs 1 1 y 1
258 oveq2 y = 1 1 y = 1 1
259 1div1e1 1 1 = 1
260 258 259 eqtrdi y = 1 1 y = 1
261 eqid y 1 ball abs 1 1 y = y 1 ball abs 1 1 y
262 1ex 1 V
263 260 261 262 fvmpt 1 1 ball abs 1 y 1 ball abs 1 1 y 1 = 1
264 251 263 ax-mp y 1 ball abs 1 1 y 1 = 1
265 257 264 eqtr2i 1 = log 1 ball abs 1 1
266 265 a1i y 1 ball abs 1 1 = log 1 ball abs 1 1
267 fvres y 1 ball abs 1 log 1 ball abs 1 y = log y
268 fvres 1 1 ball abs 1 log 1 ball abs 1 1 = log 1
269 251 268 mp1i y 1 ball abs 1 log 1 ball abs 1 1 = log 1
270 log1 log 1 = 0
271 269 270 eqtrdi y 1 ball abs 1 log 1 ball abs 1 1 = 0
272 267 271 oveq12d y 1 ball abs 1 log 1 ball abs 1 y log 1 ball abs 1 1 = log y 0
273 93 sseli y 1 ball abs 1 y 0
274 eldifsn y 0 y y 0
275 273 274 sylib y 1 ball abs 1 y y 0
276 logcl y y 0 log y
277 275 276 syl y 1 ball abs 1 log y
278 277 subid1d y 1 ball abs 1 log y 0 = log y
279 272 278 eqtr2d y 1 ball abs 1 log y = log 1 ball abs 1 y log 1 ball abs 1 1
280 279 oveq1d y 1 ball abs 1 log y y 1 = log 1 ball abs 1 y log 1 ball abs 1 1 y 1
281 266 280 ifeq12d y 1 ball abs 1 if y = 1 1 log y y 1 = if y = 1 log 1 ball abs 1 1 log 1 ball abs 1 y log 1 ball abs 1 1 y 1
282 281 mpteq2ia y 1 ball abs 1 if y = 1 1 log y y 1 = y 1 ball abs 1 if y = 1 log 1 ball abs 1 1 log 1 ball abs 1 y log 1 ball abs 1 1 y 1
283 256 206 282 dvcnp log 1 ball abs 1 : 1 ball abs 1 1 ball abs 1 1 dom log 1 ball abs 1 y 1 ball abs 1 if y = 1 1 log y y 1 TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld 1
284 255 283 mpan2 log 1 ball abs 1 : 1 ball abs 1 1 ball abs 1 y 1 ball abs 1 if y = 1 1 log y y 1 TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld 1
285 240 249 224 284 mp3an y 1 ball abs 1 if y = 1 1 log y y 1 TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld 1
286 oveq2 x = 0 A x = A 0
287 286 oveq2d x = 0 1 + A x = 1 + A 0
288 eqid x S 1 + A x = x S 1 + A x
289 ovex 1 + A 0 V
290 287 288 289 fvmpt 0 S x S 1 + A x 0 = 1 + A 0
291 231 290 syl A x S 1 + A x 0 = 1 + A 0
292 mul01 A A 0 = 0
293 292 oveq2d A 1 + A 0 = 1 + 0
294 293 59 eqtrdi A 1 + A 0 = 1
295 291 294 eqtrd A x S 1 + A x 0 = 1
296 295 fveq2d A TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld x S 1 + A x 0 = TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld 1
297 285 296 eleqtrrid A y 1 ball abs 1 if y = 1 1 log y y 1 TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld x S 1 + A x 0
298 cnpco x S 1 + A x TopOpen fld 𝑡 S CnP TopOpen fld 𝑡 1 ball abs 1 0 y 1 ball abs 1 if y = 1 1 log y y 1 TopOpen fld 𝑡 1 ball abs 1 CnP TopOpen fld x S 1 + A x 0 y 1 ball abs 1 if y = 1 1 log y y 1 x S 1 + A x TopOpen fld 𝑡 S CnP TopOpen fld 0
299 239 297 298 syl2anc A y 1 ball abs 1 if y = 1 1 log y y 1 x S 1 + A x TopOpen fld 𝑡 S CnP TopOpen fld 0
300 204 299 eqeltrrd A x S if A x = 0 1 log 1 + A x A x TopOpen fld 𝑡 S CnP TopOpen fld 0
301 208 208 211 cnmptc A y A TopOpen fld Cn TopOpen fld
302 208 cnmptid A y y TopOpen fld Cn TopOpen fld
303 208 301 302 215 cnmpt12f A y A y TopOpen fld Cn TopOpen fld
304 efcn exp : cn
305 206 cncfcn1 cn = TopOpen fld Cn TopOpen fld
306 304 305 eleqtri exp TopOpen fld Cn TopOpen fld
307 306 a1i A exp TopOpen fld Cn TopOpen fld
308 208 303 307 cnmpt11f A y e A y TopOpen fld Cn TopOpen fld
309 177 fmpttd A x S if A x = 0 1 log 1 + A x A x : S
310 309 231 ffvelrnd A x S if A x = 0 1 log 1 + A x A x 0
311 unicntop = TopOpen fld
312 311 cncnpi y e A y TopOpen fld Cn TopOpen fld x S if A x = 0 1 log 1 + A x A x 0 y e A y TopOpen fld CnP TopOpen fld x S if A x = 0 1 log 1 + A x A x 0
313 308 310 312 syl2anc A y e A y TopOpen fld CnP TopOpen fld x S if A x = 0 1 log 1 + A x A x 0
314 cnpco x S if A x = 0 1 log 1 + A x A x TopOpen fld 𝑡 S CnP TopOpen fld 0 y e A y TopOpen fld CnP TopOpen fld x S if A x = 0 1 log 1 + A x A x 0 y e A y x S if A x = 0 1 log 1 + A x A x TopOpen fld 𝑡 S CnP TopOpen fld 0
315 300 313 314 syl2anc A y e A y x S if A x = 0 1 log 1 + A x A x TopOpen fld 𝑡 S CnP TopOpen fld 0
316 189 315 eqeltrd A x if x = 0 e A 1 + A x 1 x S TopOpen fld 𝑡 S CnP TopOpen fld 0
317 206 cnfldtop TopOpen fld Top
318 317 a1i A TopOpen fld Top
319 206 cnfldtopn TopOpen fld = MetOpen abs
320 319 blopn abs ∞Met 0 1 A + 1 * 0 ball abs 1 A + 1 TopOpen fld
321 30 31 41 320 mp3an2i A 0 ball abs 1 A + 1 TopOpen fld
322 1 321 eqeltrid A S TopOpen fld
323 isopn3i TopOpen fld Top S TopOpen fld int TopOpen fld S = S
324 317 322 323 sylancr A int TopOpen fld S = S
325 231 324 eleqtrrd A 0 int TopOpen fld S
326 efcl A e A
327 326 ad2antrr A x x = 0 e A
328 84 15 86 sylancr A x ¬ x = 0 1 + A x
329 328 49 cxpcld A x ¬ x = 0 1 + A x 1 x
330 327 329 ifclda A x if x = 0 e A 1 + A x 1 x
331 330 fmpttd A x if x = 0 e A 1 + A x 1 x :
332 311 311 cnprest TopOpen fld Top S 0 int TopOpen fld S x if x = 0 e A 1 + A x 1 x : x if x = 0 e A 1 + A x 1 x TopOpen fld CnP TopOpen fld 0 x if x = 0 e A 1 + A x 1 x S TopOpen fld 𝑡 S CnP TopOpen fld 0
333 318 44 325 331 332 syl22anc A x if x = 0 e A 1 + A x 1 x TopOpen fld CnP TopOpen fld 0 x if x = 0 e A 1 + A x 1 x S TopOpen fld 𝑡 S CnP TopOpen fld 0
334 316 333 mpbird A x if x = 0 e A 1 + A x 1 x TopOpen fld CnP TopOpen fld 0
335 311 cnpresti 0 +∞ 0 0 +∞ x if x = 0 e A 1 + A x 1 x TopOpen fld CnP TopOpen fld 0 x if x = 0 e A 1 + A x 1 x 0 +∞ TopOpen fld 𝑡 0 +∞ CnP TopOpen fld 0
336 4 27 334 335 mp3an2i A x if x = 0 e A 1 + A x 1 x 0 +∞ TopOpen fld 𝑡 0 +∞ CnP TopOpen fld 0
337 25 336 eqeltrd A x 0 +∞ if x = 0 e A 1 + A 1 x 1 x TopOpen fld 𝑡 0 +∞ CnP TopOpen fld 0
338 simpl A k + A
339 rpcn k + k
340 339 adantl A k + k
341 rpne0 k + k 0
342 341 adantl A k + k 0
343 338 340 342 divcld A k + A k
344 addcl 1 A k 1 + A k
345 84 343 344 sylancr A k + 1 + A k
346 345 340 cxpcld A k + 1 + A k k
347 oveq2 k = 1 x A k = A 1 x
348 347 oveq2d k = 1 x 1 + A k = 1 + A 1 x
349 id k = 1 x k = 1 x
350 348 349 oveq12d k = 1 x 1 + A k k = 1 + A 1 x 1 x
351 eqid TopOpen fld 𝑡 0 +∞ = TopOpen fld 𝑡 0 +∞
352 326 346 350 206 351 rlimcnp3 A k + 1 + A k k e A x 0 +∞ if x = 0 e A 1 + A 1 x 1 x TopOpen fld 𝑡 0 +∞ CnP TopOpen fld 0
353 337 352 mpbird A k + 1 + A k k e A