:: Non negative real numbers. Part II
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-2019 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_2, ARYTM_3, XBOOLE_0, ARYTM_1;
notations TARSKI, SUBSET_1, ARYTM_3, ARYTM_2;
constructors ARYTM_2;
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 -> set 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)];