:: Non negative real numbers. Part I
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-2017 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
;