:: 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, XCMPLX_0, XREAL_0, REAL_1, COMPLEX1, SQUARE_1, XXREAL_0;
 constructors REAL_1, COMPLEX1, SQUARE_1, XXREAL_0;
 registrations XREAL_0, REAL_1, ARYTM_3;
 requirements REAL, NUMERALS, SUBSET, ARITHM;
 theorems XREAL_0, REAL_1, XCMPLX_0, XCMPLX_1, COMPLEX1, SQUARE_1, XREAL_1;

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
  abs x = x or abs x = -x
  proof
    per cases;
    suppose x >= 0;
      hence thesis by Def1;
    end;
    suppose x < 0;
      hence thesis by Def1;
    end;
  end;

 Lm1:
  0 <= abs x by COMPLEX1:132;

 Lm2:
  x <> 0 implies 0 < abs x by COMPLEX1:133;

canceled 5;

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

canceled;

theorem
  abs x = -x & x <> 0 implies x < 0
proof
  assume that
A1: abs x = -x and
A2: x <> 0 and
A3: x >= 0;
  0 < x by A2,A3,REAL_1:def 5;
  then -x < -0 by XREAL_1:26;
  hence contradiction by A1,A3,Def1;
end;

 Lm3:
  abs(x*y) = abs(x) * abs(y) by COMPLEX1:151;

canceled;

theorem
  -abs x <= x & x <= abs x
proof
  per cases;
  suppose
A1: x < 0;
    then A2: abs x = -x by Def1;
    0 < -x by A1,XREAL_1:60;
    hence thesis by A1,A2,XREAL_1:2;
  end;
  suppose
A3: 0 <= x;
    then A4: abs x = x by Def1;
    -x <= -0 by A3,XREAL_1:26;
    hence thesis by A3,A4,XREAL_1:2;
  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;
    then x < 0 implies abs x <= y by Def1;
    hence abs x <= y by A2,Def1;
  end;
    assume
A3: abs x <= y;
    0 <= abs x by Lm1;
    then A4: 0 <= y by A3,XREAL_1:2;
    per cases by XREAL_1:1;
    suppose
A5:   0 < x;
      -y <= -0 by A4,XREAL_1:26;
      hence thesis by A3,A5,Def1,XREAL_1:2;
    end;
    suppose
A6:   x < 0;
      then -x <= y by A3,Def1;
      then -y <= --x by XREAL_1:26;
      hence thesis by A4,A6,XREAL_1:2;
    end;
    suppose x = -0;
      hence thesis by A4,XREAL_1:26;
    end;
end;

 Lm4:
  abs(x+y) <= abs(x) + abs(y) by COMPLEX1:142;

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 Lm3;
    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) = abs(1*0") by XCMPLX_0:def 9
        .= abs (1*0) by XCMPLX_0:def 7
        .= 0 by Def1
        .= 1*0" by XCMPLX_0:def 7
        .= 1/0 by XCMPLX_0:def 9
        .= 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,Lm2;
      then abs(1/x) * 1 = 1/abs(x) by A3,XCMPLX_1:107;
      hence thesis;
    end;
  end;

 Lm5:
  abs(x/y) = abs(x)/abs(y) by COMPLEX1:153;

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 Lm1,Lm3;
   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 Lm4;
  abs(x) + abs(y) <= z + t by A1,A2,XREAL_1:9;
  hence thesis by A3,XREAL_1: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,Lm1;
    then x/y = abs(x)/abs(y) & 0 <= abs(x) & 0 <= abs(y)
      by Lm1,Lm5;
    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,REAL_1:def 5;
    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;
A8:    x < 0 & 0 < y implies x * y < x * 0 by XREAL_1:71;
        0 < x & y < 0 implies x * y < x * 0 by XREAL_1:70;
        hence thesis by A5,A7,A8,XREAL_1:1;
      end;
      per cases by A6;
      suppose that
   A9: 0 < x and
   A10: 0 < y;
A11:    0 + 0 < x + y by A9,A10,XREAL_1:10;
        abs x = x & abs y = y by A9,A10,Def1;
        then abs(x) + abs(y) = x + y;
        hence thesis by A11,Def1;
      end;
      suppose that
   A12: x < 0 and
   A13: y < 0;
A14:    x + y < 0 + 0 by A12,A13,XREAL_1:10;
        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;
A6:   x < 0 & y < 0 implies 0 * x < x * y by XREAL_1:71;
      0 < x & 0 < y implies x * 0 < x * y by XREAL_1:70;
      hence thesis by A4,A5,A6,XREAL_1:1;
    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;
      -y < -0 by A9,XREAL_1:26;
      then -y + 0 < 0 + y by A9,XREAL_1:10;
      then -(1 * x) + -y < -x + y by 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;
      0 < -x by A14,XREAL_1:60;
      then x + 0 < 0 + -x by A14,XREAL_1:10;
      then A17: x + y < -x + y by 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;
      -x < -0 by A20,XREAL_1:26;
      then -x + 0 < 0 + x by A20,XREAL_1:10;
      then -(1 * x) + -y < x + -y by 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 by A26,XREAL_1:60;
      then 0 + y < -y + 0 by A26,XREAL_1:10;
      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: c <= a + b by Lm4;
A2: 0 <= a by Lm1;
A3: 0 <= b by Lm1;
A4: 0 <= c by Lm1;
A5: 0 + 0 <= a + b by A2,A3,XREAL_1:9;
    then A6: 0 + 0 < 1 + (a + b) by XREAL_1:10;
A7: 0 < 1 + (a + b) by A5,XREAL_1:10;
A8: 0 + 0 < 1 + c by A4,XREAL_1:10;
A9: 0 + 0 < 1 + a by A2,XREAL_1:10;
A10:0 + 0 < 1 + b by A3,XREAL_1:10;
    s <= t & 0 < 1 + s & 0 < 1 + t implies s/(1 + s) <= t/(1 + t)
    proof
      assume that
A11:  s <= t and
A12:  0 < 1 + s and
A13:  0 < 1 + t;
A14:  s * 1 + s * t <= t + s * t by A11,XREAL_1:8;
A15:  0 < (1 + s)" by A12,XREAL_1:124;
A16:  0 < (1 + t)" by A13,XREAL_1:124;
      s * (1 + t) * (1 + s)" <= t * (1 + s) * (1 + s)" by A14,A15,XREAL_1:66;
      then s * (1 + t) * (1 + s)" <= t * ((1 + s) * (1 + s)");
      then s * (1 + t) * (1 + s)" <= t * 1 by A12,XCMPLX_0:def 7;
      then (s * (1 + s)") * (1 + t) * (1 + t)" <= t * (1 + t)"
        by A16,XREAL_1:66;
      then (s * (1 + s)") * ((1 + t) * (1 + t)") <= t * (1 + t)";
      then (s * (1 + s)") * 1 <= t * (1 + t)" by A13,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 A17: c/(1 + c) <= (a + b)/(1 + (a + b)) by A1,A7,A8;
    (a + b)/(1 + a + b) <= a/(1 + a) + b/(1 + b)
    proof
A18:  (a + b)/(1 + a + b) = a/(1 + a + b) + b/(1 + a + b) by XCMPLX_1:63;
A19:  0 < 1 + a & 0 < 1 + a + b implies a/(1 + a + b) <= a/(1 + a)
      proof
        assume that
A20:    0 < 1 + a and
A21:    0 < 1 + a + b;
        0 * b <= a * b by A2,A3,XREAL_1:66;
        then 0 + a <= a * b + a by XREAL_1:8;
        then A22: a * 1 + a * a <= a * (1 + b) + a * a by XREAL_1:8;
A23:    0 <= (1 + a)" by A20,XREAL_1:124;
A24:    0 <= (1 + a + b)" by A21,XREAL_1:124;
        a * (1 + a) * (1 + a)" <= a * (1 + a + b) * (1 + a)"
          by A22,A23,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 A9,XCMPLX_0:def 7;
        then a * (1 + a + b)" <= (a * (1 + a)") * (1 + a + b) * (1 + a
          + b)" by A24,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 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;
      0 < 1 + b & 0 < 1 + a + b implies b/(1 + a + b) <= b/(1 + b)
      proof
        assume that
A25:    0 < 1 + b and
A26:    0 < 1 + a + b;
        0 * b <= a * b by A2,A3,XREAL_1:66;
        then 0 + b <= a * b + b by XREAL_1:8;
        then A27: b * 1 + b * b <= (1 + a) * b + b * b by XREAL_1:8;
A28:    0 <= (1 + b)" by A25,XREAL_1:124;
A29:    0 <= (1 + a + b)" by A26,XREAL_1:124;
        (b * (1 + b)) * (1 + b)" <= (b * (1 + a + b)) * (1 + b)"
          by A27,A28,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 A10,XCMPLX_0:def 7;
        then b * (1 + a + b)" <= ((b * (1 + b)") * (1 + a + b )) *
          (1 + a + b)" by A29,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 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;
      hence thesis by A3,A9,A18,A19,XREAL_1:9,XREAL_1:10;
    end;
    hence thesis by A17,XREAL_1: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 by REAL_1:def 5;
    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,REAL_1:def 5;
    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,REAL_1:def 5;
    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,XREAL_1:1;
  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,XREAL_1:1;
  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,XREAL_1:1;
  end;

theorem
  sgn sgn x = sgn x
proof
A1: 0 < x or x < 0 or x = 0 by XREAL_1:1;
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,XREAL_1:10;
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;
A11:x + y < 0 or x + y = 0 or 0 < x + y by XREAL_1:1;
A12:sgn (x + y) = 0 implies sgn (x + y) <= sgn x + sgn y + 1 by A10;
    thus thesis by A10,A11,A12,Def2;
  end;
A13: x < 0 & 0 < y implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    assume that
A14:x < 0 and
A15:0 < y;
    sgn x = -1 by A14,Def2;
    then A16: sgn x + sgn y + 1 = 1 by A15,Def2;
A17:x + y < 0 or x + y = 0 or 0 < x + y by XREAL_1:1;
A18: sgn (x + y) = 0 implies sgn (x + y) <= sgn x + sgn y + 1 by A16;
    thus thesis by A16,A17,A18,Def2;
  end;
A19: x < 0 & y < 0 implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    assume that
A20: x < 0 and
A21: y < 0;
A22: x + y < 0 + 0 by A20,A21,XREAL_1:10;
    sgn y = -1 by A21,Def2;
    then sgn x + sgn y + 1 = -1 by A20,Def2;
    hence thesis by A22,Def2;
  end;
  x = 0 or y = 0 implies sgn (x + y) <= sgn x + sgn y + 1
  proof
    A23: x = 0 implies sgn (x + y) <= sgn x + sgn y + 1
    proof
      assume
A24:  x = 0;
      then sgn x + sgn y + 1 = 0 + sgn y + 1 by Def2 .= sgn y + 1;
      hence thesis by A24,XREAL_1:31;
    end;
    y = 0 implies sgn (x + y) <= sgn x + sgn y + 1
    proof
      assume
      A25: y = 0;
      then sgn x + sgn y + 1 = sgn x + 0 + 1 by Def2
      .= sgn x + 1;
      hence thesis by A25,XREAL_1:31;
    end;
    hence thesis by A23;
    end;
  hence thesis by A1,A7,A13,A19,XREAL_1:1;
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
         .= 1*0" by XCMPLX_0:def 9
         .= 0 by XCMPLX_0:def 7
         .= sgn(1*0) by Def2
         .= sgn(1*0") by XCMPLX_0:def 7
         .= sgn (1/x) by A1,XCMPLX_0:def 9;
    end;
    suppose
A2: x <> 0;
    then A3: sgn x <> 0 by Th33;
    (sgn x * sgn (1/x)) * (1/(sgn x)) = 1 * (1/(sgn x)) by A2,Th38;
    then sgn (1/x) * (sgn x * (1/(sgn x))) = 1/(sgn x);
    then sgn (1/x) * 1 = 1 /(sgn x) by A3,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,XREAL_1:10;
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,XREAL_1: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 by XREAL_1:1;
      then sgn (x + y) = -1 or sgn (x + y) = 0 or sgn (x + y) = 1 by Def2;
      hence thesis by A12;
    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 by XREAL_1:1;
      then sgn (x + y) = -1 or sgn (x + y) = 0 or sgn (x + y) = 1 by Def2;
      hence thesis by A16;
    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,XREAL_1:10;
      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,XREAL_1:1;
  end;

theorem
  sgn x = sgn (1/x)
  proof
    per cases;
    suppose
A1:   x = 0;
      1/0 = 1*0" by XCMPLX_0:def 9 .= 1*0 by XCMPLX_0:def 7;
      hence thesis by A1;
    end;
    suppose
A2:   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 A2,A3,XREAL_1:1;
    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 XCMPLX_0:def 7
          .= (sgn x)*0 by Def2
          .= (sgn x)*0" by XCMPLX_0:def 7
          .= (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;