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 
|- ( ph -> A e. RR )
dvbdfbdioolem1.b 
|- ( ph -> B e. RR )
dvbdfbdioolem1.f 
|- ( ph -> F : ( A (,) B ) --> RR )
dvbdfbdioolem1.dmdv 
|- ( ph -> dom ( RR _D F ) = ( A (,) B ) )
dvbdfbdioolem1.k 
|- ( ph -> K e. RR )
dvbdfbdioolem1.dvbd 
|- ( ph -> A. x e. ( A (,) B ) ( abs ` ( ( RR _D F ) ` x ) ) <_ K )
dvbdfbdioolem1.c 
|- ( ph -> C e. ( A (,) B ) )
dvbdfbdioolem1.d 
|- ( ph -> D e. ( C (,) B ) )
Assertion dvbdfbdioolem1 
|- ( ph -> ( ( abs ` ( ( F ` D ) - ( F ` C ) ) ) <_ ( K x. ( D - C ) ) /\ ( abs ` ( ( F ` D ) - ( F ` C ) ) ) <_ ( K x. ( B - A ) ) ) )

Proof

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