Volume 1, 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

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

Back to top