:: Non negative real numbers. Part II
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-2012 Association of Mizar Users


begin

theorem Th1: :: ARYTM_1:1
for x, y being Element of REAL+ st x + y = y holds
x = {}
proofend;

reconsider u = one as Element of REAL+ by ARYTM_2:20;

Lm1:  for x, y, z being Element of REAL+ st x *' y = x *' z &amp; x <> {} holds
y = z
proofend;

theorem :: ARYTM_1:2
for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )
proofend;

theorem Th3: :: ARYTM_1:3
for x, y, z being Element of REAL+ st x <=' y &amp; y <=' z holds
x <=' z
proofend;

theorem Th4: :: ARYTM_1:4
for x, y being Element of REAL+ st x <=' y &amp; y <=' x holds
x = y
proofend;

theorem Th5: :: ARYTM_1:5
for x, y being Element of REAL+ st x <=' y &amp; y = {} holds
x = {}
proofend;

theorem Th6: :: ARYTM_1:6
for x, y being Element of REAL+ st x = {} holds
x <=' y
proofend;

theorem Th7: :: ARYTM_1:7
for x, y, z being Element of REAL+ holds
( x <=' y iff x + z <=' y + z )
proofend;

theorem Th8: :: ARYTM_1:8
for x, y, z being Element of REAL+ st x <=' y holds
x *' z <=' y *' z
proofend;

Lm2:  for x, y, z being Element of REAL+ st x *' y <=' x *' z &amp; x <> {} holds
y <=' z
proofend;

definition
let x, y be Element of REAL+ ;
funcx -' y ->  Element of REAL+  means :Def1: :: ARYTM_1:def 1
it + y = x if y <=' x
otherwise it = {} ;
existence
 ( ( y <=' x implies ex b1 being Element of REAL+ st b1 + y = x ) &amp; ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) )
proofend;
correctness
consistency
for b1 being Element of REAL+ holds verum;
uniqueness
for b1, b2 being Element of REAL+ holds
( ( y <=' x &amp; b1 + y = x &amp; b2 + y = x implies b1 = b2 ) &amp; ( not y <=' x &amp; b1 = {} &amp; b2 = {} implies b1 = b2 ) );
by ARYTM_2:11;
end;

:: deftheorem Def1 defines -' ARYTM_1:def_1_:_
 for x, y, b3 being Element of REAL+ holds
( ( y <=' x implies ( b3 = x -' y iff b3 + y = x ) ) &amp; ( not y <=' x implies ( b3 = x -' y iff b3 = {} ) ) );

Lm3:  for x being Element of REAL+ holds x -' x = {}
proofend;

theorem Th9: :: ARYTM_1:9
for x, y being Element of REAL+ holds
( x <=' y or x -' y <> {} )
proofend;

theorem :: ARYTM_1:10
for x, y being Element of REAL+ st x <=' y &amp; y -' x = {} holds
x = y
proofend;

theorem Th11: :: ARYTM_1:11
for x, y being Element of REAL+ holds x -' y <=' x
proofend;

Lm4:  for x, y being Element of REAL+ st x = {} holds
y -' x = y
proofend;

Lm5:  for x, y being Element of REAL+ holds (x + y) -' y = x
proofend;

Lm6:  for x, y being Element of REAL+ st x <=' y holds
y -' (y -' x) = x
proofend;

Lm7:  for z, y, x being Element of REAL+ holds
( z -' y <=' x iff z <=' x + y )
proofend;

Lm8:  for y, x, z being Element of REAL+ st y <=' x holds
( z + y <=' x iff z <=' x -' y )
proofend;

Lm9:  for z, y, x being Element of REAL+ holds (z -' y) -' x = z -' (x + y)
proofend;

Lm10:  for y, z, x being Element of REAL+ holds (y -' z) -' x = (y -' x) -' z
proofend;

theorem :: ARYTM_1:12
for y, x, z being Element of REAL+ st y <=' x &amp; y <=' z holds
x + (z -' y) = (x -' y) + z
proofend;

theorem Th13: :: ARYTM_1:13
for z, y, x being Element of REAL+ st z <=' y holds
x + (y -' z) = (x + y) -' z
proofend;

Lm11:  for y, z, x being Element of REAL+ st y <=' z holds
x -' (z -' y) = (x + y) -' z
proofend;

Lm12:  for z, x, y being Element of REAL+ st z <=' x &amp; y <=' z holds
x -' (z -' y) = (x -' z) + y
proofend;

Lm13:  for x, z, y being Element of REAL+ st x <=' z &amp; y <=' z holds
x -' (z -' y) = y -' (z -' x)
proofend;

theorem :: ARYTM_1:14
for z, x, y being Element of REAL+ st z <=' x &amp; y <=' z holds
(x -' z) + y = x -' (z -' y)
proofend;

theorem :: ARYTM_1:15
for y, x, z being Element of REAL+ st y <=' x &amp; y <=' z holds
(z -' y) + x = (x -' y) + z
proofend;

theorem :: ARYTM_1:16
for x, y, z being Element of REAL+ st x <=' y holds
z -' y <=' z -' x
proofend;

theorem :: ARYTM_1:17
for x, y, z being Element of REAL+ st x <=' y holds
x -' z <=' y -' z
proofend;

Lm14:  for x, y, z being Element of REAL+ holds x *' (y -' z) = (x *' y) -' (x *' z)
proofend;

definition
let x, y be Element of REAL+ ;
funcx - y ->  set  equals :Def2: :: ARYTM_1:def 2
x -' y if y <=' x
otherwise [{},(y -' x)];
correctness
coherence
( ( y <=' x implies x -' y is set ) &amp; ( not y <=' x implies [{},(y -' x)] is set ) );
consistency
for b1 being set holds verum;
;
end;

:: deftheorem Def2 defines - ARYTM_1:def_2_:_
 for x, y being Element of REAL+ holds
( ( y <=' x implies x - y = x -' y ) &amp; ( not y <=' x implies x - y = [{},(y -' x)] ) );

theorem :: ARYTM_1:18
for x being Element of REAL+ holds x - x = {}
proofend;

theorem :: ARYTM_1:19
for x, y being Element of REAL+ st x = {} &amp; y <> {} holds
x - y = [{},y]
proofend;

theorem :: ARYTM_1:20
for z, y, x being Element of REAL+ st z <=' y holds
x + (y -' z) = (x + y) - z
proofend;

theorem :: ARYTM_1:21
for z, y, x being Element of REAL+ st not z <=' y holds
x - (z -' y) = (x + y) - z
proofend;

theorem :: ARYTM_1:22
for y, x, z being Element of REAL+ st y <=' x &amp; not y <=' z holds
x - (y -' z) = (x -' y) + z
proofend;

theorem :: ARYTM_1:23
for y, x, z being Element of REAL+ st not y <=' x &amp; not y <=' z holds
x - (y -' z) = z - (y -' x)
proofend;

theorem :: ARYTM_1:24
for y, x, z being Element of REAL+ st y <=' x holds
x - (y + z) = (x -' y) - z
proofend;

theorem :: ARYTM_1:25
for x, y, z being Element of REAL+ st x <=' y &amp; z <=' y holds
(y -' z) - x = (y -' x) - z
proofend;

theorem :: ARYTM_1:26
for z, y, x being Element of REAL+ st z <=' y holds
x *' (y -' z) = (x *' y) - (x *' z)
proofend;

theorem Th27: :: ARYTM_1:27
for z, y, x being Element of REAL+ st not z <=' y &amp; x <> {} holds
[{},(x *' (z -' y))] = (x *' y) - (x *' z)
proofend;

theorem :: ARYTM_1:28
for y, z, x being Element of REAL+ st y -' z <> {} &amp; z <=' y &amp; x <> {} holds
(x *' z) - (x *' y) = [{},(x *' (y -' z))]
proofend;