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
|
ffvelrnda |
|- ( ( 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
|
ffvelrnd |
|- ( 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
|
ffvelrnd |
|- ( 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 ) |