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

Theorem ioodvbdlimc1lem2 37901
 Description: Limit at the lower 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
ioodvbdlimc1lem2.a
ioodvbdlimc1lem2.b
ioodvbdlimc1lem2.altb
ioodvbdlimc1lem2.f
ioodvbdlimc1lem2.dmdv
ioodvbdlimc1lem2.dvbd
ioodvbdlimc1lem2.y
ioodvbdlimc1lem2.m
ioodvbdlimc1lem2.s
ioodvbdlimc1lem2.r
ioodvbdlimc1lem2.n
ioodvbdlimc1lem2.ch
Assertion
Ref Expression
ioodvbdlimc1lem2 lim
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,   ,,   ,,,   ,,,,   ,   ,,,,
Allowed substitution hints:   (,,,)   ()   ()   (,)   (,,)

Proof of Theorem ioodvbdlimc1lem2
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 ioodvbdlimc1lem2.m . . . . . . 7
6 ioodvbdlimc1lem2.b . . . . . . . . . . 11
7 ioodvbdlimc1lem2.a . . . . . . . . . . 11
86, 7resubcld 10068 . . . . . . . . . 10
9 ioodvbdlimc1lem2.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 ioodvbdlimc1lem2.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 ioodvbdlimc1lem2.s . . . . 5
108106, 107fmptd 6061 . . . 4
109 ioodvbdlimc1lem2.dmdv . . . . . 6
110 ioodvbdlimc1lem2.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, 135limsupre 37818 . . 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 ioodvbdlimc1lem2.n . . . . . . . . . . . . . 14
148 ioodvbdlimc1lem2.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 ioodvbdlimc1lem2.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 ioodvbdlimc1lem2.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