:: Basic Properties of Real Numbers
:: by Krzysztof Hryniewiecki
::
:: Received January 8, 1989
:: Copyright (c) 1990-2016 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;