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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
dvbdfbdioo.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
dvbdfbdioo.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
dvbdfbdioo.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
dvbdfbdioo.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
dvbdfbdioo.dvbd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 )
Assertion dvbdfbdioo ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )

Proof

Step Hyp Ref Expression
1 dvbdfbdioo.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
2 dvbdfbdioo.b ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
3 dvbdfbdioo.altb ⊢ ( 𝜑 → 𝐴 < 𝐵 )
4 dvbdfbdioo.f ⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
5 dvbdfbdioo.dmdv ⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
6 dvbdfbdioo.dvbd ⊢ ( 𝜑 → ∃ 𝑎 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 )
7 1 rexrd ⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
8 2 rexrd ⊢ ( 𝜑 → 𝐵 ∈ ℝ* )
9 1 2 readdcld ⊢ ( 𝜑 → ( 𝐴 + 𝐵 ) ∈ ℝ )
10 9 rehalfcld ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ℝ )
11 avglt1 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) ) )
12 1 2 11 syl2anc ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) ) )
13 3 12 mpbid ⊢ ( 𝜑 → 𝐴 < ( ( 𝐴 + 𝐵 ) / 2 ) )
14 avglt2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ) )
15 1 2 14 syl2anc ⊢ ( 𝜑 → ( 𝐴 < 𝐵 ↔ ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 ) )
16 3 15 mpbid ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) < 𝐵 )
17 7 8 10 13 16 eliood ⊢ ( 𝜑 → ( ( 𝐴 + 𝐵 ) / 2 ) ∈ ( 𝐴 (,) 𝐵 ) )
18 4 17 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℝ )
19 18 recnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ∈ ℂ )
20 19 abscld ⊢ ( 𝜑 → ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
21 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) ∈ ℝ )
22 simplr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → 𝑎 ∈ ℝ )
23 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → 𝐵 ∈ ℝ )
24 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → 𝐴 ∈ ℝ )
25 23 24 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( 𝐵 − 𝐴 ) ∈ ℝ )
26 22 25 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( 𝑎 · ( 𝐵 − 𝐴 ) ) ∈ ℝ )
27 21 26 readdcld ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ∈ ℝ )
28 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → 𝐴 < 𝐵 )
29 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
30 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
31 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) = ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) )
32 31 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ↔ ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ 𝑎 ) )
33 32 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ 𝑎 )
34 33 bilani ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ 𝑎 )
35 eqid ⊢ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) )
36 24 23 28 29 30 22 34 35 dvbdfbdioolem2 ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) )
37 2fveq3 ⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
38 37 breq1d ⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 ) )
39 38 cbvralvw ⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 )
40 breq2 ⊢ ( 𝑏 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) )
41 40 ralbidv ⊢ ( 𝑏 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) )
42 39 41 bitrid ⊢ ( 𝑏 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) → ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) )
43 42 rspcev ⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ∈ ℝ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
44 27 36 43 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
45 44 6 r19.29a ⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )