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 sseldi ( 𝜑𝐶 ∈ ℝ )
11 ioossre ( 𝐶 (,) 𝐵 ) ⊆ ℝ
12 11 8 sseldi ( 𝜑𝐷 ∈ ℝ )
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 ‘ ( ( 𝐹𝐷 ) − ( 𝐹𝐶 ) ) ) ≤ ( 𝐾 · ( 𝐵𝐴 ) ) ) )