:: Basic Properties of Real Numbers :: by Krzysztof Hryniewiecki :: :: Received January 8, 1989 :: Copyright (c) 1990-2018 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 NUMBERS, XREAL_0, SUBSET_1, XXREAL_0, ARYTM_1, RELAT_1, ARYTM_3, REAL_1, ARYTM_2, CARD_1, TARSKI, ZFMISC_1; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0; constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, ARYTM_2, ARYTM_1; registrations XREAL_0, ORDINAL1; requirements REAL, SUBSET, BOOLE, NUMERALS, ARITHM; definitions TARSKI, XBOOLE_0; equalities ORDINAL1; expansions TARSKI; theorems XREAL_0, XBOOLE_0, ARYTM_0, ARYTM_1, ARYTM_2, XXREAL_0, NUMBERS; begin registration cluster -> real for Element of REAL; coherence; end; registration cluster positive for Real; existence proof take 1/1; thus thesis; end; end; registration cluster positive for Element of REAL; existence proof reconsider j = 1 as Element of REAL by NUMBERS:19; take j; thus thesis; end; end; definition let x be Element of REAL; redefine func -x -> Element of REAL; coherence by XREAL_0:def 1; redefine func x" -> Element of REAL; coherence by XREAL_0:def 1; end; definition let x, y be Element of REAL; redefine func x+y -> Element of REAL; coherence by XREAL_0:def 1; redefine func x*y -> Element of REAL; coherence by XREAL_0:def 1; redefine func x-y -> Element of REAL; coherence by XREAL_0:def 1; redefine func x/y -> Element of REAL; coherence by XREAL_0:def 1; end; :: 2011.05.09, A.T reserve s,t for Element of RAT+; theorem REAL+ = { r where r is Real: 0 <= r} proof set RP = { r where r is Real: 0 <= r}; thus REAL+ c= RP proof let e be object; assume A1: e in REAL+; then reconsider r = e as Real by ARYTM_0:1; reconsider o = 0, s = r as Element of REAL+ by A1,ARYTM_2:20; o <=' s by ARYTM_1:6; then 0 <= r by ARYTM_2:20,XXREAL_0:def 5; hence e in RP; end; let e be object; assume e in RP; then A2: ex r being Real st e = r & 0 <= r; not 0 in [:{0},REAL+:] by ARYTM_0:5,ARYTM_2:20,XBOOLE_0:3; hence e in REAL+ by A2,XXREAL_0:def 5; end;