Addenda , 1989

University of Bialystok

Copyright (c) 1989 Association of Mizar Users

### The abstract of the Mizar article:

### Strong Arithmetic of Real Numbers

**by****Andrzej Trybulec**- Received January 1, 1989
- MML identifier: AXIOMS

- [ Mizar article, MML identifier index ]

environ vocabulary BOOLE, ARYTM, ARYTM_2, ARYTM_3, ORDINAL2, ARYTM_1, ORDINAL1, COMPLEX1, OPPCAT_1, RELAT_1, FUNCOP_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ORDINAL2, FUNCT_4, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0; constructors ARYTM_1, ARYTM_0, XREAL_0, XCMPLX_0, FUNCT_4, XBOOLE_0; clusters XREAL_0, ARYTM_2, ARYTM_3, ORDINAL2, NUMBERS, XCMPLX_0, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE, NUMERALS, ARITHM; begin reserve x,y,z for real number, k for natural number, i for Element of NAT; canceled 18; theorem :: AXIOMS:19 ex y st x + y = 0; theorem :: AXIOMS:20 x <> 0 implies ex y st x * y = 1; theorem :: AXIOMS:21 x <= y & y <= x implies x = y; theorem :: AXIOMS:22 x <= y & y <= z implies x <= z; canceled; theorem :: AXIOMS:24 x <= y implies x + z <= y + z; theorem :: AXIOMS:25 x <= y & 0 <= z implies x * z <= y * z; reserve r,r1,r2 for Element of REAL+; theorem :: AXIOMS:26 for X,Y being Subset of REAL st for x,y st x in X & y in Y holds x <= y ex z st for x,y st x in X & y in Y holds x <= z & z <= y; canceled; theorem :: AXIOMS:28 x in NAT & y in NAT implies x + y in NAT; theorem :: AXIOMS:29 for A being Subset of REAL st 0 in A & for x st x in A holds x + 1 in A holds NAT c= A; theorem :: AXIOMS:30 k = { i: i < k };

Back to top