:: Non negative real numbers. Part I
::  by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-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 SUBSET_1, ARYTM_3, SETFAM_1, XBOOLE_0, TARSKI, ZFMISC_1,
      ORDINAL1, ORDINAL2, ARYTM_2, CARD_1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1, ORDINAL2,
      ARYTM_3;
 constructors ARYTM_3, ORDINAL3;
 registrations XBOOLE_0, SUBSET_1, ORDINAL1, ARYTM_3, ORDINAL2, ORDINAL3;
 requirements BOOLE, SUBSET, NUMERALS;


begin

reserve r,s,t,x9,y9,z9,p,q for Element of RAT+;

definition
  func DEDEKIND_CUTS -> Subset-Family of RAT+ equals
:: ARYTM_2:def 1
  { A where A is Subset of
RAT+: r in A implies (for s st s <=' r holds s in A) & ex s st s in A & r < s }
  \ { RAT+};
end;

registration
  cluster DEDEKIND_CUTS -> non empty;
end;

definition
  func REAL+ -> set equals
:: ARYTM_2:def 2
  RAT+ \/ DEDEKIND_CUTS \ {{ s: s < t}: t <> {}};
end;

reserve x,y,z for Element of REAL+;

theorem :: ARYTM_2:1
  RAT+ c= REAL+;

theorem :: ARYTM_2:2
  omega c= REAL+;

registration
  cluster REAL+ -> non empty;
end;

definition
  let x;
  func DEDEKIND_CUT x -> Element of DEDEKIND_CUTS means
:: ARYTM_2:def 3

  ex r st x = r & it = { s : s < r } if x in RAT+ otherwise it = x;
end;

theorem :: ARYTM_2:3
  not ex y being object st [{},y] in REAL+;

definition
  let x be Element of DEDEKIND_CUTS;
  func GLUED x -> Element of REAL+ means
:: ARYTM_2:def 4

  ex r st it = r & for s holds s
  in x iff s < r if ex r st for s holds s in x iff s < r otherwise it = x;
end;

definition
  let x,y be Element of REAL+;
  pred x <=' y means
:: ARYTM_2:def 5

  ex x9,y9 st x = x9 & y = y9 & x9 <=' y9 if x in
  RAT+ & y in RAT+, x in y if x in RAT+ & not y in RAT+, not y in x if not x in
  RAT+ & y in RAT+ otherwise x c= y;
  connectedness;
end;

notation
  let x,y be Element of REAL+;
  antonym y < x for x <=' y;
end;

definition
  let A,B be Element of DEDEKIND_CUTS;
  func A + B -> Element of DEDEKIND_CUTS equals
:: ARYTM_2:def 6

  { r + s : r in A & s in
  B};
  commutativity;
end;

definition
  let A,B be Element of DEDEKIND_CUTS;
  func A *' B -> Element of DEDEKIND_CUTS equals
:: ARYTM_2:def 7
  { r *' s : r in A & s in B};
  commutativity;
end;

definition
  let x,y be Element of REAL+;
  func x + y -> Element of REAL+ equals
:: ARYTM_2:def 8

  x if y = {}, y if x = {}
  otherwise GLUED(DEDEKIND_CUT x + DEDEKIND_CUT y);
  commutativity;
  func x *' y -> Element of REAL+ equals
:: ARYTM_2:def 9
  GLUED(DEDEKIND_CUT x *' DEDEKIND_CUT
  y);
  commutativity;
end;

theorem :: ARYTM_2:4
  x = {} implies x *' y = {};

theorem :: ARYTM_2:5
  x + y = {} implies x = {};

theorem :: ARYTM_2:6
  x + (y + z) = (x + y) + z;

theorem :: ARYTM_2:7
  { A where A is Subset of RAT+: r in A implies (for s st s <=' r holds
  s in A) & ex s st s in A & r < s} is c=-linear;

theorem :: ARYTM_2:8
  for X,Y being Subset of REAL+ st (ex x st x in Y) & 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 :: ARYTM_2:9
  x <=' y implies ex z st x + z = y;

theorem :: ARYTM_2:10
  ex z st x + z = y or y + z = x;

theorem :: ARYTM_2:11
  x + y = x + z implies y = z;

theorem :: ARYTM_2:12
  x *' (y *' z) = x *' y *' z;

theorem :: ARYTM_2:13
  x *' (y + z) = (x *' y) + (x *' z);

theorem :: ARYTM_2:14
  x <> {} implies ex y st x *' y = one;

theorem :: ARYTM_2:15
  x = one implies x *' y = y;

theorem :: ARYTM_2:16
  x in omega & y in omega implies y + x in omega;

theorem :: ARYTM_2:17
  for A being Subset of REAL+ st 0 in A & for x,y st x in A & y = one
  holds x + y in A holds omega c= A;

theorem :: ARYTM_2:18
  for x st x in omega holds for y holds y in x iff y in omega & y <> x &
  y <=' x;

theorem :: ARYTM_2:19
  x = y + z implies z <=' x;

theorem :: ARYTM_2:20
  {} in REAL+ & one in REAL+;

theorem :: ARYTM_2:21
  x in RAT+ & y in RAT+ implies ex x9,y9 st x = x9 & y = y9 & x *' y = x9 *' y9
;