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 
|- ( ph -> A e. RR )
dvbdfbdioo.b 
|- ( ph -> B e. RR )
dvbdfbdioo.altb 
|- ( ph -> A < B )
dvbdfbdioo.f 
|- ( ph -> F : ( A (,) B ) --> RR )
dvbdfbdioo.dmdv 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvbdfbdioo.dvbd 
|- ( ph -> E. a e. RR A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ a )
Assertion dvbdfbdioo 
|- ( ph -> E. b e. RR A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ b )

Proof

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