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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvbdfbdioolem2.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvbdfbdioolem2.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
dvbdfbdioolem2.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
dvbdfbdioolem2.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
dvbdfbdioolem2.k ⊢ ( 𝜑 → 𝐾 ∈ ℝ )
dvbdfbdioolem2.dvbd ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝐾 )
dvbdfbdioolem2.m ⊢ 𝑀 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝐾 · ( 𝐵 − 𝐴 ) ) )
Assertion dvbdfbdioolem2 ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑀 )

Proof

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