:: Some Properties of Functions Modul and Signum
::  by Jan Popio{\l}ek
::
:: Received June 21, 1989
:: Copyright (c) 1990 Association of Mizar Users

environ

 vocabularies ARYTM, ARYTM_1, ARYTM_3, RELAT_1, ABSVALUE, COMPLEX1, SQUARE_1;
 notations ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, SQUARE_1,
      XXREAL_0;
 constructors REAL_1, SQUARE_1, COMPLEX1;
 registrations XXREAL_0, XREAL_0, REAL_1, ORDINAL1, XBOOLE_0;
 requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE;
 theorems XREAL_0, XCMPLX_0, XCMPLX_1, COMPLEX1, SQUARE_1, XREAL_1, XXREAL_0;

begin :: Absolute value

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

definition
  let x be real number;
  redefine func |.x.| equals
  :Def1:
  x if 0 <= x otherwise -x;
  correctness by COMPLEX1:129,156;
end;

theorem Th1:
  abs x = x or abs x = -x by Def1;

canceled 5;

theorem
  x = 0 iff abs x = 0 by Def1,COMPLEX1:133;

canceled;

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

canceled;

theorem
  -abs x <= x & x <= abs x
proof
  per cases;
  suppose
A1: x < 0;
    then abs 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 abs x <= y
proof
  hereby
    assume that
A1: -y <= x and
A2: x <= y;
    -x <= --y by A1,XREAL_1:26;
    hence abs x <= y by A2,Def1;
  end;
  assume
A3: abs x <= y;
  then
A4: 0 <= y by COMPLEX1:132;
  per cases;
  suppose
A5: 0 < x;
    -y <= -0 by A4;
    hence thesis by A3,A5,Def1;
  end;
  suppose
A6: x < 0;
    then -x <= y by A3,Def1;
    then -y <= --x by XREAL_1:26;
    hence thesis by A6;
  end;
  suppose x = -0;
    hence thesis by A4;
  end;
end;

canceled;

theorem Th14:
  x <> 0 implies abs(x) * abs(1/x) = 1
proof
  assume
A1: x <> 0;
A2: abs x * abs(1/x) = abs(x * (1/x)) by COMPLEX1:151;
  abs(x * (1/x)) = abs 1 by A1,XCMPLX_1:107;
  hence thesis by A2,Def1;
end;

theorem
  abs(1/x) = 1/abs(x)
proof
  per cases;
  suppose
A1: x = 0;
    hence abs(1/x) = 1/0 by Def1
      .= 1/abs(x) by A1,Def1;
  end;
  suppose
A2: x <> 0;
    then (abs(x) * abs(1/x)) * (1/abs(x)) = 1 * (1/abs(x)) by Th14;
    then
A3: abs(1/x) * (abs(x) * (1/abs(x))) = 1/abs(x);
    abs x <> 0 by A2,COMPLEX1:133;
    then abs(1/x) * 1 = 1/abs(x) by A3,XCMPLX_1:107;
    hence thesis;
  end;
end;

canceled 4;

theorem :: SQUARE_1:98
  0 <= x*y implies sqrt (x*y) = sqrt abs(x)*sqrt abs(y)
proof
  assume 0 <= x*y;
  then abs(x*y) = x*y by Def1;
  then abs(x)*abs(y) = x*y & 0 <= abs(x) & 0 <= abs(y) by COMPLEX1:132,151;
  hence thesis by SQUARE_1:97;
end;

theorem
  abs x <= z & abs y <= t implies abs(x+y) <= z + t
proof
  assume that
A1: abs(x) <= z and
A2: abs(y) <= t;
A3: abs(x+y) <= abs(x) + abs(y) by COMPLEX1:142;
  abs(x) + abs(y) <= z + t by A1,A2,XREAL_1:9;
  hence thesis by A3,XXREAL_0:2;
end;

canceled;

theorem :: SQUARE_1:100
  0 < x/y implies sqrt (x/y) = sqrt abs(x) / sqrt abs(y)
proof
  assume 0 < x/y;
  then x/y = abs(x/y) & 0 <= abs(y) by Def1,COMPLEX1:132;
  then x/y = abs(x)/abs(y) & 0 <= abs(x) & 0 <= abs(y) by COMPLEX1:132,153;
  hence thesis by SQUARE_1:99;
end;

theorem
  0 <= x * y implies abs (x+y) = abs(x) + abs(y)
proof
  assume
A1: 0 <= x * y;
  per cases by A1;
  suppose
A2: x * y = 0;
    per cases by A2,XCMPLX_1:6;
    suppose
A3:   x = 0;
      then abs(x) + abs(y) = 0 + abs(y) by Def1
        .= abs(y);
      hence thesis by A3;
    end;
    suppose
A4:   y = 0;
      then abs(x) + abs(y) = abs(x) + 0 by Def1
        .= abs(x);
      hence thesis by A4;
    end;
  end;
  suppose
A5: 0 < x * y;
A6: x < 0 & y < 0 or 0 < x & 0 < y
    proof
A7:   x <> 0 & y <> 0 by A5;
      thus thesis by A5,A7;
    end;
    per cases by A6;
    suppose that
A9:   0 < x and
A10:  0 < y;
A11:  0 + 0 < x + y by A9,A10;
      abs x = x & abs y = y by A9,A10,Def1;
      hence thesis by A11,Def1;
    end;
    suppose that
A12:  x < 0 and
A13:  y < 0;
A14:  x + y < 0 + 0 by A12,A13;
      abs(x) = -x by A12,Def1;
      then abs(x) + abs(y) = (-1) * x + -(1 * y) by A13,Def1
        .= - ( x + y );
      hence thesis by A14,Def1;
    end;
  end;
end;

theorem
  abs(x+y) = abs(x) + abs(y) implies 0 <= x * y
proof
  assume that
A1: abs(x+y) = abs(x) + abs(y) and
A2: 0 > x * y;
A3: x * y < 0 implies x < 0 & 0 < y or 0 < x & y < 0
  proof
    assume
A4: x * y < 0;
    then
A5: x <> 0 & y <> 0;
    thus thesis by A4,A5;
  end;
A7: x < 0 & 0 < y & x + y < 0 implies abs(x+y) <> abs(x) + abs(y)
  proof
    assume that
A8: x < 0 and
A9: 0 < y and
A10: x + y < 0;
    -(1 * x) + -y < -x + y by A9,XREAL_1:8;
    then
A11: -( 1 * ( x + y ) ) < -x + y;
A12: abs x = -x by A8,Def1;
    abs y = y by A9,Def1;
    hence thesis by A10,A11,A12,Def1;
  end;
A13: x < 0 & 0 < y & 0 <= x + y implies abs(x+y) <> abs(x) + abs(y)
  proof
    assume that
A14: x < 0 and
A15: 0 < y and
A16: 0 <= x + y;
A17: x + y < -x + y by A14,XREAL_1:8;
A18: abs x = -x by A14,Def1;
    abs y = y by A15,Def1;
    hence thesis by A16,A17,A18,Def1;
  end;
A19: 0 < x & y < 0 & x + y < 0 implies abs(x+y) <> abs(x) + abs(y)
  proof
    assume that
A20: 0 < x and
A21: y < 0 and
A22: x + y < 0;
    -(1 * x) + -y < x + -y by A20,XREAL_1:8;
    then
A23: - (1 * ( x + y )) < x + -y;
A24: abs x = x by A20,Def1;
    abs y = -y by A21,Def1;
    hence thesis by A22,A23,A24,Def1;
  end;
  0 < x & y < 0 & 0 <= x + y implies abs(x+y) <> abs(x) + abs(y)
  proof
    assume that
A25: 0 < x and
A26: y < 0 and
A27: 0 <= x + y;
    0 + y < -y + 0 by A26;
    then
A28: x + y < x + -y by XREAL_1:8;
A29: abs x = x by A25,Def1;
    abs y = -y by A26,Def1;
    hence thesis by A27,A28,A29,Def1;
  end;
  hence contradiction by A1,A2,A3,A7,A13,A19;
end;

theorem
  abs(x + y)/(1 + abs(x+y)) <= abs(x)/(1 + abs(x)) + abs(y)/(1 + abs(y))
proof
  set a = abs x, b = abs y, c = abs (x+y);
A1: 0 <= a by COMPLEX1:132;
A2: 0 <= b by COMPLEX1:132;
  then
A3: 0 + 0 <= a + b by A1;
  then
A4: 0 + 0 < 1 + (a + b);
A5: 0 < 1 + (a + b) by A3;
A6: 0 + 0 < 1 + c by COMPLEX1:132,XREAL_1:10;
A7: 0 + 0 < 1 + a by COMPLEX1:132,XREAL_1:10;
A8: 0 + 0 < 1 + b by COMPLEX1:132,XREAL_1:10;
  s <= t & 0 < 1 + s & 0 < 1 + t implies s/(1 + s) <= t/(1 + t)
  proof
    assume that
A9: s <= t and
A10: 0 < 1 + s and
A11: 0 < 1 + t;
A12: s * 1 + s * t <= t + s * t by A9,XREAL_1:8;
A13: 0 < (1 + s)" by A10,XREAL_1:124;
A14: 0 < (1 + t)" by A11,XREAL_1:124;
    s * (1 + t) * (1 + s)" <= t * (1 + s) * (1 + s)" by A12,A13,XREAL_1:66;
    then s * (1 + t) * (1 + s)" <= t * ((1 + s) * (1 + s)");
    then s * (1 + t) * (1 + s)" <= t * 1 by A10,XCMPLX_0:def 7;
    then (s * (1 + s)") * (1 + t) * (1 + t)" <= t * (1 + t)"
    by A14,XREAL_1:66;
    then (s * (1 + s)") * ((1 + t) * (1 + t)") <= t * (1 + t)";
    then (s * (1 + s)") * 1 <= t * (1 + t)" by A11,XCMPLX_0:def 7;
    then s/(1 + s) <= t * (1 + t)" by XCMPLX_0:def 9;
    hence thesis by XCMPLX_0:def 9;
  end;
  then
A15: c/(1 + c) <= (a + b)/(1 + (a + b)) by A5,A6,COMPLEX1:142;
  (a + b)/(1 + a + b) <= a/(1 + a) + b/(1 + b)
  proof
A16: (a + b)/(1 + a + b) = a/(1 + a + b) + b/(1 + a + b) by XCMPLX_1:63;
A17: 0 < 1 + a & 0 < 1 + a + b implies a/(1 + a + b) <= a/(1 + a)
    proof
      assume that
A18:  0 < 1 + a and
A19:  0 < 1 + a + b;
      0 * b <= a * b by A1,A2;
      then 0 + a <= a * b + a by XREAL_1:8;
      then
A20:  a * 1 + a * a <= a * (1 + b) + a * a by XREAL_1:8;
A21:  0 <= (1 + a)" by A18;
A22:  0 <= (1 + a + b)" by A19;
      a * (1 + a) * (1 + a)" <= a * (1 + a + b) * (1 + a)"
      by A20,A21,XREAL_1:66;
      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 A22,XREAL_1:66;
      then a * (1 + a + b)" <= (a * (1 + a)") * ((1 + a + b) * (1 + a + b)");
      then a * (1 + a + b)" <= (a * (1 + a)") * 1 by A4,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;
    0 < 1 + b & 0 < 1 + a + b implies b/(1 + a + b) <= b/(1 + b)
    proof
      assume that
A23:  0 < 1 + b and
A24:  0 < 1 + a + b;
      0 * b <= a * b by A1,A2;
      then 0 + b <= a * b + b by XREAL_1:8;
      then
A25:  b * 1 + b * b <= (1 + a) * b + b * b by XREAL_1:8;
A26:  0 <= (1 + b)" by A23;
A27:  0 <= (1 + a + b)" by A24;
      (b * (1 + b)) * (1 + b)" <= (b * (1 + a + b)) * (1 + b)"
      by A25,A26,XREAL_1:66;
      then b * ((1 + b) * (1 + b)") <= (b * (1 + a + b)) * (1 + b)";
      then b * 1 <= (b * (1 + a + b)) * (1 + b)" by A8,XCMPLX_0:def 7;
      then b * (1 + a + b)" <= ((b * (1 + b)") * (1 + a + b )) *
      (1 + a + b)" by A27,XREAL_1:66;
      then b * (1 + a + b)" <= (b * (1 + b)") * ((1 + a + b) *(1 + a + b)");
      then b * (1 + a + b)" <= (b * (1 + b)") * 1 by A4,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;
    hence thesis by A2,A7,A16,A17,XREAL_1:9;
  end;
  hence thesis by A15,XXREAL_0:2;
end;

:: Signum function

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

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

definition
  let x be Real;
  redefine func sgn x -> Real;
  coherence by XREAL_0:def 1;
end;

canceled 4;

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 Th33:
  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 = abs(x) * sgn x
proof
A1: 0 < x implies x = abs(x) * sgn x
  proof
    assume
A2: 0 < x;
    then abs(x) = x by Def1;
    then abs(x) * sgn x = x * 1 by A2,Def2;
    hence thesis;
  end;
A3: x < 0 implies x = abs(x) * sgn x
  proof
    assume
A4: x < 0;
    then abs(x) = -x by Def1;
    then abs(x) * sgn x = (-x) * (-1) by A4,Def2
      .= x;
    hence thesis;
  end;
  x = 0 implies x = abs(x) * sgn x
  proof
    assume
A5: x = 0;
    then sgn x = 0 by Def2;
    hence thesis by A5;
  end;
  hence thesis by A1,A3;
end;

theorem Th35:
  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: 0 * y < x * y by A2,A3,XREAL_1:70;
A5: sgn x = 1 by A2,Def2;
    sgn y = 1 by A3,Def2;
    hence thesis by A4,A5,Def2;
  end;
A6: 0 < x & y < 0 implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A7: 0 < x and
A8: y < 0;
A9: x * y < 0 * y by A7,A8,XREAL_1:71;
    sgn y = -1 by A8,Def2;
    then sgn x * sgn y = 1 * (-1) by A7,Def2
      .= -1;
    hence thesis by A9,Def2;
  end;
A10: x < 0 & 0 < y implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A11: x < 0 and
A12: 0 < y;
A13: x * y < 0 * y by A11,A12,XREAL_1:70;
    sgn y = 1 by A12,Def2;
    then sgn x * sgn y = -1 by A11,Def2;
    hence thesis by A13,Def2;
  end;
A14: x < 0 & y < 0 implies sgn (x * y) = sgn x * sgn y
  proof
    assume that
A15: x < 0 and
A16: y < 0;
A17: x * 0 < x * y by A15,A16,XREAL_1:71;
    sgn y = -1 by A16,Def2;
    then sgn x * sgn y = (-1) * (-1) by A15,Def2
      .= 1;
    hence thesis by A17,Def2;
  end;
  x = 0 or y = 0 implies sgn (x * y) = sgn x * sgn y
  proof
    assume
A18: x = 0 or y = 0;
    then sgn x = 0 or sgn y = 0 by Def2;
    hence thesis by A18,Def2;
  end;
  hence thesis by A1,A6,A10,A14;
end;

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

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

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

theorem Th39:
  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 Th38;
    then sgn (1/x) * (sgn x * (1/(sgn x))) = 1/(sgn x);
    then sgn (1/x) * 1 = 1 /(sgn x) by A2,Th33,XCMPLX_1:107;
    hence thesis;
  end;
end;

theorem
  sgn x + sgn y - 1 <= sgn ( x + y )
proof
A1: x < 0 & y < 0 implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A2: x < 0 and
A3: y < 0;
A4: x + y < 0 + 0 by A2,A3;
A5: sgn x = -1 by A2,Def2;
A6: sgn y = -1 by A3,Def2;
A7: sgn x = sgn (x + y) by A4,A5,Def2;
A8: sgn (x + y) + -1 - 1 < sgn (x + y) + -1 - 1 + 1 by XREAL_1:31;
    sgn (x + y) + -1 < sgn (x + y) + -1 + 1 by XREAL_1:31;
    hence thesis by A6,A7,A8,XXREAL_0:2;
  end;
A9: x < 0 & 0 < y implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A10: x < 0 and
A11: 0 < y;
    sgn x = -1 by A10,Def2;
    then
A12: sgn x + sgn y = -1 + 1 by A11,Def2
      .= 0;
    x + y < 0 or x + y = 0 or 0 < x + y;
    hence thesis by A12,Def2;
  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: 0 < x & 0 < y implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume that
A18: 0 < x and
A19: 0 < y;
A20: 0 + 0 < x + y by A18,A19;
    sgn y = 1 by A19,Def2;
    then sgn x + sgn y - 1 = 1 by A18,Def2;
    hence thesis by A20,Def2;
  end;
  x = 0 or y = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
  proof
    assume
A21: x = 0 or y = 0;
A22: x = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
    proof
      assume
A23:  x = 0;
      then
A24:  sgn x + sgn y - 1 = 0 + sgn y - 1 by Def2
        .= sgn y - 1;
      sgn y - 1 < sgn y + -1 + 1 by XREAL_1:31;
      hence thesis by A23,A24;
    end;
    y = 0 implies sgn x + sgn y - 1 <= sgn (x + y)
    proof
      assume
A25:  y = 0;
      then
A26:  sgn x + sgn y - 1 = sgn x + 0 - 1 by Def2
        .= sgn x - 1;
      sgn x - 1 < sgn x + -1 + 1 by XREAL_1:31;
      hence thesis by A25,A26;
    end;
    hence thesis by A21,A22;
  end;
  hence thesis by A1,A9,A13,A17;
end;

theorem
  sgn x = sgn (1/x)
proof
  per cases;
  suppose
A1: x = 0;
    thus thesis by A1;
  end;
  suppose
 x <> 0;
A3: x < 0 implies sgn x = sgn (1/x)
    proof
      assume
A4:   x < 0;
      then sgn x = -1 by Def2;
      then sgn (1/x) = 1/(-1) by Th39;
      hence thesis by A4,Def2;
    end;
    0 < x implies sgn x = sgn (1/x)
    proof
      assume
A5:   0 < x;
      sgn (1/x) = 1/(sgn x) by Th39;
      then sgn (1/x) = 1/1 by A5,Def2
        .= 1;
      hence thesis by A5,Def2;
    end;
    hence thesis by A3;
  end;
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:107
      .= ((x/y) * y) * (1/y)
      .= x * (1/y) by A2,XCMPLX_1:88;
    then sgn (x/y) = sgn x * sgn (1/y) by Th35
      .= ((sgn x)/1) * (1/(sgn y)) by Th39
      .= (sgn x * 1)/(1 * sgn y) by XCMPLX_1:77
      .= (sgn x)/(1 * sgn y);
    hence thesis;
  end;
end;

:: from SCMPDS_9. 2008.05.06, A.T.

reserve r, s for real number;

theorem
  0 <= r + abs(r)
proof
  0 <= abs(r) by COMPLEX1:132;
  then
A1: 0 + abs(r) <= abs(r) + abs(r) by XREAL_1:8;
  abs(r) + abs(r) = r + abs(r) or abs(r) + r = -r + r by Th1;
  hence thesis by A1,COMPLEX1:132;
end;

theorem
  0 <= -r + abs(r)
proof
  r <= abs(r) by COMPLEX1:162;
  then -r >= -abs(r) by XREAL_1:26;
  then -r+abs(r) >= -abs(r)+abs(r) by XREAL_1:9;
  hence thesis;
end;

theorem
  abs(r) = abs(s) implies r = s or r = -s
proof
  assume
A1: abs(r) = abs(s);
  assume
A2: r <> s;
  per cases by Th1;
  suppose abs(r) = r & abs(s) = s;
    hence r = -s by A1,A2;
  end;
  suppose abs(r) = r & abs(s) = -s;
    hence r = -s by A1;
  end;
  suppose abs(r) = -r & abs(s) = s;
    hence r = -s by A1;
  end;
  suppose abs(r) = -r & abs(s) = -s;
    hence r = -s by A1,A2;
  end;
end;