:: Introduction to Arithmetic of Real Numbers :: by Library Committee :: :: Received February 11, 2003 :: Copyright (c) 2003-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 ORDINAL1, NUMBERS, XXREAL_0, CARD_1, XCMPLX_0, SUBSET_1, ARYTM_0, FUNCOP_1, ARYTM_1, ARYTM_3, RELAT_1, ARYTM_2, ZFMISC_1, XBOOLE_0, XREAL_0, FUNCT_7, REAL_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_4, ORDINAL1, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0, XCMPLX_0, XXREAL_0; constructors FUNCT_4, ARYTM_1, ARYTM_0, XCMPLX_0, XXREAL_0; registrations ARYTM_2, NUMBERS, XCMPLX_0, XXREAL_0, ORDINAL1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; begin definition let r be object; attr r is real means :: XREAL_0:def 1 r in REAL; end; registration cluster -> real for Element of REAL; end; registration cluster -infty -> non real; cluster +infty -> non real; end; registration cluster natural -> real for object; cluster real -> complex for object; end; registration cluster real for object; cluster real for number; cluster real -> ext-real for object; end; definition mode Real is real Number; end; registration let x be Real; cluster -x -> real; cluster x" -> real; let y be Real; cluster x + y -> real; cluster x * y -> real; end; registration let x,y be Real; cluster x-y -> real; cluster x/y -> real; end; begin reserve r,s,t for Real; registration cluster positive for Real; cluster negative for Real; cluster zero for Real; end; registration let r,s be non negative Real; cluster r + s -> non negative; end; registration let r,s be non positive Real; cluster r + s -> non positive; end; registration let r be positive Real; let s be non negative Real; cluster r + s -> positive; cluster s + r -> positive; end; registration let r be negative Real; let s be non positive Real; cluster r + s -> negative; cluster s + r -> negative; end; registration let r be non positive Real; cluster -r -> non negative; end; registration let r be non negative Real; cluster -r -> non positive; end; registration let r be non negative Real, s be non positive Real; cluster r - s -> non negative; cluster s - r -> non positive; end; registration let r be positive Real; let s be non positive Real; cluster r - s -> positive; cluster s - r -> negative; end; registration let r be negative Real; let s be non negative Real; cluster r - s -> negative; cluster s - r -> positive; end; registration let r be non positive Real, s be non negative Real; cluster r*s -> non positive; cluster s*r -> non positive; end; registration let r,s be non positive Real; cluster r*s -> non negative; end; registration let r,s be non negative Real; cluster r*s -> non negative; end; registration let r be positive Real; cluster r" -> positive; end; registration let r be non positive Real; cluster r" -> non positive; end; registration let r be negative Real; cluster r" -> negative; end; registration let r be non negative Real; cluster r" -> non negative; end; registration let r be non negative Real, s be non positive Real; cluster r/s -> non positive; cluster s/r -> non positive; end; registration let r,s be non negative Real; cluster r/s -> non negative; end; registration let r,s be non positive Real; cluster r/s -> non negative; end; begin :: min & max registration let r,s be Real; cluster min(r,s) -> real; cluster max(r,s) -> real; end; definition let r,s be Real; func r -' s -> set equals :: XREAL_0:def 2 r - s if r -s >= 0 otherwise 0; end; registration let r,s be Real; cluster r -' s -> real; end; registration let r,s be Real; cluster r -' s -> non negative for Real; end; registration sethood of Real; end; :: 16.04.20121, A.T. registration let i be Real; reduce In(i,REAL) to i; end;