Metamath Proof Explorer

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 cncffvrn ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐹 ∈ ( ( 𝐴 (,) 𝐵 ) –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 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐷 ) ∈ ℝ )
78 3 7 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ ℝ )
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 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐶 (,) 𝐷 ) ) → ( ( ℝ 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 ‘ ( ( 𝐹 ‘ 𝐷 ) − ( 𝐹 ‘ 𝐶 ) ) ) ≤ ( 𝐾 · ( 𝐵 − 𝐴 ) ) ) )