:: Some Properties of Functions Modul and Signum
::  by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, XREAL_0, ORDINAL1, COMPLEX1, CARD_1, XXREAL_0, ARYTM_1,
      ARYTM_3, RELAT_1, SQUARE_1, REAL_1, ABSVALUE, INT_1, NAT_1;
 notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, INT_1, NAT_1,
      COMPLEX1, SQUARE_1, XXREAL_0;
 constructors REAL_1, SQUARE_1, COMPLEX1, INT_1;
 registrations XXREAL_0, XREAL_0, REAL_1, ORDINAL1, XBOOLE_0, INT_1;
 requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;


begin :: Absolute value

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

definition
  let x be real number;
  redefine func |.x.| equals
:: ABSVALUE:def 1

  x if 0 <= x otherwise -x;
end;

theorem :: ABSVALUE:1
  abs x = x or abs x = -x;

theorem :: ABSVALUE:2
  x = 0 iff abs x = 0;

theorem :: ABSVALUE:3
  abs x = -x & x <> 0 implies x < 0;

theorem :: ABSVALUE:4
  -abs x <= x & x <= abs x;

theorem :: ABSVALUE:5
  -y <= x & x <= y iff abs x <= y;

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

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

theorem :: ABSVALUE:8 :: SQUARE_1:98
  0 <= x*y implies sqrt (x*y) = sqrt abs(x)*sqrt abs(y);

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

theorem :: ABSVALUE:10 :: SQUARE_1:100
  0 < x/y implies sqrt (x/y) = sqrt abs(x) / sqrt abs(y);

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

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

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

:: Signum function

definition
  let x;
  func sgn x -> real number equals
:: ABSVALUE:def 2

  1 if 0 < x, -1 if x < 0 otherwise 0;
  projectivity;
end;

registration
  let x;
  cluster sgn x -> integer;
end;

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

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

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

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

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

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

canceled;

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

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

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

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

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

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

:: from SCMPDS_9. 2008.05.06, A.T.

reserve r, s for real number;

theorem :: ABSVALUE:26
  0 <= r + abs(r);

theorem :: ABSVALUE:27
  0 <= -r + abs(r);

theorem :: ABSVALUE:28
  abs(r) = abs(s) implies r = s or r = -s;

theorem :: ABSVALUE:29
  for m being Nat holds
  m = abs m;

:: from JORDAN2C, 2011.07.03, A.T,

theorem :: ABSVALUE:30
  r<=0 implies abs(r)=-r;