:: Non negative real numbers. Part II
:: by Andrzej Trybulec
::
:: Copyright (c) 1998-2021 Association of Mizar Users

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

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

proof end;

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

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

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

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

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

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

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

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

proof end;

definition
let x, y be Element of REAL+ ;
func x -' 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 ) & ( not y <=' x implies ex b1 being Element of REAL+ st b1 = {} ) )
proof end;
correctness
consistency
for b1 being Element of REAL+ holds verum
;
uniqueness
for b1, b2 being Element of REAL+ holds
( ( y <=' x & b1 + y = x & b2 + y = x implies b1 = b2 ) & ( not y <=' x & b1 = {} & 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 ) ) & ( not y <=' x implies ( b3 = x -' y iff b3 = {} ) ) );

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

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

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

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

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

proof end;

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

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

proof end;

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

proof end;

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

proof end;

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

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

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

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

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

proof end;

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

proof end;

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

proof end;

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

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

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

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

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

definition
let x, y be Element of REAL+ ;
func x - 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 ) & ( not y <=' x implies [{},(y -' x)] is set ) )
;
consistency
for b1 being set holds verum
;
by TARSKI:1;
end;

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

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

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

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

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

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

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

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

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

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

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

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