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	biimpi	⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ 𝑎 )
35	34	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑦 ) ) ≤ 𝑎 )
36		eqid	⊢ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) )
37	24 23 28 29 30 22 35 36	dvbdfbdioolem2	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) )
38		2fveq3	⊢ ( 𝑥 = 𝑦 → ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) = ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) )
39	38	breq1d	⊢ ( 𝑥 = 𝑦 → ( ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 ) )
40	39	cbvralvw	⊢ ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 )
41		breq2	⊢ ( 𝑏 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) → ( ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 ↔ ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) )
42	41	ralbidv	⊢ ( 𝑏 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) → ( ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) )
43	40 42	bitrid	⊢ ( 𝑏 = ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) → ( ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 ↔ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) )
44	43	rspcev	⊢ ( ( ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ∈ ℝ ∧ ∀ 𝑦 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑦 ) ) ≤ ( ( abs ‘ ( 𝐹 ‘ ( ( 𝐴 + 𝐵 ) / 2 ) ) ) + ( 𝑎 · ( 𝐵 − 𝐴 ) ) ) ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
45	27 37 44	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ℝ ) ∧ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝑎 ) → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )
46	45 6	r19.29a	⊢ ( 𝜑 → ∃ 𝑏 ∈ ℝ ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( 𝐹 ‘ 𝑥 ) ) ≤ 𝑏 )