Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Basic Properties of Real Numbers

by
Krzysztof Hryniewiecki

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;
```