REAL_1

:: Basic Properties of Real Numbers
::  by Krzysztof Hryniewiecki
::
:: Received January 8, 1989
:: Copyright (c) 1990-2026 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;  :: redefines - (XCMPLX_0, definition)
  coherence by XREAL_0:def 1;
  redefine func x" -> Element of REAL;  :: redefines " (XCMPLX_0, definition)
  coherence by XREAL_0:def 1;
end;

definition
  let x, y be Element of REAL;
  redefine func x+y -> Element of REAL;  :: redefines + (XCMPLX_0, definition)
  coherence by XREAL_0:def 1;
  redefine func x*y -> Element of REAL;  :: redefines * (XCMPLX_0, definition)
  coherence by XREAL_0:def 1;
  redefine func x-y -> Element of REAL;  :: redefines - (XCMPLX_0, definition)
  coherence by XREAL_0:def 1;
  redefine func x/y -> Element of REAL;  :: redefines / (XCMPLX_0, definition)
  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;