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

Theorem ioodvbdlimc1lem2OLD 37903
 Description: Limit at the lower bound of an open interval, for a function with bounded derivative. (Contributed by Glauco Siliprandi, 11-Dec-2019.) Obsolete version of ioodvbdlimc1lem2 37901 as of 3-Oct-2020. (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
ioodvbdlimc1lem2OLD.a
ioodvbdlimc1lem2OLD.b
ioodvbdlimc1lem2OLD.altb
ioodvbdlimc1lem2OLD.f
ioodvbdlimc1lem2OLD.dmdv
ioodvbdlimc1lem2OLD.dvbd
ioodvbdlimc1lem2OLD.y
ioodvbdlimc1lem2OLD.m
ioodvbdlimc1lem2OLD.s
ioodvbdlimc1lem2OLD.r
ioodvbdlimc1lem2OLD.n
ioodvbdlimc1lem2OLD.ch
Assertion
Ref Expression
ioodvbdlimc1lem2OLD lim
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,   ,,   ,,,   ,,,,   ,   ,,,,
Allowed substitution hints:   (,,,)   ()   ()   (,)   (,,)

Proof of Theorem ioodvbdlimc1lem2OLD
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uzssz 11202 . . . . . 6
2 zssre 10968 . . . . . 6
31, 2sstri 3427 . . . . 5
43a1i 11 . . . 4
5 ioodvbdlimc1lem2OLD.m . . . . . . 7
6 ioodvbdlimc1lem2OLD.b . . . . . . . . . . 11
7 ioodvbdlimc1lem2OLD.a . . . . . . . . . . 11
86, 7resubcld 10068 . . . . . . . . . 10
9 ioodvbdlimc1lem2OLD.altb . . . . . . . . . . . 12
107, 6posdifd 10221 . . . . . . . . . . . 12
119, 10mpbid 215 . . . . . . . . . . 11
1211gt0ne0d 10199 . . . . . . . . . 10
138, 12rereccld 10456 . . . . . . . . 9
14 0red 9662 . . . . . . . . . 10
158, 11recgt0d 10563 . . . . . . . . . 10
1614, 13, 15ltled 9800 . . . . . . . . 9
17 flge0nn0 12087 . . . . . . . . 9
1813, 16, 17syl2anc 673 . . . . . . . 8
19 peano2nn0 10934 . . . . . . . 8
2018, 19syl 17 . . . . . . 7
215, 20syl5eqel 2553 . . . . . 6
2221nn0zd 11061 . . . . 5
23 eqid 2471 . . . . . 6
2423uzsup 12123 . . . . 5
2522, 24syl 17 . . . 4
26 ioodvbdlimc1lem2OLD.f . . . . . . 7
2726adantr 472 . . . . . 6
287rexrd 9708 . . . . . . . 8
2928adantr 472 . . . . . . 7
306rexrd 9708 . . . . . . . 8
3130adantr 472 . . . . . . 7
327adantr 472 . . . . . . . 8
33 eluzelre 11193 . . . . . . . . . 10
3433adantl 473 . . . . . . . . 9
35 0red 9662 . . . . . . . . . . 11
36 0red 9662 . . . . . . . . . . . . 13
37 1red 9676 . . . . . . . . . . . . 13
3836, 37readdcld 9688 . . . . . . . . . . . 12
3938adantl 473 . . . . . . . . . . 11
4036ltp1d 10559 . . . . . . . . . . . 12
4140adantl 473 . . . . . . . . . . 11
42 eluzel2 11187 . . . . . . . . . . . . . 14
4342zred 11063 . . . . . . . . . . . . 13
4443adantl 473 . . . . . . . . . . . 12
4513flcld 12067 . . . . . . . . . . . . . . . 16
4645zred 11063 . . . . . . . . . . . . . . 15
47 1red 9676 . . . . . . . . . . . . . . 15
4818nn0ge0d 10952 . . . . . . . . . . . . . . 15
4914, 46, 47, 48leadd1dd 10248 . . . . . . . . . . . . . 14
5049, 5syl6breqr 4436 . . . . . . . . . . . . 13
5150adantr 472 . . . . . . . . . . . 12
52 eluzle 11195 . . . . . . . . . . . . 13
5352adantl 473 . . . . . . . . . . . 12
5439, 44, 34, 51, 53letrd 9809 . . . . . . . . . . 11
5535, 39, 34, 41, 54ltletrd 9812 . . . . . . . . . 10
5655gt0ne0d 10199 . . . . . . . . 9
5734, 56rereccld 10456 . . . . . . . 8
5832, 57readdcld 9688 . . . . . . 7
5934, 55elrpd 11361 . . . . . . . . 9
6059rpreccld 11374 . . . . . . . 8
6132, 60ltaddrpd 11394 . . . . . . 7
6221nn0red 10950 . . . . . . . . . . 11
6314, 47readdcld 9688 . . . . . . . . . . . . . 14
6446, 47readdcld 9688 . . . . . . . . . . . . . 14
6514ltp1d 10559 . . . . . . . . . . . . . 14
6614, 63, 64, 65, 49ltletrd 9812 . . . . . . . . . . . . 13
6766, 5syl6breqr 4436 . . . . . . . . . . . 12
6867gt0ne0d 10199 . . . . . . . . . . 11
6962, 68rereccld 10456 . . . . . . . . . 10
7069adantr 472 . . . . . . . . 9
7132, 70readdcld 9688 . . . . . . . 8
726adantr 472 . . . . . . . 8
7362, 67elrpd 11361 . . . . . . . . . . 11
7473adantr 472 . . . . . . . . . 10
75 1red 9676 . . . . . . . . . 10
76 0le1 10158 . . . . . . . . . . 11
7776a1i 11 . . . . . . . . . 10
7874, 59, 75, 77, 53lediv2ad 11386 . . . . . . . . 9
7957, 70, 32, 78leadd2dd 10249 . . . . . . . 8
805eqcomi 2480 . . . . . . . . . . . . 13
8180oveq2i 6319 . . . . . . . . . . . 12
8281, 69syl5eqel 2553 . . . . . . . . . . 11
8313, 15elrpd 11361 . . . . . . . . . . . . 13
8464, 66elrpd 11361 . . . . . . . . . . . . 13
85 1rp 11329 . . . . . . . . . . . . . 14
8685a1i 11 . . . . . . . . . . . . 13
87 fllelt 12066 . . . . . . . . . . . . . . 15
8813, 87syl 17 . . . . . . . . . . . . . 14
8988simprd 470 . . . . . . . . . . . . 13
9083, 84, 86, 89ltdiv2dd 37597 . . . . . . . . . . . 12
918recnd 9687 . . . . . . . . . . . . 13
9291, 12recrecd 10402 . . . . . . . . . . . 12
9390, 92breqtrd 4420 . . . . . . . . . . 11
9482, 8, 7, 93ltadd2dd 9811 . . . . . . . . . 10
955oveq2i 6319 . . . . . . . . . . . 12
9695oveq2i 6319 . . . . . . . . . . 11
9796a1i 11 . . . . . . . . . 10
987recnd 9687 . . . . . . . . . . . 12
996recnd 9687 . . . . . . . . . . . 12
10098, 99pncan3d 10008 . . . . . . . . . . 11
101100eqcomd 2477 . . . . . . . . . 10
10294, 97, 1013brtr4d 4426 . . . . . . . . 9
103102adantr 472 . . . . . . . 8
10458, 71, 72, 79, 103lelttrd 9810 . . . . . . 7
10529, 31, 58, 61, 104eliood 37691 . . . . . 6
10627, 105ffvelrnd 6038 . . . . 5
107 ioodvbdlimc1lem2OLD.s . . . . 5
108106, 107fmptd 6061 . . . 4
109 ioodvbdlimc1lem2OLD.dmdv . . . . . 6
110 ioodvbdlimc1lem2OLD.dvbd . . . . . 6
1117, 6, 9, 26, 109, 110dvbdfbdioo 37899 . . . . 5
11262adantr 472 . . . . . . . 8
113 simpr 468 . . . . . . . . . . . . . 14
114107fvmpt2 5972 . . . . . . . . . . . . . 14
115113, 106, 114syl2anc 673 . . . . . . . . . . . . 13
116115fveq2d 5883 . . . . . . . . . . . 12
117116adantlr 729 . . . . . . . . . . 11
118 simplr 770 . . . . . . . . . . . 12
119105adantlr 729 . . . . . . . . . . . 12
120 fveq2 5879 . . . . . . . . . . . . . . 15
121120fveq2d 5883 . . . . . . . . . . . . . 14
122121breq1d 4405 . . . . . . . . . . . . 13
123122rspccva 3135 . . . . . . . . . . . 12
124118, 119, 123syl2anc 673 . . . . . . . . . . 11
125117, 124eqbrtrd 4416 . . . . . . . . . 10
126125a1d 25 . . . . . . . . 9
127126ralrimiva 2809 . . . . . . . 8
128 breq1 4398 . . . . . . . . . . 11
129128imbi1d 324 . . . . . . . . . 10
130129ralbidv 2829 . . . . . . . . 9
131130rspcev 3136 . . . . . . . 8
132112, 127, 131syl2anc 673 . . . . . . 7
133132ex 441 . . . . . 6
134133reximdv 2857 . . . . 5
135111, 134mpd 15 . . . 4
1364, 25, 108, 135limsupreOLD 37819 . . 3
137136recnd 9687 . 2
138 eluzelre 11193 . . . . . . . . 9
139138adantl 473 . . . . . . . 8
140 0red 9662 . . . . . . . . . 10
14145peano2zd 11066 . . . . . . . . . . . . . 14
1425, 141syl5eqel 2553 . . . . . . . . . . . . 13
143142adantr 472 . . . . . . . . . . . 12
144143zred 11063 . . . . . . . . . . 11
145144adantr 472 . . . . . . . . . 10
14667ad2antrr 740 . . . . . . . . . 10
147 ioodvbdlimc1lem2OLD.n . . . . . . . . . . . . . 14
148 ioodvbdlimc1lem2OLD.y . . . . . . . . . . . . . . . . . . . 20
149 ioomidp 37711 . . . . . . . . . . . . . . . . . . . . . . . 24
1507, 6, 9, 149syl3anc 1292 . . . . . . . . . . . . . . . . . . . . . . 23
151 ne0i 3728 . . . . . . . . . . . . . . . . . . . . . . 23
152150, 151syl 17 . . . . . . . . . . . . . . . . . . . . . 22
153 ioossre 11721 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
154153a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
155 dvfre 22984 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
15626, 154, 155syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . 26
157109feq2d 5725 . . . . . . . . . . . . . . . . . . . . . . . . . 26
158156, 157mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . . 25
159158ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . . . 24
160159recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
161160abscld 13575 . . . . . . . . . . . . . . . . . . . . . 22
162 eqid 2471 . . . . . . . . . . . . . . . . . . . . . 22
163 eqid 2471 . . . . . . . . . . . . . . . . . . . . . 22
164152, 161, 110, 162, 163suprnmpt 37512 . . . . . . . . . . . . . . . . . . . . 21
165164simpld 466 . . . . . . . . . . . . . . . . . . . 20
166148, 165syl5eqel 2553 . . . . . . . . . . . . . . . . . . 19
167166adantr 472 . . . . . . . . . . . . . . . . . 18
168 rpre 11331 . . . . . . . . . . . . . . . . . . . 20
169168rehalfcld 10882 . . . . . . . . . . . . . . . . . . 19
170169adantl 473 . . . . . . . . . . . . . . . . . 18
171168recnd 9687 . . . . . . . . . . . . . . . . . . . 20
172171adantl 473 . . . . . . . . . . . . . . . . . . 19
173 2cnd 10704 . . . . . . . . . . . . . . . . . . 19
174 rpne0 11340 . . . . . . . . . . . . . . . . . . . 20
175174adantl 473 . . . . . . . . . . . . . . . . . . 19
176 2ne0 10724 . . . . . . . . . . . . . . . . . . . 20
177176a1i 11 . . . . . . . . . . . . . . . . . . 19
178172, 173, 175, 177divne0d 10421 . . . . . . . . . . . . . . . . . 18
179167, 170, 178redivcld 10457 . . . . . . . . . . . . . . . . 17
180179flcld 12067 . . . . . . . . . . . . . . . 16
181180peano2zd 11066 . . . . . . . . . . . . . . 15
182181, 143ifcld 3915 . . . . . . . . . . . . . 14
183147, 182syl5eqel 2553 . . . . . . . . . . . . 13
184183zred 11063 . . . . . . . . . . . 12
185184adantr 472 . . . . . . . . . . 11
186181zred 11063 . . . . . . . . . . . . . 14
187 max1 11503 . . . . . . . . . . . . . 14
188144, 186, 187syl2anc 673 . . . . . . . . . . . . 13
189188, 147syl6breqr 4436 . . . . . . . . . . . 12
190189adantr 472 . . . . . . . . . . 11
191 eluzle 11195 . . . . . . . . . . . 12
192191adantl 473 . . . . . . . . . . 11
193145, 185, 139, 190, 192letrd 9809 . . . . . . . . . 10
194140, 145, 139, 146, 193ltletrd 9812 . . . . . . . . 9
195194gt0ne0d 10199 . . . . . . . 8
196139, 195rereccld 10456 . . . . . . 7
197139, 194recgt0d 10563 . . . . . . 7
198196, 197elrpd 11361 . . . . . 6
199198adantr 472 . . . . 5
200 ioodvbdlimc1lem2OLD.ch . . . . . . . . 9
201200biimpi 199 . . . . . . . . . . . . . . . . 17
202 simp-5l 786 . . . . . . . . . . . . . . . . 17
203201, 202syl 17 . . . . . . . . . . . . . . . 16
204203, 26syl 17 . . . . . . . . . . . . . . 15
205201simplrd 771 . . . . . . . . . . . . . . 15
206204, 205ffvelrnd 6038 . . . . . . . . . . . . . 14
207206recnd 9687 . . . . . . . . . . . . 13
208203, 108syl 17 . . . . . . . . . . . . . . 15
209 simp-5r 787 . . . . . . . . . . . . . . . . . . 19
210201, 209syl 17 . . . . . . . . . . . . . . . . . 18
211 eluz2 11188 . . . . . . . . . . . . . . . . . . 19
212143, 183, 189, 211syl3anbrc 1214 . . . . . . . . . . . . . . . . . 18
213203, 210, 212syl2anc 673 . . . . . . . . . . . . . . . . 17
214 uzss 11203 . . . . . . . . . . . . . . . . 17
215213, 214syl 17 . . . . . . . . . . . . . . . 16
216 simp-4r 785 . . . . . . . . . . . . . . . . 17
217201, 216syl 17 . . . . . . . . . . . . . . . 16
218215, 217sseldd 3419 . . . . . . . . . . . . . . 15
219208, 218ffvelrnd 6038 . . . . . . . . . . . . . 14
220219recnd 9687 . . . . . . . . . . . . 13
221203, 137syl 17 . . . . . . . . . . . . 13
222207, 220, 221npncand 10029 . . . . . . . . . . . 12
223222eqcomd 2477 . . . . . . . . . . 11
224223fveq2d 5883 . . . . . . . . . 10
225206, 219resubcld 10068 . . . . . . . . . . . . . 14
226203, 136syl 17 . . . . . . . . . . . . . . 15
227219, 226resubcld 10068 . . . . . . . . . . . . . 14
228225, 227readdcld 9688 . . . . . . . . . . . . 13
229228recnd 9687 . . . . . . . . . . . 12
230229abscld 13575 . . . . . . . . . . 11
231225recnd 9687 . . . . . . . . . . . . 13
232231abscld 13575 . . . . . . . . . . . 12
233227recnd 9687 . . . . . . . . . . . . 13
234233abscld 13575 . . . . . . . . . . . 12
235232, 234readdcld 9688 . . . . . . . . . . 11
236210rpred 11364 . . . . . . . . . . 11
237231, 233abstrid 13595 . . . . . . . . . . 11
238236rehalfcld 10882 . . . . . . . . . . . . 13
239207, 220abssubd 13592 . . . . . . . . . . . . . 14
240203, 218, 115syl2anc 673 . . . . . . . . . . . . . . . . 17
241240oveq1d 6323 . . . . . . . . . . . . . . . 16
242241fveq2d 5883 . . . . . . . . . . . . . . 15
243203, 218, 106syl2anc 673 . . . . . . . . . . . . . . . . . . 19
244243, 206resubcld 10068 . . . . . . . . . . . . . . . . . 18
245244recnd 9687 . . . . . . . . . . . . . . . . 17
246245abscld 13575 . . . . . . . . . . . . . . . 16
247203, 166syl 17 . . . . . . . . . . . . . . . . 17
248203, 218, 58syl2anc 673 . . . . . . . . . . . . . . . . . 18
249153, 205sseldi 3416 . . . . . . . . . . . . . . . . . 18
250248, 249resubcld 10068 . . . . . . . . . . . . . . . . 17
251247, 250remulcld 9689 . . . . . . . . . . . . . . . 16
252203, 7syl 17 . . . . . . . . . . . . . . . . . 18
253203, 6syl 17 . . . . . . . . . . . . . . . . . 18
254203, 109syl 17 . . . . . . . . . . . . . . . . . 18
255164simprd 470 . . . . . . . . . . . . . . . . . . . . 21
256148breq2i 4403 . . . . . . . . . . . . . . . . . . . . . 22
257256ralbii 2823 . . . . . . . . . . . . . . . . . . . . 21
258255, 257sylibr 217 . . . . . . . . . . . . . . . . . . . 20
259203, 258syl 17 . . . . . . . . . . . . . . . . . . 19
260 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . 22
261260fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21
262261breq1d 4405 . . . . . . . . . . . . . . . . . . . 20
263262cbvralv 3005 . . . . . . . . . . . . . . . . . . 19
264259, 263sylibr 217 . . . . . . . . . . . . . . . . . 18
265249rexrd 9708 . . . . . . . . . . . . . . . . . . 19
266203, 30syl 17 . . . . . . . . . . . . . . . . . . 19
267249, 252resubcld 10068 . . . . . . . . . . . . . . . . . . . . 21
268267recnd 9687 . . . . . . . . . . . . . . . . . . . . . 22
269268abscld 13575 . . . . . . . . . . . . . . . . . . . . 21
2703, 218sseldi 3416 . . . . . . . . . . . . . . . . . . . . . 22
271203, 218, 56syl2anc 673 . . . . . . . . . . . . . . . . . . . . . 22
272270, 271rereccld 10456 . . . . . . . . . . . . . . . . . . . . 21
273267leabsd 13553 . . . . . . . . . . . . . . . . . . . . 21
274201simprd 470 . . . . . . . . . . . . . . . . . . . . 21
275267, 269, 272, 273, 274lelttrd 9810 . . . . . . . . . . . . . . . . . . . 20
276249, 252, 272ltsubadd2d 10232 . . . . . . . . . . . . . . . . . . . 20
277275, 276mpbid 215 . . . . . . . . . . . . . . . . . . 19
278203, 218, 104syl2anc 673 . . . . . . . . . . . . . . . . . . 19
279265, 266, 248, 277, 278eliood 37691 . . . . . . . . . . . . . . . . . 18
280252, 253, 204, 254, 247, 264, 205, 279dvbdfbdioolem1 37897 . . . . . . . . . . . . . . . . 17
281280simpld 466 . . . . . . . . . . . . . . . 16
282203, 218, 57syl2anc 673 . . . . . . . . . . . . . . . . . 18
283247, 282remulcld 9689 . . . . . . . . . . . . . . . . 17
284158, 150ffvelrnd 6038 . . . . . . . . . . . . . . . . . . . . . 22
285284recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
286285abscld 13575 . . . . . . . . . . . . . . . . . . . 20
287285absge0d 13583 . . . . . . . . . . . . . . . . . . . 20
288 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24
289288fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . 23
290148eqcomi 2480 . . . . . . . . . . . . . . . . . . . . . . . 24
291290a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
292289, 291breq12d 4408 . . . . . . . . . . . . . . . . . . . . . 22
293292rspcva 3134 . . . . . . . . . . . . . . . . . . . . 21
294150, 255, 293syl2anc 673 . . . . . . . . . . . . . . . . . . . 20
29514, 286, 166, 287, 294letrd 9809 . . . . . . . . . . . . . . . . . . 19
296203, 295syl 17 . . . . . . . . . . . . . . . . . 18
297203, 28syl 17 . . . . . . . . . . . . . . . . . . . . . 22
298 ioogtlb 37688 . . . . . . . . . . . . . . . . . . . . . 22
299297, 266, 205, 298syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21
300252, 249, 248, 299ltsub2dd 10247 . . . . . . . . . . . . . . . . . . . 20
301203, 98syl 17 . . . . . . . . . . . . . . . . . . . . 21
302282recnd 9687 . . . . . . . . . . . . . . . . . . . . 21
303301, 302pncan2d 10007 . . . . . . . . . . . . . . . . . . . 20
304300, 303breqtrd 4420 . . . . . . . . . . . . . . . . . . 19
305250, 272, 304ltled 9800 . . . . . . . . . . . . . . . . . 18
306250, 272, 247, 296, 305lemul2ad 10569 . . . . . . . . . . . . . . . . 17
307283adantr 472 . . . . . . . . . . . . . . . . . . 19
308238adantr 472 . . . . . . . . . . . . . . . . . . 19
309 oveq1 6315 . . . . . . . . . . . . . . . . . . . . 21
310302mul02d 9849 . . . . . . . . . . . . . . . . . . . . 21
311309, 310sylan9eqr 2527 . . . . . . . . . . . . . . . . . . . 20
312210rphalfcld 11376 . . . . . . . . . . . . . . . . . . . . . 22
313312rpgt0d 11367 . . . . . . . . . . . . . . . . . . . . 21
314313adantr 472 . . . . . . . . . . . . . . . . . . . 20
315311, 314eqbrtrd 4416 . . . . . . . . . . . . . . . . . . 19
316307, 308, 315ltled 9800 . . . . . . . . . . . . . . . . . 18
317247adantr 472 . . . . . . . . . . . . . . . . . . . 20
318296adantr 472 . . . . . . . . . . . . . . . . . . . 20
319 neqne 2651 . . . . . . . . . . . . . . . . . . . . 21
320319adantl 473 . . . . . . . . . . . . . . . . . . . 20
321317, 318, 320ne0gt0d 9789 . . . . . . . . . . . . . . . . . . 19
322283adantr 472 . . . . . . . . . . . . . . . . . . . 20
3233, 213sseldi 3416 . . . . . . . . . . . . . . . . . . . . . . 23
324 0red 9662 . . . . . . . . . . . . . . . . . . . . . . . . 25
325203, 210, 144syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25
326203, 67syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25
327203, 210, 189syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . 25
328324, 325, 323, 326, 327ltletrd 9812 . . . . . . . . . . . . . . . . . . . . . . . 24
329328gt0ne0d 10199 . . . . . . . . . . . . . . . . . . . . . . 23
330323, 329rereccld 10456 . . . . . . . . . . . . . . . . . . . . . 22
331247, 330remulcld 9689 . . . . . . . . . . . . . . . . . . . . 21
332331adantr 472 . . . . . . . . . . . . . . . . . . . 20
333238adantr 472 . . . . . . . . . . . . . . . . . . . 20
334282adantr 472 . . . . . . . . . . . . . . . . . . . . 21
335330adantr 472 . . . . . . . . . . . . . . . . . . . . 21
336247adantr 472 . . . . . . . . . . . . . . . . . . . . 21
337296adantr 472 . . . . . . . . . . . . . . . . . . . . 21
338323, 328elrpd 11361 . . . . . . . . . . . . . . . . . . . . . . 23
339203, 218, 59syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . 23
340 1red 9676 . . . . . . . . . . . . . . . . . . . . . . 23
34176a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
342217, 191syl 17 . . . . . . . . . . . . . . . . . . . . . . 23
343338, 339, 340, 341, 342lediv2ad 11386 . . . . . . . . . . . . . . . . . . . . . 22
344343adantr 472 . . . . . . . . . . . . . . . . . . . . 21
345334, 335, 336, 337, 344lemul2ad 10569 . . . . . . . . . . . . . . . . . . . 20
346236recnd 9687 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
347 2cnd 10704 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
348210rpne0d 11369 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
349176a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
350346, 347, 348, 349divne0d 10421 . . . . . . . . . . . . . . . . . . . . . . . . . 26
351247, 238, 350redivcld 10457 . . . . . . . . . . . . . . . . . . . . . . . . 25
352351adantr 472 . . . . . . . . . . . . . . . . . . . . . . . 24
353 simpr 468 . . . . . . . . . . . . . . . . . . . . . . . . 25
354313adantr 472 . . . . . . . . . . . . . . . . . . . . . . . . 25
355336, 333, 353, 354divgt0d 10564 . . . . . . . . . . . . . . . . . . . . . . . 24
356352, 355elrpd 11361 . . . . . . . . . . . . . . . . . . . . . . 23
357356rprecred 11375 . . . . . . . . . . . . . . . . . . . . . 22
358338adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
359 1red 9676 . . . . . . . . . . . . . . . . . . . . . . 23
36076a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23
361351flcld 12067 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
362361peano2zd 11066 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
363362zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . 26
364203, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
365362, 364ifcld 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
366147, 365syl5eqel 2553 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
367366zred 11063 . . . . . . . . . . . . . . . . . . . . . . . . . 26
368 flltp1 12069 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
369351, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26
370203, 62syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
371 max2 11505 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
372370, 363, 371syl2anc 673 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
373372, 147syl6breqr 4436 . . . . . . . . . . . . . . . . . . . . . . . . . 26
374351, 363, 367, 369, 373ltletrd 9812 . . . . . . . . . . . . . . . . . . . . . . . . 25
375351, 323, 374ltled 9800 . . . . . . . . . . . . . . . . . . . . . . . 24
376375adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
377356, 358, 359, 360, 376lediv2ad 11386 . . . . . . . . . . . . . . . . . . . . . 22
378335, 357, 336, 337, 377lemul2ad 10569 . . . . . . . . . . . . . . . . . . . . 21
379336recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
380352recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
381355gt0ne0d 10199 . . . . . . . . . . . . . . . . . . . . . . 23
382379, 380, 381divrecd 10408 . . . . . . . . . . . . . . . . . . . . . 22
383333recnd 9687 . . . . . . . . . . . . . . . . . . . . . . 23
384353gt0ne0d 10199 . . . . . . . . . . . . . . . . . . . . . . 23
385350adantr 472 . . . . . . . . . . . . . . . . . . . . . . 23
386379, 383, 384, 385ddcand 10425 . . . . . . . . . . . . . . . . . . . . . 22
387382, 386eqtr3d 2507 . . . . . . . . . . . . . . . . . . . . 21
388378, 387breqtrd 4420 . . . . . . . . . . . . . . . . . . . 20
389322, 332, 333, 345, 388letrd 9809 . . . . . . . . . . . . . . . . . . 19
390321, 389syldan 478 . . . . . . . . . . . . . . . . . 18
391316, 390pm2.61dan 808 . . . . . . . . . . . . . . . . 17
392251, 283, 238, 306, 391letrd 9809 . . . . . . . . . . . . . . . 16
393246, 251, 238, 281, 392letrd 9809 . . . . . . . . . . . . . . 15
394242, 393eqbrtrd 4416 . . . . . . . . . . . . . 14
395239, 394eqbrtrd 4416 . . . . . . . . . . . . 13
396 simpllr 777 . . . . . . . . . . . . . 14
397201, 396syl 17 . . . . . . . . . . . . 13
398232, 234, 238, 238, 395, 397leltaddd 10256 . . . . . . . . . . . 12
3993462halvesd 10881 . . . . . . . . . . . 12
400398, 399breqtrd 4420 . . . . . . . . . . 11
401230, 235, 236, 237, 400lelttrd 9810 . . . . . . . . . 10
402224, 401eqbrtrd 4416 . . . . . . . . 9
403200, 402sylbir 218 . . . . . . . 8
404403adantrl 730 . . . . . . 7
405404ex 441 . . . . . 6
406405ralrimiva 2809 . . . . 5
407 breq2 4399 . . . . . . . . 9
408407anbi2d 718 . . . . . . . 8
409408imbi1d 324 . . . . . . 7
410409ralbidv 2829 . . . . . 6
411410rspcev 3136 . . . . 5
412199, 406, 411syl2anc 673 . . . 4
413 simpr 468 . . . . . . . . . . 11
414413iftrued 3880 . . . . . . . . . 10
415 uzid 11197 . . . . . . . . . . . 12
416183, 415syl 17 . . . . . . . . . . 11
417416adantr 472 . . . . . . . . . 10
418414, 417eqeltrd 2549 . . . . . . . . 9
419418adantlr 729 . . . . . . . 8
420 iffalse 3881 . . . . . . . . . 10
421420adantl 473 . . . . . . . . 9
422183ad2antrr 740 . . . . . . . . . 10
423 simplr 770 . . . . . . . . . 10
424422zred 11063 . . . . . . . . . . 11
425423zred 11063 . . . . . . . . . . 11
426 simpr 468 . . . . . . . . . . . 12
427424, 425ltnled 9799 . . . . . . . . . . . 12
428426, 427mpbird 240 . . . . . . . . . . 11
429424, 425, 428ltled 9800 . . . . . . . . . 10
430 eluz2 11188 . . . . . . . . . 10
431422, 423, 429, 430syl3anbrc 1214 . . . . . . . . 9
432421, 431eqeltrd 2549 . . . . . . . 8
433419, 432pm2.61dan 808 . . . . . . 7
434433adantr 472 . . . . . 6
435 simpr 468 . . . . . . . 8
436 simpr 468 . . . . . . . . . 10
437183adantr 472 . . . . . . . . . . 11
438437, 436ifcld 3915 . . . . . . . . . 10
439436zred 11063 . . . . . . . . . . 11
440437zred 11063 . . . . . . . . . . 11
441 max1 11503 . . . . . . . . . . 11
442439, 440, 441syl2anc 673 . . . . . . . . . 10
443 eluz2 11188 . . . . . . . . . 10
444436, 438, 442, 443syl3anbrc 1214 . . . . . . . . 9
445444adantr 472 . . . . . . . 8
446 fveq2 5879 . . . . . . . . . . 11
447446eleq1d 2533 . . . . . . . . . 10
448446oveq1d 6323 . . . . . . . . . . . 12
449448fveq2d 5883 . . . . . . . . . . 11
450449breq1d 4405 . . . . . . . . . 10
451447, 450anbi12d 725 . . . . . . . . 9
452451rspccva 3135 . . . . . . . 8
453435, 445, 452syl2anc 673 . . . . . . 7
454453simprd 470 . . . . . 6
455 fveq2 5879 . . . . . . . . . 10
456455oveq1d 6323 . . . . . . . . 9
457456fveq2d 5883 . . . . . . . 8
458457breq1d 4405 . . . . . . 7
459458rspcev 3136 . . . . . 6
460434, 454, 459syl2anc 673 . . . . 5
461 ax-resscn 9614 . . . . . . . . . . . . . 14
462461a1i 11 . . . . . . . . . . . . 13
46326, 462fssd 5750 . . . . . . . . . . . . . 14
464 dvcn 22954 . . . . . . . . . . . . . 14
465462, 463, 154, 109, 464syl31anc 1295 . . . . . . . . . . . . 13
466 cncffvrn 22008 . . . . . . . . . . . . 13
467462, 465, 466syl2anc 673 . . . . . . . . . . . 12
46826, 467mpbird 240 . . . . . . . . . . 11
469 ioodvbdlimc1lem2OLD.r . . . . . . . . . . . 12
470105, 469fmptd 6061 . . . . . . . . . . 11
471 eqid 2471 . . . . . . . . . . 11
472 climrel 13633 . . . . . . . . . . . . 13
473472a1i 11 . . . . . . . . . . . 12
474 fvex 5889 . . . . . . . . . . . . . . . . 17
475474mptex 6152 . . . . . . . . . . . . . . . 16
476475a1i 11 . . . . . . . . . . . . . . 15
477 eqidd 2472 . . . . . . . . . . . . . . . 16
478 eqidd 2472 . . . . . . . . . . . . . . . 16
479 simpr 468 . . . . . . . . . . . . . . . 16
4807adantr 472 . . . . . . . . . . . . . . . 16
481477, 478, 479, 480fvmptd 5969 . . . . . . . . . . . . . . 15
48223, 142, 476, 98, 481climconst 13684 . . . . . . . . . . . . . 14
483474mptex 6152 . . . . . . . . . . . . . . . 16
484469, 483eqeltri 2545 . . . . . . . . . . . . . . 15
485484a1i 11 . . . . . . . . . . . . . 14
486 1cnd 9677 . . . . . . . . . . . . . . 15
487 elnnnn0b 10938 . . . . . . . . . . . . . . . 16
48821, 67, 487sylanbrc 677 . . . . . . . . . . . . . . 15
489 divcnvg 37804 . . . . . . . . . . . . . . 15
490486, 488, 489syl2anc 673 . . . . . . . . . . . . . 14
491 eqidd 2472 . . . . . . . . . . . . . . . 16
492 eqidd 2472 . . . . . . . . . . . . . . . 16
493 simpr 468 . . . . . . . . . . . . . . . 16
4947adantr 472 . . . . . . . . . . . . . . . 16
495491, 492, 493, 494fvmptd 5969 . . . . . . . . . . . . . . 15
49698adantr 472 . . . . . . . . . . . . . . 15
497495, 496eqeltrd 2549 . . . . . . . . . . . . . 14
498 eqidd 2472 . . . . . . . . . . . . . . . 16
499 oveq2 6316 . . . . . . . . . . . . . . . . 17
500499adantl 473 . . . . . . . . . . . . . . . 16
5013, 493sseldi 3416 . . . . . . . . . . . . . . . . 17
502 0red 9662 . . . . . . . . . . . . . . . . . . 19
50362adantr 472 . . . . . . . . . . . . . . . . . . 19
50467adantr 472 . . . . . . . . . . . . . . . . . . 19
505 eluzle 11195 . . . . . . . . . . . . . . . . . . . 20
506505adantl 473 . . . . . . . . . . . . . . . . . . 19
507502, 503, 501, 504, 506ltletrd 9812 . . . . . . . . . . . . . . . . . 18
508507gt0ne0d 10199 . . . . . . . . . . . . . . . . 17
509501, 508rereccld 10456 . . . . . . . . . . . . . . . 16
510498, 500, 493, 509fvmptd 5969 . . . . . . . . . . . . . . 15
511501recnd 9687 . . . . . . . . . . . . . . . 16
512511, 508reccld 10398 . . . . . . . . . . . . . . 15
513510, 512eqeltrd 2549 . . . . . . . . . . . . . 14
514469a1i 11 . . . . . . . . . . . . . . . 16
515499oveq2d 6324 . . . . . . . . . . . . . . . . 17
516515adantl 473 . . . . . . . . . . . . . . . 16
517494, 509readdcld 9688 . . . . . . . . . . . . . . . 16
518514, 516, 493, 517fvmptd 5969 . . . . . . . . . . . . . . 15
519495, 510oveq12d 6326 . . . . . . . . . . . . . . 15