let f be Function of REAL,REAL; :: thesis: for a, b, c, d, r, s being Real st ( for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ) holds

f is Lipschitzian

let a, b, c, d, r, s be Real; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ) implies f is Lipschitzian )

assume A1: for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ; :: thesis: f is Lipschitzian

ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

f is Lipschitzian

let a, b, c, d, r, s be Real; :: thesis: ( ( for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ) implies f is Lipschitzian )

assume A1: for x being Real holds f . x = max (r,(min (s,((c * (sin ((a * x) + b))) + d)))) ; :: thesis: f is Lipschitzian

ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

proof
end;

hence
f is Lipschitzian
; :: thesis: verumper cases
( c = 0 or c <> 0 )
;

end;

suppose C1:
c = 0
; :: thesis: ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

take
1
; :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum

end;|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

proof

hence
( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )

assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((0 * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((0 * (sin ((a * x2) + b))) + d)))))).| by C1, A1

.= 0 by COMPLEX1:44 ;

hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum

end;assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((0 * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((0 * (sin ((a * x2) + b))) + d)))))).| by C1, A1

.= 0 by COMPLEX1:44 ;

hence |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| by COMPLEX1:46; :: thesis: verum

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum

suppose A3:
c <> 0
; :: thesis: ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

end;

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

per cases
( a = 0 or a <> 0 )
;

end;

suppose A0:
a = 0
; :: thesis: ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

take
1
; :: thesis: ( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum

end;|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) )

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).|

proof

hence
( 0 < 1 & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| )

|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((c * (sin ((0 * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((0 * x2) + b))) + d)))))).| by A0, A1

.= 0 by COMPLEX1:44 ;

hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) by COMPLEX1:46; :: thesis: verum

end;|.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((c * (sin ((0 * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((0 * x2) + b))) + d)))))).| by A0, A1

.= 0 by COMPLEX1:44 ;

hence ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) by COMPLEX1:46; :: thesis: verum

|.((f . x1) - (f . x2)).| <= 1 * |.(x1 - x2).| ) ) ; :: thesis: verum

suppose A2:
a <> 0
; :: thesis: ex r being Real st

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

( 0 < r & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= r * |.(x1 - x2).| ) )

take
|.a.| * |.c.|
; :: thesis: ( 0 < |.a.| * |.c.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| ) )

A5: ( |.c.| > 0 & |.a.| > 0 ) by A2, A3, COMPLEX1:47;

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).|

|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| ) ) by A5; :: thesis: verum

end;|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| ) )

A5: ( |.c.| > 0 & |.a.| > 0 ) by A2, A3, COMPLEX1:47;

for x1, x2 being Real st x1 in dom f & x2 in dom f holds

|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).|

proof

hence
( 0 < |.a.| * |.c.| & ( for x1, x2 being Real st x1 in dom f & x2 in dom f holds
let x1, x2 be Real; :: thesis: ( x1 in dom f & x2 in dom f implies |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| )

assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).|

A9: |.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((a * x2) + b))) + d)))))).| by A1 ;

A7: |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((a * x2) + b))) + d)))))).| <= |.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| by LeMM01;

A8: |.c.| * |.(((a * x1) + b) - ((a * x2) + b)).| = |.c.| * |.(a * (x1 - x2)).|

.= |.c.| * (|.a.| * |.(x1 - x2).|) by COMPLEX1:65 ;

A6: ( |.(c * ((sin ((a * x1) + b)) - (sin ((a * x2) + b)))).| = |.c.| * |.((sin ((a * x1) + b)) - (sin ((a * x2) + b))).| & |.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| = |.(c * ((sin ((a * x1) + b)) - (sin ((a * x2) + b)))).| ) by COMPLEX1:65;

|.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| <= |.c.| * |.(((a * x1) + b) - ((a * x2) + b)).| by XREAL_1:64, A5, A6, LmSin2;

hence |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| by A9, A8, A7, XXREAL_0:2; :: thesis: verum

end;assume ( x1 in dom f & x2 in dom f ) ; :: thesis: |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).|

A9: |.((f . x1) - (f . x2)).| = |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (f . x2)).| by A1

.= |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((a * x2) + b))) + d)))))).| by A1 ;

A7: |.((max (r,(min (s,((c * (sin ((a * x1) + b))) + d))))) - (max (r,(min (s,((c * (sin ((a * x2) + b))) + d)))))).| <= |.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| by LeMM01;

A8: |.c.| * |.(((a * x1) + b) - ((a * x2) + b)).| = |.c.| * |.(a * (x1 - x2)).|

.= |.c.| * (|.a.| * |.(x1 - x2).|) by COMPLEX1:65 ;

A6: ( |.(c * ((sin ((a * x1) + b)) - (sin ((a * x2) + b)))).| = |.c.| * |.((sin ((a * x1) + b)) - (sin ((a * x2) + b))).| & |.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| = |.(c * ((sin ((a * x1) + b)) - (sin ((a * x2) + b)))).| ) by COMPLEX1:65;

|.(((c * (sin ((a * x1) + b))) + d) - ((c * (sin ((a * x2) + b))) + d)).| <= |.c.| * |.(((a * x1) + b) - ((a * x2) + b)).| by XREAL_1:64, A5, A6, LmSin2;

hence |.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| by A9, A8, A7, XXREAL_0:2; :: thesis: verum

|.((f . x1) - (f . x2)).| <= (|.a.| * |.c.|) * |.(x1 - x2).| ) ) by A5; :: thesis: verum