Journal of Formalized Mathematics
University of Bialystok
Copyright (c) 1998 Association of Mizar Users

### Non-Negative Real Numbers. Part II

by
Andrzej Trybulec

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)];

```