Metamath Proof Explorer

Theorem c1liplem1

Description: Lemma for c1lip1 . (Contributed by Stefan O'Rear, 15-Nov-2014)

Ref Expression
Hypotheses c1liplem1.a 
|- ( ph -> A e. RR )
c1liplem1.b 
|- ( ph -> B e. RR )
c1liplem1.le 
|- ( ph -> A <_ B )
c1liplem1.f 
|- ( ph -> F e. ( CC ^pm RR ) )
c1liplem1.dv 
|- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
c1liplem1.cn 
|- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
c1liplem1.k 
|- K = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < )
Assertion c1liplem1 
|- ( ph -> ( K e. RR /\ A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 c1liplem1.a 
 |-  ( ph -> A e. RR )
2 c1liplem1.b 
 |-  ( ph -> B e. RR )
3 c1liplem1.le 
 |-  ( ph -> A <_ B )
4 c1liplem1.f 
 |-  ( ph -> F e. ( CC ^pm RR ) )
5 c1liplem1.dv 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
6 c1liplem1.cn 
 |-  ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
7 c1liplem1.k 
 |-  K = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < )
8 imassrn 
 |-  ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ ran abs
9 absf 
 |-  abs : CC --> RR
10 frn 
 |-  ( abs : CC --> RR -> ran abs C_ RR )
11 9 10 ax-mp 
 |-  ran abs C_ RR
12 8 11 sstri 
 |-  ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR
13 12 a1i 
 |-  ( ph -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR )
14 dvf 
 |-  ( RR _D F ) : dom ( RR _D F ) --> CC
15 ffun 
 |-  ( ( RR _D F ) : dom ( RR _D F ) --> CC -> Fun ( RR _D F ) )
16 14 15 ax-mp 
 |-  Fun ( RR _D F )
17 16 a1i 
 |-  ( ph -> Fun ( RR _D F ) )
18 cncff 
 |-  ( ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( ( RR _D F ) |` ( A [,] B ) ) : ( A [,] B ) --> RR )
19 fdm 
 |-  ( ( ( RR _D F ) |` ( A [,] B ) ) : ( A [,] B ) --> RR -> dom ( ( RR _D F ) |` ( A [,] B ) ) = ( A [,] B ) )
20 5 18 19 3syl 
 |-  ( ph -> dom ( ( RR _D F ) |` ( A [,] B ) ) = ( A [,] B ) )
21 ssdmres 
 |-  ( ( A [,] B ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( A [,] B ) ) = ( A [,] B ) )
22 20 21 sylibr 
 |-  ( ph -> ( A [,] B ) C_ dom ( RR _D F ) )
23 1 rexrd 
 |-  ( ph -> A e. RR* )
24 2 rexrd 
 |-  ( ph -> B e. RR* )
25 lbicc2 
 |-  ( ( A e. RR* /\ B e. RR* /\ A <_ B ) -> A e. ( A [,] B ) )
26 23 24 3 25 syl3anc 
 |-  ( ph -> A e. ( A [,] B ) )
27 funfvima2 
 |-  ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) -> ( A e. ( A [,] B ) -> ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
28 27 imp 
 |-  ( ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) /\ A e. ( A [,] B ) ) -> ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) )
29 17 22 26 28 syl21anc 
 |-  ( ph -> ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) )
30 ffun 
 |-  ( abs : CC --> RR -> Fun abs )
31 9 30 ax-mp 
 |-  Fun abs
32 imassrn 
 |-  ( ( RR _D F ) " ( A [,] B ) ) C_ ran ( RR _D F )
33 frn 
 |-  ( ( RR _D F ) : dom ( RR _D F ) --> CC -> ran ( RR _D F ) C_ CC )
34 14 33 ax-mp 
 |-  ran ( RR _D F ) C_ CC
35 32 34 sstri 
 |-  ( ( RR _D F ) " ( A [,] B ) ) C_ CC
36 9 fdmi 
 |-  dom abs = CC
37 35 36 sseqtrri 
 |-  ( ( RR _D F ) " ( A [,] B ) ) C_ dom abs
38 funfvima2 
 |-  ( ( Fun abs /\ ( ( RR _D F ) " ( A [,] B ) ) C_ dom abs ) -> ( ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` A ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) )
39 31 37 38 mp2an 
 |-  ( ( ( RR _D F ) ` A ) e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` A ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) )
40 ne0i 
 |-  ( ( abs ` ( ( RR _D F ) ` A ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) )
41 29 39 40 3syl 
 |-  ( ph -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) )
42 ax-resscn 
 |-  RR C_ CC
43 ssid 
 |-  CC C_ CC
44 cncfss 
 |-  ( ( RR C_ CC /\ CC C_ CC ) -> ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC ) )
45 42 43 44 mp2an 
 |-  ( ( A [,] B ) -cn-> RR ) C_ ( ( A [,] B ) -cn-> CC )
46 45 5 sseldi 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) )
47 cniccbdd 
 |-  ( ( A e. RR /\ B e. RR /\ ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> CC ) ) -> E. a e. RR A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a )
48 1 2 46 47 syl3anc 
 |-  ( ph -> E. a e. RR A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a )
49 fvelima 
 |-  ( ( Fun abs /\ b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) -> E. y e. ( ( RR _D F ) " ( A [,] B ) ) ( abs ` y ) = b )
50 31 49 mpan 
 |-  ( b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) -> E. y e. ( ( RR _D F ) " ( A [,] B ) ) ( abs ` y ) = b )
51 fvres 
 |-  ( b e. ( A [,] B ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) = ( ( RR _D F ) ` b ) )
52 51 adantl 
 |-  ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) = ( ( RR _D F ) ` b ) )
53 52 fveq2d 
 |-  ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) = ( abs ` ( ( RR _D F ) ` b ) ) )
54 2fveq3 
 |-  ( x = b -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) = ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) )
55 54 breq1d 
 |-  ( x = b -> ( ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a <-> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) <_ a ) )
56 55 rspccva 
 |-  ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` b ) ) <_ a )
57 53 56 eqbrtrrd 
 |-  ( ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a /\ b e. ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` b ) ) <_ a )
58 57 adantll 
 |-  ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ b e. ( A [,] B ) ) -> ( abs ` ( ( RR _D F ) ` b ) ) <_ a )
59 fveq2 
 |-  ( ( ( RR _D F ) ` b ) = y -> ( abs ` ( ( RR _D F ) ` b ) ) = ( abs ` y ) )
60 59 breq1d 
 |-  ( ( ( RR _D F ) ` b ) = y -> ( ( abs ` ( ( RR _D F ) ` b ) ) <_ a <-> ( abs ` y ) <_ a ) )
61 58 60 syl5ibcom 
 |-  ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ b e. ( A [,] B ) ) -> ( ( ( RR _D F ) ` b ) = y -> ( abs ` y ) <_ a ) )
62 61 rexlimdva 
 |-  ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( E. b e. ( A [,] B ) ( ( RR _D F ) ` b ) = y -> ( abs ` y ) <_ a ) )
63 fvelima 
 |-  ( ( Fun ( RR _D F ) /\ y e. ( ( RR _D F ) " ( A [,] B ) ) ) -> E. b e. ( A [,] B ) ( ( RR _D F ) ` b ) = y )
64 16 63 mpan 
 |-  ( y e. ( ( RR _D F ) " ( A [,] B ) ) -> E. b e. ( A [,] B ) ( ( RR _D F ) ` b ) = y )
65 62 64 impel 
 |-  ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ y e. ( ( RR _D F ) " ( A [,] B ) ) ) -> ( abs ` y ) <_ a )
66 breq1 
 |-  ( ( abs ` y ) = b -> ( ( abs ` y ) <_ a <-> b <_ a ) )
67 65 66 syl5ibcom 
 |-  ( ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) /\ y e. ( ( RR _D F ) " ( A [,] B ) ) ) -> ( ( abs ` y ) = b -> b <_ a ) )
68 67 rexlimdva 
 |-  ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( E. y e. ( ( RR _D F ) " ( A [,] B ) ) ( abs ` y ) = b -> b <_ a ) )
69 50 68 syl5 
 |-  ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> ( b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) -> b <_ a ) )
70 69 ralrimiv 
 |-  ( ( ( ph /\ a e. RR ) /\ A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a ) -> A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a )
71 70 ex 
 |-  ( ( ph /\ a e. RR ) -> ( A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a -> A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a ) )
72 71 reximdva 
 |-  ( ph -> ( E. a e. RR A. x e. ( A [,] B ) ( abs ` ( ( ( RR _D F ) |` ( A [,] B ) ) ` x ) ) <_ a -> E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a ) )
73 48 72 mpd 
 |-  ( ph -> E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a )
74 13 41 73 suprcld 
 |-  ( ph -> sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) e. RR )
75 7 74 eqeltrid 
 |-  ( ph -> K e. RR )
76 simplrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. ( A [,] B ) )
77 76 fvresd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` y ) = ( F ` y ) )
78 cncff 
 |-  ( ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
79 6 78 syl 
 |-  ( ph -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
80 79 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
81 80 76 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` y ) e. RR )
82 81 recnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` y ) e. CC )
83 77 82 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` y ) e. CC )
84 simplrl 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. ( A [,] B ) )
85 84 fvresd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` x ) = ( F ` x ) )
86 80 84 ffvelrnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` x ) e. RR )
87 86 recnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) ` x ) e. CC )
88 85 87 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F ` x ) e. CC )
89 83 88 subcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F ` y ) - ( F ` x ) ) e. CC )
90 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
91 1 2 90 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
92 91 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A [,] B ) C_ RR )
93 92 76 sseldd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. RR )
94 92 84 sseldd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. RR )
95 93 94 resubcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. RR )
96 95 recnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. CC )
97 simpr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x < y )
98 difrp 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x < y <-> ( y - x ) e. RR+ ) )
99 94 93 98 syl2anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x < y <-> ( y - x ) e. RR+ ) )
100 97 99 mpbid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) e. RR+ )
101 100 rpne0d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( y - x ) =/= 0 )
102 89 96 101 absdivd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) = ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( abs ` ( y - x ) ) ) )
103 12 a1i 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) C_ RR )
104 41 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) =/= (/) )
105 73 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> E. a e. RR A. b e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) b <_ a )
106 31 a1i 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> Fun abs )
107 89 96 101 divcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. CC )
108 107 36 eleqtrrdi 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. dom abs )
109 94 rexrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. RR* )
110 93 rexrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. RR* )
111 94 93 97 ltled 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x <_ y )
112 ubicc2 
 |-  ( ( x e. RR* /\ y e. RR* /\ x <_ y ) -> y e. ( x [,] y ) )
113 109 110 111 112 syl3anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> y e. ( x [,] y ) )
114 113 fvresd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( x [,] y ) ) ` y ) = ( F ` y ) )
115 lbicc2 
 |-  ( ( x e. RR* /\ y e. RR* /\ x <_ y ) -> x e. ( x [,] y ) )
116 109 110 111 115 syl3anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> x e. ( x [,] y ) )
117 116 fvresd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( x [,] y ) ) ` x ) = ( F ` x ) )
118 114 117 oveq12d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) = ( ( F ` y ) - ( F ` x ) ) )
119 118 oveq1d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) = ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) )
120 iccss2 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( x [,] y ) C_ ( A [,] B ) )
121 120 ad2antlr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x [,] y ) C_ ( A [,] B ) )
122 121 resabs1d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) |` ( x [,] y ) ) = ( F |` ( x [,] y ) ) )
123 6 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
124 rescncf 
 |-  ( ( x [,] y ) C_ ( A [,] B ) -> ( ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( ( F |` ( A [,] B ) ) |` ( x [,] y ) ) e. ( ( x [,] y ) -cn-> RR ) ) )
125 121 123 124 sylc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( F |` ( A [,] B ) ) |` ( x [,] y ) ) e. ( ( x [,] y ) -cn-> RR ) )
126 122 125 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( F |` ( x [,] y ) ) e. ( ( x [,] y ) -cn-> RR ) )
127 42 a1i 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> RR C_ CC )
128 4 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> F e. ( CC ^pm RR ) )
129 cnex 
 |-  CC e. _V
130 reex 
 |-  RR e. _V
131 129 130 elpm2 
 |-  ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
132 131 simplbi 
 |-  ( F e. ( CC ^pm RR ) -> F : dom F --> CC )
133 128 132 syl 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> F : dom F --> CC )
134 131 simprbi 
 |-  ( F e. ( CC ^pm RR ) -> dom F C_ RR )
135 128 134 syl 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom F C_ RR )
136 iccssre 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x [,] y ) C_ RR )
137 94 93 136 syl2anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x [,] y ) C_ RR )
138 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
139 138 tgioo2 
 |-  ( topGen ` ran (,) ) = ( ( TopOpen ` CCfld ) |`t RR )
140 138 139 dvres 
 |-  ( ( ( RR C_ CC /\ F : dom F --> CC ) /\ ( dom F C_ RR /\ ( x [,] y ) C_ RR ) ) -> ( RR _D ( F |` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) ) )
141 127 133 135 137 140 syl22anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( RR _D ( F |` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) ) )
142 iccntr 
 |-  ( ( x e. RR /\ y e. RR ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) = ( x (,) y ) )
143 94 93 142 syl2anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) = ( x (,) y ) )
144 143 reseq2d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( RR _D F ) |` ( ( int ` ( topGen ` ran (,) ) ) ` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( x (,) y ) ) )
145 141 144 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( RR _D ( F |` ( x [,] y ) ) ) = ( ( RR _D F ) |` ( x (,) y ) ) )
146 145 dmeqd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom ( RR _D ( F |` ( x [,] y ) ) ) = dom ( ( RR _D F ) |` ( x (,) y ) ) )
147 ioossicc 
 |-  ( x (,) y ) C_ ( x [,] y )
148 147 121 sstrid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x (,) y ) C_ ( A [,] B ) )
149 22 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A [,] B ) C_ dom ( RR _D F ) )
150 148 149 sstrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( x (,) y ) C_ dom ( RR _D F ) )
151 ssdmres 
 |-  ( ( x (,) y ) C_ dom ( RR _D F ) <-> dom ( ( RR _D F ) |` ( x (,) y ) ) = ( x (,) y ) )
152 150 151 sylib 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom ( ( RR _D F ) |` ( x (,) y ) ) = ( x (,) y ) )
153 146 152 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> dom ( RR _D ( F |` ( x [,] y ) ) ) = ( x (,) y ) )
154 94 93 97 126 153 mvth 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> E. a e. ( x (,) y ) ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) )
155 145 fveq1d 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) )
156 155 adantrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) )
157 fvres 
 |-  ( a e. ( x (,) y ) -> ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) = ( ( RR _D F ) ` a ) )
158 157 ad2antll 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( ( RR _D F ) |` ( x (,) y ) ) ` a ) = ( ( RR _D F ) ` a ) )
159 156 158 eqtrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( RR _D F ) ` a ) )
160 16 a1i 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> Fun ( RR _D F ) )
161 22 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( A [,] B ) C_ dom ( RR _D F ) )
162 148 sseld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( a e. ( x (,) y ) -> a e. ( A [,] B ) ) )
163 162 impr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> a e. ( A [,] B ) )
164 funfvima2 
 |-  ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) -> ( a e. ( A [,] B ) -> ( ( RR _D F ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
165 164 imp 
 |-  ( ( ( Fun ( RR _D F ) /\ ( A [,] B ) C_ dom ( RR _D F ) ) /\ a e. ( A [,] B ) ) -> ( ( RR _D F ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) )
166 160 161 163 165 syl21anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D F ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) )
167 159 166 eqeltrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) )
168 eleq1 
 |-  ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) e. ( ( RR _D F ) " ( A [,] B ) ) <-> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
169 167 168 syl5ibcom 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ ( x < y /\ a e. ( x (,) y ) ) ) -> ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
170 169 expr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( a e. ( x (,) y ) -> ( ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) ) )
171 170 rexlimdv 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( E. a e. ( x (,) y ) ( ( RR _D ( F |` ( x [,] y ) ) ) ` a ) = ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) )
172 154 171 mpd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( ( F |` ( x [,] y ) ) ` y ) - ( ( F |` ( x [,] y ) ) ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) )
173 119 172 eqeltrrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) )
174 funfvima 
 |-  ( ( Fun abs /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. dom abs ) -> ( ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) ) )
175 174 imp 
 |-  ( ( ( Fun abs /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. dom abs ) /\ ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) e. ( ( RR _D F ) " ( A [,] B ) ) ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) )
176 106 108 173 175 syl21anc 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) e. ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) )
177 103 104 105 176 suprubd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) <_ sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) )
178 177 7 breqtrrdi 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( ( F ` y ) - ( F ` x ) ) / ( y - x ) ) ) <_ K )
179 102 178 eqbrtrrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( abs ` ( y - x ) ) ) <_ K )
180 89 abscld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) e. RR )
181 75 ad2antrr 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> K e. RR )
182 96 101 absrpcld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( y - x ) ) e. RR+ )
183 180 181 182 ledivmuld 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( ( abs ` ( ( F ` y ) - ( F ` x ) ) ) / ( abs ` ( y - x ) ) ) <_ K <-> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( ( abs ` ( y - x ) ) x. K ) ) )
184 179 183 mpbid 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( ( abs ` ( y - x ) ) x. K ) )
185 182 rpcnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( y - x ) ) e. CC )
186 181 recnd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> K e. CC )
187 185 186 mulcomd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( abs ` ( y - x ) ) x. K ) = ( K x. ( abs ` ( y - x ) ) ) )
188 184 187 breqtrd 
 |-  ( ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) )
189 188 ex 
 |-  ( ( ph /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) )
190 189 ralrimivva 
 |-  ( ph -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) )
191 75 190 jca 
 |-  ( ph -> ( K e. RR /\ A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( K x. ( abs ` ( y - x ) ) ) ) ) )