:: Real Numbers - Basic Theorems
::  by Library Committee
::
:: Received February 9, 2005
:: Copyright (c) 2005-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, ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1,
      CARD_1, XXREAL_0, ARYTM_0, FUNCOP_1, XBOOLE_0, ARYTM_1, RELAT_1,
      XCMPLX_0;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
      ARYTM_1, ARYTM_0, XCMPLX_0, XREAL_0, NUMBERS, XXREAL_0;
 constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0;
 registrations ARYTM_2, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ORDINAL1,
      XBOOLE_0;
 requirements BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
 definitions XXREAL_0;
 theorems TARSKI, ARYTM_2, ARYTM_1, ARYTM_0, XBOOLE_0, XCMPLX_0, XCMPLX_1,
      XREAL_0, ZFMISC_1, XXREAL_0, NUMBERS, XTUPLE_0;

begin

reserve a,b,c,d for real number;
reserve r,s for real number;

Lm1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9 & s
= y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9 being
Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ & r in
[:{0},REAL+:] implies r <= s

proof
  assume

A1: (r in REAL+ & s in REAL+ & ex x9,y9 being Element of REAL+ st r = x9
  & s = y9 & x9 <=' y9) or (r in [:{0},REAL+:] & s in [:{0},REAL+:] & ex x9,y9

being Element of REAL+ st r = [0,x9] & s = [0,y9] & y9 <=' x9) or s in REAL+ &
  r in [:{0},REAL+:];

  per cases;
  case
    r in REAL+ & s in REAL+;
    hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
  end;
  case
    r in [:{0},REAL+:] & s in [:{0},REAL+:];
    hence thesis by A1,ARYTM_0:5,XBOOLE_0:3;
  end;
  case

    not(r in REAL+ & s in REAL+) & not (r in [:{0},REAL+:] & s in [:{0
    },REAL+:]);

    hence thesis by A1;
  end;
end;

Lm2: for x1,x2 being Element of REAL st a = [*x1,x2*] holds x2 = 0 & a = x1
proof
  let x1,x2 being Element of REAL;
  assume
A1: a = [*x1,x2*];
A2: a in REAL by XREAL_0:def 1;
  thus now
    assume x2 <> 0;
    then a = (0,1) --> (x1,x2) by A1,ARYTM_0:def 5;
    hence contradiction by A2,ARYTM_0:8;
  end;
  hence thesis by A1,ARYTM_0:def 5;
end;

Lm3: for a9,b9 being Element of REAL, a,b st a9 = a & b9 = b holds +(a9,b9) =
a + b

proof
  let a9,b9 be Element of REAL, a,b such that
A1: a9 = a and
A2: b9 = b;
  consider x1,x2,y1,y2 being Element of REAL such that
A3: a = [* x1,x2 *] and
A4: b = [*y1,y2*] and
A5: a+b = [*+(x1,y1),+(x2,y2)*] by XCMPLX_0:def 4;
A6: y2 = 0 by A4,Lm2;
  x2 = 0 by A3,Lm2;
  then
A7: +(x2,y2) = 0 by A6,ARYTM_0:11;
A8: b = y1 by A4,Lm2;
  a = x1 by A3,Lm2;
  hence thesis by A1,A2,A5,A8,A7,ARYTM_0:def 5;
end;

Lm4: {} in {{}} by TARSKI:def 1;

Lm5: a <= b implies a + c <= b + c
proof
  reconsider x1=a, y1=b, z1=c as Element of REAL by XREAL_0:def 1;
A1: +(y1,z1) = b + c by Lm3;
A2: +(x1,z1) = a + c by Lm3;
  assume
A3: a <= b;
  per cases by A3,XXREAL_0:def 5;
  suppose that
A4: a in REAL+ and
A5: b in REAL+ and
A6: c in REAL+;
    consider b9,c99 being Element of REAL+ such that
A7: b = b9 and
A8: c = c99 and
A9: +(y1,z1) = b9 + c99 by A5,A6,ARYTM_0:def 1;
    consider a9,c9 being Element of REAL+ such that
A10: a = a9 and
A11: c = c9 and
A12: +(x1,z1) = a9 + c9 by A4,A6,ARYTM_0:def 1;

    ex a99,b99 being Element of REAL+ st a = a99 & b = b99 & a99 <='
    b99 by A3,A4,A5,XXREAL_0:def 5;

    then a9 + c9 <=' b9 + c99 by A10,A11,A7,A8,ARYTM_1:7;
    hence thesis by A1,A2,A12,A9,Lm1;
  end;
  suppose that
A13: a in [:{0},REAL+:] and
A14: b in REAL+ and
A15: c in REAL+;
    consider b9,c99 being Element of REAL+ such that
    b = b9 and
A16: c = c99 and
A17: +(y1,z1) = b9 + c99 by A14,A15,ARYTM_0:def 1;
    consider a9,c9 being Element of REAL+ such that
    a = [0,a9] and
A18: c = c9 and
A19: +(x1,z1) = c9 - a9 by A13,A15,ARYTM_0:def 1;
    now
      per cases;
      suppose
A20:    a9 <=' c9;
A21:    c9 -' a9 <=' c9 by ARYTM_1:11;
        c9 <=' b9 + c99 by A18,A16,ARYTM_2:19;
        then
A22:    c9 -' a9 <=' b9 + c99 by A21,ARYTM_1:3;
        c9 - a9 = c9 -' a9 by A20,ARYTM_1:def 2;
        hence thesis by A1,A2,A19,A17,A22,Lm1;
      end;
      suppose
        not a9 <=' c9;
        then c9 - a9 = [0,a9 -' c9] by ARYTM_1:def 2;
        then c9 - a9 in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
        then
A23:    not a + c in REAL+ by A2,A19,ARYTM_0:5,XBOOLE_0:3;
        not b + c in [:{0},REAL+:] by A1,A17,ARYTM_0:5,XBOOLE_0:3;
        hence thesis by A23,XXREAL_0:def 5;
      end;
    end;
    hence thesis;
  end;
  suppose that
A24: a in [:{0},REAL+:] and
A25: b in [:{0},REAL+:] and
A26: c in REAL+;
    consider b9,c99 being Element of REAL+ such that
A27: b = [0,b9] and
A28: c = c99 and
A29: +(y1,z1) = c99 - b9 by A25,A26,ARYTM_0:def 1;
    consider a99,b99 being Element of REAL+ such that
A30: a = [0,a99] and
A31: b = [0,b99] and
A32: b99 <=' a99 by A3,A24,A25,XXREAL_0:def 5;
    consider a9,c9 being Element of REAL+ such that
A33: a = [0,a9] and
A34: c = c9 and
A35: +(x1,z1) = c9 - a9 by A24,A26,ARYTM_0:def 1;
A36: a9 = a99 by A30,A33,XTUPLE_0:1;
A37: b9 = b99 by A31,A27,XTUPLE_0:1;
    now
      per cases;
      suppose
A38:    a9 <=' c9;
        then b9 <=' c9 by A32,A36,A37,ARYTM_1:3;
        then
A39:    c9 - b9 = c9 -' b9 by ARYTM_1:def 2;
A40:    c9 - a9 = c9 -' a9 by A38,ARYTM_1:def 2;
        c9 -' a9 <=' c99 -' b9 by A32,A34,A28,A36,A37,ARYTM_1:16;
        hence thesis by A1,A2,A34,A35,A28,A29,A40,A39,Lm1;
      end;
      suppose
        not a9 <=' c9;
        then
A41:    +(x1,z1) = [0,a9 -' c9] by A35,ARYTM_1:def 2;
        then
A42:    +(x1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
        now
          per cases;
          suppose
            b9 <=' c9;
            then c9 - b9 = c9 -' b9 by ARYTM_1:def 2;

            then
A43:        not +(y1,z1) in [:{0},REAL+:] by A34,A28,A29,ARYTM_0:5,XBOOLE_0:3;

            not +(x1,z1) in REAL+ by A42,ARYTM_0:5,XBOOLE_0:3;
            hence thesis by A1,A2,A43,XXREAL_0:def 5;
          end;
          suppose
A44:        not b9 <=' c9;
A45:        b9 -' c9 <=' a9 -' c9 by A32,A36,A37,ARYTM_1:17;
A46:        +(y1,z1) = [0,b9 -' c9] by A34,A28,A29,A44,ARYTM_1:def 2;
            then +(y1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
            hence thesis by A1,A2,A41,A42,A46,A45,Lm1;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose that
A47: a in REAL+ and
A48: b in REAL+ and
A49: c in [:{0},REAL+:];
    consider b9,c99 being Element of REAL+ such that
A50: b = b9 and
A51: c = [0,c99] and
A52: +(y1,z1) = b9 - c99 by A48,A49,ARYTM_0:def 1;
    consider a9,c9 being Element of REAL+ such that
A53: a = a9 and
A54: c = [0,c9] and
A55: +(x1,z1) = a9 - c9 by A47,A49,ARYTM_0:def 1;
A56: c9 = c99 by A54,A51,XTUPLE_0:1;

A57: ex a99,b99 being Element of REAL+ st a = a99 & b = b99 & a99 <='
    b99 by A3,A47,A48,XXREAL_0:def 5;

    now
      per cases;
      suppose
A58:    c9 <=' a9;
        then c9 <=' b9 by A57,A53,A50,ARYTM_1:3;
        then
A59:    b9 - c9 = b9 -' c9 by ARYTM_1:def 2;
A60:    a9 - c9 = a9 -' c9 by A58,ARYTM_1:def 2;
        a9 -' c9 <=' b9 -' c99 by A57,A53,A50,A56,ARYTM_1:17;
        hence thesis by A1,A2,A55,A52,A56,A60,A59,Lm1;
      end;
      suppose
        not c9 <=' a9;
        then
A61:    +(x1,z1) = [0,c9 -' a9] by A55,ARYTM_1:def 2;
        then
A62:    +(x1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
        now
          per cases;
          suppose
            c9 <=' b9;
            then b9 - c9 = b9 -' c9 by ARYTM_1:def 2;

            then
A63:        not +(y1,z1) in [:{0},REAL+:] by A52,A56,ARYTM_0:5,XBOOLE_0:3;

            not +(x1,z1) in REAL+ by A62,ARYTM_0:5,XBOOLE_0:3;
            hence thesis by A1,A2,A63,XXREAL_0:def 5;
          end;
          suppose
A64:        not c9 <=' b9;
A65:        c9 -' b9 <=' c9 -' a9 by A57,A53,A50,ARYTM_1:16;
A66:        +(y1,z1) = [0,c9 -' b9] by A52,A56,A64,ARYTM_1:def 2;
            then +(y1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
            hence thesis by A1,A2,A61,A62,A66,A65,Lm1;
          end;
        end;
        hence thesis;
      end;
    end;
    hence thesis;
  end;
  suppose that
A67: a in [:{0},REAL+:] and
A68: b in REAL+ and
A69: c in [:{0},REAL+:];
A70: not c in REAL+ by A69,ARYTM_0:5,XBOOLE_0:3;
    not a in REAL+ by A67,ARYTM_0:5,XBOOLE_0:3;
    then consider a9,c9 being Element of REAL+ such that
    a = [0,a9] and
A71: c = [0,c9] and
A72: +(x1,z1) = [0,a9 + c9] by A70,ARYTM_0:def 1;
A73: +(x1,z1) in [:{0},REAL+:] by A72,Lm4,ZFMISC_1:87;
    consider b9,c99 being Element of REAL+ such that
    b = b9 and
A74: c = [0,c99] and
A75: +(y1,z1) = b9 - c99 by A68,A69,ARYTM_0:def 1;
A76: c9 = c99 by A71,A74,XTUPLE_0:1;
    now
      per cases;
      suppose
        c9 <=' b9;
        then b9 - c99 = b9 -' c99 by A76,ARYTM_1:def 2;
        then
A77:    not +(y1,z1) in [:{0},REAL+:] by A75,ARYTM_0:5,XBOOLE_0:3;
        not +(x1,z1) in REAL+ by A73,ARYTM_0:5,XBOOLE_0:3;
        hence thesis by A1,A2,A77,XXREAL_0:def 5;
      end;
      suppose
A78:    not c9 <=' b9;
A79:    c9 <=' c9 + a9 by ARYTM_2:19;
        c9 -' b9 <=' c9 by ARYTM_1:11;
        then
A80:    c9 -' b9 <=' c9 + a9 by A79,ARYTM_1:3;
A81:    +(y1,z1) = [0,c9 -' b9] by A75,A76,A78,ARYTM_1:def 2;
        then +(y1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
        hence thesis by A1,A2,A72,A73,A81,A80,Lm1;
      end;
    end;
    hence thesis;
  end;
  suppose that
A82: a in [:{0},REAL+:] and
A83: b in [:{0},REAL+:] and
A84: c in [:{0},REAL+:];
A85: not c in REAL+ by A84,ARYTM_0:5,XBOOLE_0:3;
A86: not c in REAL+ by A84,ARYTM_0:5,XBOOLE_0:3;
    not a in REAL+ by A82,ARYTM_0:5,XBOOLE_0:3;
    then consider a9,c9 being Element of REAL+ such that
A87: a = [0,a9] and
A88: c = [0,c9] and
A89: +(x1,z1) = [0,a9 + c9] by A86,ARYTM_0:def 1;
A90: +(x1,z1) in [:{0},REAL+:] by A89,Lm4,ZFMISC_1:87;
    not b in REAL+ by A83,ARYTM_0:5,XBOOLE_0:3;
    then consider b9,c99 being Element of REAL+ such that
A91: b = [0,b9] and
A92: c = [0,c99] and
A93: +(y1,z1) = [0,b9 + c99] by A85,ARYTM_0:def 1;
A94: +(y1,z1) in [:{0},REAL+:] by A93,Lm4,ZFMISC_1:87;
A95: c9 = c99 by A88,A92,XTUPLE_0:1;
    consider a99,b99 being Element of REAL+ such that
A96: a = [0,a99] and
A97: b = [0,b99] and
A98: b99 <=' a99 by A3,A82,A83,XXREAL_0:def 5;
A99: b9 = b99 by A97,A91,XTUPLE_0:1;
    a9 = a99 by A96,A87,XTUPLE_0:1;
    then b9 + c9 <=' a9 + c99 by A98,A99,A95,ARYTM_1:7;
    hence thesis by A1,A2,A89,A93,A95,A90,A94,Lm1;
  end;
end;

Lm6: a <= b & c <= d implies a+c <= b+d
proof
  assume a<=b;
  then
A1: a+c <= b+c by Lm5;
  assume c <= d;
  then b+c <= b+d by Lm5;
  hence thesis by A1,XXREAL_0:2;
end;

Lm7: a <= b implies a-c <= b-c
proof
  a <= b implies a + -c <= b + -c by Lm5;
  hence thesis;
end;

Lm8: a < b & c <= d implies a+c < b+d
proof
  assume that
A1: a<b and
A2: c <= d;
  for a,b,c,d holds a<b & c <= d implies a+c < b+d
  proof
    let a,b,c,d;
    assume
A3: a<b;
    assume
A4: c <= d;
A5: a+c <> b+d
    proof
      a+c <= d+a by A4,Lm5;
      then
A6:   a+c-d<=a+d-d by Lm7;
      assume a+c = b+d;
      hence contradiction by A3,A6;
    end;
    a+c <= b+d by A3,A4,Lm6;
    hence thesis by A5,XXREAL_0:1;
  end;
  hence thesis by A1,A2;
end;

Lm9: 0 < a implies b < b+a
proof
  assume 0<a;
  then b+0<b+a by Lm8;
  hence thesis;
end;

theorem Th1:
  ex b st a < b
proof
  take a+1;
  a+0<a+1 by Lm8;
  hence thesis;
end;

theorem Th2:
  ex b st b < a
proof
  take a-1;
  a+ -1<a+ -0 by Lm8;
  hence thesis;
end;

theorem
  ex c st a < c & b < c
proof
  per cases;
  suppose
A1: a <= b;
    take z = b + 1;
    b < z by Lm9;
    hence thesis by A1,XXREAL_0:2;
  end;
  suppose
A2: b <= a;
    take z = a + 1;
    a < z by Lm9;
    hence thesis by A2,XXREAL_0:2;
  end;
end;

Lm10: a+c <= b+c implies a <= b
proof
  assume a+c <= b+c;
  then a+c+(-c)<=b+c+(-c) by Lm5;
  hence thesis;
end;

theorem
  ex c st c < a & c < b
proof
  per cases;
  suppose
A1: a <= b;
    take z = a+-1;
    z < a+0 by Lm10;
    hence thesis by A1,XXREAL_0:2;
  end;
  suppose
A2: b <= a;
    take z = b+-1;
    z < b+0 by Lm10;
    hence thesis by A2,XXREAL_0:2;
  end;
end;

Lm11: for a9,b9 being Element of REAL, a,b st a9 = a & b9 = b holds *(a9,b9) =
a * b

proof
  let a9,b9 be Element of REAL, a,b such that
A1: a9 = a and
A2: b9 = b;
  consider x1,x2,y1,y2 being Element of REAL such that
A3: a = [* x1,x2 *] and
A4: b = [*y1,y2*] and

A5: a*b = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by XCMPLX_0:def 5
;

A6: b = y1 by A4,Lm2;
  x2 = 0 by A3,Lm2;
  then
A7: *(x2,y1) = 0 by ARYTM_0:12;
A8: y2 = 0 by A4,Lm2;
  then *(x1,y2) = 0 by ARYTM_0:12;
  then
A9: +(*(x1,y2),*(x2,y1)) = 0 by A7,ARYTM_0:11;
  a = x1 by A3,Lm2;
  hence *(a9,b9) = +(*(x1,y1),*(opp x2,y2)) by A1,A2,A6,A8,ARYTM_0:11,12
    .= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:15
    .= a * b by A5,A9,ARYTM_0:def 5;
end;
reconsider o = 0 as Element of REAL+ by ARYTM_2:20;

Lm12: a <= b & 0 <= c implies a*c <= b*c
proof
  assume that
A1: a <= b and
A2: 0 <= c;
  not o in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
  then
A3: c in REAL+ by A2,XXREAL_0:def 5;
  reconsider x1=a, y1=b, z1=c as Element of REAL by XREAL_0:def 1;
A4: *(y1,z1) = b * c by Lm11;
A5: *(x1,z1) = a * c by Lm11;
  assume
A6: not thesis;
  then
A7: c <> 0;
  per cases by A1,XXREAL_0:def 5;
  suppose that
A8: a in REAL+ and
A9: b in REAL+;
    consider b9,c99 being Element of REAL+ such that
A10: b = b9 and
A11: c = c99 and
A12: *(y1,z1) = b9 *' c99 by A3,A9,ARYTM_0:def 2;
    consider a9,c9 being Element of REAL+ such that
A13: a = a9 and
A14: c = c9 and
A15: *(x1,z1) = a9 *' c9 by A3,A8,ARYTM_0:def 2;

    ex a99,b99 being Element of REAL+ st a = a99 & b = b99 & a99 <='
    b99 by A1,A8,A9,XXREAL_0:def 5;

    then a9 *' c9 <=' b9 *' c9 by A13,A10,ARYTM_1:8;
    hence contradiction by A4,A5,A6,A14,A15,A11,A12,Lm1;
  end;
  suppose that
A16: a in [:{0},REAL+:] and
A17: b in REAL+;

    ex a9,c9 being Element of REAL+ st a = [0,a9] & c = c9 & *(x1,z1)
    = [0,c9 *' a9] by A3,A7,A16,ARYTM_0:def 2;

    then *(x1,z1) in [:{0},REAL+:] by Lm4,ZFMISC_1:87;
    then
A18: not *(x1,z1) in REAL+ by ARYTM_0:5,XBOOLE_0:3;

    ex b9,c99 being Element of REAL+ st b = b9 & c = c99 & * (y1,z1) =
    b9 *' c99 by A3,A17,ARYTM_0:def 2;

    then not *(y1,z1) in [:{0},REAL+:] by ARYTM_0:5,XBOOLE_0:3;
    hence contradiction by A4,A5,A6,A18,XXREAL_0:def 5;
  end;
  suppose that
A19: a in [:{0},REAL+:] and
A20: b in [:{0},REAL+:];
    consider b9,c99 being Element of REAL+ such that
A21: b = [0,b9] and
A22: c = c99 and
A23: *(y1,z1) = [0,c99 *' b9] by A3,A7,A20,ARYTM_0:def 2;
A24: *(y1,z1) in [:{0},REAL+:] by A23,Lm4,ZFMISC_1:87;
    consider a99,b99 being Element of REAL+ such that
A25: a = [0,a99] and
A26: b = [0,b99] and
A27: b99 <=' a99 by A1,A19,A20,XXREAL_0:def 5;
A28: b9 = b99 by A26,A21,XTUPLE_0:1;
    consider a9,c9 being Element of REAL+ such that
A29: a = [0,a9] and
A30: c = c9 and
A31: *(x1,z1) = [0,c9 *' a9] by A3,A7,A19,ARYTM_0:def 2;
A32: *(x1,z1) in [:{0},REAL+:] by A31,Lm4,ZFMISC_1:87;
    a9 = a99 by A25,A29,XTUPLE_0:1;
    then b9 *' c9 <=' a9 *' c9 by A27,A28,ARYTM_1:8;
    hence contradiction by A4,A5,A6,A30,A31,A22,A23,A32,A24,Lm1;
  end;
end;

Lm13: 0 < c & a < b implies a*c < b*c
proof
  assume
A1: 0<c;
  assume
A2: a<b;
A3: a*c <> b*c
  proof
    assume a*c = b*c;
    then a*(c*c")=b*c*c" by XCMPLX_1:4;
    then a*1=b*(c*c") by A1,XCMPLX_0:def 7;
    then a=b*1 by A1,XCMPLX_0:def 7;
    hence contradiction by A2;
  end;
  a*c <= b*c by A1,A2,Lm12;
  hence thesis by A3,XXREAL_0:1;
end;

theorem Th5:
  a < b implies ex c st a < c & c < b
proof
  assume
A1: a<b;
  take z=(a+b)/2;
  1*a+a<a+b by A1,Lm10;
  then 2"*(2*a)<2"*(a+b) by Lm13;
  hence a<z;
  a+b<1*b+b by A1,Lm10;
  then 2"*(a+b)<2"*(2*b) by Lm13;
  hence thesis;
end;

begin

theorem
  a <= b iff a + c <= b + c by Lm5,Lm10;

theorem
  a <= b & c <= d implies a+c <= b+d by Lm6;

theorem
  a < b & c <= d implies a+c < b+d by Lm8;

Lm14: a<=b implies -b<=-a
proof
  assume a<=b;
  then a-b<=b-b by Lm7;
  then a-b-a<=0-a by Lm7;
  hence thesis;
end;

Lm15: -b<=-a implies a<=b
proof
  assume -b<=-a;
  then -(-a)<=-(-b) by Lm14;
  hence thesis;
end;

begin

theorem Th9:
  a <= b iff a-c <= b-c
proof
  thus a <= b implies a-c <= b-c by Lm7;
  assume a-c <= b-c;
  then a+ (-c) + c <= b+ (-c)+c by Lm5;
  hence thesis;
end;

theorem
  a <= b iff c-b <= c-a
proof
  hereby
    assume
A1: a <= b;
    assume c-a < c-b;
    then -(c-b)<-(c-a) by Lm15;
    then b-c < a-c;
    hence contradiction by A1,Lm7;
  end;
  assume c-a>=c-b;
  then -(c-a)<=-(c-b) by Lm14;
  then a-c <= b-c;
  hence thesis by Th9;
end;

Lm16: a+b <= c implies a <= c-b
proof
  assume a+b<=c;
  then a+b-b<=c-b by Lm7;
  hence thesis;
end;

Lm17: a <= b-c implies a+c <= b
proof
  assume a <= b-c;
  then a+c <= b - c + c by Lm5;
  hence thesis;
end;

Lm18: a <= b+c implies a-b <= c
proof
  assume a<=b+c;
  then a-b <= c+b-b by Lm7;
  hence thesis;
end;

Lm19: a-b <= c implies a <= b+c
proof
  assume a-b <= c;
  then a + -b <= c;
  then a <= c - -b by Lm16;
  hence thesis;
end;

theorem
  a <= b-c implies c <= b-a
proof
  assume a<=b-c;
  then a+c <= b by Lm17;
  hence thesis by Lm16;
end;

theorem
  a-b <= c implies a-c <= b
proof
  assume c>=a-b;
  then c+b>=a by Lm19;
  hence thesis by Lm18;
end;

theorem Th13:
  a <= b & c <= d implies a-d <= b-c
proof
  assume that
A1: a <= b and
A2: c <= d;
  -d <= -c by A2,Lm14;
  then a+ -d <= b+ -c by A1,Lm6;
  hence thesis;
end;

theorem Th14:
  a < b & c <= d implies a-d < b-c
proof
  assume that
A1: a < b and
A2: c <= d;
  - d <= - c by A2,Lm14;
  then a+ -d < b+ -c by A1,Lm8;
  hence thesis;
end;

theorem Th15:
  a <= b & c < d implies a-d < b-c
proof
  assume that
A1: a <= b and
A2: c < d;
  c-b < d-a by A1,A2,Th14;
  then -(d-a) < -(c-b) by Lm15;
  hence thesis;
end;

Lm20: a+b<=c+d implies a-c <= d-b
proof
  assume a+b<=c+d;
  then a<=c+d-b by Lm16;
  then a<=c+(d-b);
  hence thesis by Lm18;
end;

theorem
  a-b <= c-d implies a-c <= b-d
proof
  assume a-b<=c-d;
  then a-b+d<=c by Lm17;
  then a+d-b<=c;
  then a+d<=c+b by Lm19;
  hence thesis by Lm20;
end;

theorem
  a-b <= c-d implies d-b <= c-a
proof
  assume a-b<=c-d;
  then a-b+d<=c by Lm17;
  then a+d-b<=c;
  then a+d<=c+b by Lm19;
  hence thesis by Lm20;
end;

theorem
  a-b <= c-d implies d-c <= b-a
proof
  assume a-b<=c-d;
  then a-b+d<=c by Lm17;
  then a+d-b<=c;
  then a+d<=c+b by Lm19;
  hence thesis by Lm20;
end;

begin

theorem
  a+b <= c iff a <= c-b by Lm16,Lm17;

theorem
  a <= b+c iff a-b <= c by Lm18,Lm19;

theorem
  a+b<=c+d iff a-c <= d-b
proof
  thus a+b<=c+d implies a-c <= d-b by Lm20;
  assume
A1: a-c <= d-b;
  assume c+d<a+b;
  then d<b+a-c by Lm19;
  then d<b+(a-c);
  hence thesis by A1,Lm17;
end;

theorem
  a+b<=c-d implies a+d<=c-b
proof
  assume
A1: a+b<=c-d;
  per cases by A1;
  suppose
    a+b<=c-d;
    then a+b+d<=c by Lm17;
    then a+d+b<=c;
    hence thesis by Lm16;
  end;
  suppose
    b+a<=c-d;
    then a+b+d<=c by Lm17;
    then a+d+b<=c;
    hence thesis by Lm16;
  end;
end;

theorem
  a-b<=c+d implies a-d<=c+b
proof
  assume
A1: c+d>=a-b;
  per cases by A1;
  suppose
    c+d>=a-b;
    then c+d+b>=a by Lm19;
    then c+b+d>=a;
    hence thesis by Lm18;
  end;
  suppose
    d+c>=a-b;
    then c+d+b>=a by Lm19;
    then c+b+d>=a;
    hence thesis by Lm18;
  end;
end;

begin

theorem
  a<=b iff -b<=-a by Lm14,Lm15;

Lm21: a < b implies 0 < b-a
proof
  assume a < b;
  then a + 0 < b;
  hence thesis by Lm19;
end;

theorem Th25:
  a<=-b implies b<=-a
proof
  assume a<=-b;
  then a+b<=-b+b by Lm5;
  then b--a<=0;
  hence thesis by Lm21;
end;

Lm22: a <= b implies 0 <= b-a
proof
  assume a <= b;
  then a - a <= b - a by Lm7;
  hence thesis;
end;

theorem Th26:
  -b<=a implies -a<=b
proof
  assume
A1: -b<=a;
  assume b<-a;
  then b+a<-a+a by Lm10;
  then a--b<0;
  hence thesis by A1,Lm22;
end;

begin

theorem
  0 <= a & 0 <= b & a+b = 0 implies a = 0;

theorem
  a <= 0 & b <= 0 & a+b = 0 implies a = 0;

begin

theorem
  0 < a implies b < b+a by Lm9;

theorem
  a < 0 implies a+b < b
proof
  assume a<0;
  then b+a<0+b by Lm10;
  hence thesis;
end;

Lm23: a < b implies a-b < 0
proof
  assume
A1: a < b;
  assume a-b>=0;
  then a-b+b>=0+b by Lm5;
  hence thesis by A1;
end;

theorem
  0 <= a implies b <= a+b
proof
  assume
A1: 0 <= a;
  assume
A2: a+b<b;
  per cases by A2;
  suppose
    a+b<b;
    then a+b-b<0 by Lm23;
    hence thesis by A1;
  end;
  suppose
    b-a>b;
    then b+-a-b>0 by Lm21;
    hence thesis by A1;
  end;
end;

theorem
  a <= 0 implies a+b <= b
proof
  assume a<=0;
  then b+a<=0+b by Lm6;
  hence thesis;
end;

begin

theorem
  0 <= a & 0 <= b implies 0 <= a+b;

theorem
  0 <= a & 0 < b implies 0 < a+b;

theorem Th35:
  a <= 0 & c <= b implies c+a <= b
proof
  assume that
A1: a <= 0 and
A2: c <= b;
  a+c <= 0+b by A1,A2,Lm6;
  hence thesis;
end;

theorem Th36:
  a <= 0 & c < b implies c+a < b
proof
  assume that
A1: a <= 0 and
A2: c < b;
  a+c < 0+b by A1,A2,Lm8;
  hence thesis;
end;

theorem Th37:
  a < 0 & c <= b implies c+a < b
proof
  assume that
A1: a < 0 and
A2: c <= b;
  a+c < 0+b by A1,A2,Lm8;
  hence thesis;
end;

theorem Th38:
  0 <= a & b <= c implies b <= a+c
proof
  assume that
A1: 0 <= a and
A2: b <= c;
  b+0 <= a+c by A1,A2,Lm6;
  hence thesis;
end;

theorem Th39:
  0 < a & b <= c implies b < a+c
proof
  assume that
A1: 0 < a and
A2: b <= c;
  b+0 < a+c by A1,A2,Lm8;
  hence thesis;
end;

theorem Th40:
  0 <= a & b < c implies b < a+c
proof
  assume that
A1: 0 <= a and
A2: b < c;
  b+0 < a+c by A1,A2,Lm8;
  hence thesis;
end;

Lm24: c < 0 & a < b implies b*c < a*c
proof
  assume
A1: c < 0;
  assume a<b;
  then a*(-c)<b*(-c) by A1,Lm13;
  then -(a*c)<-(b*c);
  hence thesis by Lm14;
end;

Lm25: 0 <= c & b <= a implies b/c <= a/c
proof
  assume that
A1: 0<=c and
A2: b <= a;
  per cases by A1;
  suppose
    c = 0;
    then
A3: c" = 0;
    then b*c" = 0;
    then
A4: b/c = 0 by XCMPLX_0:def 9;
    a*c" = 0 by A3;
    hence thesis by A4,XCMPLX_0:def 9;
  end;
  suppose
A5: 0<c;
    assume a/c < b/c;
    then a/c*c < b/c*c by A5,Lm13;
    then a<b/c*c by A5,XCMPLX_1:87;
    hence contradiction by A2,A5,XCMPLX_1:87;
  end;
end;

Lm26: 0 < c & a < b implies a/c < b/c
proof
  assume
A1: 0<c;
  a<b implies a/c < b/c
  proof
    assume a<b;
    then a*c"<b*c" by A1,Lm13;
    then a/c <b*c" by XCMPLX_0:def 9;
    hence thesis by XCMPLX_0:def 9;
  end;
  hence thesis;
end;

Lm27: 0 < a implies a/2 < a
proof
  assume 0<a;
  then 0+a/2<a/2+a/2 by Lm10;
  hence thesis;
end;

begin

theorem
  (for a being real number st a>0 holds c <= b+a) implies c <= b
proof
  assume
A1: for a st a>0 holds b+a>=c;
  set d=c-b;
  assume b<c;
  then
A2: 0<d by Lm21;
  then b+d/2<b+d by Lm10,Lm27;
  hence contradiction by A1,A2;
end;

theorem
  (for a being real number st a<0 holds b+a <= c) implies b <= c
proof
  assume
A1: for a st a<0 holds b+a<=c;
  set d=c-b;
  assume c < b;
  then
A2: 0>c-b by Lm23;
  then (-d)/2<-d by Lm27;
  then c+-d/2<c+-d by Lm10;
  then c-d/2<c-d;
  then c < b+d/2 by Lm16;
  hence contradiction by A1,A2;
end;

begin

theorem
  0 <= a implies b-a <= b
proof
  0 <= a implies b - a <= b - 0 by Th13;
  hence thesis;
end;

theorem Th44:
  0 < a implies b-a < b
proof
  assume 0 < a;
  then b + -a < b + 0 by Lm10;
  hence thesis;
end;

theorem
  a <= 0 implies b <= b-a
proof
  assume a<=0;
  then b+a<=0+b by Lm6;
  hence thesis by Lm16;
end;

theorem
  a < 0 implies b < b-a
proof
  assume a<0;
  then b+a<0+b by Lm10;
  hence thesis by Lm19;
end;

theorem
  a <= b implies a-b <= 0
proof
  assume
A1: a <= b;
  assume a-b>0;
  then a-b+b>0+b by Lm10;
  hence thesis by A1;
end;

theorem Th48:
  a <= b implies 0 <= b-a
proof
  assume a <= b;
  then a - a <= b - a by Lm7;
  hence thesis;
end;

theorem
  a < b implies a-b < 0 by Lm23;

theorem
  a < b implies 0 < b-a by Lm21;

theorem
  0 <= a & b < c implies b-a < c
proof
  assume that
A1: 0 <= a and
A2: b < c;
  b+0 < a+c by A1,A2,Th40;
  hence thesis by Lm17;
end;

theorem
  a <= 0 & b <= c implies b <= c-a
proof
  assume that
A1: a <= 0 and
A2: b <= c;
  b+a <= c by A1,A2,Th35;
  hence thesis by Lm16;
end;

theorem
  a <= 0 & b < c implies b < c-a
proof
  assume that
A1: a <= 0 and
A2: b < c;
  b+a < c by A1,A2,Th36;
  hence thesis by Lm19;
end;

theorem
  a < 0 & b <= c implies b < c-a
proof
  assume that
A1: a < 0 and
A2: b <= c;
  a+b < c by A1,A2,Th37;
  hence thesis by Lm19;
end;

theorem
  a <> b implies 0 < a-b or 0 < b-a
proof
  assume
A1: a <> b;
  per cases by A1,XXREAL_0:1;
  suppose
    a < b;
    then 0 + a < b;
    hence thesis by Lm19;
  end;
  suppose
    b < a;
    then 0 + b < a;
    hence thesis by Lm19;
  end;
end;

begin

theorem
  (for a being real number st a<0 holds c <= b-a) implies b>=c
proof
  assume
A1: for a st a<0 holds b-a>=c;
  set d=b-c;
  assume b<c;
  then
A2: 0>b-c by Lm23;
  then (-d)/2<-d by Lm27;
  then b+-d/2<b+-d by Lm10;
  then b-d/2<b-d;
  hence contradiction by A1,A2;
end;

theorem
  (for a being real number st a>0 holds b-a <= c) implies b<=c
proof
  assume
A1: for a st a>0 holds b-a<=c;
  set d=b-c;
  assume b>c;
  then
A2: 0<d by Lm21;
  then c+d/2<c+d by Lm10,Lm27;
  then c < b-d/2 by Lm19;
  hence contradiction by A1,A2;
end;

begin

theorem
  a < 0 iff 0 < -a;

theorem
  a <= -b implies a+b <= 0
proof
  assume a<=-b;
  then a+b<=-b+b by Lm5;
  hence thesis;
end;

theorem
  -a <= b implies 0 <= a+b
proof
  assume b>=-a;
  then b+a>=-a+a by Lm5;
  hence thesis;
end;

theorem
  a < -b implies a+b < 0
proof
  assume a<-b;
  then a+b<-b+b by Lm10;
  hence thesis;
end;

theorem
  -b < a implies 0 < a+b
proof
  assume a>-b;
  then a+b>-b+b by Lm10;
  hence thesis;
end;

Lm28: a <= b & c <= 0 implies b*c <= a*c
proof
  assume
A1: a<=b;
  assume c <= 0;
  then a*(-c)<=b*(-c) by A1,Lm12;
  then -(a*c)<=-(b*c);
  hence thesis by Lm15;
end;

begin

theorem
  0 <= a*a
proof
  per cases;
  suppose
    0 <= a;
    hence thesis;
  end;
  suppose
    not 0 <= a;
    hence thesis;
  end;
end;

theorem
  a <= b & 0 <= c implies a*c <= b*c by Lm12;

theorem
  a <= b & c <= 0 implies b*c <= a*c by Lm28;

theorem Th66:
  0 <= a & a <= b & 0 <= c & c <= d implies a*c <= b*d
proof
  assume that
A1: 0<=a and
A2: a<=b and
A3: 0<=c and
A4: c <= d;
A5: a*c <= b*c by A2,A3,Lm12;
  b*c <= b*d by A1,A2,A4,Lm12;
  hence thesis by A5,XXREAL_0:2;
end;

theorem
  a <= 0 & b <= a & c <= 0 & d <= c implies a*c <= b*d
proof
  assume that
A1: 0>=a and
A2: a>=b and
A3: 0>=c and
A4: c>=d;
A5: -c <= -d by A4,Lm14;
  -a<=-b by A2,Lm14;
  then (-a)*(-c)<=(-b)*(-d) by A1,A3,A5,Th66;
  hence thesis;
end;

theorem
  0 < c & a < b implies a*c < b*c by Lm13;

theorem
  c < 0 & a < b implies b*c < a*c by Lm24;

theorem
  a < 0 & b <= a & c < 0 & d < c implies a*c < b*d
proof
  assume that
A1: 0>a and
A2: a>=b and
A3: 0>c and
A4: c>d;
A5: a*c < a*d by A1,A4,Lm24;
  a*d<=b*d by A2,A3,A4,Lm28;
  hence thesis by A5,XXREAL_0:2;
end;

begin

theorem
  0 <= a & 0 <= b & 0 <= c & 0 <= d & a*c+b*d = 0 implies a = 0 or c = 0;

Lm29: c < 0 & a < b implies b/c < a/c
proof
  assume that
A1: c < 0 and
A2: a < b;
  a/(-c)<b/(-c) by A1,A2,Lm26;
  then -a/c < b/(-c) by XCMPLX_1:188;
  then -a/c < -b/c by XCMPLX_1:188;
  hence thesis by Lm14;
end;

Lm30: c <= 0 & b/c < a/c implies a < b
proof
  assume that
A1: c <= 0 and
A2: b/c < a/c;
A3: now
    assume c = 0;
    then
A4: c" = 0;
    a/c = a*c" by XCMPLX_0:def 9
      .= b*c" by A4
      .= b/c by XCMPLX_0:def 9;
    hence contradiction by A2;
  end;
  then a/c*c < b/c*c by A1,A2,Lm24;
  then a<b/c*c by A3,XCMPLX_1:87;
  hence thesis by A3,XCMPLX_1:87;
end;

begin

theorem
  0 <= c & b <= a implies b/c <= a/c by Lm25;

theorem
  c <= 0 & a <= b implies b/c <= a/c by Lm30;

theorem
  0 < c & a < b implies a/c < b/c by Lm26;

theorem
  c < 0 & a < b implies b/c < a/c by Lm29;

theorem
  0 < c & 0 < a & a < b implies c/b < c/a
proof
  assume that
A1: 0<c and
A2: 0<a and
A3: a<b;
  a*b"<b*b" by A2,A3,Lm13;
  then a*b"<1 by A2,A3,XCMPLX_0:def 7;
  then a"*(a*b")<a"*1 by A2,Lm13;
  then a"*a*b"<a";
  then 1*b"<a" by A2,XCMPLX_0:def 7;
  then c*b"<c*a" by A1,Lm13;
  then c/b<c*a" by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

Lm31: b < 0 & a < b implies b" < a"
proof
A1: a" = 1/a by XCMPLX_1:215;
  assume that
A2: 0>b and
A3: a<b;
  b*(a")<a*(a") by A2,A3,Lm24;
  then b*(a")<1 by A1,A2,A3,XCMPLX_1:87;
  then b"*(b*(a"))>1*(b") by A2,Lm24;
  then b"*b*(a")>1*(b");
  then 1*(a")>1*(b") by A2,XCMPLX_0:def 7;
  hence thesis;
end;

begin

theorem Th77:
  0 < b & a*b <= c implies a <= c/b
proof
  assume that
A1: b>0 and
A2: a*b<=c;
  a*b/b<=c/b by A1,A2,Lm25;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th78:
  b < 0 & a*b <= c implies c/b <= a
proof
  assume that
A1: b<0 and
A2: a*b<=c;
  a*b/b>=c/b by A1,A2,Lm30;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th79:
  0 < b & c <= a*b implies c/b <= a
proof
  assume that
A1: b>0 and
A2: a*b>=c;
  a*b/b>=c/b by A1,A2,Lm25;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th80:
  b < 0 & c <= a*b implies a <= c/b
proof
  assume that
A1: b<0 and
A2: a*b>=c;
  a*b/b<=c/b by A1,A2,Lm30;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th81:
  0 < b & a*b < c implies a< c/b
proof
  assume that
A1: b>0 and
A2: a*b<c;
  a*b/b<c/b by A1,A2,Lm26;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th82:
  b < 0 & a*b < c implies c/b < a
proof
  assume that
A1: b<0 and
A2: a*b<c;
  a*b/b>c/b by A1,A2,Lm29;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th83:
  0 < b & c < a*b implies c/b < a
proof
  assume that
A1: b>0 and
A2: a*b>c;
  a*b/b>c/b by A1,A2,Lm26;
  hence thesis by A1,XCMPLX_1:89;
end;

theorem Th84:
  b < 0 & c < a*b implies a < c/b
proof
  assume that
A1: b<0 and
A2: a*b>c;
  a*b/b<c/b by A1,A2,Lm29;
  hence thesis by A1,XCMPLX_1:89;
end;

Lm32: 0 < a & a <= b implies b" <= a"
proof
  assume that
A1: 0<a and
A2: a<=b;
  a*(b")<=b*(b") by A1,A2,Lm12;
  then a*(b")<=1 by A1,A2,XCMPLX_0:def 7;
  then a"*(a*b")<=1*a" by A1,Lm12;
  then a"*a*b"<=1*a";
  then 1*b"<=1*a" by A1,XCMPLX_0:def 7;
  hence thesis;
end;

Lm33: b < 0 & a <= b implies b" <= a"
proof
  assume that
A1: 0>b and
A2: a<=b;
  b*(a")<=a*(a") by A1,A2,Lm28;
  then b*(a")<=1 by A1,A2,XCMPLX_0:def 7;
  then b"*(b*(a"))>=1*(b") by A1,Lm28;
  then b"*b*a">=1*b";
  then 1*a">=1*b" by A1,XCMPLX_0:def 7;
  hence thesis;
end;

begin

theorem
  0 < a & a <= b implies b" <= a" by Lm32;

theorem
  b < 0 & a <= b implies b" <= a" by Lm33;

theorem
  b < 0 & a < b implies b" < a" by Lm31;

Lm34: 0 < a & a < b implies b" < a"
proof
A1: b" = 1/b by XCMPLX_1:215;
  assume that
A2: 0<a and
A3: a<b;
  a*(b")<b*(b") by A2,A3,Lm13;
  then a*(b")<1 by A1,A2,A3,XCMPLX_1:87;
  then a"*(a*(b"))<1*(a") by A2,Lm13;
  then a"*a*b"<1*(a");
  then 1*b"<1*(a") by A2,XCMPLX_0:def 7;
  hence thesis;
end;

theorem
  0 < a & a < b implies b" < a" by Lm34;

theorem
  0 < b" & b" <= a" implies a <= b
proof
  assume that
A1: b">0 and
A2: a">=b";
  a""<=b"" by A1,A2,Lm32;
  hence thesis;
end;

theorem
  a" < 0 & b" <= a" implies a <= b
proof
  assume that
A1: a"<0 and
A2: a">=b";
  a""<=b"" by A1,A2,Lm33;
  hence thesis;
end;

theorem
  0 < b" & b" < a" implies a < b
proof
  assume that
A1: b">0 and
A2: a">b";
  a""<b"" by A1,A2,Lm34;
  hence thesis;
end;

theorem
  a" < 0 & b" < a" implies a < b
proof
  assume that
A1: a"<0 and
A2: a">b";
  a""<b"" by A1,A2,Lm31;
  hence thesis;
end;

Lm35: for a being non negative non positive real number holds 0 = a*b;

begin

theorem
  0 <= a & (b-a)*(b+a) <= 0 implies -a <= b & b <= a
proof
  assume that
A1: a>=0 and
A2: (b-a)*(b+a)<=0;
  b+0<=b+a by A1,Lm6;
  then b+a>=0 by A1,A2;
  then
A3: b>=0-a by Lm18;
  b-a>=0 & b+a<=0 or b-a<=0 & b+a>=0 by A2;
  then b<=a+0 by A1,Lm19;
  hence thesis by A3;
end;

theorem
  0 <= a & (b-a)*(b+a) < 0 implies -a < b & b < a
proof
  assume that
A1: a>=0 and
A2: (b-a)*(b+a)<0;
A3: b-a>0 & b+a<0 or b-a<0 & b+a>0 by A2,Lm35;
  then
A4: b<a+0 by A1,Lm16;
  b+0<=b+a by A1,Lm6;
  then b>0-a by A1,A3,Lm17;
  hence thesis by A4;
end;

theorem
  0 <= (b-a)*(b+a) implies b <= -a or a <= b
proof
  assume (b-a)*(b+a)>=0;
  then b-a>=0 & b+a>=0 or b-a<=0 & b+a<=0;
  then b-a+a>=0+a or b+a<=0 by Lm6;
  then b>=0+a or b+a-a<=0-a by Lm7;
  hence thesis;
end;

theorem
  0 <= a & 0 <= c & a < b & c < d implies a*c < b*d
proof
  assume that
A1: 0<=a and
A2: 0<=c and
A3: a<b and
A4: c < d;
A5: a*c <= a*d by A1,A4,Lm12;
  a*d<b*d by A2,A3,A4,Lm13;
  hence thesis by A5,XXREAL_0:2;
end;

theorem
  0 <= a & 0 < c & a < b & c <= d implies a*c < b*d
proof
  assume that
A1: 0<=a and
A2: 0<c and
A3: a<b and
A4: c <=d;
A5: a*c <=a*d by A1,A4,Lm12;
  a*d<b*d by A2,A3,A4,Lm13;
  hence thesis by A5,XXREAL_0:2;
end;

theorem Th98:
  0 < a & 0 < c & a <= b & c < d implies a*c < b*d
proof
  assume that
A1: 0<a and
A2: 0<c and
A3: a<=b and
A4: c < d;
A5: a*c < a*d by A1,A4,Lm13;
  a*d<=b*d by A2,A3,A4,Lm12;
  hence thesis by A5,XXREAL_0:2;
end;

theorem
  0 < c & b < 0 & a < b implies c/b < c/a
proof
  assume that
A1: c>0 and
A2: b<0 and
A3: a<b;
  a">b" by A2,A3,Lm31;
  then a"*c>b"*c by A1,Lm13;
  then c/a>b"*c by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  c < 0 & 0 < a & a < b implies c/a < c/b
proof
  assume that
A1: c < 0 and
A2: a>0 and
A3: a<b;
  a">b" by A2,A3,Lm34;
  then a"*c < b"*c by A1,Lm24;
  then c/a<b"*c by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  c < 0 & b < 0 & a < b implies c/a < c/b
proof
  assume that
A1: c < 0 and
A2: b<0 and
A3: a<b;
  a">b" by A2,A3,Lm31;
  then a"*c < b"*c by A1,Lm24;
  then c/a<b"*c by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  0 < b & 0 < d & a*d <= c*b implies a/b <= c/d
proof
  assume that
A1: b>0 and
A2: d>0 and
A3: a*d<=c*b;
  a*d/b<=c by A1,A3,Th79;
  then a/b*d<=c by XCMPLX_1:74;
  hence thesis by A2,Th77;
end;

theorem
  b < 0 & d < 0 & a*d <= c*b implies a/b <= c/d
proof
  assume that
A1: b<0 and
A2: d<0 and
A3: a*d<=c*b;
  a*d/b>=c by A1,A3,Th80;
  then a/b*d>=c by XCMPLX_1:74;
  hence thesis by A2,Th80;
end;

theorem
  0 < b & d < 0 & a*d <= c*b implies c/d <= a/b
proof
  assume that
A1: b>0 and
A2: d<0 and
A3: a*d<=c*b;
  a*d/b<=c by A1,A3,Th79;
  then a/b*d<=c by XCMPLX_1:74;
  hence thesis by A2,Th78;
end;

theorem
  b < 0 & 0 < d & a*d <= c*b implies c/d <= a/b
proof
  assume that
A1: b<0 and
A2: d>0 and
A3: a*d<=c*b;
  a*d/b>=c by A1,A3,Th80;
  then a/b*d>=c by XCMPLX_1:74;
  hence thesis by A2,Th79;
end;

theorem
  0 < b & 0 < d & a*d < c*b implies a/b < c/d
proof
  assume that
A1: b>0 and
A2: d>0 and
A3: a*d<c*b;
  a*d/b<c by A1,A3,Th83;
  then a/b*d<c by XCMPLX_1:74;
  hence thesis by A2,Th81;
end;

theorem
  b < 0 & d < 0 & a*d < c*b implies a/b < c/d
proof
  assume that
A1: b<0 and
A2: d<0 and
A3: a*d<c*b;
  a*d/b>c by A1,A3,Th84;
  then a/b*d>c by XCMPLX_1:74;
  hence thesis by A2,Th84;
end;

theorem
  0 < b & d < 0 & a*d < c*b implies c/d < a/b
proof
  assume that
A1: b>0 and
A2: d<0 and
A3: a*d<c*b;
  a*d/b<c by A1,A3,Th83;
  then a/b*d<c by XCMPLX_1:74;
  hence thesis by A2,Th82;
end;

theorem
  b < 0 & 0 < d & a*d < c*b implies c/d < a/b
proof
  assume that
A1: b<0 and
A2: d>0 and
A3: a*d<c*b;
  a*d/b>c by A1,A3,Th84;
  then a/b*d>c by XCMPLX_1:74;
  hence thesis by A2,Th83;
end;

theorem
  b < 0 & d < 0 & a*b < c/d implies a*d < c/b
proof
  assume that
A1: b<0 and
A2: d<0;
  assume a*b<c/d;
  then a*b*d>c by A2,Th78;
  then a*d*b>c;
  hence thesis by A1,Th84;
end;

theorem
  0 < b & 0 < d & a*b < c/d implies a*d < c/b
proof
  assume that
A1: b>0 and
A2: d>0;
  assume a*b<c/d;
  then a*b*d<c by A2,Th79;
  then a*d*b<c;
  hence thesis by A1,Th81;
end;

theorem
  b < 0 & d < 0 & c/d < a*b implies c/b < a*d
proof
  assume that
A1: b<0 and
A2: d<0;
  assume a*b>c/d;
  then a*b*d<c by A2,Th80;
  then a*d*b<c;
  hence thesis by A1,Th82;
end;

theorem
  0 < b & 0 < d & c/d < a*b implies c/b < a*d
proof
  assume that
A1: b>0 and
A2: d>0;
  assume a*b>c/d;
  then a*b*d>c by A2,Th77;
  then a*d*b>c;
  hence thesis by A1,Th83;
end;

theorem
  b < 0 & 0 < d & a*b < c/d implies c/b < a*d
proof
  assume that
A1: b<0 and
A2: d>0;
  assume a*b<c/d;
  then a*b*d<c by A2,Th79;
  then a*d*b<c;
  hence thesis by A1,Th82;
end;

theorem
  0 < b & d < 0 & a*b < c/d implies c/b < a*d
proof
  assume that
A1: b>0 and
A2: d<0;
  assume a*b<c/d;
  then a*b*d>c by A2,Th78;
  then a*d*b>c;
  hence thesis by A1,Th83;
end;

theorem
  b < 0 & 0 < d & c/d < a*b implies a*d < c/b
proof
  assume that
A1: b<0 and
A2: d>0;
  assume a*b>c/d;
  then a*b*d>c by A2,Th77;
  then a*d*b>c;
  hence thesis by A1,Th84;
end;

theorem
  0 < b & d < 0 & c/d < a*b implies a*d < c/b
proof
  assume that
A1: b>0 and
A2: d<0;
  assume a*b>c/d;
  then a*b*d<c by A2,Th80;
  then a*d*b<c;
  hence thesis by A1,Th81;
end;

theorem
  0 < a & 0 <= c & a <= b implies c/b <= c/a
proof
  assume that
A1: 0<a and
A2: 0<=c and
A3: a<=b;
  a*b"<=b*b" by A1,A3,Lm12;
  then a*b"<=1 by A1,A3,XCMPLX_0:def 7;
  then a"*(a*b")<=a"*1 by A1,Lm12;
  then a"*a*b"<=a";
  then 1*b"<=a" by A1,XCMPLX_0:def 7;
  then c*b"<=c*a" by A2,Lm12;
  then c/b<=c*a" by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  0 <= c & b < 0 & a <= b implies c/b <= c/a
proof
  assume that
A1: c>=0 and
A2: b<0 and
A3: a<=b;
  a">=b" by A2,A3,Lm33;
  then a"*c>=b"*c by A1,Lm12;
  then c/a>=b"*c by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  c <= 0 & 0 < a & a <= b implies c/a <= c/b
proof
  assume
A1: c <= 0;
  assume that
A2: a>0 and
A3: a<=b;
  a">=b" by A2,A3,Lm32;
  then a"*c <= b"*c by A1,Lm28;
  then c/a<=b"*c by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  c <= 0 & b < 0 & a <= b implies c/a <= c/b
proof
  assume that
A1: c <= 0 and
A2: b<0 and
A3: a<=b;
  a">=b" by A2,A3,Lm33;
  then a"*c <= b"*c by A1,Lm28;
  then c/a<=b"*c by XCMPLX_0:def 9;
  hence thesis by XCMPLX_0:def 9;
end;

theorem
  0 < a iff 0 < a";

theorem
  a < 0 iff a" < 0;

theorem Th124:
  a < 0 & 0 < b implies a" < b"
proof
  assume that
A1: a<0 and
A2: b>0;
  a"<0 by A1;
  hence thesis by A2;
end;

theorem
  a" < 0 & 0 < b" implies a < b
proof
  assume that
A1: a"<0 and
A2: b">0;
  a""<b"" by A1,A2,Th124;
  hence thesis;
end;

begin

theorem
  a <= 0 & 0 <= a implies 0 = a*b by Lm35;

theorem
  0 <= a & 0 <= b implies 0 <= a*b;

theorem
  a <= 0 & b <= 0 implies 0 <= a*b;

theorem
  0 < a & 0 < b implies 0 < a*b;

theorem
  a < 0 & b < 0 implies 0 < a*b;

theorem
  0 <= a & b <= 0 implies a*b <= 0;

theorem
  0 < a & b < 0 implies a*b < 0;

theorem
  a*b<0 implies a>0 & b<0 or a<0 & b>0
proof
  assume
A1: a*b<0;
  then
A2: b <> 0;
  a <> 0 by A1;
  hence thesis by A1,A2;
end;

theorem
  a*b>0 implies a>0 & b>0 or a<0 & b<0
proof
  assume
A1: a*b>0;
  then
A2: b <> 0;
  a <> 0 by A1;
  hence thesis by A1,A2;
end;

theorem
  a <= 0 & b <= 0 implies 0 <= a/b;

theorem
  0 <= a & 0 <= b implies 0 <= a/b;

theorem
  0 <= a & b <= 0 implies a/b <= 0;

theorem
  a <= 0 & 0 <= b implies a/b <= 0;

theorem
  0 < a & 0 < b implies 0 < a/b;

theorem
  a < 0 & b < 0 implies 0 < a/b;

theorem
  a < 0 & 0 < b implies a/b < 0;

theorem
  a < 0 & 0 < b implies b/a < 0;

theorem
  a/b<0 implies b<0 & a>0 or b>0 & a<0
proof
  assume
A1: a/b<0;
  then
A2: a <> 0;
  a/b = a*b" by XCMPLX_0:def 9;
  then b" <> 0 by A1;
  hence thesis by A1,A2;
end;

theorem
  a/b>0 implies b>0 & a>0 or b<0 & a<0
proof
  assume
A1: a/b>0;
  then
A2: a <> 0;
  a/b = a*b" by XCMPLX_0:def 9;
  then b" <> 0 by A1;
  hence thesis by A1,A2;
end;

begin

theorem
  a <= b implies a < b+1
proof
  assume a<=b;
  then
A1: a-1<=b-1 by Lm7;
  b-1<b-1+1 by Lm9;
  then a-1<b by A1,XXREAL_0:2;
  then a-1+1<b+1 by Lm10;
  hence thesis;
end;

theorem
  a - 1 < a
proof
  a+- 1 < a + 0 by Lm10;
  hence thesis;
end;

theorem
  a <= b implies a-1 < b
proof
  assume a<=b;
  then
A1: a-1<=b-1 by Lm7;
  b-1<b-1+1 by Lm9;
  hence thesis by A1,XXREAL_0:2;
end;

theorem
  -1 < a implies 0 < 1+a
proof
  assume -1<a;
  then -1+1<a+1 by Lm8;
  hence thesis;
end;

theorem
  a<1 implies 1-a>0 by Lm21;

begin

theorem
  a <= 1 & 0 <= b & b <= 1 & a*b = 1 implies a=1
proof
  assume that
A1: a<=1 and
A2: 0<=b and
A3: b<=1 and
A4: a*b=1;
  now
    per cases by A2;
    case
      b=0;
      hence contradiction by A4;
    end;
    case
A5:   b>0;
      then a=b" by A4,XCMPLX_0:def 7;
      then a>=1" by A3,A5,Lm32;
      hence thesis by A1,XXREAL_0:1;
    end;
  end;
  hence thesis;
end;

theorem
  0 <= a & 1 <= b implies a <= a*b
proof
  assume that
A1: a>=0 and
A2: b>=1;
  a*b>=a*1 by A1,A2,Lm12;
  hence thesis;
end;

theorem
  a <= 0 & b <= 1 implies a <= a*b
proof
  assume that
A1: a<=0 and
A2: b<=1;
  a*b>=a*1 by A1,A2,Lm28;
  hence thesis;
end;

theorem
  0 <= a & b <= 1 implies a*b <= a
proof
  assume that
A1: a>=0 and
A2: b<=1;
  a*b<=a*1 by A1,A2,Lm12;
  hence thesis;
end;

theorem
  a <= 0 & 1 <= b implies a*b <= a
proof
  assume that
A1: a<=0 and
A2: b>=1;
  a*b<=a*1 by A1,A2,Lm28;
  hence thesis;
end;

theorem Th155:
  0 < a & 1 < b implies a < a*b
proof
  assume that
A1: a>0 and
A2: b>1;
  a*b>a*1 by A1,A2,Lm13;
  hence thesis;
end;

theorem
  a < 0 & b < 1 implies a < a*b
proof
  assume that
A1: a<0 and
A2: b<1;
  a*b>a*1 by A1,A2,Lm24;
  hence thesis;
end;

theorem
  0 < a & b < 1 implies a*b < a
proof
  assume that
A1: a>0 and
A2: b<1;
  a*b<a*1 by A1,A2,Lm13;
  hence thesis;
end;

theorem
  a < 0 & 1 < b implies a*b < a
proof
  assume that
A1: a<0 and
A2: b>1;
  a*b<a*1 by A1,A2,Lm24;
  hence thesis;
end;

theorem
  1 <= a & 1 <= b implies 1 <= a*b
proof
  assume that
A1: a>=1 and
A2: b>=1;
  a*b>=b*1 by A1,A2,Lm12;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  0 <= a & a <= 1 & b <= 1 implies a*b <= 1
proof
  assume that
A1: 0<=a and
A2: a<=1 and
A3: b<=1;
  a*b<=1*a by A1,A3,Lm12;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  1 < a & 1 <= b implies 1 < a*b
proof
  assume that
A1: a>1 and
A2: b>=1;
  a*b>b*1 by A1,A2,Lm13;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  0 <= a & a < 1 & b <= 1 implies a*b < 1
proof
  assume that
A1: 0<=a and
A2: a<1 and
A3: b<=1;
  a*b<=1*a by A1,A3,Lm12;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  a <= -1 & b <= -1 implies 1 <= a*b
proof
  assume that
A1: a<=-1 and
A2: b<=-1;
A3: -b>=--1 by A2,Lm14;
  a*b>=b*(-1) by A1,A2,Lm28;
  hence thesis by A3,XXREAL_0:2;
end;

theorem
  a < -1 & b <= -1 implies 1 < a*b
proof
  assume that
A1: a<-1 and
A2: b<=-1;
A3: -b>=--1 by A2,Lm14;
  a*b>b*(-1) by A1,A2,Lm24;
  hence thesis by A3,XXREAL_0:2;
end;

theorem
  a <= 0 & -1 <= a & -1 <= b implies a*b <= 1
proof
  assume that
A1: 0>=a and
A2: a>=-1 and
A3: b>=-1;
A4: -a<=--1 by A2,Lm14;
  a*b<=(-1)*a by A1,A3,Lm28;
  hence thesis by A4,XXREAL_0:2;
end;

theorem
  a <= 0 & -1 < a & -1 <= b implies a*b < 1
proof
  assume that
A1: 0>=a and
A2: a>-1 and
A3: b>=-1;
A4: -a<--1 by A2,Lm15;
  a*b<=(-1)*a by A1,A3,Lm28;
  hence thesis by A4,XXREAL_0:2;
end;

begin

theorem Th167:
  (for a st 1 < a holds c <= b*a) implies c <= b
proof
  assume
A1: for a st a>1 holds b*a>=c;
  assume
A2: not thesis;
A3: b>=0
  proof
A4: c <= b*2 by A1;
    assume b<0;
    then
A5: b*2<0;
    then c < 0 by A1;
    then b/c>c/c by A2,Lm29;
    then b/c>1 by A5,A4,XCMPLX_1:60;
    then
A6: b*(b/c)>=c by A1;
    b*(b/c)<c*(b/c) by A2,A5,A4,Lm13;
    then b*(b/c)<b by A5,A4,XCMPLX_1:87;
    hence contradiction by A2,A6,XXREAL_0:2;
  end;
  per cases by A3;
  suppose
A7: b>0;
    then b/b<c/b by A2,Lm26;
    then 1<c/b by A7,XCMPLX_1:60;
    then consider d being real number such that
A8: 1<d and
A9: d<c/b by Th5;
    b*d<b*(c/b) by A7,A9,Lm13;
    then b*d<c by A7,XCMPLX_1:87;
    hence contradiction by A1,A8;
  end;
  suppose
A10: b=0;
    b*2>=c by A1;
    hence contradiction by A2,A10;
  end;
end;

Lm36: 1 < a implies a" < 1
proof
  assume
A1: 1<a;
  then 1*a"<a*a" by Lm13;
  hence thesis by A1,XCMPLX_0:def 7;
end;

theorem
  (for a st 0 < a & a < 1 holds b*a <= c) implies b <= c
proof
  assume
A1: for a st 0<a & a<1 holds b*a<=c;
  now
    let d;
    assume
A2: d>1;
    then b*(d")<=c by A1,Lm36;
    then b/d<=c by XCMPLX_0:def 9;
    hence b<=c*d by A2,Th81;
  end;
  hence thesis by Th167;
end;

Lm37: a <= b & 0 <= a implies a/b <= 1
proof
  assume
A1: a <= b;
  assume
A2: 0 <= a;
  per cases by A2;
  suppose
    a = 0;
    hence thesis;
  end;
  suppose
A3: a > 0;
    then a/b<=b/b by A1,Lm25;
    hence thesis by A1,A3,XCMPLX_1:60;
  end;
end;

Lm38: b <= a & 0 <= a implies b/a <= 1
proof
  assume
A1: b <= a;
  assume
A2: a>=0;
  per cases by A2;
  suppose
    a = 0;
    then a" = 0;
    then b*a" < 1;
    hence thesis by XCMPLX_0:def 9;
  end;
  suppose
A3: a > 0;
    assume b/a>1;
    then b/a*a>1*a by A3,Lm13;
    hence thesis by A1,A3,XCMPLX_1:87;
  end;
end;

theorem
  (for a st 0 < a & a < 1 holds b <= a*c) implies b <= 0
proof
  assume that
A1: for a st 0 < a & a < 1 holds b <= a*c and
A2: b > 0;
A3: b*2 > b by A2,Th155;
  then
A4: b > b/2 by Th83;
  per cases;
  suppose
    c <= 0;
    then 1/2*c <= 0;
    hence contradiction by A1,A2;
  end;
  suppose that
A5: c <= b and
A6: c > 0;
    set a = c/(2*b);
    c/b*2 > c/b by A2,A6,Th155;
    then c/b > c/b/2 by Th83;
    then
A7: c/b > c/(b*2) by XCMPLX_1:78;
    c/b <= 1 by A5,A6,Lm37;
    then a < 1 by A7,XXREAL_0:2;
    then
A8: a*c >= b by A1,A2,A6;
    per cases;
    suppose
      c >= b;
      then b = c by A5,XXREAL_0:1;
      then a*c = b/2 by A6,XCMPLX_1:92;
      hence contradiction by A2,A8,Th83,Th155;
    end;
    suppose
A9:   c < b;
      then a*c < c/(2*b)*b by A6,Th98;
      then
A10:  a*c < c/2 by A2,XCMPLX_1:92;
      c/2 < b/2 by A9,Lm26;
      then a*c < b/2 by A10,XXREAL_0:2;
      hence contradiction by A4,A8,XXREAL_0:2;
    end;
  end;
  suppose that
A11: b <= c and
A12: c > 0;
    set a = b/(2*c);
    b/c*2 > b/c by A2,A12,Th155;
    then b/c > b/c/2 by Th83;
    then
A13: b/c > b/(c*2) by XCMPLX_1:78;
    b/c <= 1 by A11,A12,Lm38;
    then a < 1 by A13,XXREAL_0:2;
    then
A14: a*c >= b by A1,A2,A12;
    a*c = b/2 by A12,XCMPLX_1:92;
    hence contradiction by A3,A14,Th83;
  end;
end;

theorem
  0 <= d & d <= 1 & 0 <= a & 0 <= b & d*a+(1-d)*b=0 implies d=0 & b=0 or
  d=1 & a=0 or a=0 & b=0
proof
  assume that
A1: 0<=d and
A2: d<=1 and
A3: a>=0 and
A4: b>=0 and
A5: d*a+(1-d)*b=0;
  d-d<=1-d by A2,Lm7;
  then 1-d=0 or b=0 by A1,A3,A4,A5;
  hence thesis by A5;
end;

theorem
  0 <= d & a <= b implies a <= (1-d)*a+d*b
proof
  assume that
A1: 0<=d and
A2: a<=b;
  d*a<=d*b by A1,A2,Lm12;
  then (1-d)*a+d*a<=(1-d)*a+d*b by Lm6;
  hence thesis;
end;

theorem
  d <= 1 & a <= b implies (1-d)*a+d*b <= b
proof
  assume that
A1: d<=1 and
A2: a<=b;
  1-d>=0 by A1,Th48;
  then (1-d)*a<=(1-d)*b by A2,Lm12;
  then (1-d)*a+d*b<=(1-d)*b+d*b by Lm6;
  hence thesis;
end;

theorem
  0 <= d & d <= 1 & a <= b & a <= c implies a <= (1-d)*b+d*c
proof
  assume that
A1: 0<=d and
A2: d<=1 and
A3: a<=b and
A4: a<=c;
  1-d>=0 by A2,Th48;
  then
A5: (1-d)*a<=(1-d)*b by A3,Lm12;
A6: (1-d)*a+d*a = a;
  d*a<=d*c by A1,A4,Lm12;
  hence thesis by A5,A6,Lm6;
end;

theorem
  0 <= d & d <= 1 & b <= a & c <= a implies (1-d)*b+d*c <= a
proof
  assume that
A1: 0<=d and
A2: d<=1 and
A3: a>=b and
A4: a>=c;
  1-d>=0 by A2,Th48;
  then
A5: (1-d)*a>=(1-d)*b by A3,Lm12;
A6: (1-d)*a+d*a = a;
  d*a>=d*c by A1,A4,Lm12;
  hence thesis by A5,A6,Lm6;
end;

theorem
  0 <= d & d <= 1 & a < b & a < c implies a < (1-d)*b+d*c
proof
  assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a<b and
A4: a<c;
  per cases;
  suppose
    d=0;
    hence thesis by A3;
  end;
  suppose
    d=1;
    hence thesis by A4;
  end;
  suppose
A5: not(d=0 or d=1);
    then d<1 by A2,XXREAL_0:1;
    then 1-d>0 by Lm21;
    then
A6: (1-d)*a<(1-d)*b by A3,Lm13;
A7: (1-d)*a+d*a=a;
    d*a<d*c by A1,A4,A5,Lm13;
    hence thesis by A6,A7,Lm8;
  end;
end;

theorem
  0 <= d & d <= 1 & b < a & c < a implies (1-d)*b+d*c < a
proof
  assume that
A1: 0 <= d and
A2: d <= 1 and
A3: a>b and
A4: a>c;
  per cases;
  suppose
    d=0;
    hence thesis by A3;
  end;
  suppose
    d=1;
    hence thesis by A4;
  end;
  suppose
A5: not(d=0 or d=1);
    then d<1 by A2,XXREAL_0:1;
    then 1-d>0 by Lm21;
    then
A6: (1-d)*a>(1-d)*b by A3,Lm13;
A7: (1-d)*a+d*a=a;
    d*a>d*c by A1,A4,A5,Lm13;
    hence thesis by A6,A7,Lm8;
  end;
end;

theorem
  0 < d & d < 1 & a <= b & a < c implies a < (1-d)*b+d*c
proof
  assume that
A1: 0 < d and
A2: d < 1 and
A3: a <= b and
A4: a < c;
  1-d > 0 by A2,Lm21;
  then
A5: (1-d)*a <= (1-d)*b by A3,Lm12;
A6: (1-d)*a+d*a = a;
  d*a < d*c by A1,A4,Lm13;
  hence thesis by A5,A6,Lm8;
end;

theorem
  0 < d & d < 1 & b < a & c <= a implies (1-d)*b+d*c < a
proof
  assume that
A1: 0 < d and
A2: d < 1 and
A3: a > b and
A4: a >= c;
  1-d > 0 by A2,Lm21;
  then
A5: (1-d)*a > (1-d)*b by A3,Lm13;
A6: (1-d)*a+d*a = a;
  d*a >= d*c by A1,A4,Lm12;
  hence thesis by A5,A6,Lm8;
end;

theorem
  0 <= d & d <= 1 & a <= (1-d)*a+d*b & b < (1-d)*a+d*b implies d = 0
proof
  assume that
A1: d >= 0 and
A2: d <= 1 and
A3: a <= (1-d)*a + d*b and
A4: b < (1-d)*a + d*b;
  set s = (1-d)*a + d*b;
  assume d <> 0;
  then
A5: d*b < d*s by A1,A4,Lm13;
  1-d >= 0 by A2,Th48;
  then
A6: (1-d)*a <= (1-d)*s by A3,Lm12;
  1*s = (1-d)*s + d*s;
  hence contradiction by A5,A6,Lm8;
end;

theorem
  0 <= d & d <= 1 & (1-d)*a+d*b <= a & (1-d)*a+d*b < b implies d = 0
proof
  assume that
A1: d >= 0 and
A2: d <= 1 and
A3: a >= (1-d)*a + d*b and
A4: b > (1-d)*a + d*b;
  set s = (1-d)*a + d*b;
  assume d <> 0;
  then
A5: d*b > d*s by A1,A4,Lm13;
  1-d >= 0 by A2,Th48;
  then
A6: (1-d)*a >= (1-d)*s by A3,Lm12;
  1*s = (1-d)*s + d*s;
  hence contradiction by A5,A6,Lm8;
end;

begin

theorem
  0 < a & a <= b implies 1 <= b/a
proof
  assume that
A1: 0<a and
A2: a<=b;
  b/a>=a/a by A1,A2,Lm25;
  hence thesis by A1,XCMPLX_1:60;
end;

theorem
  a < 0 & b <= a implies 1 <= b/a
proof
  assume that
A1: a < 0 and
A2: b<=a;
  b/a>=a/a by A1,A2,Lm30;
  hence thesis by A1,XCMPLX_1:60;
end;

theorem
  0 <= a & a <= b implies a/b <= 1 by Lm37;

theorem
  b <= a & a <= 0 implies a/b <= 1
proof
  assume
A1: b <= a;
  assume
A2: a <= 0;
  per cases by A2;
  suppose
    a = 0;
    hence thesis;
  end;
  suppose
A3: a < 0;
    then a/b<=b/b by A1,Lm30;
    hence thesis by A1,A3,XCMPLX_1:60;
  end;
end;

theorem
  0 <= a & b <= a implies b/a <= 1 by Lm38;

theorem
  a <= 0 & a <= b implies b/a <= 1
proof
  assume
A1: a<=0;
  per cases by A1;
  suppose
    a = 0;
    then a" = 0;
    then b*a" = 0;
    hence thesis by XCMPLX_0:def 9;
  end;
  suppose
A2: a<0;
    assume
A3: a <= b;
    assume b/a>1;
    then b/a*a<1*a by A2,Lm24;
    hence thesis by A2,A3,XCMPLX_1:87;
  end;
end;

theorem
  0 < a & a < b implies 1 < b/a
proof
  assume
A1: a>0;
  assume
A2: a < b;
  assume b/a<=1;
  then b/a*a<=1*a by A1,Lm12;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  a < 0 & b < a implies 1 < b/a
proof
  assume that
A1: a < 0 and
A2: b<a;
  b/a>a/a by A1,A2,Lm29;
  hence thesis by A1,XCMPLX_1:60;
end;

theorem
  0 <= a & a < b implies a/b < 1
proof
  assume that
A1: 0 <= a and
A2: a < b;
  a/b<b/b by A1,A2,Lm26;
  hence thesis by A1,A2,XCMPLX_1:60;
end;

theorem
  a <= 0 & b < a implies a/b < 1
proof
  assume that
A1: a <= 0 and
A2: b<a;
  a/b<b/b by A1,A2,Lm29;
  hence thesis by A1,A2,XCMPLX_1:60;
end;

theorem
  0 < a & b < a implies b/a < 1
proof
  assume
A1: a > 0;
  assume
A2: b < a;
  assume b/a>=1;
  then b/a*a>=1*a by A1,Lm12;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  a < 0 & a < b implies b/a < 1
proof
  assume
A1: a<0;
  assume
A2: a < b;
  assume b/a>=1;
  then b/a*a<=1*a by A1,Lm28;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

begin

theorem
  0 <= b & -b <= a implies -1 <= a/b
proof
  assume
A1: b>=0;
  per cases by A1;
  suppose
    b = 0;
    then b" = 0;
    then a*b" = 0;
    hence thesis by XCMPLX_0:def 9;
  end;
  suppose
A2: b>0;
    assume
A3: -b <= a;
    assume a/b<-1;
    then a/b*b<(-1)*b by A2,Lm13;
    hence thesis by A2,A3,XCMPLX_1:87;
  end;
end;

theorem
  0 <= b & -a <= b implies -1 <= a/b
proof
  assume
A1: b >= 0;
  per cases by A1;
  suppose
    b = 0;
    then b" = 0;
    then a*b" = 0;
    hence thesis by XCMPLX_0:def 9;
  end;
  suppose
A2: b > 0;
    assume
A3: -a <= b;
    assume a/b<-1;
    then a/b*b<(-1)*b by A2,Lm13;
    then a<-b by A2,XCMPLX_1:87;
    hence thesis by A3,Th26;
  end;
end;

theorem
  b <= 0 & a <= -b implies -1 <= a/b
proof
  assume
A1: b<=0;
  per cases by A1;
  suppose
    b=0;
    then b" =0;
    then a*b" = 0;
    hence thesis by XCMPLX_0:def 9;
  end;
  suppose
A2: b < 0;
    assume
A3: a <= -b;
    assume a/b<-1;
    then a/b*b>(-1)*b by A2,Lm24;
    hence thesis by A2,A3,XCMPLX_1:87;
  end;
end;

theorem
  b <= 0 & b <= -a implies -1 <= a/b
proof
  assume
A1: b<=0;
  per cases by A1;
  suppose
    b = 0;
    then b" =0;
    then a*b" = 0;
    hence thesis by XCMPLX_0:def 9;
  end;
  suppose
A2: b < 0;
    assume
A3: b <= -a;
    assume a/b<-1;
    then a/b*b>(-1)*b by A2,Lm24;
    then a>-b by A2,XCMPLX_1:87;
    hence thesis by A3,Th25;
  end;
end;

theorem
  0 < b & -b < a implies -1 < a/b
proof
  assume
A1: b>0;
  assume
A2: -b < a;
  assume a/b<=-1;
  then a/b*b<=(-1)*b by A1,Lm12;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  0 < b & -a < b implies -1 < a/b
proof
  assume
A1: b>0;
  assume
A2: -a < b;
  assume a/b<=-1;
  then a/b*b<=(-1)*b by A1,Lm12;
  then a<=-b by A1,XCMPLX_1:87;
  hence thesis by A2,Th25;
end;

theorem
  b < 0 & a < -b implies -1 < a/b
proof
  assume
A1: b<0;
  assume
A2: a < -b;
  assume a/b<=-1;
  then a/b*b>=(-1)*b by A1,Lm28;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  b < 0 & b < -a implies -1 < a/b
proof
  assume
A1: b<0;
  assume
A2: b < -a;
  assume a/b<=-1;
  then a/b*b>=(-1)*b by A1,Lm28;
  then a>=-b by A1,XCMPLX_1:87;
  hence thesis by A2,Th26;
end;

theorem
  0 < b & a <= -b implies a/b <= -1
proof
  assume
A1: b>0;
  assume
A2: a <= -b;
  assume a/b>-1;
  then a/b*b>(-1)*b by A1,Lm13;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  0 < b & b <= -a implies a/b <= -1
proof
  assume
A1: b>0;
  assume
A2: b <= -a;
  assume a/b>-1;
  then a/b*b>(-1)*b by A1,Lm13;
  then a>-b by A1,XCMPLX_1:87;
  hence thesis by A2,Th25;
end;

theorem
  b < 0 & -b <= a implies a/b <= -1
proof
  assume
A1: b<0;
  assume
A2: -b <= a;
  assume a/b>-1;
  then a/b*b<(-1)*b by A1,Lm24;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  b < 0 & -a <= b implies a/b <= -1
proof
  assume
A1: b<0;
  assume
A2: -a <= b;
  assume a/b>-1;
  then a/b*b<(-1)*b by A1,Lm24;
  then a<-b by A1,XCMPLX_1:87;
  hence thesis by A2,Th26;
end;

theorem
  0 < b & a < -b implies a/b < -1
proof
  assume
A1: b>0;
  assume
A2: a < -b;
  assume a/b>=-1;
  then a/b*b>=(-1)*b by A1,Lm12;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  0 < b & b < -a implies a/b < -1
proof
  assume
A1: b>0;
  assume
A2: b < -a;
  assume a/b>=-1;
  then a/b*b>=(-1)*b by A1,Lm12;
  then a>=-b by A1,XCMPLX_1:87;
  hence thesis by A2,Th26;
end;

theorem
  b < 0 & -b < a implies a/b < -1
proof
  assume
A1: b<0;
  assume
A2: -b < a;
  assume a/b>=-1;
  then a/b*b<=(-1)*b by A1,Lm28;
  hence thesis by A1,A2,XCMPLX_1:87;
end;

theorem
  b < 0 & -a < b implies a/b < -1
proof
  assume
A1: b<0;
  assume
A2: -a < b;
  assume a/b>=-1;
  then a/b*b<=(-1)*b by A1,Lm28;
  then a<=-b by A1,XCMPLX_1:87;
  hence thesis by A2,Th25;
end;

begin

theorem Th209:
  (for a being real number st 0 < a & a < 1 holds c <= b/a)
  implies c <= b
proof
  assume
A1: for a st a>0 & a<1 holds b/a>=c;
  now
    let d;
    assume d>1;
    then
A2: b/(d")>=c by A1,Lm36;
    d" = 1/d by XCMPLX_1:215;
    then b*d/1>=c by A2,XCMPLX_1:77;
    hence b*d>=c;
  end;
  hence thesis by Th167;
end;

theorem
  (for a being real number st 1 < a holds b/a <= c) implies b <= c
proof
  (for a st a>1 holds b/a<=c) implies b<=c
  proof
    assume
A1: for a st a>1 holds b/a<=c;
    now
      let d;
A2:   d" = 1/d by XCMPLX_1:215;
      assume that
A3:   0<d and
A4:   d<1;
      d">1" by A3,A4,Lm34;
      then b/(d")<=c by A1;
      then b*d/1<=c by A2,XCMPLX_1:77;
      hence b<=c/d by A3,Th77;
    end;
    hence thesis by Th209;
  end;
  hence thesis;
end;

theorem
  1 <= a implies a" <= 1
proof
  1 <= a implies a" <= 1" by Lm32;
  hence thesis;
end;

theorem
  1 < a implies a" < 1 by Lm36;

theorem
  a <= -1 implies -1 <= a"
proof
  a <= -1 implies (-1)" <= a" by Lm33;
  hence thesis;
end;

theorem
  a < -1 implies -1 < a"
proof
  a < -1 implies (-1)" < a" by Lm31;
  hence thesis;
end;

begin

theorem
  0 < a implies 0 < a/2;

theorem
  0 < a implies a/2 < a by Lm27;

theorem
  a <= 1/2 implies 2 * a - 1 <= 0
proof
  assume a <= 1/2;
  then 2 * a <= 2 * (1/2) by Lm12;
  then 2 * a <= 1 + 0;
  hence thesis by Lm18;
end;

theorem
  a <= 1/2 implies 0 <= 1 - 2 * a
proof
  assume a <= 1/2;
  then 2 * a <= 2 * (1/2) by Lm12;
  then 2 * a + 0 <= 1;
  hence thesis by Lm16;
end;

theorem
  a >= 1/2 implies 2 * a - 1 >= 0
proof
  assume a >= 1/2;
  then 2 * a >= 2 * (1/2) by Lm12;
  then 2 * a >= 1 + 0;
  hence thesis by Lm16;
end;

theorem
  a >= 1/2 implies 0 >= 1 - 2 * a
proof
  assume a >= 1/2;
  then 2 * a >= 2 * (1/2) by Lm12;
  then 2 * a + 0 >= 1;
  hence thesis by Lm18;
end;

begin

theorem
  0 < a implies a/3 < a
proof
  assume
A1: 0<a;
  then
A2: a/3+a/3+0<a/3+a/3+a/3 by Lm10;
  0+a/3<a/3+a/3 by A1,Lm10;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  0 < a implies 0 < a/3;

begin

theorem
  0 < a implies a/4 < a
proof
  assume
A1: 0<a;
  then
A2: 0+a/4<a/4+a/4 by Lm10;
  then a/4< a/4+a/4+a/4 by A1,Lm10;
  then a/4+a/4<a/4+a/4+a/4+a/4 by Lm10;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  0 < a implies 0 < a/4;

theorem
  for a,b st b<>0 ex c st a=b/c
proof
  let a,b;
  assume
A1: b<>0;
  then consider c being complex number such that
A2: a=b/c by XCMPLX_1:232;
  per cases;
  suppose
    c = 0;
    hence thesis by A2;
  end;
  suppose
    c <> 0;
    then c = b/a by A1,A2,XCMPLX_1:54;
    then reconsider c as real number;
    take c;
    thus thesis by A2;
  end;
end;

begin :: Addenda

:: from TOPREAL3, 2006.07.15, A.T.

theorem
  r<s implies r < (r+s)/2 & (r+s)/2 < s
proof
  assume r<s;
  then
A1: r/2 < s/2 by Lm26;
  then r/2 + r/2 < r/2 + s/2 by Lm10;
  hence r < (r+s)/2;
  r/2 + s/2 < s/2 + s/2 by A1,Lm10;
  hence thesis;
end;

:: missing, 2007.01.16, A.T.

registration
  cluster -> ext-real for Element of REAL;
  coherence;
end;

reserve p,q,r,s,t for ext-real number;

theorem Th227:
  r < t implies ex s st r < s & s < t
proof
  assume
A1: r < t;
  then
A2: r <> +infty by XXREAL_0:3;
A3: t <> -infty by A1,XXREAL_0:5;
  per cases by A2,A3,XXREAL_0:14;
  suppose that
A4: r = -infty and
A5: t = +infty;
    take 0;
    thus thesis by A4,A5;
  end;
  suppose that
A6: r = -infty and
A7: t in REAL;
    reconsider t as real number by A7;
    consider s being real number such that
A8: s < t by Th2;
    take s;
    s in REAL by XREAL_0:def 1;
    hence r < s by A6,XXREAL_0:12;
    thus thesis by A8;
  end;
  suppose that
A9: r in REAL and
A10: t = +infty;
    reconsider r9 = r as real number by A9;
    consider s being real number such that
A11: r9 < s by Th1;
    take s;
    thus r < s by A11;
    s in REAL by XREAL_0:def 1;
    hence thesis by A10,XXREAL_0:9;
  end;
  suppose that
A12: r in REAL and
A13: t in REAL;
    reconsider r,t as real number by A12,A13;
    consider s being real number such that
A14: r < s and
A15: s < t by A1,Th5;
    take s;
    thus thesis by A14,A15;
  end;
end;

theorem
  r < s & (for q st r < q & q < s holds t <= q) implies t <= r
proof
  assume that
A1: r < s and
A2: for q st r < q & q < s holds t <= q;
  for q st r < q holds t <= q
  proof
    let q such that
A3: r < q;
    per cases;
    suppose
      q < s;
      hence thesis by A2,A3;
    end;
    suppose
A4:   s <= q;
      consider p such that
A5:   r < p and
A6:   p < s by A1,Th227;
      t <= p by A2,A5,A6;
      then t <= s by A6,XXREAL_0:2;
      hence thesis by A4,XXREAL_0:2;
    end;
  end;
  hence thesis by Th227;
end;

theorem
  r < s & (for q st r < q & q < s holds q <= t) implies s <= t
proof
  assume that
A1: r < s and
A2: for q st r < q & q < s holds q <= t;
  for q st t < q holds s <= q
  proof
    let q such that
A3: t < q and
A4: q < s;
    per cases;
    suppose
      r < q;
      hence thesis by A2,A3,A4;
    end;
    suppose
A5:   q <= r;
      consider p such that
A6:   r < p and
A7:   p < s by A1,Th227;
      p <= t by A2,A6,A7;
      then r <= t by A6,XXREAL_0:2;
      hence thesis by A3,A5,XXREAL_0:2;
    end;
  end;
  hence thesis by Th227;
end;

:: missing, 2008.08.13, A.T.

theorem
  0 <= a & b <= c implies b-a <= c
proof
  assume that
A1: 0 <= a and
A2: b <= c;
  b+0 <= a+c by A1,A2,Th38;
  hence thesis by Lm18;
end;

theorem
  0 < a & b <= c implies b-a < c
proof
  assume that
A1: 0 < a and
A2: b <= c;
  b+0 < a+c by A1,A2,Th39;
  hence thesis by Lm17;
end;

begin

theorem
  a -' a = 0
proof
  a-a = 0;
  hence thesis by XREAL_0:def 2;
end;

theorem Th233:
  b <= a implies a -' b = a - b
proof
  assume a >= b;
  then a - b >= 0 by Th48;
  hence thesis by XREAL_0:def 2;
end;

theorem
  c <= a & c <= b & a -' c = b -' c implies a = b
proof
  assume that
A1: a >= c and
A2: b >= c and
A3: a -' c = b -' c;
  a - c >= 0 by A1,Th48;
  then
A4: a -' c = a - c by XREAL_0:def 2;
  b - c >= 0 by A2,Th48;
  then a + (-c) = b + (-c) by A3,A4,XREAL_0:def 2;
  hence thesis;
end;

theorem
  a >= b implies a -' b + b = a
proof
  assume a >= b;
  then a - b = a -' b by Th233;
  hence thesis;
end;

:: from LEXBFS, 2008.08.23, A.T.

theorem
  a <= b & c < a implies b -' a < b -' c
proof
  assume that
A1: a <= b and
A2: c < a;
A3: b - a < b - c by A2,Th15;
  b -' c = b - c by A1,A2,Th233,XXREAL_0:2;
  hence thesis by A1,A3,Th233;
end;

:: missing, 2010.05.18, A.T.

theorem
 1 <= a implies a -' 1 < a
 proof
  assume 1 <= a;
   then a -' 1 = a - 1 by Th233;
  hence a -' 1 < a by Th44;
 end;