Journal of Formalized Mathematics
EMM, 2003
University of Bialystok
Copyright (c) 2003 Association of Mizar Users

### Introduction to Arithmetic of Real Numbers

by
Library Committee

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;

```