:: Some Properties of Functions Modul and Signum
::  by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990-2019 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, 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, COMPLEX1,
      SQUARE_1, XXREAL_0;
 constructors REAL_1, SQUARE_1, COMPLEX1, INT_1, XXREAL_0;
 registrations XXREAL_0, XREAL_0, ORDINAL1, NAT_1, INT_1;
 requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
 theorems XCMPLX_0, XCMPLX_1, COMPLEX1, SQUARE_1, XREAL_1, XXREAL_0;

begin :: Absolute value

reserve x, y, z, r, s, t for Real;

definition let x be Real;
  redefine func |.x.| equals  :Def1:
  x if 0 <= x otherwise -x;
  correctness by COMPLEX1:43,70;
end;

registration
  let x be non negative Real;
  reduce |.x.| to x;
  reducibility by Def1;
end;

theorem
  |.x.| = x or |.x.| = -x by Def1;

theorem
  x = 0 iff |.x.| = 0 by COMPLEX1:47;

theorem
  |.x.| = -x & x <> 0 implies x < 0 by Def1;

theorem
  -|.x.| <= x & x <= |.x.|
proof
  per cases;
  suppose
A1: x < 0;
    then |.x.| = -x by Def1;
    hence thesis by A1;
  end;
  suppose
A2: 0 <= x;
    then -x <= -0;
    hence thesis by A2,Def1;
  end;
end;

theorem
  -y <= x & x <= y iff |.x.| <= y
proof
  hereby
    assume that
A1: -y <= x and
A2: x <= y;
    -x <= --y by A1,XREAL_1:24;
    hence |.x.| <= y by A2,Def1;
  end;
  assume
A3: |.x.| <= y;
    then
A4: 0 <= y by COMPLEX1:46;
  per cases;
  suppose 0 < x;
    hence thesis by A3,A4,Def1;
  end;
  suppose
A5: x < 0;
    then -x <= y by A3,Def1;
    then -y <= --x by XREAL_1:24;
    hence thesis by A5;
  end;
  suppose x = -0;
    hence thesis by A3;
  end;
end;

theorem
  x <> 0 implies |.x.| * |.1/x.| = 1
proof
  assume x <> 0;
  then |.x.| * |.1/x.| = |.x * (1/x).| & |.x * (1/x).| = |.1.|
  by COMPLEX1:65,XCMPLX_1:106;
  hence thesis;
end;

theorem
  |.1/x.| = 1/|.x.| by COMPLEX1:80;

theorem :: SQUARE_1:98
  0 <= x*y implies sqrt (x*y) = sqrt |.x.|*sqrt |.y.|
proof
  assume 0 <= x*y;
  then |.x*y.| = x*y by Def1;
  then
A1: |.x.|*|.y.| = x*y by COMPLEX1:65;
  0 <= |.x.| & 0 <= |.y.| by COMPLEX1:46;
  hence thesis by A1,SQUARE_1:29;
end;

theorem
  |.x.| <= z & |.y.| <= t implies |.x+y.| <= z + t
proof
  assume |.x.| <= z & |.y.| <= t;
  then |.x+y.| <= |.x.| + |.y.| & |.x.| + |.y.| <= z + t by COMPLEX1:56
,XREAL_1:7;
  hence thesis by XXREAL_0:2;
end;

theorem :: SQUARE_1:100
  0 < x/y implies sqrt (x/y) = sqrt |.x.| / sqrt |.y.|
proof
  assume 0 < x/y;
  then x/y = |.x/y.| by Def1;
  then
A1: x/y = |.x.|/|.y.| by COMPLEX1:67;
  0 <= |.x.| & 0 <= |.y.| by COMPLEX1:46;
  hence thesis by A1,SQUARE_1:30;
end;

theorem
  0 <= x * y implies |.x+y.| = |.x.| + |.y.|
proof
  assume
A1: 0 <= x * y;
  per cases by A1;
  suppose
 x * y = 0;
    then x = 0 or y = 0 by XCMPLX_1:6;
    hence thesis;
  end;
  suppose
A5: 0 < x * y;
    then
A6: x <> 0 & y <> 0;
    per cases by A5,A6;
    suppose that
A7:   0 < x & 0 < y;
      |.x.| = x & |.y.| = y by A7,Def1;
      hence thesis by A7,Def1;
    end;
    suppose that
A8:   x < 0 and
A9:   y < 0;
      |.x.| = -x by A8,Def1;
      then |.x.| + |.y.| = (-1) * x + -(1 * y) by A9,Def1
        .= - ( x + y );
      hence thesis by A8,A9,Def1;
    end;
  end;
end;

theorem
  |.x+y.| = |.x.| + |.y.| implies 0 <= x * y
proof
A1: x * y < 0 implies x < 0 & 0 < y or 0 < x & y < 0
  proof
    assume
A2: x * y < 0;
    then x <> 0 & y <> 0;
    hence thesis by A2;
  end;
A3: x < 0 & 0 < y & x + y < 0 implies |.x+y.| <> |.x.| + |.y.|
  proof
    assume that
A4: x < 0 and
A5: 0 < y and
A6: x + y < 0;
    -(1 * x) + -y < -x + y by A5,XREAL_1:6;
    then
A7: -( 1 * ( x + y ) ) < -x + y;
    |.x.| = -x & |.y.| = y by A4,A5,Def1;
    hence thesis by A6,A7,Def1;
  end;
A8: 0 < x & y < 0 & x + y < 0 implies |.x+y.| <> |.x.| + |.y.|
  proof
    assume that
A9: 0 < x and
A10: y < 0 and
A11: x + y < 0;
    -(1 * x) + -y < x + -y by A9,XREAL_1:6;
    then
A12: - (1 * ( x + y )) < x + -y;
    |.x.| = x & |.y.| = -y by A9,A10,Def1;
    hence thesis by A11,A12,Def1;
  end;
A13: 0 < x & y < 0 & 0 <= x + y implies |.x+y.| <> |.x.| + |.y.|
  proof
    assume that
A14: 0 < x and
A15: y < 0 and
A16: 0 <= x + y;
A17: |.y.| = -y by A15,Def1;
    x + y < x + -y & |.x.| = x by A14,A15,Def1,XREAL_1:6;
    hence thesis by A16,A17,Def1;
  end;
A18: x < 0 & 0 < y & 0 <= x + y implies |.x+y.| <> |.x.| + |.y.|
  proof
    assume that
A19: x < 0 and
A20: 0 < y and
A21: 0 <= x + y;
A22: |.y.| = y by A20,Def1;
    x + y < -x + y & |.x.| = -x by A19,Def1,XREAL_1:6;
    hence thesis by A21,A22,Def1;
  end;
  assume |.x+y.| = |.x.| + |.y.| & 0 > x * y;
  hence contradiction by A1,A3,A18,A8,A13;
end;

theorem
  |.x+y.|/(1 + |.x+y.|) <= |.x.|/(1 + |.x.|) + |.y.|/(1 + |.y.|)
proof
A1: s <= t & 0 < 1 + s & 0 < 1 + t implies s/(1 + s) <= t/(1 + t)
  proof
    assume that
A2: s <= t and
A3: 0 < 1 + s and
A4: 0 < 1 + t;
    s * 1 + s * t <= t + s * t by A2,XREAL_1:6;
    then s * (1 + t) * (1 + s)" <= t * (1 + s) * (1 + s)" by A3,XREAL_1:64;
    then s * (1 + t) * (1 + s)" <= t * ((1 + s) * (1 + s)");
    then s * (1 + t) * (1 + s)" <= t * 1 by A3,XCMPLX_0:def 7;
    then (s * (1 + s)") * (1 + t) * (1 + t)" <= t * (1 + t)" by A4,XREAL_1:64;
    then (s * (1 + s)") * ((1 + t) * (1 + t)") <= t * (1 + t)";
    then (s * (1 + s)") * 1 <= t * (1 + t)" by A4,XCMPLX_0:def 7;
    then s/(1 + s) <= t * (1 + t)" by XCMPLX_0:def 9;
    hence thesis by XCMPLX_0:def 9;
  end;
  set a = |.x.|, b = |.y.|, c = |.x+y.|;
A5: 0 <= a by COMPLEX1:46;
A6: 0 <= b by COMPLEX1:46;
A7: 0 + 0 < 1 + a by COMPLEX1:46,XREAL_1:8;
A8: 0 < 1 + a & 0 < 1 + a + b implies a/(1 + a + b) <= a/(1 + a)
  proof
    assume that
A9: 0 < 1 + a and
A10: 0 < 1 + a + b;
    0 + a <= a * b + a by A5,A6,XREAL_1:6;
    then a * 1 + a * a <= a * (1 + b) + a * a by XREAL_1:6;
    then a * (1 + a) * (1 + a)" <= a * (1 + a + b) * (1 + a)" by A9,XREAL_1:64;
    then a * ((1 + a) * (1 + a)") <= a * (1 + a + b) * (1 + a)";
    then a * 1 <= a * (1 + a + b) * (1 + a)" by A7,XCMPLX_0:def 7;
    then a * (1 + a + b)" <= (a * (1 + a)") * (1 + a + b) * (1 + a + b)" by A10
,XREAL_1:64;
    then a * (1 + a + b)" <= (a * (1 + a)") * ((1 + a + b) * (1 + a + b)");
    then a * (1 + a + b)" <= (a * (1 + a)") * 1 by A5,A6,XCMPLX_0:def 7;
    then a/(1 + a + b) <= a * (1 + a)" by XCMPLX_0:def 9;
    hence thesis by XCMPLX_0:def 9;
  end;
A11: 0 + 0 < 1 + b by COMPLEX1:46,XREAL_1:8;
A12: 0 < 1 + b & 0 < 1 + a + b implies b/(1 + a + b) <= b/(1 + b)
  proof
    assume that
A13: 0 < 1 + b and
A14: 0 < 1 + a + b;
    0 + b <= a * b + b by A5,A6,XREAL_1:6;
    then b * 1 + b * b <= (1 + a) * b + b * b by XREAL_1:6;
    then (b * (1 + b)) * (1 + b)" <= (b * (1 + a + b)) * (1 + b)" by A13,
XREAL_1:64;
    then b * ((1 + b) * (1 + b)") <= (b * (1 + a + b)) * (1 + b)";
    then b * 1 <= (b * (1 + a + b)) * (1 + b)" by A11,XCMPLX_0:def 7;
    then
    b * (1 + a + b)" <= ((b * (1 + b)") * (1 + a + b )) * (1 + a + b)" by A14,
XREAL_1:64;
    then b * (1 + a + b)" <= (b * (1 + b)") * ((1 + a + b) *(1 + a + b)");
    then b * (1 + a + b)" <= (b * (1 + b)") * 1 by A5,A6,XCMPLX_0:def 7;
    then b/(1 + a + b) <= b * (1 + b)" by XCMPLX_0:def 9;
    hence thesis by XCMPLX_0:def 9;
  end;
  0 + 0 < 1 + c by COMPLEX1:46,XREAL_1:8;
  then
A15: c/(1 + c) <= (a + b)/(1 + (a + b)) by A5,A6,A1,COMPLEX1:56;
  (a + b)/(1 + a + b) = a/(1 + a + b) + b/(1 + a + b) by XCMPLX_1:62;
  then (a + b)/(1 + a + b) <= a/(1 + a) + b/(1 + b) by A6,A7,A8,A12,XREAL_1:7;
  hence thesis by A15,XXREAL_0:2;
end;

:: Signum function

definition
  let x;
  func sgn x -> Real equals
  :Def2:
  1 if 0 < x, -1 if x < 0 otherwise 0;
  coherence;
  consistency;
  projectivity;
end;

registration
  let x;
  cluster sgn x -> integer;
  coherence
  proof
    x = 0 or x > 0 or x < 0;
    hence thesis by Def2;
  end;
end;

theorem
  sgn x = 1 implies 0 < x
proof
  assume that
A1: sgn x = 1 and
A2: 0 >= x;
  x < 0 or x = 0 by A2;
  hence contradiction by A1,Def2;
end;

theorem
  sgn x = -1 implies x < 0
proof
  assume that
A1: sgn x = -1 and
A2: x >= 0;
  0 < x or x = 0 by A2;
  hence contradiction by A1,Def2;
end;

theorem Th16:
  sgn x = 0 implies x = 0
proof
  assume that
A1: sgn x = 0 and
A2: x <> 0;
  0 < x or x < 0 by A2;
  hence contradiction by A1,Def2;
end;

theorem
  x = |.x.| * sgn x
proof
A1: 0 < x implies x = |.x.| * sgn x
  proof
    assume
A2: 0 < x;
    then |.x.| = x by Def1;
    then |.x.| * sgn x = x * 1 by A2,Def2;
    hence thesis;
  end;
A3: x < 0 implies x = |.x.| * sgn x
  proof
    assume
A4: x < 0;
    then |.x.| = -x by Def1;
    then |.x.| * sgn x = (-x) * (-1) by A4,Def2
      .= x;
    hence thesis;
  end;
  x = 0 implies x = |.x.| * sgn x;
  hence thesis by A1,A3;
end;

theorem Th18:
  sgn (x * y) = sgn x * sgn y
proof
A1: 0 < x & 0 < y implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A2: 0 < x and
A3: 0 < y;
A4: sgn y = 1 by A3,Def2;
    0 * y < x * y & sgn x = 1 by A2,A3,Def2,XREAL_1:68;
    hence thesis by A4,Def2;
  end;
A5: 0 < x & y < 0 implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A6: 0 < x and
A7: y < 0;
    sgn y = -1 by A7,Def2;
    then
A8: sgn x * sgn y = 1 * (-1) by A6,Def2
      .= -1;
    x * y < 0 * y by A6,A7,XREAL_1:69;
    hence thesis by A8,Def2;
  end;
A9: x < 0 & y < 0 implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A10: x < 0 and
A11: y < 0;
    sgn y = -1 by A11,Def2;
    then
A12: sgn x * sgn y = (-1) * (-1) by A10,Def2
      .= 1;
    x * 0 < x * y by A10,A11,XREAL_1:69;
    hence thesis by A12,Def2;
  end;
A13: x < 0 & 0 < y implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A14: x < 0 and
A15: 0 < y;
    sgn y = 1 by A15,Def2;
    then
A16: sgn x * sgn y = -1 by A14,Def2;
    x * y < 0 * y by A14,A15,XREAL_1:68;
    hence thesis by A16,Def2;
  end;
  x = 0 or y = 0 implies sgn (x * y) = sgn x * sgn y
  proof
    assume
A17: x = 0 or y = 0;
    then sgn x = 0 or sgn y = 0 by Def2;
    hence thesis by A17;
  end;
  hence thesis by A1,A5,A13,A9;
end;

::$CT

theorem
  sgn (x + y) <= sgn x + sgn y + 1
proof
A1: y = 0 implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    assume
A2: y = 0;
    then sgn x + sgn y + 1 = sgn x + 0 + 1 by Def2
      .= sgn x + 1;
    hence thesis by A2,XREAL_1:29;
  end;
A3: 0 < x & 0 < y implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    sgn x < sgn x + 1 by XREAL_1:29;
    then
A4: sgn x + 0 < sgn x + 1 + 1 by XREAL_1:8;
    assume
A5: 0 < x & 0 < y;
    then sgn x = 1 & sgn y = 1 by Def2;
    hence thesis by A5,A4,Def2;
  end;
A6: x < 0 & 0 < y implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    assume that
A7: x < 0 and
A8: 0 < y;
    sgn x = -1 by A7,Def2;
    then
A9: sgn x + sgn y + 1 = 1 by A8,Def2;
    x + y < 0 or x + y = 0 or 0 < x + y;
    hence thesis by A9,Def2;
  end;
A10: 0 < x & y < 0 implies sgn (x + y) <= sgn x + sgn y +1
  proof
    assume that
A11: 0 < x and
A12: y < 0;
    sgn x = 1 by A11,Def2;
    then
A13: sgn x + sgn y + 1 = 1 + -1 + 1 by A12,Def2
      .= 1;
    x + y < 0 or x + y = 0 or 0 < x + y;
    hence thesis by A13,Def2;
  end;
A14: x < 0 & y < 0 implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    assume that
A15: x < 0 and
A16: y < 0;
    sgn y = -1 by A16,Def2;
    then sgn x + sgn y + 1 = -1 by A15,Def2;
    hence thesis by A15,A16,Def2;
  end;
  x = 0 implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    assume
A17: x = 0;
    then sgn x + sgn y + 1 = 0 + sgn y + 1 by Def2
      .= sgn y + 1;
    hence thesis by A17,XREAL_1:29;
  end;
  hence thesis by A3,A10,A6,A14,A1;
end;

theorem Th20:
  x <> 0 implies sgn x * sgn (1/x) = 1
proof
  assume x <> 0;
  then sgn ( x * (1/x) ) = sgn 1 by XCMPLX_1:106;
  then sgn ( x * (1/x) ) = 1 by Def2;
  hence thesis by Th18;
end;

theorem Th21:
  1/(sgn x) = sgn (1/x)
proof
  per cases;
  suppose
A1: x = 0;
    hence 1/(sgn x) = 1/0 by Def2
      .= sgn (1/x) by A1,Def2;
  end;
  suppose
A2: x <> 0;
    then (sgn x * sgn (1/x)) * (1/(sgn x)) = 1 * (1/(sgn x)) by Th20;
    then sgn (1/x) * (sgn x * (1/(sgn x))) = 1/(sgn x);
    then sgn (1/x) * 1 = 1 /(sgn x) by A2,Th16,XCMPLX_1:106;
    hence thesis;
  end;
end;

theorem
  sgn x + sgn y - 1 <= sgn ( x + y )
proof
A1: x = 0 or y = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
A2: y = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
    proof
A3:   sgn x - 1 < sgn x + -1 + 1 by XREAL_1:29;
      assume
A4:   y = 0;
      then sgn x + sgn y - 1 = sgn x + 0 - 1 by Def2
        .= sgn x - 1;
      hence thesis by A4,A3;
    end;
A5: x = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
    proof
A6:   sgn y - 1 < sgn y + -1 + 1 by XREAL_1:29;
      assume
A7:   x = 0;
      then sgn x + sgn y - 1 = 0 + sgn y - 1 by Def2
        .= sgn y - 1;
      hence thesis by A7,A6;
    end;
    assume x = 0 or y = 0;
    hence thesis by A5,A2;
  end;
A8: x < 0 & y < 0 implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A9: x < 0 and
A10: y < 0;
    sgn x = -1 by A9,Def2;
    then
A11: sgn x = sgn (x + y) by A9,A10,Def2;
A12: sgn (x + y) + -1 - 1 < sgn (x + y) + -1 - 1 + 1 & sgn (x + y) + -1 <
    sgn (x + y) + -1 + 1 by XREAL_1:29;
    sgn y = -1 by A10,Def2;
    hence thesis by A11,A12,XXREAL_0:2;
  end;
A13: 0 < x & y < 0 implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A14: 0 < x and
A15: y < 0;
    sgn x = 1 by A14,Def2;
    then
A16: sgn x + sgn y = 1 + -1 by A15,Def2
      .= 0;
    x + y < 0 or x + y = 0 or 0 < x + y;
    hence thesis by A16,Def2;
  end;
A17: x < 0 & 0 < y implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A18: x < 0 and
A19: 0 < y;
    sgn x = -1 by A18,Def2;
    then
A20: sgn x + sgn y = -1 + 1 by A19,Def2
      .= 0;
    x + y < 0 or x + y = 0 or 0 < x + y;
    hence thesis by A20,Def2;
  end;
  0 < x & 0 < y implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A21: 0 < x and
A22: 0 < y;
    sgn y = 1 by A22,Def2;
    then sgn x + sgn y - 1 = 1 by A21,Def2;
    hence thesis by A21,A22,Def2;
  end;
  hence thesis by A8,A17,A13,A1;
end;

theorem
  sgn x = sgn (1/x)
proof
A1: 0 < x implies sgn x = sgn (1/x)
    proof
      assume
A2:   0 < x;
      sgn (1/x) = 1/(sgn x) by Th21;
      then sgn (1/x) = 1/1 by A2,Def2
        .= 1;
      hence thesis by A2,Def2;
    end;
    x < 0 implies sgn x = sgn (1/x)
    proof
      assume
A3:   x < 0;
      then sgn x = -1 by Def2;
      then sgn (1/x) = 1/(-1) by Th21;
      hence thesis by A3,Def2;
    end;
    hence thesis by A1;
end;

theorem
  sgn (x/y) = (sgn x)/(sgn y)
proof
  per cases;
  suppose
A1: y = 0;
    hence sgn (x/y) = sgn (x*0") by XCMPLX_0:def 9
      .= (sgn x)*0" by Def2
      .= (sgn x)/0 by XCMPLX_0:def 9
      .= (sgn x)/(sgn y) by A1,Def2;
  end;
  suppose
A2: y <> 0;
    x/y = (x/y) * 1 .= (x/y) * (y * (1/y)) by A2,XCMPLX_1:106
      .= ((x/y) * y) * (1/y)
      .= x * (1/y) by A2,XCMPLX_1:87;
    then sgn (x/y) = sgn x * sgn (1/y) by Th18
      .= ((sgn x)/1) * (1/(sgn y)) by Th21
      .= (sgn x * 1)/(1 * sgn y) by XCMPLX_1:76
      .= (sgn x)/(1 * sgn y);
    hence thesis;
  end;
end;

:: from SCMPDS_9. 2008.05.06, A.T.

theorem
  0 <= r + |.r.|
proof
A1: 0 <= |.r.| by COMPLEX1:46;
  |.r.| + |.r.| = r + |.r.| or |.r.| + r = -r + r by Def1;
  hence thesis by A1;
end;

theorem
  0 <= -r + |.r.|
proof
  -r >= -|.r.| by XREAL_1:24,COMPLEX1:76;
  then -r+|.r.| >= -|.r.|+|.r.| by XREAL_1:7;
  hence thesis;
end;

theorem
  |.r.| = |.s.| implies r = s or r = -s
proof
  assume
A1: |.r.| = |.s.|;
  assume
A2: r <> s;
  per cases by Def1;
  suppose
    |.r.| = r & |.s.| = s;
    hence thesis by A1,A2;
  end;
  suppose
    |.r.| = r & |.s.| = -s;
    hence thesis by A1;
  end;
  suppose
    |.r.| = -r & |.s.| = s;
    hence thesis by A1;
  end;
  suppose
    |.r.| = -r & |.s.| = -s;
    hence thesis by A1,A2;
  end;
end;

theorem
  for m being Nat holds m = |.m.|;

:: from JORDAN2C, 2011.07.03, A.T,

theorem
  r <= 0 implies |.r.| = -r
proof
  assume r<=0;
  then r < 0 or r = 0;
  hence thesis by Def1;
end;