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 φ A
dvbdfbdioolem2.b φ B
dvbdfbdioolem2.altb φ A < B
dvbdfbdioolem2.f φ F : A B
dvbdfbdioolem2.dmdv φ dom F = A B
dvbdfbdioolem2.k φ K
dvbdfbdioolem2.dvbd φ x A B F x K
dvbdfbdioolem2.m M = F A + B 2 + K B A
Assertion dvbdfbdioolem2 φ x A B F x M

Proof

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