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

Lm1: {} in {{} }
by TARSKI:def 1;

Lm2: now
let e be set ; :: thesis: not one = [0,e]
assume A1: one = [0,e] ; :: thesis: contradiction
{0} = 0 \/ {0}
.= succ 0 by ORDINAL1:def 1
.= {{0},{0,e}} by A1, ORDINAL2:def 4, TARSKI:def 5 ;
then {0} in {0} by TARSKI:def 2;
hence contradiction ; :: thesis: verum
end;

theorem Th1: :: ARYTM_0:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
REAL+ c= REAL
proof end;

theorem Th2: :: ARYTM_0:2  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+ st x <> {} holds
[{} ,x] in REAL
proof end;

theorem Th3: :: ARYTM_0:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for y being set st [{} ,y] in REAL holds
y <> {}
proof end;

theorem Th4: :: ARYTM_0: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+ holds x - y in REAL
proof end;

theorem Th5: :: ARYTM_0:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
REAL+ misses [:{{} },REAL+ :]
proof end;

theorem Th6: :: ARYTM_0: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 - y = {} holds
x = y
proof end;

theorem Th7: :: ARYTM_0:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being set holds not one = [a,b]
proof end;

theorem Th8: :: ARYTM_0: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 <> {} & x *' y = x *' z holds
y = z
proof end;

definition
let x, y be Element of REAL ;
canceled;
func + x,y -> Element of REAL means :Def2: :: ARYTM_0:def 2
ex x', y' being Element of REAL+ st
( x = x' & y = y' & it = x' + y' ) if ( x in REAL+ & y in REAL+ )
ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & it = x' - y' ) if ( x in REAL+ & y in [:{0},REAL+ :] )
ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & it = y' - x' ) if ( y in REAL+ & x in [:{0},REAL+ :] )
otherwise ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & it = [0,(x' + y')] );
existence
( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) ) & ( x in REAL+ & y in [:{0},REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = x' - y' ) ) & ( y in REAL+ & x in [:{0},REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = y' - x' ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] ) & ( not y in REAL+ or not x in [:{0},REAL+ :] ) implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = [0,(x' + y')] ) ) )
proof end;
uniqueness
for b1, b2 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b2 = x' + y' ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+ :] & ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = x' - y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b2 = x' - y' ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = y' - x' ) & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b2 = y' - x' ) implies b1 = b2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] ) & ( not y in REAL+ or not x in [:{0},REAL+ :] ) & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = [0,(x' + y')] ) & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b2 = [0,(x' + y')] ) implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) iff ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = x' - y' ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = y' - x' ) ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & y in REAL+ & x in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = x' - y' ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = y' - x' ) ) ) )
by Th5, XBOOLE_0:3;
commutativity
for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' + y' ) ) & ( x in REAL+ & y in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = x' - y' ) ) & ( y in REAL+ & x in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = y' - x' ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] ) & ( not y in REAL+ or not x in [:{0},REAL+ :] ) implies ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = [0,(x' + y')] ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & b1 = x' + y' ) ) & ( y in REAL+ & x in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( y = x' & x = [0,y'] & b1 = x' - y' ) ) & ( x in REAL+ & y in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0,x'] & x = y' & b1 = y' - x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+ :] ) & ( not x in REAL+ or not y in [:{0},REAL+ :] ) implies ex x', y' being Element of REAL+ st
( y = [0,x'] & x = [0,y'] & b1 = [0,(x' + y')] ) ) )
;
func * x,y -> Element of REAL means :Def3: :: ARYTM_0:def 3
ex x', y' being Element of REAL+ st
( x = x' & y = y' & it = x' *' y' ) if ( x in REAL+ & y in REAL+ )
ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & it = [0,(x' *' y')] ) if ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 )
ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & it = [0,(y' *' x')] ) if ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 )
ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & it = y' *' x' ) if ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] )
otherwise it = 0;
existence
( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = [0,(x' *' y')] ) ) & ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = [0,(y' *' x')] ) ) & ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ex b1 being Element of REAL ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = y' *' x' ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+ :] or not y <> 0 ) & ( not x in [:{0},REAL+ :] or not y in [:{0},REAL+ :] ) implies ex b1 being Element of REAL st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) & ex x', y' being Element of REAL+ st
( x = x' & y = y' & b2 = x' *' y' ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 & ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = [0,(x' *' y')] ) & ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b2 = [0,(x' *' y')] ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = [0,(y' *' x')] ) & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b2 = [0,(y' *' x')] ) implies b1 = b2 ) & ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = y' *' x' ) & ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b2 = y' *' x' ) implies b1 = b2 ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+ :] or not y <> 0 ) & ( not x in [:{0},REAL+ :] or not y in [:{0},REAL+ :] ) & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+ :] & x <> 0 implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) iff ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = [0,(x' *' y')] ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+ :] & y <> 0 implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = [0,(y' *' x')] ) ) ) & ( x in REAL+ & y in REAL+ & x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = y' *' x' ) ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 & y in REAL+ & x in [:{0},REAL+ :] & y <> 0 implies ( ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = [0,(x' *' y')] ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = [0,(y' *' x')] ) ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 & x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = [0,(x' *' y')] ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = y' *' x' ) ) ) & ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 & x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ( ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = [0,(y' *' x')] ) iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = y' *' x' ) ) ) )
by Th5, XBOOLE_0:3;
commutativity
for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x', y' being Element of REAL+ st
( x = x' & y = y' & b1 = x' *' y' ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 implies ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b1 = [0,(x' *' y')] ) ) & ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 implies ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b1 = [0,(y' *' x')] ) ) & ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b1 = y' *' x' ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+ :] or not y <> 0 ) & ( not x in [:{0},REAL+ :] or not y in [:{0},REAL+ :] ) implies b1 = 0 ) holds
( ( y in REAL+ & x in REAL+ implies ex x', y' being Element of REAL+ st
( y = x' & x = y' & b1 = x' *' y' ) ) & ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 implies ex x', y' being Element of REAL+ st
( y = x' & x = [0,y'] & b1 = [0,(x' *' y')] ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 implies ex x', y' being Element of REAL+ st
( y = [0,x'] & x = y' & b1 = [0,(y' *' x')] ) ) & ( y in [:{0},REAL+ :] & x in [:{0},REAL+ :] implies ex x', y' being Element of REAL+ st
( y = [0,x'] & x = [0,y'] & b1 = y' *' x' ) ) & ( ( not y in REAL+ or not x in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+ :] or not y <> 0 ) & ( not x in REAL+ or not y in [:{0},REAL+ :] or not x <> 0 ) & ( not y in [:{0},REAL+ :] or not x in [:{0},REAL+ :] ) implies b1 = 0 ) )
;
end;

:: deftheorem ARYTM_0:def 1 :
canceled;

:: deftheorem Def2 defines + ARYTM_0:def 2 :
for x, y, b3 being Element of REAL holds
( ( x in REAL+ & y in REAL+ implies ( b3 = + x,y iff ex x', y' being Element of REAL+ st
( x = x' & y = y' & b3 = x' + y' ) ) ) & ( x in REAL+ & y in [:{0},REAL+ :] implies ( b3 = + x,y iff ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b3 = x' - y' ) ) ) & ( y in REAL+ & x in [:{0},REAL+ :] implies ( b3 = + x,y iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b3 = y' - x' ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] ) & ( not y in REAL+ or not x in [:{0},REAL+ :] ) implies ( b3 = + x,y iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b3 = [0,(x' + y')] ) ) ) );

:: deftheorem Def3 defines * ARYTM_0:def 3 :
for x, y, b3 being Element of REAL holds
( ( x in REAL+ & y in REAL+ implies ( b3 = * x,y iff ex x', y' being Element of REAL+ st
( x = x' & y = y' & b3 = x' *' y' ) ) ) & ( x in REAL+ & y in [:{0},REAL+ :] & x <> 0 implies ( b3 = * x,y iff ex x', y' being Element of REAL+ st
( x = x' & y = [0,y'] & b3 = [0,(x' *' y')] ) ) ) & ( y in REAL+ & x in [:{0},REAL+ :] & y <> 0 implies ( b3 = * x,y iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = y' & b3 = [0,(y' *' x')] ) ) ) & ( x in [:{0},REAL+ :] & y in [:{0},REAL+ :] implies ( b3 = * x,y iff ex x', y' being Element of REAL+ st
( x = [0,x'] & y = [0,y'] & b3 = y' *' x' ) ) ) & ( ( not x in REAL+ or not y in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+ :] or not x <> 0 ) & ( not y in REAL+ or not x in [:{0},REAL+ :] or not y <> 0 ) & ( not x in [:{0},REAL+ :] or not y in [:{0},REAL+ :] ) implies ( b3 = * x,y iff b3 = 0 ) ) );

definition
let x be Element of REAL ;
func opp x -> Element of REAL means :Def4: :: ARYTM_0:def 4
+ x,it = 0;
existence
ex b1 being Element of REAL st + x,b1 = 0
proof end;
uniqueness
for b1, b2 being Element of REAL st + x,b1 = 0 & + x,b2 = 0 holds
b1 = b2
proof end;
involutiveness
for b1, b2 being Element of REAL st + b2,b1 = 0 holds
+ b1,b2 = 0
;
func inv x -> Element of REAL means :Def5: :: ARYTM_0:def 5
* x,it = one if x <> 0
otherwise it = 0;
existence
( ( x <> 0 implies ex b1 being Element of REAL st * x,b1 = one ) & ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) )
proof end;
uniqueness
for b1, b2 being Element of REAL holds
( ( x <> 0 & * x,b1 = one & * x,b2 = one implies b1 = b2 ) & ( not x <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
proof end;
consistency
for b1 being Element of REAL holds verum
;
involutiveness
for b1, b2 being Element of REAL st ( b2 <> 0 implies * b2,b1 = one ) & ( not b2 <> 0 implies b1 = 0 ) holds
( ( b1 <> 0 implies * b1,b2 = one ) & ( not b1 <> 0 implies b2 = 0 ) )
proof end;
end;

:: deftheorem Def4 defines opp ARYTM_0:def 4 :
for x, b2 being Element of REAL holds
( b2 = opp x iff + x,b2 = 0 );

:: deftheorem Def5 defines inv ARYTM_0:def 5 :
for x, b2 being Element of REAL holds
( ( x <> 0 implies ( b2 = inv x iff * x,b2 = one ) ) & ( not x <> 0 implies ( b2 = inv x iff b2 = 0 ) ) );

Lm3: for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
proof end;

theorem :: ARYTM_0:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th10: :: ARYTM_0:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for a, b being Element of REAL holds not 0,one --> a,b in REAL
proof end;

definition
let x, y be Element of REAL ;
canceled;
func [*x,y*] -> Element of COMPLEX equals :Def7: :: ARYTM_0:def 7
x if y = 0
otherwise 0,one --> x,y;
consistency
for b1 being Element of COMPLEX holds verum
;
coherence
( ( y = 0 implies x is Element of COMPLEX ) & ( not y = 0 implies 0,one --> x,y is Element of COMPLEX ) )
proof end;
end;

:: deftheorem ARYTM_0:def 6 :
canceled;

:: deftheorem Def7 defines [* ARYTM_0:def 7 :
for x, y being Element of REAL holds
( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = 0,one --> x,y ) );

theorem :: ARYTM_0:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for c being Element of COMPLEX ex r, s being Element of REAL st c = [*r,s*]
proof end;

theorem :: ARYTM_0:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x1, x2, y1, y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds
( x1 = y1 & x2 = y2 )
proof end;

set RR = [:{0},REAL+ :] \ {[0,0]};

reconsider o = 0 as Element of REAL by Th1, ARYTM_2:21;

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

theorem Th14: :: ARYTM_0:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for x, o being Element of REAL st o = 0 holds
* x,o = 0
proof end;

theorem Th15: :: ARYTM_0:15  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,z) = * (* x,y),z
proof end;

theorem Th16: :: ARYTM_0: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 holds * x,(+ y,z) = + (* x,y),(* x,z)
proof end;

theorem :: ARYTM_0:17  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 * (opp x),y = opp (* x,y)
proof end;

theorem Th18: :: ARYTM_0: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 in REAL+
proof end;

theorem :: ARYTM_0: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,x),(* y,y) = 0 holds
x = 0
proof end;

theorem Th20: :: ARYTM_0:20  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 <> 0 & * x,y = one & * x,z = one holds
y = z
proof end;

theorem Th21: :: ARYTM_0:21  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 y = one holds
* x,y = x
proof end;

reconsider j = one as Element of REAL by Th1, ARYTM_2:21;

theorem :: ARYTM_0:22  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 y <> 0 holds
* (* x,y),(inv y) = x
proof end;

theorem Th23: :: ARYTM_0:23  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 = 0 or x = 0 or y = 0 )
proof end;

theorem :: ARYTM_0:24  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 inv (* x,y) = * (inv x),(inv y)
proof end;

theorem Th25: :: ARYTM_0: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 holds + x,(+ y,z) = + (+ x,y),z
proof end;

theorem :: ARYTM_0:26  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*] in REAL holds
y = 0
proof end;

theorem :: ARYTM_0:27  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 opp (+ x,y) = + (opp x),(opp y)
proof end;