Addenda , 1998

University of Bialystok

Copyright (c) 1998 Association of Mizar Users

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

Back to top