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

### Strong Arithmetic of Real Numbers

by
Andrzej Trybulec

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