The abstract of the Mizar article:

Introduction to Arithmetic of Real Numbers

by

Library Committee

Received February 11, 2003

MML identifier: XREAL_0

[ Mizar article, MML identifier index ]

environ

 vocabulary XREAL_0, ARYTM_2, BOOLE, ARYTM_1, ARYTM_3, ORDINAL2, ARYTM,
      RELAT_1, ASYMPT_0, ZF_LANG, XCMPLX_0, COMPLEX1, FUNCOP_1, OPPCAT_1,
      ORDINAL1;
 notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_4, ORDINAL1, ORDINAL2,
      ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0;
 constructors ARYTM_1, ARYTM_0, ORDINAL2, XCMPLX_0, FUNCT_4, XBOOLE_0, TARSKI;
 clusters ARYTM_2, NUMBERS, ARYTM_3, ORDINAL2, SUBSET_1, XBOOLE_0, XCMPLX_0,
      ZFMISC_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin

definition let r be number;
  attr r is real means
:: XREAL_0:def 1
    r in REAL;
end;

definition
  cluster natural -> real number;
  cluster real -> complex number;
end;

definition
  cluster real number;
end;

definition let x,y be real number;
  pred x <= y means
:: XREAL_0:def 2
   ex x',y' being Element of REAL+ st x = x' & y = y' & x' <=' y'
              if x in REAL+ & y in REAL+,
  ex x',y' being Element of REAL+ st x = [0,x'] & y = [0,y'] & y' <=' x'
              if x in [:{0},REAL+:] & y in [:{0},REAL+:]
  otherwise y in REAL+ & x in [:{0},REAL+:];
  reflexivity;
  connectedness;
  synonym y >= x;
  antonym y < x;
  antonym x > y;
end;

definition let x be real number;
  attr x is positive means
:: XREAL_0:def 3
     x > 0;
  attr x is negative means
:: XREAL_0:def 4
     x < 0;
end;

definition let x be real number;
  cluster -x -> real;
  cluster x" -> real;
  let y be real number;
  cluster x + y -> real;
  cluster x * y -> real;
end;

definition let x,y be real number;
  cluster x-y -> real;
  cluster x/y -> real;
end;

begin

 reserve r,s,t for real number;

definition
 cluster positive -> non negative non zero (real number);
 cluster non negative non zero -> positive (real number);
 cluster negative -> non positive non zero (real number);
 cluster non positive non zero -> negative (real number);
 cluster zero -> non negative non positive (real number);
 cluster non negative non positive -> zero (real number);
end;

definition
 cluster positive (real number);
 cluster negative (real number);
 cluster zero (real number);
end;

definition let r,s be non negative (real number);
 cluster r + s -> non negative;
end;

definition let r,s be non positive (real number);
 cluster r + s -> non positive;
end;

definition let r be positive (real number);
 let s be non negative (real number);
 cluster r + s -> positive;
 cluster s + r -> positive;
end;

definition let r be negative (real number);
 let s be non positive (real number);
 cluster r + s -> negative;
 cluster s + r -> negative;
end;

definition let r be non positive (real number);
 cluster -r -> non negative;
end;

definition let r be non negative (real number);
 cluster -r -> non positive;
end;

definition
 let r be non negative (real number),
     s be non positive (real number);
 cluster r - s -> non negative;
 cluster s - r -> non positive;
end;

definition let r be positive (real number);
 let s be non positive (real number);
 cluster r - s -> positive;
 cluster s - r -> negative;
end;

definition let r be negative (real number);
 let s be non negative (real number);
 cluster r - s -> negative;
 cluster s - r -> positive;
end;

definition
 let r be non positive (real number),
     s be non negative (real number);
 cluster r*s -> non positive;
 cluster s*r -> non positive;
end;

definition
 let r,s be non positive (real number);
 cluster r*s -> non negative;
end;

definition let r,s be non negative (real number);
 cluster r*s -> non negative;
end;

definition let r be non positive (real number);
 cluster r" -> non positive;
end;

definition let r be non negative (real number);
 cluster r" -> non negative;
end;

definition
 let r be non negative (real number),
     s be non positive (real number);
 cluster r/s -> non positive;
 cluster s/r -> non positive;
end;

definition let r,s be non negative (real number);
 cluster r/s -> non negative;
end;

definition
 let r,s be non positive (real number);
 cluster r/s -> non negative;
end;