:: by Andrzej Trybulec

::

:: Received March 7, 1998

:: Copyright (c) 1998-2017 Association of Mizar Users

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 & x <> {} holds

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+ ;

( ( y <=' x implies ex b_{1} being Element of REAL+ st b_{1} + y = x ) & ( not y <=' x implies ex b_{1} being Element of REAL+ st b_{1} = {} ) )

consistency

for b_{1} being Element of REAL+ holds verum;

uniqueness

for b_{1}, b_{2} being Element of REAL+ holds

( ( y <=' x & b_{1} + y = x & b_{2} + y = x implies b_{1} = b_{2} ) & ( not y <=' x & b_{1} = {} & b_{2} = {} implies b_{1} = b_{2} ) );

by ARYTM_2:11;

end;
func x -' y -> Element of REAL+ means :Def1: :: ARYTM_1:def 1

it + y = x if y <=' x

otherwise it = {} ;

existence it + y = x if y <=' x

otherwise it = {} ;

( ( y <=' x implies ex b

proof end;

correctness consistency

for b

uniqueness

for b

( ( y <=' x & b

by ARYTM_2:11;

:: deftheorem Def1 defines -' ARYTM_1:def 1 :

for x, y, b_{3} being Element of REAL+ holds

( ( y <=' x implies ( b_{3} = x -' y iff b_{3} + y = x ) ) & ( not y <=' x implies ( b_{3} = x -' y iff b_{3} = {} ) ) );

for x, y, b

( ( y <=' x implies ( b

Lm3: for x being Element of REAL+ holds x -' 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;

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;

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+ ;

correctness

coherence

( ( y <=' x implies x -' y is set ) & ( not y <=' x implies [{},(y -' x)] is set ) );

consistency

for b_{1} being set holds verum;

by TARSKI:1;

end;
correctness

coherence

( ( y <=' x implies x -' y is set ) & ( not y <=' x implies [{},(y -' x)] is set ) );

consistency

for b

by TARSKI:1;

:: 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)] ) );

for x, y being Element of REAL+ holds

( ( y <=' x implies x - y = x -' y ) & ( not y <=' x implies x - y = [{},(y -' x)] ) );

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)

[{},(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))]

(x *' z) - (x *' y) = [{},(x *' (y -' z))]

proof end;