The abstract of the Mizar article:

Some Properties of Functions Modul and Signum

by

Jan Popiolek

Received June 21, 1989

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);