The abstract of the Mizar article:

Basic Properties of Real Numbers

by

Krzysztof Hryniewiecki

Received January 8, 1989

MML identifier: REAL_1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM, ARYTM_1, RELAT_1, ARYTM_3;
 notation TARSKI, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0;
 constructors ARYTM_0, XREAL_0, XCMPLX_0, XBOOLE_0;
 clusters NUMBERS, XREAL_0, ARYTM_3, ZFMISC_1, XBOOLE_0;
 requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM;


begin

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

definition
 cluster -> real Element of REAL;
end;

definition
  mode Real is Element of REAL;
end;

definition let x be Real;
  redefine func -x -> Real;
  redefine func x" -> Real;
end;

definition let x,y be Real;
  redefine func x+y -> Real;
  redefine func x*y -> Real;
  redefine func x-y -> Real;
  redefine func x/y -> Real;
end;

canceled 24;

theorem :: REAL_1:25
    x-0=x;

theorem :: REAL_1:26
    -0=0;

canceled 22;

theorem :: REAL_1:49
  x <= y implies x - z <= y - z;

theorem :: REAL_1:50
  x<=y iff -y<=-x;

canceled;

theorem :: REAL_1:52
  x<=y & z<=0 implies y*z<=x*z;

theorem :: REAL_1:53
  x+z<=y+z implies x <= y;

theorem :: REAL_1:54
    x-z<=y-z implies x <= y;

theorem :: REAL_1:55
  x<=y & z<=t implies x+z<=y+t;

definition let y,x be real number;
  redefine canceled 4;

pred x<y means
:: REAL_1:def 5
x<=y & x<>y;
end;

canceled 10;

theorem :: REAL_1:66
    x < 0 iff 0 < -x;

theorem :: REAL_1:67
  x<y & z<=t implies x+z<y+t;

canceled;

theorem :: REAL_1:69
    0<x implies y<y+x;

theorem :: REAL_1:70
  0<z & x<y implies x*z<y*z;

theorem :: REAL_1:71
  z<0 & x<y implies y*z<x*z;

theorem :: REAL_1:72
  0<z implies 0<z";

theorem :: REAL_1:73
  0<z implies (x<y iff x/z<y/z);

theorem :: REAL_1:74
    z<0 implies (x<y iff y/z<x/z);

:: REAL is dense

theorem :: REAL_1:75
    x<y implies ex z st x<z & z<y;

:: REAL is unlimited

theorem :: REAL_1:76
    for x ex y st x<y;

theorem :: REAL_1:77
    for x ex y st y<x;

:: Continuity of REAL

scheme SepReal { P[Real]}:
   ex X being Subset of REAL st
     for x being Real holds x in X iff P[x];

canceled 6;

theorem :: REAL_1:84
  x+y <= z iff x <= z-y;

canceled;

theorem :: REAL_1:86
    x <= y+z iff x-y <= z;

canceled 5;

theorem :: REAL_1:92
    (x <= y & z <= t implies x - t <= y - z) &
  (x < y & z <= t or x <= y & z < t implies x-t < y-z);

theorem :: REAL_1:93
    0 <= x*x;