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

Theorem dvbdfbdioolem2 31929
 Description: A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
dvbdfbdioolem2.a
dvbdfbdioolem2.b
dvbdfbdioolem2.altb
dvbdfbdioolem2.f
dvbdfbdioolem2.dmdv
dvbdfbdioolem2.k
dvbdfbdioolem2.dvbd
dvbdfbdioolem2.m
Assertion
Ref Expression
dvbdfbdioolem2
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem dvbdfbdioolem2
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dvbdfbdioolem2.f . . . . . . . 8
21ffvelrnda 6032 . . . . . . 7
32recnd 9639 . . . . . 6
43abscld 13279 . . . . 5
5 dvbdfbdioolem2.a . . . . . . . . . . 11
65rexrd 9660 . . . . . . . . . 10
7 dvbdfbdioolem2.b . . . . . . . . . . 11
87rexrd 9660 . . . . . . . . . 10
95, 7readdcld 9640 . . . . . . . . . . 11
109rehalfcld 10806 . . . . . . . . . 10
11 dvbdfbdioolem2.altb . . . . . . . . . . 11
12 avglt1 10797 . . . . . . . . . . . 12
135, 7, 12syl2anc 661 . . . . . . . . . . 11
1411, 13mpbid 210 . . . . . . . . . 10
15 avglt2 10798 . . . . . . . . . . . 12
165, 7, 15syl2anc 661 . . . . . . . . . . 11
1711, 16mpbid 210 . . . . . . . . . 10
186, 8, 10, 14, 17eliood 31734 . . . . . . . . 9
191, 18ffvelrnd 6033 . . . . . . . 8
2019recnd 9639 . . . . . . 7
2120abscld 13279 . . . . . 6
2221adantr 465 . . . . 5
234, 22resubcld 10008 . . . 4
24 dvbdfbdioolem2.k . . . . . 6
2524adantr 465 . . . . 5
267adantr 465 . . . . . 6
275adantr 465 . . . . . 6
2826, 27resubcld 10008 . . . . 5
2925, 28remulcld 9641 . . . 4
3020adantr 465 . . . . . . 7
313, 30subcld 9950 . . . . . 6
3231abscld 13279 . . . . 5
333, 30abs2difd 13300 . . . . 5
34 simpll 753 . . . . . . 7
3510rexrd 9660 . . . . . . . . 9
3635ad2antrr 725 . . . . . . . 8
378ad2antrr 725 . . . . . . . 8
38 elioore 11584 . . . . . . . . . 10
3938adantl 466 . . . . . . . . 9
4039adantr 465 . . . . . . . 8
41 simpr 461 . . . . . . . 8
426adantr 465 . . . . . . . . . 10
438adantr 465 . . . . . . . . . 10
44 simpr 461 . . . . . . . . . 10
45 iooltub 31751 . . . . . . . . . 10
4642, 43, 44, 45syl3anc 1228 . . . . . . . . 9
4746adantr 465 . . . . . . . 8
4836, 37, 40, 41, 47eliood 31734 . . . . . . 7
495adantr 465 . . . . . . . . 9
507adantr 465 . . . . . . . . 9
511adantr 465 . . . . . . . . 9
52 dvbdfbdioolem2.dmdv . . . . . . . . . 10
5352adantr 465 . . . . . . . . 9
5424adantr 465 . . . . . . . . 9
55 dvbdfbdioolem2.dvbd . . . . . . . . . . 11
56 fveq2 5872 . . . . . . . . . . . . . 14
5756fveq2d 5876 . . . . . . . . . . . . 13
5857breq1d 4466 . . . . . . . . . . . 12
5958cbvralv 3084 . . . . . . . . . . 11
6055, 59sylib 196 . . . . . . . . . 10
6160adantr 465 . . . . . . . . 9
6218adantr 465 . . . . . . . . 9
63 simpr 461 . . . . . . . . 9
6449, 50, 51, 53, 54, 61, 62, 63dvbdfbdioolem1 31928 . . . . . . . 8
6564simprd 463 . . . . . . 7
6634, 48, 65syl2anc 661 . . . . . 6
67 fveq2 5872 . . . . . . . . . . . . . 14
6867eqcomd 2465 . . . . . . . . . . . . 13
6968adantl 466 . . . . . . . . . . . 12
7020adantr 465 . . . . . . . . . . . 12
7169, 70eqeltrd 2545 . . . . . . . . . . 11
7271, 69subeq0bd 10006 . . . . . . . . . 10
7372abs00bd 13136 . . . . . . . . 9
7424adantr 465 . . . . . . . . . 10
757adantr 465 . . . . . . . . . . 11
765adantr 465 . . . . . . . . . . 11
7775, 76resubcld 10008 . . . . . . . . . 10
78 0red 9614 . . . . . . . . . . . 12
79 ioossre 11611 . . . . . . . . . . . . . . . 16
80 dvfre 22480 . . . . . . . . . . . . . . . 16
811, 79, 80sylancl 662 . . . . . . . . . . . . . . 15
8218, 52eleqtrrd 2548 . . . . . . . . . . . . . . 15
8381, 82ffvelrnd 6033 . . . . . . . . . . . . . 14
8483recnd 9639 . . . . . . . . . . . . 13
8584abscld 13279 . . . . . . . . . . . 12
8684absge0d 13287 . . . . . . . . . . . 12
87 fveq2 5872 . . . . . . . . . . . . . . . 16
8887fveq2d 5876 . . . . . . . . . . . . . . 15
8988breq1d 4466 . . . . . . . . . . . . . 14
9089rspccva 3209 . . . . . . . . . . . . 13
9155, 18, 90syl2anc 661 . . . . . . . . . . . 12
9278, 85, 24, 86, 91letrd 9756 . . . . . . . . . . 11
9392adantr 465 . . . . . . . . . 10
947, 5resubcld 10008 . . . . . . . . . . . 12
955, 7posdifd 10160 . . . . . . . . . . . . 13
9611, 95mpbid 210 . . . . . . . . . . . 12
9778, 94, 96ltled 9750 . . . . . . . . . . 11
9897adantr 465 . . . . . . . . . 10
9974, 77, 93, 98mulge0d 10150 . . . . . . . . 9
10073, 99eqbrtrd 4476 . . . . . . . 8
101100adant423 31628 . . . . . . 7
102 simpll 753 . . . . . . . 8
10339ad2antrr 725 . . . . . . . . 9
10410ad3antrrr 729 . . . . . . . . 9
10539adantr 465 . . . . . . . . . . 11
10610ad2antrr 725 . . . . . . . . . . 11
107 simpr 461 . . . . . . . . . . 11
108105, 106, 107nltled 31680 . . . . . . . . . 10
109108adantr 465 . . . . . . . . 9
110 neqne 31637 . . . . . . . . . 10
111110adantl 466 . . . . . . . . 9
112103, 104, 109, 111leneltd 31697 . . . . . . . 8
1133, 30abssubd 13296 . . . . . . . . . 10
114113adantr 465 . . . . . . . . 9
1155ad2antrr 725 . . . . . . . . . . 11
1167ad2antrr 725 . . . . . . . . . . 11
1171ad2antrr 725 . . . . . . . . . . 11
11852ad2antrr 725 . . . . . . . . . . 11
11924ad2antrr 725 . . . . . . . . . . 11
12060ad2antrr 725 . . . . . . . . . . 11
12144adantr 465 . . . . . . . . . . 11
12238rexrd 9660 . . . . . . . . . . . . 13
123122ad2antlr 726 . . . . . . . . . . . 12
1248ad2antrr 725 . . . . . . . . . . . 12
12510ad2antrr 725 . . . . . . . . . . . 12
126 simpr 461 . . . . . . . . . . . 12
12717ad2antrr 725 . . . . . . . . . . . 12
128123, 124, 125, 126, 127eliood 31734 . . . . . . . . . . 11
129115, 116, 117, 118, 119, 120, 121, 128dvbdfbdioolem1 31928 . . . . . . . . . 10
130129simprd 463 . . . . . . . . 9
131114, 130eqbrtrd 4476 . . . . . . . 8
132102, 112, 131syl2anc 661 . . . . . . 7
133101, 132pm2.61dan 791 . . . . . 6
13466, 133pm2.61dan 791 . . . . 5
13523, 32, 29, 33, 134letrd 9756 . . . 4
13623, 29, 22, 135leadd1dd 10187 . . 3
1374recnd 9639 . . . . 5
13822recnd 9639 . . . . 5
139137, 138npcand 9954 . . . 4
140139eqcomd 2465 . . 3
141 dvbdfbdioolem2.m . . . . 5
14221recnd 9639 . . . . . 6
14324recnd 9639 . . . . . . 7
1447recnd 9639 . . . . . . . 8
1455recnd 9639 . . . . . . . 8
146144, 145subcld 9950 . . . . . . 7
147143, 146mulcld 9633 . . . . . 6
148142, 147addcomd 9799 . . . . 5
149141, 148syl5eq 2510 . . . 4