The abstract of the Mizar article:

Non-Negative Real Numbers. Part II

by

Andrzej Trybulec

Received March 7, 1998

MML identifier: ARYTM_1

[ Mizar article, MML identifier index ]

environ

 vocabulary ARYTM_2, BOOLE, ORDINAL2, ARYTM_3, ARYTM_1;
 notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL2, ARYTM_2;
 constructors ARYTM_2, XBOOLE_0;
 clusters ZFMISC_1, XBOOLE_0;
 requirements SUBSET;


begin

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

theorem :: ARYTM_1:1
 x + y = y implies x = {};

theorem :: ARYTM_1:2
   x *' y = {} implies x = {} or y = {};

theorem :: ARYTM_1:3
 x <=' y & y <=' z implies x <=' z;

theorem :: ARYTM_1:4
 x <=' y & y <=' x implies x = y;

theorem :: ARYTM_1:5
 x <=' y & y = {} implies x = {};

theorem :: ARYTM_1:6
 x = {} implies x <=' y;

theorem :: ARYTM_1:7
 x <=' y iff x + z <=' y + z;

theorem :: ARYTM_1:8
 x <=' y implies x *' z <=' y *' z;

definition let x,y be Element of REAL+;
 func x -' y -> Element of REAL+ means
:: ARYTM_1:def 1
 it + y = x if y <=' x
  otherwise it = {};
end;

theorem :: ARYTM_1:9
 x <=' y or x -' y <> {};

theorem :: ARYTM_1:10
   x <=' y & y -' x = {} implies x = y;

theorem :: ARYTM_1:11
 x -' y <=' x;

theorem :: ARYTM_1:12
   y <=' x & y <=' z implies x + (z -' y) = x -' y + z;

theorem :: ARYTM_1:13
 z <=' y implies x + (y -' z) = x + y -' z;

theorem :: ARYTM_1:14
   z <=' x & y <=' z implies x -' z + y = x -' (z -' y);

theorem :: ARYTM_1:15
   y <=' x & y <=' z implies z -' y + x = x -' y + z;

theorem :: ARYTM_1:16
   x <=' y implies z -' y <=' z -' x;

theorem :: ARYTM_1:17
   x <=' y implies x -' z <=' y -' z;

definition let x,y be Element of REAL+;
 func x - y equals
:: ARYTM_1:def 2

  x -' y if y <=' x
  otherwise [{},y -' x];
end;

theorem :: ARYTM_1:18
   x - x = {};

theorem :: ARYTM_1:19
   x = {} & y <> {} implies x - y = [{},y];

theorem :: ARYTM_1:20
   z <=' y implies x + (y -' z) = x + y - z;

theorem :: ARYTM_1:21
   not z <=' y implies x - (z -' y) = x + y - z;

theorem :: ARYTM_1:22
   y <=' x & not y <=' z implies x - (y -' z) = x -' y + z;

theorem :: ARYTM_1:23
   not y <=' x & not y <=' z implies x - (y -' z) = z - (y -' x);

theorem :: ARYTM_1:24
   y <=' x implies x - (y + z) = x -' y - z;

theorem :: ARYTM_1:25
   x <=' y & z <=' y implies y -' z - x = y -' x - z;

theorem :: ARYTM_1:26
   z <=' y implies x *' (y -' z) = (x *' y) - (x *' z);

theorem :: ARYTM_1:27
 not z <=' y & x <> {} implies [{},x *' (z -' y)] = (x *' y) - (x *' z);

theorem :: ARYTM_1:28
   y -' z <> {} & z <=' y & x <> {} implies
      (x *' z) - (x *' y) = [{},x *' (y -' z)];