:: Non negative real numbers. Part II
:: by Andrzej Trybulec
::
:: Received March 7, 1998
:: Copyright (c) 1998-2018 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 b₁ being Element of REAL+ st b₁ + y = x ) & ( not y <=' x implies ex b₁ being Element of REAL+ st b₁ = {} ) )

proof end;

correctness
consistency
for b₁ being Element of REAL+ holds verum;
uniqueness
for b₁, b₂ being Element of REAL+ holds
( ( y <=' x & b₁ + y = x & b₂ + y = x implies b₁ = b₂ ) & ( not y <=' x & b₁ = {} & b₂ = {} implies b₁ = b₂ ) );
by ARYTM_2:11;

end;

:: deftheorem Def1 defines -' ARYTM_1:def 1 :
for x, y, b₃ being Element of REAL+ holds
( ( y <=' x implies ( b₃ = x -' y iff b₃ + y = x ) ) & ( not y <=' x implies ( b₃ = x -' y iff b₃ = {} ) ) );

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 b₁ 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;