Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ioodvbdlimc2lem Structured version   Visualization version   Unicode version

Theorem ioodvbdlimc2lem 37808
 Description: Limit at the upper bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) (Revised by AV, 3-Oct-2020.)
Hypotheses
Ref Expression
ioodvbdlimc2lem.a
ioodvbdlimc2lem.b
ioodvbdlimc2lem.altb
ioodvbdlimc2lem.f
ioodvbdlimc2lem.dmdv
ioodvbdlimc2lem.dvbd
ioodvbdlimc2lem.y
ioodvbdlimc2lem.m
ioodvbdlimc2lem.s
ioodvbdlimc2lem.r
ioodvbdlimc2lem.n
ioodvbdlimc2lem.ch
Assertion
Ref Expression
ioodvbdlimc2lem lim
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,   ,,   ,,,   ,,,,   ,   ,,,,
Allowed substitution hints:   (,,,)   ()   ()   (,)   (,,)

Proof of Theorem ioodvbdlimc2lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 11178 . . . . . 6
2 zssre 10944 . . . . . 6
31, 2sstri 3441 . . . . 5
43a1i 11 . . . 4
5 ioodvbdlimc2lem.m . . . . . . 7
6 ioodvbdlimc2lem.b . . . . . . . . . . 11
7 ioodvbdlimc2lem.a . . . . . . . . . . 11
86, 7resubcld 10047 . . . . . . . . . 10
9 ioodvbdlimc2lem.altb . . . . . . . . . . . 12
107, 6posdifd 10200 . . . . . . . . . . . 12
119, 10mpbid 214 . . . . . . . . . . 11
1211gt0ne0d 10178 . . . . . . . . . 10
138, 12rereccld 10434 . . . . . . . . 9
14 0red 9644 . . . . . . . . . 10
158, 11recgt0d 10541 . . . . . . . . . 10
1614, 13, 15ltled 9783 . . . . . . . . 9
17 flge0nn0 12054 . . . . . . . . 9
1813, 16, 17syl2anc 667 . . . . . . . 8
19 peano2nn0 10910 . . . . . . . 8
2018, 19syl 17 . . . . . . 7
215, 20syl5eqel 2533 . . . . . 6
2221nn0zd 11038 . . . . 5
23 eqid 2451 . . . . . 6
2423uzsup 12090 . . . . 5
2522, 24syl 17 . . . 4
26 ioodvbdlimc2lem.f . . . . . . 7
2726adantr 467 . . . . . 6
287rexrd 9690 . . . . . . . 8
2928adantr 467 . . . . . . 7
306rexrd 9690 . . . . . . . 8
3130adantr 467 . . . . . . 7
326adantr 467 . . . . . . . 8
33 eluzelre 11169 . . . . . . . . . 10
3433adantl 468 . . . . . . . . 9
35 0red 9644 . . . . . . . . . . 11
36 0red 9644 . . . . . . . . . . . . 13
37 1red 9658 . . . . . . . . . . . . 13
3836, 37readdcld 9670 . . . . . . . . . . . 12
3938adantl 468 . . . . . . . . . . 11
4036ltp1d 10537 . . . . . . . . . . . 12
4140adantl 468 . . . . . . . . . . 11
42 eluzel2 11164 . . . . . . . . . . . . . 14
4342zred 11040 . . . . . . . . . . . . 13
4443adantl 468 . . . . . . . . . . . 12
4513flcld 12034 . . . . . . . . . . . . . . . 16
4645zred 11040 . . . . . . . . . . . . . . 15
47 1red 9658 . . . . . . . . . . . . . . 15
4818nn0ge0d 10928 . . . . . . . . . . . . . . 15
4914, 46, 47, 48leadd1dd 10227 . . . . . . . . . . . . . 14
5049, 5syl6breqr 4443 . . . . . . . . . . . . 13
5150adantr 467 . . . . . . . . . . . 12
52 eluzle 11171 . . . . . . . . . . . . 13
5352adantl 468 . . . . . . . . . . . 12
5439, 44, 34, 51, 53letrd 9792 . . . . . . . . . . 11
5535, 39, 34, 41, 54ltletrd 9795 . . . . . . . . . 10
5655gt0ne0d 10178 . . . . . . . . 9
5734, 56rereccld 10434 . . . . . . . 8
5832, 57resubcld 10047 . . . . . . 7
597adantr 467 . . . . . . . 8
6021nn0red 10926 . . . . . . . . . . 11
6114, 47readdcld 9670 . . . . . . . . . . . . . 14
6246, 47readdcld 9670 . . . . . . . . . . . . . 14
6314ltp1d 10537 . . . . . . . . . . . . . 14
6414, 61, 62, 63, 49ltletrd 9795 . . . . . . . . . . . . 13
6564, 5syl6breqr 4443 . . . . . . . . . . . 12
6665gt0ne0d 10178 . . . . . . . . . . 11
6760, 66rereccld 10434 . . . . . . . . . 10
6867adantr 467 . . . . . . . . 9
6932, 68resubcld 10047 . . . . . . . 8
705eqcomi 2460 . . . . . . . . . . . . 13
7170oveq2i 6301 . . . . . . . . . . . 12
7271, 67syl5eqel 2533 . . . . . . . . . . 11
7313, 15elrpd 11338 . . . . . . . . . . . . 13
7462, 64elrpd 11338 . . . . . . . . . . . . 13
75 1rp 11306 . . . . . . . . . . . . . 14
7675a1i 11 . . . . . . . . . . . . 13
77 fllelt 12033 . . . . . . . . . . . . . . 15
7813, 77syl 17 . . . . . . . . . . . . . 14
7978simprd 465 . . . . . . . . . . . . 13
8073, 74, 76, 79ltdiv2dd 37509 . . . . . . . . . . . 12
818recnd 9669 . . . . . . . . . . . . 13
8281, 12recrecd 10380 . . . . . . . . . . . 12
8380, 82breqtrd 4427 . . . . . . . . . . 11
8472, 8, 6, 83ltsub2dd 10226 . . . . . . . . . 10
856recnd 9669 . . . . . . . . . . 11
867recnd 9669 . . . . . . . . . . 11
8785, 86nncand 9991 . . . . . . . . . 10
8871oveq2i 6301 . . . . . . . . . . 11
8988a1i 11 . . . . . . . . . 10
9084, 87, 893brtr3d 4432 . . . . . . . . 9
9190adantr 467 . . . . . . . 8
9260, 65elrpd 11338 . . . . . . . . . . 11
9392adantr 467 . . . . . . . . . 10
9434, 55elrpd 11338 . . . . . . . . . 10
95 1red 9658 . . . . . . . . . 10
96 0le1 10137 . . . . . . . . . . 11
9796a1i 11 . . . . . . . . . 10
9893, 94, 95, 97, 53lediv2ad 11363 . . . . . . . . 9
9957, 68, 32, 98lesub2dd 10230 . . . . . . . 8
10059, 69, 58, 91, 99ltletrd 9795 . . . . . . 7
10194rpreccld 11351 . . . . . . . 8
10232, 101ltsubrpd 11370 . . . . . . 7
10329, 31, 58, 100, 102eliood 37595 . . . . . 6
10427, 103ffvelrnd 6023 . . . . 5
105 ioodvbdlimc2lem.s . . . . 5
106104, 105fmptd 6046 . . . 4
107 ioodvbdlimc2lem.dmdv . . . . . 6
108 ioodvbdlimc2lem.dvbd . . . . . 6
1097, 6, 9, 26, 107, 108dvbdfbdioo 37802 . . . . 5
11060adantr 467 . . . . . . . 8
111 simpr 463 . . . . . . . . . . . . . 14
112105fvmpt2 5957 . . . . . . . . . . . . . 14
113111, 104, 112syl2anc 667 . . . . . . . . . . . . 13
114113fveq2d 5869 . . . . . . . . . . . 12
115114adantlr 721 . . . . . . . . . . 11
116 simplr 762 . . . . . . . . . . . 12
117103adantlr 721 . . . . . . . . . . . 12
118 fveq2 5865 . . . . . . . . . . . . . . 15
119118fveq2d 5869 . . . . . . . . . . . . . 14
120119breq1d 4412 . . . . . . . . . . . . 13
121120rspccva 3149 . . . . . . . . . . . 12
122116, 117, 121syl2anc 667 . . . . . . . . . . 11
123115, 122eqbrtrd 4423 . . . . . . . . . 10
124123a1d 26 . . . . . . . . 9
125124ralrimiva 2802 . . . . . . . 8
126 breq1 4405 . . . . . . . . . . 11
127126imbi1d 319 . . . . . . . . . 10
128127ralbidv 2827 . . . . . . . . 9
129128rspcev 3150 . . . . . . . 8
130110, 125, 129syl2anc 667 . . . . . . 7
131130ex 436 . . . . . 6
132131reximdv 2861 . . . . 5
133109, 132mpd 15 . . . 4
1344, 25, 106, 133limsupre 37721 . . 3
135134recnd 9669 . 2
136 eluzelre 11169 . . . . . . . . 9
137136adantl 468 . . . . . . . 8
138 0red 9644 . . . . . . . . . 10
13945peano2zd 11043 . . . . . . . . . . . . . 14
1405, 139syl5eqel 2533 . . . . . . . . . . . . 13
141140adantr 467 . . . . . . . . . . . 12
142141zred 11040 . . . . . . . . . . 11
143142adantr 467 . . . . . . . . . 10
14465ad2antrr 732 . . . . . . . . . 10
145 ioodvbdlimc2lem.n . . . . . . . . . . . . . 14
146 ioodvbdlimc2lem.y . . . . . . . . . . . . . . . . . . . 20
147 ioomidp 37615 . . . . . . . . . . . . . . . . . . . . . . . 24
1487, 6, 9, 147syl3anc 1268 . . . . . . . . . . . . . . . . . . . . . . 23
149 ne0i 3737 . . . . . . . . . . . . . . . . . . . . . . 23
150148, 149syl 17 . . . . . . . . . . . . . . . . . . . . . 22
151 ioossre 11696 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
152151a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
153 dvfre 22905 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
15426, 152, 153syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . 26
155107feq2d 5715 . . . . . . . . . . . . . . . . . . . . . . . . . 26
156154, 155mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . . 25
157156ffvelrnda 6022 . . . . . . . . . . . . . . . . . . . . . . . 24
158157recnd 9669 . . . . . . . . . . . . . . . . . . . . . . 23
159158abscld 13498 . . . . . . . . . . . . . . . . . . . . . 22
160 eqid 2451 . . . . . . . . . . . . . . . . . . . . . 22
161 eqid 2451 . . . . . . . . . . . . . . . . . . . . . 22
162150, 159, 108, 160, 161suprnmpt 37439 . . . . . . . . . . . . . . . . . . . . 21
163162simpld 461 . . . . . . . . . . . . . . . . . . . 20
164146, 163syl5eqel 2533 . . . . . . . . . . . . . . . . . . 19
165164adantr 467 . . . . . . . . . . . . . . . . . 18
166 rpre 11308 . . . . . . . . . . . . . . . . . . . 20
167166rehalfcld 10859 . . . . . . . . . . . . . . . . . . 19
168167adantl 468 . . . . . . . . . . . . . . . . . 18
169166recnd 9669 . . . . . . . . . . . . . . . . . . . 20
170169adantl 468 . . . . . . . . . . . . . . . . . . 19
171 2cnd 10682 . . . . . . . . . . . . . . . . . . 19
172 rpne0 11317 . . . . . . . . . . . . . . . . . . . 20
173172adantl 468 . . . . . . . . . . . . . . . . . . 19
174 2ne0 10702 . . . . . . . . . . . . . . . . . . . 20
175174a1i 11 . . . . . . . . . . . . . . . . . . 19
176170, 171, 173, 175divne0d 10399 . . . . . . . . . . . . . . . . . 18
177165, 168, 176redivcld 10435 . . . . . . . . . . . . . . . . 17
178177flcld 12034 . . . . . . . . . . . . . . . 16
179178peano2zd 11043 . . . . . . . . . . . . . . 15
180179, 141ifcld 3924 . . . . . . . . . . . . . 14
181145, 180syl5eqel 2533 . . . . . . . . . . . . 13
182181zred 11040 . . . . . . . . . . . 12
183182adantr 467 . . . . . . . . . . 11
184179zred 11040 . . . . . . . . . . . . . 14
185 max1 11480 . . . . . . . . . . . . . 14
186142, 184, 185syl2anc 667 . . . . . . . . . . . . 13
187186, 145syl6breqr 4443 . . . . . . . . . . . 12
188187adantr 467 . . . . . . . . . . 11
189 eluzle 11171 . . . . . . . . . . . 12
190189adantl 468 . . . . . . . . . . 11
191143, 183, 137, 188, 190letrd 9792 . . . . . . . . . 10
192138, 143, 137, 144, 191ltletrd 9795 . . . . . . . . 9
193192gt0ne0d 10178 . . . . . . . 8
194137, 193rereccld 10434 . . . . . . 7
195137, 192recgt0d 10541 . . . . . . 7
196194, 195elrpd 11338 . . . . . 6
197196adantr 467 . . . . 5
198 ioodvbdlimc2lem.ch . . . . . . . . 9
199198biimpi 198 . . . . . . . . . . . . . . . . 17
200 simp-5l 778 . . . . . . . . . . . . . . . . 17
201199, 200syl 17 . . . . . . . . . . . . . . . 16
202201, 26syl 17 . . . . . . . . . . . . . . 15
203199simplrd 763 . . . . . . . . . . . . . . 15
204202, 203ffvelrnd 6023 . . . . . . . . . . . . . 14
205204recnd 9669 . . . . . . . . . . . . 13
206201, 106syl 17 . . . . . . . . . . . . . . 15
207 simp-5r 779 . . . . . . . . . . . . . . . . . . 19
208199, 207syl 17 . . . . . . . . . . . . . . . . . 18
209 eluz2 11165 . . . . . . . . . . . . . . . . . . 19
210141, 181, 187, 209syl3anbrc 1192 . . . . . . . . . . . . . . . . . 18
211201, 208, 210syl2anc 667 . . . . . . . . . . . . . . . . 17
212 uzss 11179 . . . . . . . . . . . . . . . . 17
213211, 212syl 17 . . . . . . . . . . . . . . . 16
214 simp-4r 777 . . . . . . . . . . . . . . . . 17
215199, 214syl 17 . . . . . . . . . . . . . . . 16
216213, 215sseldd 3433 . . . . . . . . . . . . . . 15
217206, 216ffvelrnd 6023 . . . . . . . . . . . . . 14
218217recnd 9669 . . . . . . . . . . . . 13
219201, 135syl 17 . . . . . . . . . . . . 13
220205, 218, 219npncand 10010 . . . . . . . . . . . 12
221220eqcomd 2457 . . . . . . . . . . 11
222221fveq2d 5869 . . . . . . . . . 10
223204, 217resubcld 10047 . . . . . . . . . . . . . 14
224201, 134syl 17 . . . . . . . . . . . . . . 15
225217, 224resubcld 10047 . . . . . . . . . . . . . 14
226223, 225readdcld 9670 . . . . . . . . . . . . 13
227226recnd 9669 . . . . . . . . . . . 12
228227abscld 13498 . . . . . . . . . . 11
229223recnd 9669 . . . . . . . . . . . . 13
230229abscld 13498 . . . . . . . . . . . 12
231225recnd 9669 . . . . . . . . . . . . 13
232231abscld 13498 . . . . . . . . . . . 12
233230, 232readdcld 9670 . . . . . . . . . . 11
234208rpred 11341 . . . . . . . . . . 11
235229, 231abstrid 13518 . . . . . . . . . . 11
236234rehalfcld 10859 . . . . . . . . . . . . 13
237201, 216, 113syl2anc 667 . . . . . . . . . . . . . . . 16
238237oveq2d 6306 . . . . . . . . . . . . . . 15
239238fveq2d 5869 . . . . . . . . . . . . . 14
240239, 230eqeltrrd 2530 . . . . . . . . . . . . . . 15
241201, 164syl 17 . . . . . . . . . . . . . . . 16
242151, 203sseldi 3430 . . . . . . . . . . . . . . . . 17
243201, 216, 58syl2anc 667 . . . . . . . . . . . . . . . . 17
244242, 243resubcld 10047 . . . . . . . . . . . . . . . 16
245241, 244remulcld 9671 . . . . . . . . . . . . . . 15
246201, 7syl 17 . . . . . . . . . . . . . . . . 17
247201, 6syl 17 . . . . . . . . . . . . . . . . 17
248201, 107syl 17 . . . . . . . . . . . . . . . . 17
249162simprd 465 . . . . . . . . . . . . . . . . . . . 20
250146breq2i 4410 . . . . . . . . . . . . . . . . . . . . 21
251250ralbii 2819 . . . . . . . . . . . . . . . . . . . 20
252249, 251sylibr 216 . . . . . . . . . . . . . . . . . . 19
253201, 252syl 17 . . . . . . . . . . . . . . . . . 18
254 fveq2 5865 . . . . . . . . . . . . . . . . . . . . 21
255254fveq2d 5869 . . . . . . . . . . . . . . . . . . . 20
256255breq1d 4412 . . . . . . . . . . . . . . . . . . 19
257256cbvralv 3019 . . . . . . . . . . . . . . . . . 18
258253, 257sylibr 216 . . . . . . . . . . . . . . . . 17
259201, 216, 103syl2anc 667 . . . . . . . . . . . . . . . . 17
260243rexrd 9690 . . . . . . . . . . . . . . . . . 18
261201, 30syl 17 . . . . . . . . . . . . . . . . . 18
2623, 216sseldi 3430 . . . . . . . . . . . . . . . . . . . 20
263201, 216, 56syl2anc 667 . . . . . . . . . . . . . . . . . . . 20
264262, 263rereccld 10434 . . . . . . . . . . . . . . . . . . 19
265247, 242resubcld 10047 . . . . . . . . . . . . . . . . . . . 20
266242, 247resubcld 10047 . . . . . . . . . . . . . . . . . . . . . 22
267266recnd 9669 . . . . . . . . . . . . . . . . . . . . 21
268267abscld 13498 . . . . . . . . . . . . . . . . . . . 20
269265leabsd 13476 . . . . . . . . . . . . . . . . . . . . 21
270201, 85syl 17 . . . . . . . . . . . . . . . . . . . . . 22
271242recnd 9669 . . . . . . . . . . . . . . . . . . . . . 22
272270, 271abssubd 13515 . . . . . . . . . . . . . . . . . . . . 21
273269, 272breqtrd 4427 . . . . . . . . . . . . . . . . . . . 20
274199simprd 465 . . . . . . . . . . . . . . . . . . . 20
275265, 268, 264, 273, 274lelttrd 9793 . . . . . . . . . . . . . . . . . . 19
276247, 242, 264, 275ltsub23d 10218 . . . . . . . . . . . . . . . . . 18
277201, 28syl 17 . . . . . . . . . . . . . . . . . . 19
278 iooltub 37610 . . . . . . . . . . . . . . . . . . 19
279277, 261, 203, 278syl3anc 1268 . . . . . . . . . . . . . . . . . 18
280260, 261, 242, 276, 279eliood 37595 . . . . . . . . . . . . . . . . 17
281246, 247, 202, 248, 241, 258, 259, 280dvbdfbdioolem1 37800 . . . . . . . . . . . . . . . 16
282281simpld 461 . . . . . . . . . . . . . . 15
283201, 216, 57syl2anc 667 . . . . . . . . . . . . . . . . 17
284241, 283remulcld 9671 . . . . . . . . . . . . . . . 16
285156, 148ffvelrnd 6023 . . . . . . . . . . . . . . . . . . . . 21
286285recnd 9669 . . . . . . . . . . . . . . . . . . . 20
287286abscld 13498 . . . . . . . . . . . . . . . . . . 19
288286absge0d 13506 . . . . . . . . . . . . . . . . . . 19
289 fveq2 5865 . . . . . . . . . . . . . . . . . . . . . . 23
290289fveq2d 5869 . . . . . . . . . . . . . . . . . . . . . 22
291146eqcomi 2460 . . . . . . . . . . . . . . . . . . . . . . 23
292291a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
293290, 292breq12d 4415 . . . . . . . . . . . . . . . . . . . . 21
294293rspcva 3148 . . . . . . . . . . . . . . . . . . . 20
295148, 249, 294syl2anc 667 . . . . . . . . . . . . . . . . . . 19
29614, 287, 164, 288, 295letrd 9792 . . . . . . . . . . . . . . . . . 18
297201, 296syl 17 . . . . . . . . . . . . . . . . 17
298283recnd 9669 . . . . . . . . . . . . . . . . . . . 20
299 sub31 37504 . . . . . . . . . . . . . . . . . . . 20
300271, 270, 298, 299syl3anc 1268 . . . . . . . . . . . . . . . . . . 19
301242, 247posdifd 10200 . . . . . . . . . . . . . . . . . . . . . 22
302279, 301mpbid 214 . . . . . . . . . . . . . . . . . . . . 21
303265, 302elrpd 11338 . . . . . . . . . . . . . . . . . . . 20
304283, 303ltsubrpd 11370 . . . . . . . . . . . . . . . . . . 19
305300, 304eqbrtrd 4423 . . . . . . . . . . . . . . . . . 18
306244, 283, 305ltled 9783 . . . . . . . . . . . . . . . . 17
307244, 283, 241, 297, 306lemul2ad 10547 . . . . . . . . . . . . . . . 16
308284adantr 467 . . . . . . . . . . . . . . . . . 18
309236adantr 467 . . . . . . . . . . . . . . . . . 18
310 oveq1 6297 . . . . . . . . . . . . . . . . . . . 20
311298mul02d 9831 . . . . . . . . . . . . . . . . . . . 20
312310, 311sylan9eqr 2507 . . . . . . . . . . . . . . . . . . 19
313208rphalfcld 11353 . . . . . . . . . . . . . . . . . . . . 21
314313rpgt0d 11344 . . . . . . . . . . . . . . . . . . . 20
315314adantr 467 . . . . . . . . . . . . . . . . . . 19
316312, 315eqbrtrd 4423 . . . . . . . . . . . . . . . . . 18
317308, 309, 316ltled 9783 . . . . . . . . . . . . . . . . 17
318241adantr 467 . . . . . . . . . . . . . . . . . . 19
319297adantr 467 . . . . . . . . . . . . . . . . . . 19
320 neqne 37374 . . . . . . . . . . . . . . . . . . . 20
321320adantl 468 . . . . . . . . . . . . . . . . . . 19
322318, 319, 321ne0gt0d 9772 . . . . . . . . . . . . . . . . . 18
323284adantr 467 . . . . . . . . . . . . . . . . . . 19
3243, 211sseldi 3430 . . . . . . . . . . . . . . . . . . . . . 22
325 0red 9644 . . . . . . . . . . . . . . . . . . . . . . . 24
326201, 208, 142syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . 24
327201, 65syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24
328201, 208, 187syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . 24
329325, 326, 324, 327, 328ltletrd 9795 . . . . . . . . . . . . . . . . . . . . . . 23
330329gt0ne0d 10178 . . . . . . . . . . . . . . . . . . . . . 22
331324, 330rereccld 10434 . . . . . . . . . . . . . . . . . . . . 21
332241, 331remulcld 9671 . . . . . . . . . . . . . . . . . . . 20
333332adantr 467 . . . . . . . . . . . . . . . . . . 19
334236adantr 467 . . . . . . . . . . . . . . . . . . 19
335283adantr 467 . . . . . . . . . . . . . . . . . . . 20
336331adantr 467 . . . . . . . . . . . . . . . . . . . 20
337241adantr 467 . . . . . . . . . . . . . . . . . . . 20
338297adantr 467 . . . . . . . . . . . . . . . . . . . 20
339324, 329elrpd 11338 . . . . . . . . . . . . . . . . . . . . . 22
340201, 216, 94syl2anc 667 . . . . . . . . . . . . . . . . . . . . . 22
341 1red 9658 . . . . . . . . . . . . . . . . . . . . . 22
34296a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
343215, 189syl 17 . . . . . . . . . . . . . . . . . . . . . 22
344339, 340, 341, 342, 343lediv2ad 11363 . . . . . . . . . . . . . . . . . . . . 21
345344adantr 467 . . . . . . . . . . . . . . . . . . . 20
346335, 336, 337, 338, 345lemul2ad 10547 . . . . . . . . . . . . . . . . . . 19
347234recnd 9669 . . . . . . . . . . . . . . . . . . . . . . . . . 26
348 2cnd 10682 . . . . . . . . . . . . . . . . . . . . . . . . . 26
349208rpne0d 11346 . . . . . . . . . . . . . . . . . . . . . . . . . 26
350174a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26
351347, 348, 349, 350divne0d 10399 . . . . . . . . . . . . . . . . . . . . . . . . 25
352241, 236, 351redivcld 10435 . . . . . . . . . . . . . . . . . . . . . . . 24
353352adantr 467 . . . . . . . . . . . . . . . . . . . . . . 23
354 simpr 463 . . . . . . . . . . . . . . . . . . . . . . . 24
355314adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24
356337, 334, 354, 355divgt0d 10542 . . . . . . . . . . . . . . . . . . . . . . 23
357353, 356elrpd 11338 . . . . . . . . . . . . . . . . . . . . . 22
358357rprecred 11352 . . . . . . . . . . . . . . . . . . . . 21
359339adantr 467 . . . . . . . . . . . . . . . . . . . . . 22
360 1red 9658 . . . . . . . . . . . . . . . . . . . . . 22
36196a1i 11 . . . . . . . . . . . . . . . . . . . . . 22
362352flcld 12034 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
363362peano2zd 11043 . . . . . . . . . . . . . . . . . . . . . . . . . 26
364363zred 11040 . . . . . . . . . . . . . . . . . . . . . . . . 25
365201, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
366363, 365ifcld 3924 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
367145, 366syl5eqel 2533 . . . . . . . . . . . . . . . . . . . . . . . . . 26
368367zred 11040 . . . . . . . . . . . . . . . . . . . . . . . . 25
369 flltp1 12036 . . . . . . . . . . . . . . . . . . . . . . . . . 26
370352, 369syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
371201, 60syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
372 max2 11482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
373371, 364, 372syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . 26
374373, 145syl6breqr 4443 . . . . . . . . . . . . . . . . . . . . . . . . 25
375352, 364, 368, 370, 374ltletrd 9795 . . . . . . . . . . . . . . . . . . . . . . . 24
376352, 324, 375ltled 9783 . . . . . . . . . . . . . . . . . . . . . . 23
377376adantr 467 . . . . . . . . . . . . . . . . . . . . . 22
378357, 359, 360, 361, 377lediv2ad 11363 . . . . . . . . . . . . . . . . . . . . 21
379336, 358, 337, 338, 378lemul2ad 10547 . . . . . . . . . . . . . . . . . . . 20
380337recnd 9669 . . . . . . . . . . . . . . . . . . . . . 22
381353recnd 9669 . . . . . . . . . . . . . . . . . . . . . 22
382356gt0ne0d 10178 . . . . . . . . . . . . . . . . . . . . . 22
383380, 381, 382divrecd 10386 . . . . . . . . . . . . . . . . . . . . 21
384334recnd 9669 . . . . . . . . . . . . . . . . . . . . . 22
385354gt0ne0d 10178 . . . . . . . . . . . . . . . . . . . . . 22
386351adantr 467 . . . . . . . . . . . . . . . . . . . . . 22
387380, 384, 385, 386ddcand 10403 . . . . . . . . . . . . . . . . . . . . 21
388383, 387eqtr3d 2487 . . . . . . . . . . . . . . . . . . . 20
389379, 388breqtrd 4427 . . . . . . . . . . . . . . . . . . 19
390323, 333, 334, 346, 389letrd 9792 . . . . . . . . . . . . . . . . . 18
391322, 390syldan 473 . . . . . . . . . . . . . . . . 17
392317, 391pm2.61dan 800 . . . . . . . . . . . . . . . 16
393245, 284, 236, 307, 392letrd 9792 . . . . . . . . . . . . . . 15
394240, 245, 236, 282, 393letrd 9792 . . . . . . . . . . . . . 14
395239, 394eqbrtrd 4423 . . . . . . . . . . . . 13
396 simpllr 769 . . . . . . . . . . . . . 14
397199, 396syl 17 . . . . . . . . . . . . 13
398230, 232, 236, 236, 395, 397leltaddd 10235 . . . . . . . . . . . 12
3993472halvesd 10858 . . . . . . . . . . . 12
400398, 399breqtrd 4427 . . . . . . . . . . 11
401228, 233, 234, 235, 400lelttrd 9793 . . . . . . . . . 10
402222, 401eqbrtrd 4423 . . . . . . . . 9
403198, 402sylbir 217 . . . . . . . 8
404403adantrl 722 . . . . . . 7
405404ex 436 . . . . . 6
406405ralrimiva 2802 . . . . 5
407 breq2 4406 . . . . . . . . 9
408407anbi2d 710 . . . . . . . 8
409408imbi1d 319 . . . . . . 7
410409ralbidv 2827 . . . . . 6
411410rspcev 3150 . . . . 5
412197, 406, 411syl2anc 667 . . . 4
413 simpr 463 . . . . . . . . . . 11
414413iftrued 3889 . . . . . . . . . 10
415 uzid 11173 . . . . . . . . . . . 12
416181, 415syl 17 . . . . . . . . . . 11
417416adantr 467 . . . . . . . . . 10
418414, 417eqeltrd 2529 . . . . . . . . 9
419418adantlr 721 . . . . . . . 8
420 iffalse 3890 . . . . . . . . . 10
421420adantl 468 . . . . . . . . 9
422181ad2antrr 732 . . . . . . . . . 10
423 simplr 762 . . . . . . . . . 10
424422zred 11040 . . . . . . . . . . 11
425423zred 11040 . . . . . . . . . . 11
426 simpr 463 . . . . . . . . . . . 12
427424, 425ltnled 9782 . . . . . . . . . . . 12
428426, 427mpbird 236 . . . . . . . . . . 11
429424, 425, 428ltled 9783 . . . . . . . . . 10
430 eluz2 11165 . . . . . . . . . 10
431422, 423, 429, 430syl3anbrc 1192 . . . . . . . . 9
432421, 431eqeltrd 2529 . . . . . . . 8
433419, 432pm2.61dan 800 . . . . . . 7
434433adantr 467 . . . . . 6
435 simpr 463 . . . . . . . 8
436 simpr 463 . . . . . . . . . 10
437181adantr 467 . . . . . . . . . . 11
438437, 436ifcld 3924 . . . . . . . . . 10
439436zred 11040 . . . . . . . . . . 11
440437zred 11040 . . . . . . . . . . 11
441 max1 11480 . . . . . . . . . . 11
442439, 440, 441syl2anc 667 . . . . . . . . . 10
443 eluz2 11165 . . . . . . . . . 10
444436, 438, 442, 443syl3anbrc 1192 . . . . . . . . 9
445444adantr 467 . . . . . . . 8
446 fveq2 5865 . . . . . . . . . . 11
447446eleq1d 2513 . . . . . . . . . 10
448446oveq1d 6305 . . . . . . . . . . . 12
449448fveq2d 5869 . . . . . . . . . . 11
450449breq1d 4412 . . . . . . . . . 10
451447, 450anbi12d 717 . . . . . . . . 9
452451rspccva 3149 . . . . . . . 8
453435, 445, 452syl2anc 667 . . . . . . 7
454453simprd 465 . . . . . 6
455 fveq2 5865 . . . . . . . . . 10
456455oveq1d 6305 . . . . . . . . 9
457456fveq2d 5869 . . . . . . . 8
458457breq1d 4412 . . . . . . 7
459458rspcev 3150 . . . . . 6
460434, 454, 459syl2anc 667 . . . . 5
461 ax-resscn 9596 . . . . . . . . . . . . . 14
462461a1i 11 . . . . . . . . . . . . 13
46326, 462fssd 5738 . . . . . . . . . . . . . 14
464 dvcn 22875 . . . . . . . . . . . . . 14
465462, 463, 152, 107, 464syl31anc 1271 . . . . . . . . . . . . 13
466 cncffvrn 21930 . . . . . . . . . . . . 13
467462, 465, 466syl2anc 667 . . . . . . . . . . . 12
46826, 467mpbird 236 . . . . . . . . . . 11
469 ioodvbdlimc2lem.r . . . . . . . . . . . 12
470103, 469fmptd 6046 . . . . . . . . . . 11
471 eqid 2451 . . . . . . . . . . 11
472 climrel 13556 . . . . . . . . . . . . 13
473472a1i 11 . . . . . . . . . . . 12
474 fvex 5875 . . . . . . . . . . . . . . . . 17
475474mptex 6136 . . . . . . . . . . . . . . . 16
476475a1i 11 . . . . . . . . . . . . . . 15
477 eqidd 2452 . . . . . . . . . . . . . . . 16
478 eqidd 2452 . . . . . . . . . . . . . . . 16
479 simpr 463 . . . . . . . . . . . . . . . 16
4806adantr 467 . . . . . . . . . . . . . . . 16
481477, 478, 479, 480fvmptd 5954 . . . . . . . . . . . . . . 15
48223, 22, 476, 85, 481climconst 13607 . . . . . . . . . . . . . 14
483474mptex 6136 . . . . . . . . . . . . . . . 16
484469, 483eqeltri 2525 . . . . . . . . . . . . . . 15
485484a1i 11 . . . . . . . . . . . . . 14
486 1cnd 9659 . . . . . . . . . . . . . . 15
487 elnnnn0b 10914 . . . . . . . . . . . . . . . 16
48821, 65, 487sylanbrc 670 . . . . . . . . . . . . . . 15
489 divcnvg 37707 . . . . . . . . . . . . . . 15
490486, 488, 489syl2anc 667 . . . . . . . . . . . . . 14
491 eqidd 2452 . . . . . . . . . . . . . . . . 17
492 eqidd 2452 . . . . . . . . . . . . . . . . 17
493 simpr 463 . . . . . . . . . . . . . . . . 17
4946adantr 467 . . . . . . . . . . . . . . . . 17
495491, 492, 493, 494fvmptd 5954 . . . . . . . . . . . . . . . 16
496495, 494eqeltrd 2529 . . . . . . . . . . . . . . 15
497496recnd 9669 . . . . . . . . . . . . . 14
498 eqidd 2452 . . . . . . . . . . . . . . . 16
499 oveq2 6298 . . . . . . . . . . . . . . . . 17
500499adantl 468 . . . . . . . . . . . . . . . 16
5013, 493sseldi 3430 . . . . . . . . . . . . . . . . 17
502 0red 9644 . . . . . . . . . . . . . . . . . . 19
50360adantr 467 . . . . . . . . . . . . . . . . . . 19
50465adantr 467 . . . . . . . . . . . . . . . . . . 19
505 eluzle 11171 . . . . . . . . . . . . . . . . . . . 20
506505adantl 468 . . . . . . . . . . . . . . . . . . 19
507502, 503, 501, 504, 506ltletrd 9795 . . . . . . . . . . . . . . . . . 18
508507gt0ne0d 10178 . . . . . . . . . . . . . . . . 17
509501, 508rereccld 10434 . . . . . . . . . . . . . . . 16
510498, 500, 493, 509fvmptd 5954 . . . . . . . . . . . . . . 15
511501recnd 9669 . . . . . . . . . . . . . . . 16
512511, 508reccld 10376 . . . . . . . . . . . . . . 15
513510, 512eqeltrd 2529 . . . . . . . . . . . . . 14
514499oveq2d 6306 . . . . . . . . . . . . . . . . 17
515 ovex 6318 . . . . . . . . . . . . . . . . 17
516514, 469, 515fvmpt 5948 . . . . . . . . . . . . . . . 16
517516adantl 468 . . . . . . . . . . . . . . 15
518495, 510oveq12d 6308 . . . . . . . . . . . . . . 15
519517, 518eqtr4d 2488 . . . . . . . . . . . . . 14
52023, 22, 482, 485, 490, 497, 513, 519climsub 13697 . . . . . . . . . . . . 13
52185subid1d 9975 . . . . . . . . . . . . 13
522520, 521