Metamath Proof Explorer

Theorem c1lip1

Description: C^1 functions are Lipschitz continuous on closed intervals. (Contributed by Stefan O'Rear, 16-Nov-2014)

Ref Expression
Hypotheses c1lip1.a 
|- ( ph -> A e. RR )
c1lip1.b 
|- ( ph -> B e. RR )
c1lip1.f 
|- ( ph -> F e. ( CC ^pm RR ) )
c1lip1.dv 
|- ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
c1lip1.cn 
|- ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
Assertion c1lip1 
|- ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )

Proof

Step Hyp Ref Expression
1 c1lip1.a 
 |-  ( ph -> A e. RR )
2 c1lip1.b 
 |-  ( ph -> B e. RR )
3 c1lip1.f 
 |-  ( ph -> F e. ( CC ^pm RR ) )
4 c1lip1.dv 
 |-  ( ph -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
5 c1lip1.cn 
 |-  ( ph -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
6 0re 
 |-  0 e. RR
7 6 ne0ii 
 |-  RR =/= (/)
8 ral0 
 |-  A. x e. (/) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) )
9 1 rexrd 
 |-  ( ph -> A e. RR* )
10 2 rexrd 
 |-  ( ph -> B e. RR* )
11 icc0 
 |-  ( ( A e. RR* /\ B e. RR* ) -> ( ( A [,] B ) = (/) <-> B < A ) )
12 9 10 11 syl2anc 
 |-  ( ph -> ( ( A [,] B ) = (/) <-> B < A ) )
13 12 biimpar 
 |-  ( ( ph /\ B < A ) -> ( A [,] B ) = (/) )
14 13 raleqdv 
 |-  ( ( ph /\ B < A ) -> ( A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) <-> A. x e. (/) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
15 8 14 mpbiri 
 |-  ( ( ph /\ B < A ) -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
16 15 ralrimivw 
 |-  ( ( ph /\ B < A ) -> A. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
17 r19.2z 
 |-  ( ( RR =/= (/) /\ A. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
18 7 16 17 sylancr 
 |-  ( ( ph /\ B < A ) -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
19 1 adantr 
 |-  ( ( ph /\ A <_ B ) -> A e. RR )
20 2 adantr 
 |-  ( ( ph /\ A <_ B ) -> B e. RR )
21 simpr 
 |-  ( ( ph /\ A <_ B ) -> A <_ B )
22 3 adantr 
 |-  ( ( ph /\ A <_ B ) -> F e. ( CC ^pm RR ) )
23 4 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( ( RR _D F ) |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
24 5 adantr 
 |-  ( ( ph /\ A <_ B ) -> ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) )
25 eqid 
 |-  sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < )
26 19 20 21 22 23 24 25 c1liplem1 
 |-  ( ( ph /\ A <_ B ) -> ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) e. RR /\ A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) x. ( abs ` ( b - a ) ) ) ) ) )
27 oveq1 
 |-  ( k = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) -> ( k x. ( abs ` ( b - a ) ) ) = ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) x. ( abs ` ( b - a ) ) ) )
28 27 breq2d 
 |-  ( k = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) x. ( abs ` ( b - a ) ) ) ) )
29 28 imbi2d 
 |-  ( k = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) -> ( ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) <-> ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) x. ( abs ` ( b - a ) ) ) ) ) )
30 29 2ralbidv 
 |-  ( k = sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) <-> A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) x. ( abs ` ( b - a ) ) ) ) ) )
31 30 rspcev 
 |-  ( ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) e. RR /\ A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( sup ( ( abs " ( ( RR _D F ) " ( A [,] B ) ) ) , RR , < ) x. ( abs ` ( b - a ) ) ) ) ) -> E. k e. RR A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) )
32 26 31 syl 
 |-  ( ( ph /\ A <_ B ) -> E. k e. RR A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) )
33 breq1 
 |-  ( a = x -> ( a < b <-> x < b ) )
34 fveq2 
 |-  ( a = x -> ( F ` a ) = ( F ` x ) )
35 34 oveq2d 
 |-  ( a = x -> ( ( F ` b ) - ( F ` a ) ) = ( ( F ` b ) - ( F ` x ) ) )
36 35 fveq2d 
 |-  ( a = x -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = ( abs ` ( ( F ` b ) - ( F ` x ) ) ) )
37 oveq2 
 |-  ( a = x -> ( b - a ) = ( b - x ) )
38 37 fveq2d 
 |-  ( a = x -> ( abs ` ( b - a ) ) = ( abs ` ( b - x ) ) )
39 38 oveq2d 
 |-  ( a = x -> ( k x. ( abs ` ( b - a ) ) ) = ( k x. ( abs ` ( b - x ) ) ) )
40 36 39 breq12d 
 |-  ( a = x -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( b - x ) ) ) ) )
41 33 40 imbi12d 
 |-  ( a = x -> ( ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) <-> ( x < b -> ( abs ` ( ( F ` b ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( b - x ) ) ) ) ) )
42 breq2 
 |-  ( b = y -> ( x < b <-> x < y ) )
43 fveq2 
 |-  ( b = y -> ( F ` b ) = ( F ` y ) )
44 43 fvoveq1d 
 |-  ( b = y -> ( abs ` ( ( F ` b ) - ( F ` x ) ) ) = ( abs ` ( ( F ` y ) - ( F ` x ) ) ) )
45 fvoveq1 
 |-  ( b = y -> ( abs ` ( b - x ) ) = ( abs ` ( y - x ) ) )
46 45 oveq2d 
 |-  ( b = y -> ( k x. ( abs ` ( b - x ) ) ) = ( k x. ( abs ` ( y - x ) ) ) )
47 44 46 breq12d 
 |-  ( b = y -> ( ( abs ` ( ( F ` b ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( b - x ) ) ) <-> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
48 42 47 imbi12d 
 |-  ( b = y -> ( ( x < b -> ( abs ` ( ( F ` b ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( b - x ) ) ) ) <-> ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) ) )
49 41 48 rspc2v 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) ) )
50 49 ad2antlr 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) ) )
51 pm2.27 
 |-  ( x < y -> ( ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
52 51 adantl 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( ( x < y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
53 50 52 syld 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x < y ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
54 0le0 
 |-  0 <_ 0
55 fvres 
 |-  ( x e. ( A [,] B ) -> ( ( F |` ( A [,] B ) ) ` x ) = ( F ` x ) )
56 55 ad2antrl 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( F |` ( A [,] B ) ) ` x ) = ( F ` x ) )
57 cncff 
 |-  ( ( F |` ( A [,] B ) ) e. ( ( A [,] B ) -cn-> RR ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
58 5 57 syl 
 |-  ( ph -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
59 58 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ k e. RR ) -> ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR )
60 simpl 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> x e. ( A [,] B ) )
61 ffvelrn 
 |-  ( ( ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR /\ x e. ( A [,] B ) ) -> ( ( F |` ( A [,] B ) ) ` x ) e. RR )
62 59 60 61 syl2an 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( F |` ( A [,] B ) ) ` x ) e. RR )
63 56 62 eqeltrrd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( F ` x ) e. RR )
64 63 recnd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( F ` x ) e. CC )
65 64 subidd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( F ` x ) - ( F ` x ) ) = 0 )
66 65 abs00bd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` x ) - ( F ` x ) ) ) = 0 )
67 iccssre 
 |-  ( ( A e. RR /\ B e. RR ) -> ( A [,] B ) C_ RR )
68 1 2 67 syl2anc 
 |-  ( ph -> ( A [,] B ) C_ RR )
69 68 ad3antrrr 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( A [,] B ) C_ RR )
70 simprl 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> x e. ( A [,] B ) )
71 69 70 sseldd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> x e. RR )
72 71 recnd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> x e. CC )
73 72 subidd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x - x ) = 0 )
74 73 abs00bd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( abs ` ( x - x ) ) = 0 )
75 74 oveq2d 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( k x. ( abs ` ( x - x ) ) ) = ( k x. 0 ) )
76 simplr 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> k e. RR )
77 76 recnd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> k e. CC )
78 77 mul01d 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( k x. 0 ) = 0 )
79 75 78 eqtrd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( k x. ( abs ` ( x - x ) ) ) = 0 )
80 66 79 breq12d 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( abs ` ( ( F ` x ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( x - x ) ) ) <-> 0 <_ 0 ) )
81 54 80 mpbiri 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` x ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( x - x ) ) ) )
82 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
83 82 fvoveq1d 
 |-  ( x = y -> ( abs ` ( ( F ` x ) - ( F ` x ) ) ) = ( abs ` ( ( F ` y ) - ( F ` x ) ) ) )
84 fvoveq1 
 |-  ( x = y -> ( abs ` ( x - x ) ) = ( abs ` ( y - x ) ) )
85 84 oveq2d 
 |-  ( x = y -> ( k x. ( abs ` ( x - x ) ) ) = ( k x. ( abs ` ( y - x ) ) ) )
86 83 85 breq12d 
 |-  ( x = y -> ( ( abs ` ( ( F ` x ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( x - x ) ) ) <-> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
87 81 86 syl5ibcom 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x = y -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
88 87 imp 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x = y ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
89 88 a1d 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ x = y ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
90 breq1 
 |-  ( a = y -> ( a < b <-> y < b ) )
91 fveq2 
 |-  ( a = y -> ( F ` a ) = ( F ` y ) )
92 91 oveq2d 
 |-  ( a = y -> ( ( F ` b ) - ( F ` a ) ) = ( ( F ` b ) - ( F ` y ) ) )
93 92 fveq2d 
 |-  ( a = y -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) = ( abs ` ( ( F ` b ) - ( F ` y ) ) ) )
94 oveq2 
 |-  ( a = y -> ( b - a ) = ( b - y ) )
95 94 fveq2d 
 |-  ( a = y -> ( abs ` ( b - a ) ) = ( abs ` ( b - y ) ) )
96 95 oveq2d 
 |-  ( a = y -> ( k x. ( abs ` ( b - a ) ) ) = ( k x. ( abs ` ( b - y ) ) ) )
97 93 96 breq12d 
 |-  ( a = y -> ( ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) <-> ( abs ` ( ( F ` b ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( b - y ) ) ) ) )
98 90 97 imbi12d 
 |-  ( a = y -> ( ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) <-> ( y < b -> ( abs ` ( ( F ` b ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( b - y ) ) ) ) ) )
99 breq2 
 |-  ( b = x -> ( y < b <-> y < x ) )
100 fveq2 
 |-  ( b = x -> ( F ` b ) = ( F ` x ) )
101 100 fvoveq1d 
 |-  ( b = x -> ( abs ` ( ( F ` b ) - ( F ` y ) ) ) = ( abs ` ( ( F ` x ) - ( F ` y ) ) ) )
102 fvoveq1 
 |-  ( b = x -> ( abs ` ( b - y ) ) = ( abs ` ( x - y ) ) )
103 102 oveq2d 
 |-  ( b = x -> ( k x. ( abs ` ( b - y ) ) ) = ( k x. ( abs ` ( x - y ) ) ) )
104 101 103 breq12d 
 |-  ( b = x -> ( ( abs ` ( ( F ` b ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( b - y ) ) ) <-> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) ) )
105 99 104 imbi12d 
 |-  ( b = x -> ( ( y < b -> ( abs ` ( ( F ` b ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( b - y ) ) ) ) <-> ( y < x -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) ) ) )
106 98 105 rspc2v 
 |-  ( ( y e. ( A [,] B ) /\ x e. ( A [,] B ) ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( y < x -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) ) ) )
107 106 ancoms 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( y < x -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) ) ) )
108 107 ad2antlr 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( y < x -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) ) ) )
109 simpr 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> y < x )
110 fvres 
 |-  ( y e. ( A [,] B ) -> ( ( F |` ( A [,] B ) ) ` y ) = ( F ` y ) )
111 110 ad2antll 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( F |` ( A [,] B ) ) ` y ) = ( F ` y ) )
112 simpr 
 |-  ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> y e. ( A [,] B ) )
113 ffvelrn 
 |-  ( ( ( F |` ( A [,] B ) ) : ( A [,] B ) --> RR /\ y e. ( A [,] B ) ) -> ( ( F |` ( A [,] B ) ) ` y ) e. RR )
114 59 112 113 syl2an 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( ( F |` ( A [,] B ) ) ` y ) e. RR )
115 111 114 eqeltrrd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( F ` y ) e. RR )
116 115 recnd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( F ` y ) e. CC )
117 64 116 abssubd 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) = ( abs ` ( ( F ` y ) - ( F ` x ) ) ) )
118 117 adantr 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) = ( abs ` ( ( F ` y ) - ( F ` x ) ) ) )
119 68 ad2antrr 
 |-  ( ( ( ph /\ A <_ B ) /\ k e. RR ) -> ( A [,] B ) C_ RR )
120 119 sseld 
 |-  ( ( ( ph /\ A <_ B ) /\ k e. RR ) -> ( x e. ( A [,] B ) -> x e. RR ) )
121 119 sseld 
 |-  ( ( ( ph /\ A <_ B ) /\ k e. RR ) -> ( y e. ( A [,] B ) -> y e. RR ) )
122 120 121 anim12d 
 |-  ( ( ( ph /\ A <_ B ) /\ k e. RR ) -> ( ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) -> ( x e. RR /\ y e. RR ) ) )
123 122 imp 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x e. RR /\ y e. RR ) )
124 recn 
 |-  ( x e. RR -> x e. CC )
125 recn 
 |-  ( y e. RR -> y e. CC )
126 abssub 
 |-  ( ( x e. CC /\ y e. CC ) -> ( abs ` ( x - y ) ) = ( abs ` ( y - x ) ) )
127 124 125 126 syl2an 
 |-  ( ( x e. RR /\ y e. RR ) -> ( abs ` ( x - y ) ) = ( abs ` ( y - x ) ) )
128 123 127 syl 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( abs ` ( x - y ) ) = ( abs ` ( y - x ) ) )
129 128 adantr 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( abs ` ( x - y ) ) = ( abs ` ( y - x ) ) )
130 129 oveq2d 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( k x. ( abs ` ( x - y ) ) ) = ( k x. ( abs ` ( y - x ) ) ) )
131 118 130 breq12d 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) <-> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
132 131 biimpd 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
133 109 132 embantd 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( ( y < x -> ( abs ` ( ( F ` x ) - ( F ` y ) ) ) <_ ( k x. ( abs ` ( x - y ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
134 108 133 syld 
 |-  ( ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) /\ y < x ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
135 lttri4 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x < y \/ x = y \/ y < x ) )
136 123 135 syl 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( x < y \/ x = y \/ y < x ) )
137 53 89 134 136 mpjao3dan 
 |-  ( ( ( ( ph /\ A <_ B ) /\ k e. RR ) /\ ( x e. ( A [,] B ) /\ y e. ( A [,] B ) ) ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
138 137 ralrimdvva 
 |-  ( ( ( ph /\ A <_ B ) /\ k e. RR ) -> ( A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
139 138 reximdva 
 |-  ( ( ph /\ A <_ B ) -> ( E. k e. RR A. a e. ( A [,] B ) A. b e. ( A [,] B ) ( a < b -> ( abs ` ( ( F ` b ) - ( F ` a ) ) ) <_ ( k x. ( abs ` ( b - a ) ) ) ) -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) ) )
140 32 139 mpd 
 |-  ( ( ph /\ A <_ B ) -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )
141 18 140 2 1 ltlecasei 
 |-  ( ph -> E. k e. RR A. x e. ( A [,] B ) A. y e. ( A [,] B ) ( abs ` ( ( F ` y ) - ( F ` x ) ) ) <_ ( k x. ( abs ` ( y - x ) ) ) )