:: ARYTM_1 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem Th1: :: ARYTM_1:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ st x + y = y holds
x = {}
proof end;

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

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

theorem :: ARYTM_1:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ holds
( not x *' y = {} or x = {} or y = {} )
proof end;

theorem Th3: :: ARYTM_1:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Element of REAL+ st x <=' y & y <=' z holds
x <=' z
proof end;

theorem Th4: :: ARYTM_1:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ st x <=' y & y <=' x holds
x = y
proof end;

theorem Th5: :: ARYTM_1:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ st x <=' y & y = {} holds
x = {}
proof end;

theorem Th6: :: ARYTM_1:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ st x = {} holds
x <=' y
proof end;

theorem Th7: :: ARYTM_1:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Element of REAL+ holds
( x <=' y iff x + z <=' y + z )
proof end;

theorem Th8: :: ARYTM_1:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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:12;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ holds
( x <=' y or x -' y <> {} )
proof end;

theorem :: ARYTM_1:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ st x <=' y & y -' x = {} holds
x = y
proof end;

theorem Th11: :: ARYTM_1:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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 z, y, x being Element of REAL+ holds
( z -' y <=' x iff z <=' x + y )
proof end;

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

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

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

theorem :: ARYTM_1:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x, z being Element of REAL+ st y <=' x & y <=' z holds
x + (z -' y) = (x -' y) + z
proof end;

theorem Th13: :: ARYTM_1:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, y, x being Element of REAL+ st z <=' y holds
x + (y -' z) = (x + y) -' z
proof end;

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

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

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

theorem :: ARYTM_1:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, x, y being Element of REAL+ st z <=' x & y <=' z holds
(x -' z) + y = x -' (z -' y)
proof end;

theorem :: ARYTM_1:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x, z being Element of REAL+ st y <=' x & y <=' z holds
(z -' y) + x = (x -' y) + z
proof end;

theorem :: ARYTM_1:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y, z being Element of REAL+ st x <=' y holds
z -' y <=' z -' x
proof end;

theorem :: ARYTM_1:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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;
;
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x being Element of REAL+ holds x - x = {}
proof end;

theorem :: ARYTM_1:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, y being Element of REAL+ st x = {} & y <> {} holds
x - y = [{} ,y]
proof end;

theorem :: ARYTM_1:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, y, x being Element of REAL+ st z <=' y holds
x + (y -' z) = (x + y) - z
proof end;

theorem :: ARYTM_1:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, y, x being Element of REAL+ st not z <=' y holds
x - (z -' y) = (x + y) - z
proof end;

theorem :: ARYTM_1:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x, z being Element of REAL+ st y <=' x & not y <=' z holds
x - (y -' z) = (x -' y) + z
proof end;

theorem :: ARYTM_1:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x, 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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, x, z being Element of REAL+ st y <=' x holds
x - (y + z) = (x -' y) - z
proof end;

theorem :: ARYTM_1:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
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  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, y, x being Element of REAL+ st z <=' y holds
x *' (y -' z) = (x *' y) - (x *' z)
proof end;

theorem Th27: :: ARYTM_1:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for z, y, x being Element of REAL+ st not z <=' y & x <> {} holds
[{} ,(x *' (z -' y))] = (x *' y) - (x *' z)
proof end;

theorem :: ARYTM_1:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y, z, x being Element of REAL+ st y -' z <> {} & z <=' y & x <> {} holds
(x *' z) - (x *' y) = [{} ,(x *' (y -' z))]
proof end;