begin
Lm1:
{} in {{}}
by TARSKI:def 1;
begin
Lm2:
for a, b being set holds not 1 = [a,b]
begin
definition
let x,
y be
Element of
REAL ;
func + (
x,
y)
-> Element of
REAL means :
Def1:
ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = y9 &
it = x9 + y9 )
if (
x in REAL+ &
y in REAL+ )
ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = [0,y9] &
it = x9 - y9 )
if (
x in REAL+ &
y in [:{0},REAL+:] )
ex
x9,
y9 being
Element of
REAL+ st
(
x = [0,x9] &
y = y9 &
it = y9 - x9 )
if (
y in REAL+ &
x in [:{0},REAL+:] )
otherwise ex
x9,
y9 being
Element of
REAL+ st
(
x = [0,x9] &
y = [0,y9] &
it = [0,(x9 + y9)] );
existence
( ( x in REAL+ & y in REAL+ implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) )
uniqueness
for b1, b2 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b2 = x9 + y9 ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b2 = x9 - y9 ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b2 = y9 - x9 ) 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 x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b2 = [0,(x9 + y9)] ) implies b1 = b2 ) )
consistency
for b1 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & x in REAL+ & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 + y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & y in REAL+ & x in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = x9 - y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) ) )
by Th5, XBOOLE_0:3;
commutativity
for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 + y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = x9 - y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] ) ) holds
( ( y in REAL+ & x in REAL+ implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & b1 = x9 + y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = [0,y9] & b1 = x9 - y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = y9 & b1 = y9 - x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & b1 = [0,(x9 + y9)] ) ) )
;
func * (
x,
y)
-> Element of
REAL means :
Def2:
ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = y9 &
it = x9 *' y9 )
if (
x in REAL+ &
y in REAL+ )
ex
x9,
y9 being
Element of
REAL+ st
(
x = x9 &
y = [0,y9] &
it = [0,(x9 *' y9)] )
if (
x in REAL+ &
y in [:{0},REAL+:] &
x <> 0 )
ex
x9,
y9 being
Element of
REAL+ st
(
x = [0,x9] &
y = y9 &
it = [0,(y9 *' x9)] )
if (
y in REAL+ &
x in [:{0},REAL+:] &
y <> 0 )
ex
x9,
y9 being
Element of
REAL+ st
(
x = [0,x9] &
y = [0,y9] &
it = y9 *' x9 )
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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( 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 ) )
uniqueness
for b1, b2 being Element of REAL holds
( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b2 = x9 *' y9 ) implies b1 = b2 ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b2 = [0,(x9 *' y9)] ) implies b1 = b2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b2 = [0,(y9 *' x9)] ) implies b1 = b2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b2 = y9 *' x9 ) 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 ) )
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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) ) & ( x in REAL+ & y in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in REAL+ & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 *' y9 ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) ) )
by Th5, XBOOLE_0:3;
commutativity
for b1, x, y being Element of REAL st ( x in REAL+ & y in REAL+ implies ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b1 = x9 *' y9 ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b1 = [0,(y9 *' x9)] ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = y9 *' x9 ) ) & ( ( 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 x9, y9 being Element of REAL+ st
( y = x9 & x = y9 & b1 = x9 *' y9 ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ex x9, y9 being Element of REAL+ st
( y = x9 & x = [0,y9] & b1 = [0,(x9 *' y9)] ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = y9 & b1 = [0,(y9 *' x9)] ) ) & ( y in [:{0},REAL+:] & x in [:{0},REAL+:] implies ex x9, y9 being Element of REAL+ st
( y = [0,x9] & x = [0,y9] & b1 = y9 *' x9 ) ) & ( ( 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 Def1 defines
+ ARYTM_0:def 1 :
for x, y, b3 being Element of REAL holds
( ( x in REAL+ & y in REAL+ implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b3 = x9 + y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b3 = x9 - y9 ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] implies ( b3 = + (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b3 = y9 - x9 ) ) ) & ( ( 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 x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b3 = [0,(x9 + y9)] ) ) ) );
::
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 x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & b3 = x9 *' y9 ) ) ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & b3 = [0,(x9 *' y9)] ) ) ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & b3 = [0,(y9 *' x9)] ) ) ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] implies ( b3 = * (x,y) iff ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b3 = y9 *' x9 ) ) ) & ( ( 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 ;
existence
ex b1 being Element of REAL st + (x,b1) = 0
uniqueness
for b1, b2 being Element of REAL st + (x,b1) = 0 & + (x,b2) = 0 holds
b1 = b2
involutiveness
for b1, b2 being Element of REAL st + (b2,b1) = 0 holds
+ (b1,b2) = 0
;
existence
( ( x <> 0 implies ex b1 being Element of REAL st * (x,b1) = 1 ) & ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) )
uniqueness
for b1, b2 being Element of REAL holds
( ( x <> 0 & * (x,b1) = 1 & * (x,b2) = 1 implies b1 = b2 ) & ( not x <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) )
consistency
for b1 being Element of REAL holds verum
;
involutiveness
for b1, b2 being Element of REAL st ( b2 <> 0 implies * (b2,b1) = 1 ) & ( not b2 <> 0 implies b1 = 0 ) holds
( ( b1 <> 0 implies * (b1,b2) = 1 ) & ( not b1 <> 0 implies b2 = 0 ) )
end;
begin
Lm3:
for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
set RR = [:{0},REAL+:] \ {[0,0]};
reconsider o = 0 as Element of REAL ;
reconsider j = 1 as Element of REAL ;