dvbdfbdioolem1

Description: Given a function with bounded derivative, on an open interval, here is an absolute bound to the difference of the image of two points in the interval. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	dvbdfbdioolem1.a	$⊢ φ \to A \in ℝ$
	dvbdfbdioolem1.b	$⊢ φ \to B \in ℝ$
	dvbdfbdioolem1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
	dvbdfbdioolem1.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
	dvbdfbdioolem1.k	$⊢ φ \to K \in ℝ$
	dvbdfbdioolem1.dvbd	$⊢ φ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq K$
	dvbdfbdioolem1.c	$⊢ φ \to C \in (A, B)$
	dvbdfbdioolem1.d	$⊢ φ \to D \in (C, B)$
Assertion	dvbdfbdioolem1	$⊢ φ \to (\|F (D) - F (C)\| \leq K (D - C) \land \|F (D) - F (C)\| \leq K (B - A))$

Proof

Step	Hyp	Ref	Expression
1		dvbdfbdioolem1.a	$⊢ φ \to A \in ℝ$
2		dvbdfbdioolem1.b	$⊢ φ \to B \in ℝ$
3		dvbdfbdioolem1.f	$⊢ φ \to F : (A, B) ⟶ ℝ$
4		dvbdfbdioolem1.dmdv	$⊢ φ \to dom F_{ℝ}^{'} = (A, B)$
5		dvbdfbdioolem1.k	$⊢ φ \to K \in ℝ$
6		dvbdfbdioolem1.dvbd	$⊢ φ \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq K$
7		dvbdfbdioolem1.c	$⊢ φ \to C \in (A, B)$
8		dvbdfbdioolem1.d	$⊢ φ \to D \in (C, B)$
9		ioossre	$⊢ (A, B) \subseteq ℝ$
10	9 7	sseldi	$⊢ φ \to C \in ℝ$
11		ioossre	$⊢ (C, B) \subseteq ℝ$
12	11 8	sseldi	$⊢ φ \to D \in ℝ$
13	10	rexrd	$⊢ φ \to C \in ℝ^{*}$
14	2	rexrd	$⊢ φ \to B \in ℝ^{*}$
15		ioogtlb	$⊢ (C \in ℝ^{} \land B \in ℝ^{} \land D \in (C, B)) \to C < D$
16	13 14 8 15	syl3anc	$⊢ φ \to C < D$
17	1	rexrd	$⊢ φ \to A \in ℝ^{*}$
18		ioogtlb	$⊢ (A \in ℝ^{} \land B \in ℝ^{} \land C \in (A, B)) \to A < C$
19	17 14 7 18	syl3anc	$⊢ φ \to A < C$
20		iooltub	$⊢ (C \in ℝ^{} \land B \in ℝ^{} \land D \in (C, B)) \to D < B$
21	13 14 8 20	syl3anc	$⊢ φ \to D < B$
22		iccssioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A < C \land D < B)) \to [C, D] \subseteq (A, B)$
23	17 14 19 21 22	syl22anc	$⊢ φ \to [C, D] \subseteq (A, B)$
24		ax-resscn	$⊢ ℝ \subseteq ℂ$
25	24	a1i	$⊢ φ \to ℝ \subseteq ℂ$
26	3 25	fssd	$⊢ φ \to F : (A, B) ⟶ ℂ$
27	9	a1i	$⊢ φ \to (A, B) \subseteq ℝ$
28		dvcn	$⊢ ((ℝ \subseteq ℂ \land F : (A, B) ⟶ ℂ \land (A, B) \subseteq ℝ) \land dom F_{ℝ}^{'} = (A, B)) \to F : (A, B) \underset{cn}{⟶} ℂ$
29	25 26 27 4 28	syl31anc	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℂ$
30		cncffvrn	$⊢ (ℝ \subseteq ℂ \land F : (A, B) \underset{cn}{⟶} ℂ) \to (F : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow F : (A, B) ⟶ ℝ)$
31	25 29 30	syl2anc	$⊢ φ \to (F : (A, B) \underset{cn}{⟶} ℝ \leftrightarrow F : (A, B) ⟶ ℝ)$
32	3 31	mpbird	$⊢ φ \to F : (A, B) \underset{cn}{⟶} ℝ$
33		rescncf	$⊢ [C, D] \subseteq (A, B) \to (F : (A, B) \underset{cn}{⟶} ℝ \to ({F ↾}_{[C, D]}) : [C, D] \underset{cn}{⟶} ℝ)$
34	23 32 33	sylc	$⊢ φ \to ({F ↾}_{[C, D]}) : [C, D] \underset{cn}{⟶} ℝ$
35	23 27	sstrd	$⊢ φ \to [C, D] \subseteq ℝ$
36		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
37	36	tgioo2	$⊢ topGen (ran (.)) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℝ$
38	36 37	dvres	$⊢ ((ℝ \subseteq ℂ \land F : (A, B) ⟶ ℂ) \land ((A, B) \subseteq ℝ \land [C, D] \subseteq ℝ)) \to ℝ D ({F ↾}_{[C, D]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([C, D])}$
39	25 26 27 35 38	syl22anc	$⊢ φ \to ℝ D ({F ↾}_{[C, D]}) = {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([C, D])}$
40		iccntr	$⊢ (C \in ℝ \land D \in ℝ) \to int (topGen (ran (.))) ([C, D]) = (C, D)$
41	10 12 40	syl2anc	$⊢ φ \to int (topGen (ran (.))) ([C, D]) = (C, D)$
42	41	reseq2d	$⊢ φ \to {F_{ℝ}^{'} ↾}_{int (topGen (ran (.))) ([C, D])} = {F_{ℝ}^{'} ↾}_{(C, D)}$
43	39 42	eqtrd	$⊢ φ \to ℝ D ({F ↾}_{[C, D]}) = {F_{ℝ}^{'} ↾}_{(C, D)}$
44	43	dmeqd	$⊢ φ \to dom {({F ↾}_{[C, D]})}_{ℝ}^{'} = dom ({F_{ℝ}^{'} ↾}_{(C, D)})$
45	1 10 19	ltled	$⊢ φ \to A \leq C$
46	12 2 21	ltled	$⊢ φ \to D \leq B$
47		ioossioo	$⊢ ((A \in ℝ^{} \land B \in ℝ^{}) \land (A \leq C \land D \leq B)) \to (C, D) \subseteq (A, B)$
48	17 14 45 46 47	syl22anc	$⊢ φ \to (C, D) \subseteq (A, B)$
49	48 4	sseqtrrd	$⊢ φ \to (C, D) \subseteq dom F_{ℝ}^{'}$
50		ssdmres	$⊢ (C, D) \subseteq dom F_{ℝ}^{'} \leftrightarrow dom ({F_{ℝ}^{'} ↾}_{(C, D)}) = (C, D)$
51	49 50	sylib	$⊢ φ \to dom ({F_{ℝ}^{'} ↾}_{(C, D)}) = (C, D)$
52	44 51	eqtrd	$⊢ φ \to dom {({F ↾}_{[C, D]})}_{ℝ}^{'} = (C, D)$
53	10 12 16 34 52	mvth	$⊢ φ \to \exists x \in (C, D) {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}$
54	43	fveq1d	$⊢ φ \to {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = ({F_{ℝ}^{'} ↾}_{(C, D)}) (x)$
55		fvres	$⊢ x \in (C, D) \to ({F_{ℝ}^{'} ↾}_{(C, D)}) (x) = F_{ℝ}^{'} (x)$
56	54 55	sylan9eq	$⊢ (φ \land x \in (C, D)) \to {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = F_{ℝ}^{'} (x)$
57	56	eqcomd	$⊢ (φ \land x \in (C, D)) \to F_{ℝ}^{'} (x) = {({F ↾}_{[C, D]})}_{ℝ}^{'} (x)$
58	57	3adant3	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to F_{ℝ}^{'} (x) = {({F ↾}_{[C, D]})}_{ℝ}^{'} (x)$
59		simp3	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}$
60	12	rexrd	$⊢ φ \to D \in ℝ^{*}$
61	10 12 16	ltled	$⊢ φ \to C \leq D$
62		ubicc2	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C \leq D) \to D \in [C, D]$
63	13 60 61 62	syl3anc	$⊢ φ \to D \in [C, D]$
64		fvres	$⊢ D \in [C, D] \to ({F ↾}_{[C, D]}) (D) = F (D)$
65	63 64	syl	$⊢ φ \to ({F ↾}_{[C, D]}) (D) = F (D)$
66		lbicc2	$⊢ (C \in ℝ^{} \land D \in ℝ^{} \land C \leq D) \to C \in [C, D]$
67	13 60 61 66	syl3anc	$⊢ φ \to C \in [C, D]$
68		fvres	$⊢ C \in [C, D] \to ({F ↾}_{[C, D]}) (C) = F (C)$
69	67 68	syl	$⊢ φ \to ({F ↾}_{[C, D]}) (C) = F (C)$
70	65 69	oveq12d	$⊢ φ \to ({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C) = F (D) - F (C)$
71	70	oveq1d	$⊢ φ \to \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C} = \frac{F (D) - F (C)}{D - C}$
72	71	3ad2ant1	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C} = \frac{F (D) - F (C)}{D - C}$
73	58 59 72	3eqtrd	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}$
74		simp3	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}$
75	74	eqcomd	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \frac{F (D) - F (C)}{D - C} = F_{ℝ}^{'} (x)$
76	23 63	sseldd	$⊢ φ \to D \in (A, B)$
77	3 76	ffvelrnd	$⊢ φ \to F (D) \in ℝ$
78	3 7	ffvelrnd	$⊢ φ \to F (C) \in ℝ$
79	77 78	resubcld	$⊢ φ \to F (D) - F (C) \in ℝ$
80	79	recnd	$⊢ φ \to F (D) - F (C) \in ℂ$
81	80	3ad2ant1	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to F (D) - F (C) \in ℂ$
82		dvfre	$⊢ (F : (A, B) ⟶ ℝ \land (A, B) \subseteq ℝ) \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
83	3 27 82	syl2anc	$⊢ φ \to F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ$
84	4	feq2d	$⊢ φ \to (F_{ℝ}^{'} : dom F_{ℝ}^{'} ⟶ ℝ \leftrightarrow F_{ℝ}^{'} : (A, B) ⟶ ℝ)$
85	83 84	mpbid	$⊢ φ \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
86	85	adantr	$⊢ (φ \land x \in (C, D)) \to F_{ℝ}^{'} : (A, B) ⟶ ℝ$
87	48	sselda	$⊢ (φ \land x \in (C, D)) \to x \in (A, B)$
88	86 87	ffvelrnd	$⊢ (φ \land x \in (C, D)) \to F_{ℝ}^{'} (x) \in ℝ$
89	88	recnd	$⊢ (φ \land x \in (C, D)) \to F_{ℝ}^{'} (x) \in ℂ$
90	89	3adant3	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to F_{ℝ}^{'} (x) \in ℂ$
91	12 10	resubcld	$⊢ φ \to D - C \in ℝ$
92	91	recnd	$⊢ φ \to D - C \in ℂ$
93	92	3ad2ant1	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to D - C \in ℂ$
94	10 12	posdifd	$⊢ φ \to (C < D \leftrightarrow 0 < D - C)$
95	16 94	mpbid	$⊢ φ \to 0 < D - C$
96	95	gt0ne0d	$⊢ φ \to D - C \neq 0$
97	96	3ad2ant1	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to D - C \neq 0$
98	81 90 93 97	divmul3d	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to (\frac{F (D) - F (C)}{D - C} = F_{ℝ}^{'} (x) \leftrightarrow F (D) - F (C) = F_{ℝ}^{'} (x) (D - C))$
99	75 98	mpbid	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to F (D) - F (C) = F_{ℝ}^{'} (x) (D - C)$
100	99	fveq2d	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F (D) - F (C)\| = \|F_{ℝ}^{'} (x) (D - C)\|$
101	92	adantr	$⊢ (φ \land x \in (C, D)) \to D - C \in ℂ$
102	89 101	absmuld	$⊢ (φ \land x \in (C, D)) \to \|F_{ℝ}^{'} (x) (D - C)\| = \|F_{ℝ}^{'} (x)\| \|D - C\|$
103	102	3adant3	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F_{ℝ}^{'} (x) (D - C)\| = \|F_{ℝ}^{'} (x)\| \|D - C\|$
104	100 103	eqtrd	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F (D) - F (C)\| = \|F_{ℝ}^{'} (x)\| \|D - C\|$
105	10 12 61	abssubge0d	$⊢ φ \to \|D - C\| = D - C$
106	105	oveq2d	$⊢ φ \to \|F_{ℝ}^{'} (x)\| \|D - C\| = \|F_{ℝ}^{'} (x)\| (D - C)$
107	106	3ad2ant1	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F_{ℝ}^{'} (x)\| \|D - C\| = \|F_{ℝ}^{'} (x)\| (D - C)$
108	104 107	eqtrd	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F (D) - F (C)\| = \|F_{ℝ}^{'} (x)\| (D - C)$
109	89	abscld	$⊢ (φ \land x \in (C, D)) \to \|F_{ℝ}^{'} (x)\| \in ℝ$
110	5	adantr	$⊢ (φ \land x \in (C, D)) \to K \in ℝ$
111	91	adantr	$⊢ (φ \land x \in (C, D)) \to D - C \in ℝ$
112		0red	$⊢ φ \to 0 \in ℝ$
113	112 91 95	ltled	$⊢ φ \to 0 \leq D - C$
114	113	adantr	$⊢ (φ \land x \in (C, D)) \to 0 \leq D - C$
115	6	adantr	$⊢ (φ \land x \in (C, D)) \to \forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq K$
116		rspa	$⊢ (\forall x \in (A, B) \|F_{ℝ}^{'} (x)\| \leq K \land x \in (A, B)) \to \|F_{ℝ}^{'} (x)\| \leq K$
117	115 87 116	syl2anc	$⊢ (φ \land x \in (C, D)) \to \|F_{ℝ}^{'} (x)\| \leq K$
118	109 110 111 114 117	lemul1ad	$⊢ (φ \land x \in (C, D)) \to \|F_{ℝ}^{'} (x)\| (D - C) \leq K (D - C)$
119	118	3adant3	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F_{ℝ}^{'} (x)\| (D - C) \leq K (D - C)$
120	108 119	eqbrtrd	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F (D) - F (C)\| \leq K (D - C)$
121	73 120	syld3an3	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to \|F (D) - F (C)\| \leq K (D - C)$
122	101	abscld	$⊢ (φ \land x \in (C, D)) \to \|D - C\| \in ℝ$
123	2 1	resubcld	$⊢ φ \to B - A \in ℝ$
124	123	adantr	$⊢ (φ \land x \in (C, D)) \to B - A \in ℝ$
125	89	absge0d	$⊢ (φ \land x \in (C, D)) \to 0 \leq \|F_{ℝ}^{'} (x)\|$
126	101	absge0d	$⊢ (φ \land x \in (C, D)) \to 0 \leq \|D - C\|$
127	12 1 2 10 46 45	le2subd	$⊢ φ \to D - C \leq B - A$
128	105 127	eqbrtrd	$⊢ φ \to \|D - C\| \leq B - A$
129	128	adantr	$⊢ (φ \land x \in (C, D)) \to \|D - C\| \leq B - A$
130	109 110 122 124 125 126 117 129	lemul12ad	$⊢ (φ \land x \in (C, D)) \to \|F_{ℝ}^{'} (x)\| \|D - C\| \leq K (B - A)$
131	130	3adant3	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F_{ℝ}^{'} (x)\| \|D - C\| \leq K (B - A)$
132	104 131	eqbrtrd	$⊢ (φ \land x \in (C, D) \land F_{ℝ}^{'} (x) = \frac{F (D) - F (C)}{D - C}) \to \|F (D) - F (C)\| \leq K (B - A)$
133	73 132	syld3an3	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to \|F (D) - F (C)\| \leq K (B - A)$
134	121 133	jca	$⊢ (φ \land x \in (C, D) \land {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C}) \to (\|F (D) - F (C)\| \leq K (D - C) \land \|F (D) - F (C)\| \leq K (B - A))$
135	134	rexlimdv3a	$⊢ φ \to (\exists x \in (C, D) {({F ↾}_{[C, D]})}_{ℝ}^{'} (x) = \frac{({F ↾}_{[C, D]}) (D) - ({F ↾}_{[C, D]}) (C)}{D - C} \to (\|F (D) - F (C)\| \leq K (D - C) \land \|F (D) - F (C)\| \leq K (B - A)))$
136	53 135	mpd	$⊢ φ \to (\|F (D) - F (C)\| \leq K (D - C) \land \|F (D) - F (C)\| \leq K (B - A))$

Metamath Proof Explorer

Theorem dvbdfbdioolem1

Proof