Theorem 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	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	dvbdfbdioolem1.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	dvbdfbdioolem1.f	⊢ ( 𝜑 → 𝐹 : ( 𝐴 (,) 𝐵 ) ⟶ ℝ )
	dvbdfbdioolem1.dmdv	⊢ ( 𝜑 → dom ( ℝ D 𝐹 ) = ( 𝐴 (,) 𝐵 ) )
	dvbdfbdioolem1.k	⊢ ( 𝜑 → 𝐾 ∈ ℝ )
	dvbdfbdioolem1.dvbd	⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐴 (,) 𝐵 ) ( abs ‘ ( ( ℝ D 𝐹 ) ‘ 𝑥 ) ) ≤ 𝐾 )
	dvbdfbdioolem1.c	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 (,) 𝐵 ) )
	dvbdfbdioolem1.d	⊢ ( 𝜑 → 𝐷 ∈ ( 𝐶 (,) 𝐵 ) )
Assertion	dvbdfbdioolem1	⊢ ( 𝜑 → ( ( abs ‘ ( ( 𝐹 ‘ 𝐷 ) − ( 𝐹 ‘ 𝐶 ) ) ) ≤ ( 𝐾 · ( 𝐷 − 𝐶 ) ) ∧ ( abs ‘ ( ( 𝐹 ‘ 𝐷 ) − ( 𝐹 ‘ 𝐶 ) ) ) ≤ ( 𝐾 · ( 𝐵 − 𝐴 ) ) ) )

Proof

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