:: Basic Properties of Real Numbers - Requirements
::  by Library Committee
::
:: Received February 27, 2003
:: Copyright (c) 2003-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 XREAL_0, ORDINAL1, XXREAL_0, NUMBERS, ARYTM_2, SUBSET_1, ARYTM_3,
      ZFMISC_1, CARD_1, XCMPLX_0;
 notations TARSKI, ZFMISC_1, SUBSET_1, ARYTM_2, ORDINAL1, NUMBERS, XXREAL_0,
      XREAL_0;
 constructors ARYTM_2, NUMBERS, XXREAL_0, XREAL_0;
 registrations ARYTM_2, XREAL_0, ORDINAL1, XBOOLE_0;
 requirements SUBSET, BOOLE;
 theorems XBOOLE_0, ZFMISC_1, ARYTM_0, ARYTM_1, XREAL_0, NUMBERS, XXREAL_0,
      XTUPLE_0;

begin

:: This file contains statements which are obvious for Mizar checker if
:: "requirements REAL" is included in the environment description of an article.
:: They are published for testing purposes only.
:: Users should use appropriate requirements instead of referencing
:: to these theorems.
:: Note that the checker needs also "requirements BOOLE" to accept
:: the statements with attribute 'zero'.

reserve x, y, z for real number;

Lm1: x <= y & y <= x implies x = y
proof
  assume that
A1: x <= y and
A2: y <= x;
A3: x in REAL & y in REAL by XREAL_0:def 1;
  per cases by A3,NUMBERS:def 1,XBOOLE_0:def 3;
  suppose
    x in REAL+ & y in REAL+;
    then
    (ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & x9 <=' y9 )& ex
y99, x99 being Element of REAL+ st y = y99 & x = x99 & y99 <=' x99 by A1,A2,
XXREAL_0:def 5;
    hence thesis by ARYTM_1:4;
  end;
  suppose
A4: x in REAL+ & y in [:{0},REAL+:];
    then
    ( not(x in REAL+ & y in REAL+))& not(x in [:{0},REAL+:] & y in [:{0},
    REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
    hence thesis by A1,A4,XXREAL_0:def 5;
  end;
  suppose
A5: y in REAL+ & x in [:{0},REAL+:];
    then
    ( not(x in REAL+ & y in REAL+))& not(x in [:{0},REAL+:] & y in [:{0},
    REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
    hence thesis by A2,A5,XXREAL_0:def 5;
  end;
  suppose that
A6: x in [:{0},REAL+:] & y in [:{0},REAL+:];
    consider x9,y9 being Element of REAL+ such that
A7: x = [0,x9] & y = [0,y9] and
A8: y9 <=' x9 by A1,A6,XXREAL_0:def 5;
    consider y99,x99 being Element of REAL+ such that
A9: y = [0,y99] & x = [0,x99] and
A10: x99 <=' y99 by A2,A6,XXREAL_0:def 5;
    x9 = x99 & y9 = y99 by A7,A9,XTUPLE_0:1;
    hence thesis by A8,A9,A10,ARYTM_1:4;
  end;
end;

Lm2: x <= y & y <= z implies x <= z
proof
  assume that
A1: x <= y and
A2: y <= z;
A3: x in REAL & y in REAL by XREAL_0:def 1;
A4: z in REAL by XREAL_0:def 1;
  per cases by A3,A4,NUMBERS:def 1,XBOOLE_0:def 3;
  suppose that
A5: x in REAL+ and
A6: y in REAL+ and
A7: z in REAL+;
    consider y99,z9 being Element of REAL+ such that
A8: y = y99 and
A9: z = z9 and
A10: y99 <=' z9 by A2,A6,A7,XXREAL_0:def 5;
    consider x9,y9 being Element of REAL+ such that
A11: x = x9 and
A12: y = y9 & x9 <=' y9 by A1,A5,A6,XXREAL_0:def 5;
    x9 <=' z9 by A12,A8,A10,ARYTM_1:3;
    hence thesis by A11,A9,XXREAL_0:def 5;
  end;
  suppose
A13: x in REAL+ & y in [:{0},REAL+:];
    then
    ( not(x in REAL+ & y in REAL+))& not(x in [:{0},REAL+:] & y in [:{0},
    REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
    hence thesis by A1,A13,XXREAL_0:def 5;
  end;
  suppose
A14: y in REAL+ & z in [:{0},REAL+:];
    then
    ( not(z in REAL+ & y in REAL+))& not(z in [:{0},REAL+:] & y in [:{0},
    REAL+:]) by ARYTM_0:5,XBOOLE_0:3;
    hence thesis by A2,A14,XXREAL_0:def 5;
  end;
  suppose that
A15: x in [:{0},REAL+:] and
A16: z in REAL+;
    ( not(x in REAL+ & z in REAL+))& not(x in [:{0},REAL+:] & z in [:{0},
    REAL+:]) by A15,A16,ARYTM_0:5,XBOOLE_0:3;
    hence thesis by A16,XXREAL_0:def 5;
  end;
  suppose that
A17: x in [:{0},REAL+:] and
A18: y in [:{0},REAL+:] and
A19: z in [:{0},REAL+:];
    consider y99,z9 being Element of REAL+ such that
A20: y = [0,y99] and
A21: z = [0,z9] and
A22: z9 <=' y99 by A2,A18,A19,XXREAL_0:def 5;
    consider x9,y9 being Element of REAL+ such that
A23: x = [0,x9] and
A24: y = [0,y9] and
A25: y9 <=' x9 by A1,A17,A18,XXREAL_0:def 5;
    y9 = y99 by A24,A20,XTUPLE_0:1;
    then z9 <=' x9 by A25,A22,ARYTM_1:3;
    hence thesis by A17,A19,A23,A21,XXREAL_0:def 5;
  end;
end;

theorem
  x <= y & x is positive implies y is positive
proof
  assume that
A1: x <= y and
A2: x is positive;
  x > 0 by A2,XXREAL_0:def 6;
  then y > 0 by A1,Lm2;
  hence thesis by XXREAL_0:def 6;
end;

theorem
  x <= y & y is negative implies x is negative
proof
  assume that
A1: x <= y and
A2: y is negative;
  y < 0 by A2,XXREAL_0:def 7;
  then x < 0 by A1,Lm2;
  hence thesis by XXREAL_0:def 7;
end;

theorem
  x <= y & x is non negative implies y is non negative
proof
  assume that
A1: x <= y and
A2: x is non negative and
A3: y is negative;
  y < 0 by A3,XXREAL_0:def 7;
  then x < 0 by A1,Lm2;
  hence thesis by A2,XXREAL_0:def 7;
end;

theorem
  x <= y & y is non positive implies x is non positive
proof
  assume that
A1: x <= y and
A2: y is non positive and
A3: x is positive;
  x > 0 by A3,XXREAL_0:def 6;
  then y > 0 by A1,Lm2;
  hence thesis by A2,XXREAL_0:def 6;
end;

theorem
  x <= y & y is non zero & x is non negative implies y is positive
proof
  assume that
A1: x <= y and
A2: y is non zero and
A3: x is non negative and
A4: y is non positive;
  y <= 0 by A4,XXREAL_0:def 6;
  then
A5: y < 0 by A2,Lm1;
  x >= 0 by A3,XXREAL_0:def 7;
  hence thesis by A1,A5,Lm2;
end;

theorem
  x <= y & x is non zero & y is non positive implies x is negative
proof
  assume that
A1: x <= y and
A2: x is non zero and
A3: y is non positive and
A4: x is non negative;
  x >= 0 by A4,XXREAL_0:def 7;
  then
A5: x > 0 by A2,Lm1;
  y <= 0 by A3,XXREAL_0:def 6;
  hence thesis by A1,A5,Lm2;
end;

theorem
  not x <= y & x is non positive implies y is negative
proof
  assume that
A1: x > y and
A2: x is non positive & y is non negative;
  x <= 0 & y >= 0 by A2,XXREAL_0:def 6,def 7;
  hence thesis by A1,Lm2;
end;

theorem
  not x <= y & y is non negative implies x is positive
proof
  assume that
A1: x > y and
A2: y is non negative & x is non positive;
  x <= 0 & y >= 0 by A2,XXREAL_0:def 6,def 7;
  hence thesis by A1,Lm2;
end;
 
::theorem
::  numeral(X) & X <> 0 implies X is positive;