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 ⊢ φ → A ∈ ℝ
dvbdfbdioo.b ⊢ φ → B ∈ ℝ
dvbdfbdioo.altb ⊢ φ → A < B
dvbdfbdioo.f ⊢ φ → F : A B ⟶ ℝ
dvbdfbdioo.dmdv ⊢ φ → dom ⁡ F ℝ ′ = A B
dvbdfbdioo.dvbd ⊢ φ → ∃ a ∈ ℝ ∀ x ∈ A B F ℝ ′ ⁡ x ≤ a
Assertion dvbdfbdioo ⊢ φ → ∃ b ∈ ℝ ∀ x ∈ A B F ⁡ x ≤ b

Proof

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