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	$⊢ φ \to A \in ℝ$
	dvbdfbdioolem2.b	$⊢ φ \to B \in ℝ$
	dvbdfbdioolem2.altb	$⊢ φ \to A < B$
	dvbdfbdioolem2.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	dvbdfbdioolem2.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	dvbdfbdioolem2.k	$⊢ φ \to K \in ℝ$
	dvbdfbdioolem2.dvbd	$⊢ φ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq K$
	dvbdfbdioolem2.m	$⊢ M = \|F (\frac{A + B}{2})\| + K (B - A)$
Assertion	dvbdfbdioolem2	$⊢ φ \to \forall x \in (A, B) \|F (x)\| \leq M$

Proof

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

Metamath Proof Explorer

Theorem dvbdfbdioolem2

Proof