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	$$⊢\phi \to A\in ℝ$$
	dvbdfbdioo.b	$$⊢\phi \to B\in ℝ$$
	dvbdfbdioo.altb	$$⊢\phi \to A<B$$
	dvbdfbdioo.f	$$⊢\phi \to F:\left(A,B\right)⟶ℝ$$
	dvbdfbdioo.dmdv	$$⊢\phi \to \mathrm{dom}{F}_{ℝ}^{\prime }=\left(A,B\right)$$
	dvbdfbdioo.dvbd	$$⊢\phi \to \exists a\in ℝ\forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a$$
Assertion	dvbdfbdioo	$$⊢\phi \to \exists b\in ℝ\forall x\in \left(A,B\right)\left|F\left(x\right)\right|\le b$$

Proof

Step	Hyp	Ref	Expression
1		dvbdfbdioo.a	$$⊢\phi \to A\in ℝ$$
2		dvbdfbdioo.b	$$⊢\phi \to B\in ℝ$$
3		dvbdfbdioo.altb	$$⊢\phi \to A<B$$
4		dvbdfbdioo.f	$$⊢\phi \to F:\left(A,B\right)⟶ℝ$$
5		dvbdfbdioo.dmdv	$$⊢\phi \to \mathrm{dom}{F}_{ℝ}^{\prime }=\left(A,B\right)$$
6		dvbdfbdioo.dvbd	$$⊢\phi \to \exists a\in ℝ\forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a$$
7	1	rexrd	$$⊢\phi \to A\in {ℝ}^{*}$$
8	2	rexrd	$$⊢\phi \to B\in {ℝ}^{*}$$
9	1 2	readdcld	$$⊢\phi \to A+B\in ℝ$$
10	9	rehalfcld	$$⊢\phi \to \frac{A+B}{2}\in ℝ$$
11		avglt1	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow A<\frac{A+B}{2}\right)$$
12	1 2 11	syl2anc	$$⊢\phi \to \left(A<B\leftrightarrow A<\frac{A+B}{2}\right)$$
13	3 12	mpbid	$$⊢\phi \to A<\frac{A+B}{2}$$
14		avglt2	$$⊢\left(A\in ℝ\wedge B\in ℝ\right)\to \left(A<B\leftrightarrow \frac{A+B}{2}<B\right)$$
15	1 2 14	syl2anc	$$⊢\phi \to \left(A<B\leftrightarrow \frac{A+B}{2}<B\right)$$
16	3 15	mpbid	$$⊢\phi \to \frac{A+B}{2}<B$$
17	7 8 10 13 16	eliood	$$⊢\phi \to \frac{A+B}{2}\in \left(A,B\right)$$
18	4 17	ffvelcdmd	$$⊢\phi \to F\left(\frac{A+B}{2}\right)\in ℝ$$
19	18	recnd	$$⊢\phi \to F\left(\frac{A+B}{2}\right)\in ℂ$$
20	19	abscld	$$⊢\phi \to \left|F\left(\frac{A+B}{2}\right)\right|\in ℝ$$
21	20	ad2antrr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to \left|F\left(\frac{A+B}{2}\right)\right|\in ℝ$$
22		simplr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to a\in ℝ$$
23	2	ad2antrr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to B\in ℝ$$
24	1	ad2antrr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to A\in ℝ$$
25	23 24	resubcld	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to B-A\in ℝ$$
26	22 25	remulcld	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to a\left(B-A\right)\in ℝ$$
27	21 26	readdcld	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to \left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\in ℝ$$
28	3	ad2antrr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to A<B$$
29	4	ad2antrr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to F:\left(A,B\right)⟶ℝ$$
30	5	ad2antrr	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to \mathrm{dom}{F}_{ℝ}^{\prime }=\left(A,B\right)$$
31		2fveq3	$$⊢x=y\to \left|F_{ℝ}^{\prime }\left(x\right)\right|=\left|F_{ℝ}^{\prime }\left(y\right)\right|$$
32	31	breq1d	$$⊢x=y\to \left(\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\leftrightarrow \left|F_{ℝ}^{\prime }\left(y\right)\right|\le a\right)$$
33	32	cbvralvw	$$⊢\forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\leftrightarrow \forall y\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(y\right)\right|\le a$$
34	33	biimpi	$$⊢\forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\to \forall y\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(y\right)\right|\le a$$
35	34	adantl	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to \forall y\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(y\right)\right|\le a$$
36		eqid	$$⊢\left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)=\left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)$$
37	24 23 28 29 30 22 35 36	dvbdfbdioolem2	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to \forall y\in \left(A,B\right)\left|F\left(y\right)\right|\le \left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)$$
38		2fveq3	$$⊢x=y\to \left|F\left(x\right)\right|=\left|F\left(y\right)\right|$$
39	38	breq1d	$$⊢x=y\to \left(\left|F\left(x\right)\right|\le b\leftrightarrow \left|F\left(y\right)\right|\le b\right)$$
40	39	cbvralvw	$$⊢\forall x\in \left(A,B\right)\left|F\left(x\right)\right|\le b\leftrightarrow \forall y\in \left(A,B\right)\left|F\left(y\right)\right|\le b$$
41		breq2	$$⊢b=\left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\to \left(\left|F\left(y\right)\right|\le b\leftrightarrow \left|F\left(y\right)\right|\le \left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\right)$$
42	41	ralbidv	$$⊢b=\left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\to \left(\forall y\in \left(A,B\right)\left|F\left(y\right)\right|\le b\leftrightarrow \forall y\in \left(A,B\right)\left|F\left(y\right)\right|\le \left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\right)$$
43	40 42	bitrid	$$⊢b=\left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\to \left(\forall x\in \left(A,B\right)\left|F\left(x\right)\right|\le b\leftrightarrow \forall y\in \left(A,B\right)\left|F\left(y\right)\right|\le \left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\right)$$
44	43	rspcev	$$⊢\left(\left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\in ℝ\wedge \forall y\in \left(A,B\right)\left|F\left(y\right)\right|\le \left|F\left(\frac{A+B}{2}\right)\right|+a\left(B-A\right)\right)\to \exists b\in ℝ\forall x\in \left(A,B\right)\left|F\left(x\right)\right|\le b$$
45	27 37 44	syl2anc	$$⊢\left(\left(\phi \wedge a\in ℝ\right)\wedge \forall x\in \left(A,B\right)\left|F_{ℝ}^{\prime }\left(x\right)\right|\le a\right)\to \exists b\in ℝ\forall x\in \left(A,B\right)\left|F\left(x\right)\right|\le b$$
46	45 6	r19.29a	$$⊢\phi \to \exists b\in ℝ\forall x\in \left(A,B\right)\left|F\left(x\right)\right|\le b$$