Metamath Proof Explorer

Theorem dvbdfbdioolem2

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

Ref Expression
Hypotheses dvbdfbdioolem2.a 
|- ( ph -> A e. RR )
dvbdfbdioolem2.b 
|- ( ph -> B e. RR )
dvbdfbdioolem2.altb 
|- ( ph -> A < B )
dvbdfbdioolem2.f 
|- ( ph -> F : ( A (,) B ) --> RR )
dvbdfbdioolem2.dmdv 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvbdfbdioolem2.k 
|- ( ph -> K e. RR )
dvbdfbdioolem2.dvbd 
|- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K )
dvbdfbdioolem2.m 
|- M = ( ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) + ( K x. ( B - A ) ) )
Assertion dvbdfbdioolem2 
|- ( ph -> A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ M )

Proof

Step Hyp Ref Expression
1 dvbdfbdioolem2.a 
 |-  ( ph -> A e. RR )
2 dvbdfbdioolem2.b 
 |-  ( ph -> B e. RR )
3 dvbdfbdioolem2.altb 
 |-  ( ph -> A < B )
4 dvbdfbdioolem2.f 
 |-  ( ph -> F : ( A (,) B ) --> RR )
5 dvbdfbdioolem2.dmdv 
 |-  ( ph -> dom ( RR _D F ) = ( A (,) B ) )
6 dvbdfbdioolem2.k 
 |-  ( ph -> K e. RR )
7 dvbdfbdioolem2.dvbd 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K )
8 dvbdfbdioolem2.m 
 |-  M = ( ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) + ( K x. ( B - A ) ) )
9 4 ffvelcdmda 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. RR )
10 9 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` x ) e. CC )
11 10 abscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( F ` x ) ) e. RR )
12 1 rexrd 
 |-  ( ph -> A e. RR* )
13 2 rexrd 
 |-  ( ph -> B e. RR* )
14 1 2 readdcld 
 |-  ( ph -> ( A + B ) e. RR )
15 14 rehalfcld 
 |-  ( ph -> ( ( A + B ) / 2 ) e. RR )
16 avglt1 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )
17 1 2 16 syl2anc 
 |-  ( ph -> ( A < B <-> A < ( ( A + B ) / 2 ) ) )
18 3 17 mpbid 
 |-  ( ph -> A < ( ( A + B ) / 2 ) )
19 avglt2 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
20 1 2 19 syl2anc 
 |-  ( ph -> ( A < B <-> ( ( A + B ) / 2 ) < B ) )
21 3 20 mpbid 
 |-  ( ph -> ( ( A + B ) / 2 ) < B )
22 12 13 15 18 21 eliood 
 |-  ( ph -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
23 4 22 ffvelcdmd 
 |-  ( ph -> ( F ` ( ( A + B ) / 2 ) ) e. RR )
24 23 recnd 
 |-  ( ph -> ( F ` ( ( A + B ) / 2 ) ) e. CC )
25 24 abscld 
 |-  ( ph -> ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) e. RR )
26 25 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) e. RR )
27 11 26 resubcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( abs ` ( F ` x ) ) - ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) e. RR )
28 6 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> K e. RR )
29 2 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> B e. RR )
30 1 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR )
31 29 30 resubcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( B - A ) e. RR )
32 28 31 remulcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( K x. ( B - A ) ) e. RR )
33 24 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( F ` ( ( A + B ) / 2 ) ) e. CC )
34 10 33 subcld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) e. CC )
35 34 abscld 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) e. RR )
36 10 33 abs2difd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( abs ` ( F ` x ) ) - ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) )
37 simpll 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> ph )
38 15 rexrd 
 |-  ( ph -> ( ( A + B ) / 2 ) e. RR* )
39 38 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> ( ( A + B ) / 2 ) e. RR* )
40 13 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> B e. RR* )
41 elioore 
 |-  ( x e. ( A (,) B ) -> x e. RR )
42 41 adantl 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. RR )
43 42 adantr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> x e. RR )
44 simpr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> ( ( A + B ) / 2 ) < x )
45 12 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> A e. RR* )
46 13 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> B e. RR* )
47 simpr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x e. ( A (,) B ) )
48 iooltub 
 |-  ( ( A e. RR* /\ B e. RR* /\ x e. ( A (,) B ) ) -> x < B )
49 45 46 47 48 syl3anc 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> x < B )
50 49 adantr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> x < B )
51 39 40 43 44 50 eliood 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> x e. ( ( ( A + B ) / 2 ) (,) B ) )
52 1 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> A e. RR )
53 2 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> B e. RR )
54 4 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> F : ( A (,) B ) --> RR )
55 5 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> dom ( RR _D F ) = ( A (,) B ) )
56 6 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> K e. RR )
57 2fveq3 
 |-  ( x = y -> ( abs ` ( ( RR _D F ) ` x ) ) = ( abs ` ( ( RR _D F ) ` y ) ) )
58 57 breq1d 
 |-  ( x = y -> ( ( abs ` ( ( RR _D F ) ` x ) ) <_ K <-> ( abs ` ( ( RR _D F ) ` y ) ) <_ K ) )
59 58 cbvralvw 
 |-  ( A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K <-> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ K )
60 7 59 sylib 
 |-  ( ph -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ K )
61 60 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ K )
62 22 adantr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> ( ( A + B ) / 2 ) e. ( A (,) B ) )
63 simpr 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> x e. ( ( ( A + B ) / 2 ) (,) B ) )
64 52 53 54 55 56 61 62 63 dvbdfbdioolem1 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> ( ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( x - ( ( A + B ) / 2 ) ) ) /\ ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) ) )
65 64 simprd 
 |-  ( ( ph /\ x e. ( ( ( A + B ) / 2 ) (,) B ) ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
66 37 51 65 syl2anc 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ ( ( A + B ) / 2 ) < x ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
67 fveq2 
 |-  ( ( ( A + B ) / 2 ) = x -> ( F ` ( ( A + B ) / 2 ) ) = ( F ` x ) )
68 67 eqcomd 
 |-  ( ( ( A + B ) / 2 ) = x -> ( F ` x ) = ( F ` ( ( A + B ) / 2 ) ) )
69 68 adantl 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( F ` x ) = ( F ` ( ( A + B ) / 2 ) ) )
70 24 adantr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( F ` ( ( A + B ) / 2 ) ) e. CC )
71 69 70 eqeltrd 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( F ` x ) e. CC )
72 71 69 subeq0bd 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) = 0 )
73 72 abs00bd 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) = 0 )
74 6 adantr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> K e. RR )
75 2 adantr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> B e. RR )
76 1 adantr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> A e. RR )
77 75 76 resubcld 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( B - A ) e. RR )
78 0red 
 |-  ( ph -> 0 e. RR )
79 ioossre 
 |-  ( A (,) B ) C_ RR
80 dvfre 
 |-  ( ( F : ( A (,) B ) --> RR /\ ( A (,) B ) C_ RR ) -> ( RR _D F ) : dom ( RR _D F ) --> RR )
81 4 79 80 sylancl 
 |-  ( ph -> ( RR _D F ) : dom ( RR _D F ) --> RR )
82 22 5 eleqtrrd 
 |-  ( ph -> ( ( A + B ) / 2 ) e. dom ( RR _D F ) )
83 81 82 ffvelcdmd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. RR )
84 83 recnd 
 |-  ( ph -> ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) e. CC )
85 84 abscld 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) e. RR )
86 84 absge0d 
 |-  ( ph -> 0 <_ ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
87 2fveq3 
 |-  ( x = ( ( A + B ) / 2 ) -> ( abs ` ( ( RR _D F ) ` x ) ) = ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) )
88 87 breq1d 
 |-  ( x = ( ( A + B ) / 2 ) -> ( ( abs ` ( ( RR _D F ) ` x ) ) <_ K <-> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ K ) )
89 88 rspccva 
 |-  ( ( A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K /\ ( ( A + B ) / 2 ) e. ( A (,) B ) ) -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ K )
90 7 22 89 syl2anc 
 |-  ( ph -> ( abs ` ( ( RR _D F ) ` ( ( A + B ) / 2 ) ) ) <_ K )
91 78 85 6 86 90 letrd 
 |-  ( ph -> 0 <_ K )
92 91 adantr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> 0 <_ K )
93 2 1 resubcld 
 |-  ( ph -> ( B - A ) e. RR )
94 1 2 posdifd 
 |-  ( ph -> ( A < B <-> 0 < ( B - A ) ) )
95 3 94 mpbid 
 |-  ( ph -> 0 < ( B - A ) )
96 78 93 95 ltled 
 |-  ( ph -> 0 <_ ( B - A ) )
97 96 adantr 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> 0 <_ ( B - A ) )
98 74 77 92 97 mulge0d 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> 0 <_ ( K x. ( B - A ) ) )
99 73 98 eqbrtrd 
 |-  ( ( ph /\ ( ( A + B ) / 2 ) = x ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
100 99 ad4ant14 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ ( ( A + B ) / 2 ) = x ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
101 simpll 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> ( ph /\ x e. ( A (,) B ) ) )
102 42 ad2antrr 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> x e. RR )
103 15 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> ( ( A + B ) / 2 ) e. RR )
104 42 adantr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) -> x e. RR )
105 15 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) -> ( ( A + B ) / 2 ) e. RR )
106 simpr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) -> -. ( ( A + B ) / 2 ) < x )
107 104 105 106 nltled 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) -> x <_ ( ( A + B ) / 2 ) )
108 107 adantr 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> x <_ ( ( A + B ) / 2 ) )
109 neqne 
 |-  ( -. ( ( A + B ) / 2 ) = x -> ( ( A + B ) / 2 ) =/= x )
110 109 adantl 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> ( ( A + B ) / 2 ) =/= x )
111 102 103 108 110 leneltd 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> x < ( ( A + B ) / 2 ) )
112 10 33 abssubd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) = ( abs ` ( ( F ` ( ( A + B ) / 2 ) ) - ( F ` x ) ) ) )
113 112 adantr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) = ( abs ` ( ( F ` ( ( A + B ) / 2 ) ) - ( F ` x ) ) ) )
114 1 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> A e. RR )
115 2 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> B e. RR )
116 4 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> F : ( A (,) B ) --> RR )
117 5 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> dom ( RR _D F ) = ( A (,) B ) )
118 6 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> K e. RR )
119 60 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> A. y e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` y ) ) <_ K )
120 47 adantr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> x e. ( A (,) B ) )
121 41 rexrd 
 |-  ( x e. ( A (,) B ) -> x e. RR* )
122 121 ad2antlr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> x e. RR* )
123 13 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> B e. RR* )
124 15 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( ( A + B ) / 2 ) e. RR )
125 simpr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> x < ( ( A + B ) / 2 ) )
126 21 ad2antrr 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( ( A + B ) / 2 ) < B )
127 122 123 124 125 126 eliood 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( ( A + B ) / 2 ) e. ( x (,) B ) )
128 114 115 116 117 118 119 120 127 dvbdfbdioolem1 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( ( abs ` ( ( F ` ( ( A + B ) / 2 ) ) - ( F ` x ) ) ) <_ ( K x. ( ( ( A + B ) / 2 ) - x ) ) /\ ( abs ` ( ( F ` ( ( A + B ) / 2 ) ) - ( F ` x ) ) ) <_ ( K x. ( B - A ) ) ) )
129 128 simprd 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( abs ` ( ( F ` ( ( A + B ) / 2 ) ) - ( F ` x ) ) ) <_ ( K x. ( B - A ) ) )
130 113 129 eqbrtrd 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ x < ( ( A + B ) / 2 ) ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
131 101 111 130 syl2anc 
 |-  ( ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) /\ -. ( ( A + B ) / 2 ) = x ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
132 100 131 pm2.61dan 
 |-  ( ( ( ph /\ x e. ( A (,) B ) ) /\ -. ( ( A + B ) / 2 ) < x ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
133 66 132 pm2.61dan 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( ( F ` x ) - ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
134 27 35 32 36 133 letrd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( abs ` ( F ` x ) ) - ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( K x. ( B - A ) ) )
135 27 32 26 134 leadd1dd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( abs ` ( F ` x ) ) - ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) <_ ( ( K x. ( B - A ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) )
136 11 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( F ` x ) ) e. CC )
137 26 recnd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) e. CC )
138 136 137 npcand 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( ( ( abs ` ( F ` x ) ) - ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) = ( abs ` ( F ` x ) ) )
139 138 eqcomd 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( F ` x ) ) = ( ( ( abs ` ( F ` x ) ) - ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) )
140 25 recnd 
 |-  ( ph -> ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) e. CC )
141 6 recnd 
 |-  ( ph -> K e. CC )
142 2 recnd 
 |-  ( ph -> B e. CC )
143 1 recnd 
 |-  ( ph -> A e. CC )
144 142 143 subcld 
 |-  ( ph -> ( B - A ) e. CC )
145 141 144 mulcld 
 |-  ( ph -> ( K x. ( B - A ) ) e. CC )
146 140 145 addcomd 
 |-  ( ph -> ( ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) + ( K x. ( B - A ) ) ) = ( ( K x. ( B - A ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) )
147 8 146 eqtrid 
 |-  ( ph -> M = ( ( K x. ( B - A ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) )
148 147 adantr 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> M = ( ( K x. ( B - A ) ) + ( abs ` ( F ` ( ( A + B ) / 2 ) ) ) ) )
149 135 139 148 3brtr4d 
 |-  ( ( ph /\ x e. ( A (,) B ) ) -> ( abs ` ( F ` x ) ) <_ M )
150 149 ralrimiva 
 |-  ( ph -> A. x e. ( A (,) B ) ( abs ` ( F ` x ) ) <_ M )