Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

Some Properties of Functions Modul and Signum

by
Jan Popiolek

MML identifier: ABSVALUE
[ Mizar article, MML identifier index ]

environ

vocabulary ARYTM, ARYTM_1, ARYTM_3, RELAT_1, ABSVALUE;
notation ORDINAL1, XCMPLX_0, XREAL_0, REAL_1;
constructors REAL_1, XCMPLX_0, XREAL_0, XBOOLE_0;
clusters XREAL_0, REAL_1, ARYTM_3, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, ARITHM;

begin

reserve x, y, z, s, t for real number;

definition let x;
func abs x -> real number equals
:: ABSVALUE:def 1
x if 0 <= x
otherwise -x;
projectivity;
end;

definition let x be Real;
redefine func abs x -> Real;
end;

canceled 4;

theorem :: ABSVALUE:5
0 <= abs(x);

theorem :: ABSVALUE:6
x <> 0 implies 0 < abs(x);

theorem :: ABSVALUE:7
x = 0 iff abs(x) = 0;

canceled;

theorem :: ABSVALUE:9
abs(x) = -x & x <> 0 implies x < 0;

theorem :: ABSVALUE:10
abs(x*y) = abs(x) * abs(y);

theorem :: ABSVALUE:11
-abs(x) <= x & x <= abs(x);

theorem :: ABSVALUE:12
-y <= x & x <= y iff abs(x) <= y;

theorem :: ABSVALUE:13
abs(x+y) <= abs(x) + abs(y);

theorem :: ABSVALUE:14
x <> 0 implies abs(x) * abs(1/x) = 1;

theorem :: ABSVALUE:15
abs(1/x) = 1/abs(x);

theorem :: ABSVALUE:16
abs(x/y) = abs(x)/abs(y);

theorem :: ABSVALUE:17
abs(x) = abs(-x);

theorem :: ABSVALUE:18
abs(x) - abs(y) <= abs(x-y);

theorem :: ABSVALUE:19
abs(x-y) <= abs(x) + abs(y);

canceled;

theorem :: ABSVALUE:21
abs(x) <= z & abs(y) <= t implies abs(x+y) <= z + t;

theorem :: ABSVALUE:22
abs(abs(x) - abs(y)) <= abs(x-y);

canceled;

theorem :: ABSVALUE:24
0 <= x * y implies abs(x+y) = abs(x) + abs(y);

theorem :: ABSVALUE:25
abs(x+y) = abs(x) + abs(y) implies 0 <= x * y;

theorem :: ABSVALUE:26
abs(x+y)/(1 + abs(x+y)) <= abs(x)/(1 + abs(x)) + abs(y)/(1 +abs(y));

definition let x;
func sgn x equals
:: ABSVALUE:def 2
1 if 0 < x,
-1 if x < 0
otherwise 0;
end;

definition let x;
cluster sgn x -> real;
end;

definition let x be Real;
redefine func sgn x -> Real;
end;

canceled 4;

theorem :: ABSVALUE:31
sgn x = 1 implies 0 < x;

theorem :: ABSVALUE:32
sgn x = -1 implies x < 0;

theorem :: ABSVALUE:33
sgn x = 0 implies x = 0;

theorem :: ABSVALUE:34
x = abs(x) * sgn x;

theorem :: ABSVALUE:35
sgn (x * y) = sgn x * sgn y;

theorem :: ABSVALUE:36
sgn sgn x = sgn x;

theorem :: ABSVALUE:37
sgn (x + y) <= sgn x + sgn y + 1;

theorem :: ABSVALUE:38
x <> 0 implies sgn x * sgn (1/x) = 1;

theorem :: ABSVALUE:39
1/(sgn x) = sgn (1/x);

theorem :: ABSVALUE:40
sgn x + sgn y - 1 <= sgn ( x + y );

theorem :: ABSVALUE:41
sgn x = sgn (1/x);

theorem :: ABSVALUE:42
sgn (x/y) = (sgn x)/(sgn y);