:: Strong arithmetic of real numbers
:: by Andrzej Trybulec
::
:: Received January 1, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_2, SUBSET_1, ARYTM_3, ZFMISC_1, CARD_1, XXREAL_0, NUMBERS,
ARYTM_0, FUNCOP_1, XBOOLE_0, TARSKI, NAT_1, REAL_1, ORDINAL1;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, FUNCT_4, ARYTM_2,
NUMBERS, ARYTM_0, XCMPLX_0, XREAL_0, XXREAL_0;
constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0, XREAL_0;
registrations ORDINAL1, ARYTM_2, XREAL_0;
requirements SUBSET, BOOLE, NUMERALS;
begin
reserve r,s for Real;
reserve x,y,z for Real;
reserve r,r1,r2 for Element of REAL+;
theorem :: AXIOMS:1
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;
theorem :: AXIOMS:2
x in NAT & y in NAT implies x + y in NAT;
theorem :: AXIOMS:3
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:4
for k being natural Number holds k = { i where i is Nat: i < k };