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