Metamath Proof Explorer


Theorem dvbdfbdioo

Description: A function on an open interval, with bounded derivative, is bounded. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses dvbdfbdioo.a φ A
dvbdfbdioo.b φ B
dvbdfbdioo.altb φ A < B
dvbdfbdioo.f φ F : A B
dvbdfbdioo.dmdv φ dom F = A B
dvbdfbdioo.dvbd φ a x A B F x a
Assertion dvbdfbdioo φ b x A B F x b

Proof

Step Hyp Ref Expression
1 dvbdfbdioo.a φ A
2 dvbdfbdioo.b φ B
3 dvbdfbdioo.altb φ A < B
4 dvbdfbdioo.f φ F : A B
5 dvbdfbdioo.dmdv φ dom F = A B
6 dvbdfbdioo.dvbd φ a x A B F x a
7 1 rexrd φ A *
8 2 rexrd φ B *
9 1 2 readdcld φ A + B
10 9 rehalfcld φ A + B 2
11 avglt1 A B A < B A < A + B 2
12 1 2 11 syl2anc φ A < B A < A + B 2
13 3 12 mpbid φ A < A + B 2
14 avglt2 A B A < B A + B 2 < B
15 1 2 14 syl2anc φ A < B A + B 2 < B
16 3 15 mpbid φ A + B 2 < B
17 7 8 10 13 16 eliood φ A + B 2 A B
18 4 17 ffvelrnd φ F A + B 2
19 18 recnd φ F A + B 2
20 19 abscld φ F A + B 2
21 20 ad2antrr φ a x A B F x a F A + B 2
22 simplr φ a x A B F x a a
23 2 ad2antrr φ a x A B F x a B
24 1 ad2antrr φ a x A B F x a A
25 23 24 resubcld φ a x A B F x a B A
26 22 25 remulcld φ a x A B F x a a B A
27 21 26 readdcld φ a x A B F x a F A + B 2 + a B A
28 3 ad2antrr φ a x A B F x a A < B
29 4 ad2antrr φ a x A B F x a F : A B
30 5 ad2antrr φ a x A B F x a dom F = A B
31 2fveq3 x = y F x = F y
32 31 breq1d x = y F x a F y a
33 32 cbvralvw x A B F x a y A B F y a
34 33 biimpi x A B F x a y A B F y a
35 34 adantl φ a x A B F x a y A B F y a
36 eqid F A + B 2 + a B A = F A + B 2 + a B A
37 24 23 28 29 30 22 35 36 dvbdfbdioolem2 φ a x A B F x a y A B F y F A + B 2 + a B A
38 2fveq3 x = y F x = F y
39 38 breq1d x = y F x b F y b
40 39 cbvralvw x A B F x b y A B F y b
41 breq2 b = F A + B 2 + a B A F y b F y F A + B 2 + a B A
42 41 ralbidv b = F A + B 2 + a B A y A B F y b y A B F y F A + B 2 + a B A
43 40 42 syl5bb b = F A + B 2 + a B A x A B F x b y A B F y F A + B 2 + a B A
44 43 rspcev F A + B 2 + a B A y A B F y F A + B 2 + a B A b x A B F x b
45 27 37 44 syl2anc φ a x A B F x a b x A B F x b
46 45 6 r19.29a φ b x A B F x b