:: ARYTM_0 semantic presentation
begin
Lm1: {} in {{}}
by TARSKI:def_1;
theorem Th1: :: ARYTM_0:1
REAL+ c= REAL
proof
REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7;
hence REAL+ c= REAL by ARYTM_2:3, NUMBERS:def_1, ZFMISC_1:34; ::_thesis: verum
end;
theorem Th2: :: ARYTM_0:2
for x being Element of REAL+ st x <> {} holds
[{},x] in REAL
proof
let x be Element of REAL+ ; ::_thesis: ( x <> {} implies [{},x] in REAL )
assume A1: x <> {} ; ::_thesis: [{},x] in REAL
A2: now__::_thesis:_not_[{},x]_in_{[{},{}]}
assume [{},x] in {[{},{}]} ; ::_thesis: contradiction
then [{},x] = [{},{}] by TARSKI:def_1;
hence contradiction by A1, XTUPLE_0:1; ::_thesis: verum
end;
{} in {{}} by TARSKI:def_1;
then [{},x] in [:{{}},REAL+:] by ZFMISC_1:87;
then [{},x] in REAL+ \/ [:{{}},REAL+:] by XBOOLE_0:def_3;
hence [{},x] in REAL by A2, NUMBERS:def_1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th3: :: ARYTM_0:3
for y being set st [{},y] in REAL holds
y <> {}
proof
let y be set ; ::_thesis: ( [{},y] in REAL implies y <> {} )
assume that
A1: [{},y] in REAL and
A2: y = {} ; ::_thesis: contradiction
[{},y] in {[{},{}]} by A2, TARSKI:def_1;
hence contradiction by A1, NUMBERS:def_1, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem Th4: :: ARYTM_0:4
for x, y being Element of REAL+ holds x - y in REAL
proof
let x, y be Element of REAL+ ; ::_thesis: x - y in REAL
percases ( y <=' x or not y <=' x ) ;
suppose y <=' x ; ::_thesis: x - y in REAL
then x - y = x -' y by ARYTM_1:def_2;
then x - y in REAL+ ;
hence x - y in REAL by Th1; ::_thesis: verum
end;
supposeA1: not y <=' x ; ::_thesis: x - y in REAL
then x - y = [{},(y -' x)] by ARYTM_1:def_2;
hence x - y in REAL by A1, Th2, ARYTM_1:9; ::_thesis: verum
end;
end;
end;
theorem Th5: :: ARYTM_0:5
REAL+ misses [:{{}},REAL+:]
proof
assume REAL+ meets [:{{}},REAL+:] ; ::_thesis: contradiction
then consider x being set such that
A1: x in REAL+ and
A2: x in [:{{}},REAL+:] by XBOOLE_0:3;
consider x1, x2 being set such that
A3: x1 in {{}} and
x2 in REAL+ and
A4: x = [x1,x2] by A2, ZFMISC_1:84;
x1 = {} by A3, TARSKI:def_1;
hence contradiction by A1, A4, ARYTM_2:3; ::_thesis: verum
end;
begin
theorem Th6: :: ARYTM_0:6
for x, y being Element of REAL+ st x - y = {} holds
x = y
proof
let x, y be Element of REAL+ ; ::_thesis: ( x - y = {} implies x = y )
assume A1: x - y = {} ; ::_thesis: x = y
{} <> [{},(y -' x)] ;
then ( y <=' x & x -' y = {} ) by A1, ARYTM_1:def_2;
hence x = y by ARYTM_1:10; ::_thesis: verum
end;
Lm2: for a, b being set holds not 1 = [a,b]
proof
let a, b be set ; ::_thesis: not 1 = [a,b]
assume 1 = [a,b] ; ::_thesis: contradiction
then A1: {{}} = {{a,b},{a}} by ORDINAL3:15, TARSKI:def_5;
{a} in {{a,b},{a}} by TARSKI:def_2;
hence contradiction by A1, TARSKI:def_1; ::_thesis: verum
end;
theorem Th7: :: ARYTM_0:7
for x, y, z being Element of REAL+ st x <> {} & x *' y = x *' z holds
y = z
proof
let x, y, z be Element of REAL+ ; ::_thesis: ( x <> {} & x *' y = x *' z implies y = z )
assume that
A1: x <> {} and
A2: x *' y = x *' z ; ::_thesis: y = z
percases ( z <=' y or y <=' z ) ;
supposeA3: z <=' y ; ::_thesis: y = z
then x *' (y -' z) = (x *' y) - (x *' z) by ARYTM_1:26
.= {} by A2, ARYTM_1:18 ;
then {} = y -' z by A1, ARYTM_1:2
.= y - z by A3, ARYTM_1:def_2 ;
hence y = z by Th6; ::_thesis: verum
end;
supposeA4: y <=' z ; ::_thesis: y = z
then x *' (z -' y) = (x *' z) - (x *' y) by ARYTM_1:26
.= {} by A2, ARYTM_1:18 ;
then {} = z -' y by A1, ARYTM_1:2
.= z - y by A4, ARYTM_1:def_2 ;
hence y = z by Th6; ::_thesis: verum
end;
end;
end;
begin
definition
let x, y be Element of REAL ;
func + (x,y) -> Element of REAL means :Def1: :: ARYTM_0:def 1
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)] ) ) )
proof
hereby ::_thesis: ( ( 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)] ) ) )
assume ( x in REAL+ & y in REAL+ ) ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT = x9 + y9 )
then reconsider x9 = x, y9 = y as Element of REAL+ ;
x9 + y9 in REAL+ ;
then reconsider IT = x9 + y9 as Element of REAL by Th1;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT = x9 + y9 )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = x9 & y = y9 & IT = x9 + y9 )
take y9 = y9; ::_thesis: ( x = x9 & y = y9 & IT = x9 + y9 )
thus ( x = x9 & y = y9 & IT = x9 + y9 ) ; ::_thesis: verum
end;
A1: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
hereby ::_thesis: ( ( 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)] ) ) )
assume x in REAL+ ; ::_thesis: ( y in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 ) )
then reconsider x9 = x as Element of REAL+ ;
assume y in [:{0},REAL+:] ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 )
then consider z, y9 being set such that
A2: z in {0} and
A3: y9 in REAL+ and
A4: y = [z,y9] by ZFMISC_1:84;
reconsider y9 = y9 as Element of REAL+ by A3;
reconsider IT = x9 - y9 as Element of REAL by Th4;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = x9 - y9 )
take y9 = y9; ::_thesis: ( x = x9 & y = [0,y9] & IT = x9 - y9 )
thus ( x = x9 & y = [0,y9] & IT = x9 - y9 ) by A2, A4, TARSKI:def_1; ::_thesis: verum
end;
hereby ::_thesis: ( ( 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)] ) )
assume y in REAL+ ; ::_thesis: ( x in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 ) )
then reconsider y9 = y as Element of REAL+ ;
assume x in [:{0},REAL+:] ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 )
then consider z, x9 being set such that
A5: z in {0} and
A6: x9 in REAL+ and
A7: x = [z,x9] by ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A6;
reconsider IT = y9 - x9 as Element of REAL by Th4;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = y9 - x9 )
take y9 = y9; ::_thesis: ( x = [0,x9] & y = y9 & IT = y9 - x9 )
thus ( x = [0,x9] & y = y9 & IT = y9 - x9 ) by A5, A7, TARSKI:def_1; ::_thesis: verum
end;
assume that
A8: ( not x in REAL+ or not y in REAL+ ) and
A9: ( not x in REAL+ or not y in [:{0},REAL+:] ) and
A10: ( not y in REAL+ or not x in [:{0},REAL+:] ) ; ::_thesis: ex b1 being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & b1 = [0,(x9 + y9)] )
A11: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
then ( x in REAL+ or x in [:{0},REAL+:] ) by XBOOLE_0:def_3;
then consider z1, x9 being set such that
A12: z1 in {0} and
A13: x9 in REAL+ and
A14: x = [z1,x9] by A1, A8, A9, XBOOLE_0:def_3, ZFMISC_1:84;
( y in REAL+ or y in [:{0},REAL+:] ) by A1, XBOOLE_0:def_3;
then consider z2, y9 being set such that
A15: z2 in {0} and
A16: y9 in REAL+ and
A17: y = [z2,y9] by A11, A8, A10, XBOOLE_0:def_3, ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A13;
reconsider y9 = y9 as Element of REAL+ by A16;
x = [0,x9] by A12, A14, TARSKI:def_1;
then x9 + y9 <> 0 by Th3, ARYTM_2:5;
then reconsider IT = [0,(y9 + x9)] as Element of REAL by Th2;
take IT ; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
take x9 ; ::_thesis: ex y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
take y9 ; ::_thesis: ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] )
thus ( x = [0,x9] & y = [0,y9] & IT = [0,(x9 + y9)] ) by A12, A14, A15, A17, TARSKI:def_1; ::_thesis: verum
end;
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 ) )
proof
let IT1, IT2 be Element of REAL ; ::_thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 + y9 ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT2 = x9 - y9 ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) )
thus ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 + y9 ) implies IT1 = IT2 ) ; ::_thesis: ( ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT2 = x9 - y9 ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) )
thus ( x in REAL+ & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = x9 - y9 ) & ex x99, y99 being Element of REAL+ st
( x = x99 & y = [0,y99] & IT2 = x99 - y99 ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = y9 - x9 ) implies IT1 = IT2 ) & ( ( 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] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 ) )
thus ( y in REAL+ & x in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = y9 - x9 ) & ex x99, y99 being Element of REAL+ st
( x = [0,x99] & y = y99 & IT2 = y99 - x99 ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( 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] & IT1 = [0,(x9 + y9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = [0,(x9 + y9)] ) implies IT1 = IT2 )
assume that
( not x in REAL+ or not y in REAL+ ) and
( not x in REAL+ or not y in [:{0},REAL+:] ) and
( not y in REAL+ or not x in [:{0},REAL+:] ) ; ::_thesis: ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not IT1 = [0,(x9 + y9)] ) or for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not IT2 = [0,(x9 + y9)] ) or IT1 = IT2 )
given x9, y9 being Element of REAL+ such that A18: x = [0,x9] and
A19: ( y = [0,y9] & IT1 = [0,(x9 + y9)] ) ; ::_thesis: ( for x9, y9 being Element of REAL+ holds
( not x = [0,x9] or not y = [0,y9] or not IT2 = [0,(x9 + y9)] ) or IT1 = IT2 )
given x99, y99 being Element of REAL+ such that A20: x = [0,x99] and
A21: ( y = [0,y99] & IT2 = [0,(x99 + y99)] ) ; ::_thesis: IT1 = IT2
x9 = x99 by A18, A20, XTUPLE_0:1;
hence IT1 = IT2 by A19, A21, XTUPLE_0:1; ::_thesis: verum
end;
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: :: ARYTM_0:def 2
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 ) )
proof
hereby ::_thesis: ( ( 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 ) )
assume ( x in REAL+ & y in REAL+ ) ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT = x9 *' y9 )
then reconsider x9 = x, y9 = y as Element of REAL+ ;
x9 *' y9 in REAL+ ;
then reconsider IT = x9 *' y9 as Element of REAL by Th1;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT = x9 *' y9 )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = x9 & y = y9 & IT = x9 *' y9 )
take y9 = y9; ::_thesis: ( x = x9 & y = y9 & IT = x9 *' y9 )
thus ( x = x9 & y = y9 & IT = x9 *' y9 ) ; ::_thesis: verum
end;
hereby ::_thesis: ( ( 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 ) )
assume x in REAL+ ; ::_thesis: ( y in [:{0},REAL+:] & x <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) )
then reconsider x9 = x as Element of REAL+ ;
assume y in [:{0},REAL+:] ; ::_thesis: ( x <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) )
then consider z, y9 being set such that
A22: z in {0} and
A23: y9 in REAL+ and
A24: y = [z,y9] by ZFMISC_1:84;
reconsider y9 = y9 as Element of REAL+ by A23;
y = [0,y9] by A22, A24, TARSKI:def_1;
then A25: y9 <> 0 by Th3;
assume x <> 0 ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )
then reconsider IT = [0,(x9 *' y9)] as Element of REAL by A25, Th2, ARYTM_1:2;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )
take y9 = y9; ::_thesis: ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] )
thus ( x = x9 & y = [0,y9] & IT = [0,(x9 *' y9)] ) by A22, A24, TARSKI:def_1; ::_thesis: verum
end;
hereby ::_thesis: ( ( 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 ) )
assume y in REAL+ ; ::_thesis: ( x in [:{0},REAL+:] & y <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) )
then reconsider y9 = y as Element of REAL+ ;
assume x in [:{0},REAL+:] ; ::_thesis: ( y <> 0 implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) )
then consider z, x9 being set such that
A26: z in {0} and
A27: x9 in REAL+ and
A28: x = [z,x9] by ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A27;
x = [0,x9] by A26, A28, TARSKI:def_1;
then A29: x9 <> 0 by Th3;
assume y <> 0 ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )
then reconsider IT = [0,(y9 *' x9)] as Element of REAL by A29, Th2, ARYTM_1:2;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )
take y9 = y9; ::_thesis: ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] )
thus ( x = [0,x9] & y = y9 & IT = [0,(y9 *' x9)] ) by A26, A28, TARSKI:def_1; ::_thesis: verum
end;
hereby ::_thesis: ( ( 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 )
assume x in [:{0},REAL+:] ; ::_thesis: ( y in [:{0},REAL+:] implies ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) )
then consider z1, x9 being set such that
A30: z1 in {0} and
A31: x9 in REAL+ and
A32: x = [z1,x9] by ZFMISC_1:84;
reconsider x9 = x9 as Element of REAL+ by A31;
assume y in [:{0},REAL+:] ; ::_thesis: ex IT being Element of REAL ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )
then consider z2, y9 being set such that
A33: z2 in {0} and
A34: y9 in REAL+ and
A35: y = [z2,y9] by ZFMISC_1:84;
reconsider y9 = y9 as Element of REAL+ by A34;
x9 *' y9 in REAL+ ;
then reconsider IT = y9 *' x9 as Element of REAL by Th1;
take IT = IT; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )
take y9 = y9; ::_thesis: ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 )
thus ( x = [0,x9] & y = [0,y9] & IT = y9 *' x9 ) by A30, A32, A33, A35, TARSKI:def_1; ::_thesis: verum
end;
thus ( ( 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 ) ; ::_thesis: verum
end;
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 ) )
proof
let IT1, IT2 be Element of REAL ; ::_thesis: ( ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 *' y9 ) implies IT1 = IT2 ) & ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT2 = [0,(x9 *' y9)] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = [0,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
thus ( x in REAL+ & y in REAL+ & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & IT2 = x9 *' y9 ) implies IT1 = IT2 ) ; ::_thesis: ( ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = [0,(x9 *' y9)] ) & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT2 = [0,(x9 *' y9)] ) implies IT1 = IT2 ) & ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = [0,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
thus ( x in REAL+ & y in [:{0},REAL+:] & x <> 0 & ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & IT1 = [0,(x9 *' y9)] ) & ex x99, y99 being Element of REAL+ st
( x = x99 & y = [0,y99] & IT2 = [0,(x99 *' y99)] ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT2 = [0,(y9 *' x9)] ) implies IT1 = IT2 ) & ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
thus ( y in REAL+ & x in [:{0},REAL+:] & y <> 0 & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & IT1 = [0,(y9 *' x9)] ) & ex x99, y99 being Element of REAL+ st
( x = [0,x99] & y = y99 & IT2 = [0,(y99 *' x99)] ) implies IT1 = IT2 ) by XTUPLE_0:1; ::_thesis: ( ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT2 = y9 *' x9 ) implies IT1 = IT2 ) & ( ( 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+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) )
hereby ::_thesis: ( ( 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+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 )
assume that
x in [:{0},REAL+:] and
y in [:{0},REAL+:] ; ::_thesis: ( ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & IT1 = y9 *' x9 ) & ex x99, y99 being Element of REAL+ st
( x = [0,x99] & y = [0,y99] & IT2 = y99 *' x99 ) implies IT1 = IT2 )
given x9, y9 being Element of REAL+ such that A36: x = [0,x9] and
A37: ( y = [0,y9] & IT1 = y9 *' x9 ) ; ::_thesis: ( ex x99, y99 being Element of REAL+ st
( x = [0,x99] & y = [0,y99] & IT2 = y99 *' x99 ) implies IT1 = IT2 )
given x99, y99 being Element of REAL+ such that A38: x = [0,x99] and
A39: ( y = [0,y99] & IT2 = y99 *' x99 ) ; ::_thesis: IT1 = IT2
x9 = x99 by A36, A38, XTUPLE_0:1;
hence IT1 = IT2 by A37, A39, XTUPLE_0:1; ::_thesis: verum
end;
thus ( ( 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+:] ) & IT1 = 0 & IT2 = 0 implies IT1 = IT2 ) ; ::_thesis: verum
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 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 ;
func opp x -> Element of REAL means :Def3: :: ARYTM_0:def 3
+ (x,it) = 0 ;
existence
ex b1 being Element of REAL st + (x,b1) = 0
proof
reconsider z9 = 0 as Element of REAL+ by ARYTM_2:20;
A1: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
percases ( x = 0 or ( x in REAL+ & x <> 0 ) or x in [:{0},REAL+:] ) by A1, XBOOLE_0:def_3;
supposeA2: x = 0 ; ::_thesis: ex b1 being Element of REAL st + (x,b1) = 0
then reconsider x9 = x as Element of REAL+ by ARYTM_2:20;
take x ; ::_thesis: + (x,x) = 0
x9 + x9 = 0 by A2, ARYTM_2:def_8;
hence + (x,x) = 0 by Def1; ::_thesis: verum
end;
supposethat A3: x in REAL+ and
A4: x <> 0 ; ::_thesis: ex b1 being Element of REAL st + (x,b1) = 0
A5: [0,x] <> [0,0] by A4, XTUPLE_0:1;
0 in {0} by TARSKI:def_1;
then A6: [0,x] in [:{0},REAL+:] by A3, ZFMISC_1:87;
then [0,x] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3;
then reconsider y = [0,x] as Element of REAL by A5, NUMBERS:def_1, ZFMISC_1:56;
reconsider x9 = x as Element of REAL+ by A3;
A7: x9 <=' x9 ;
take y ; ::_thesis: + (x,y) = 0
z9 + x9 = x9 by ARYTM_2:def_8;
then z9 = x9 -' x9 by A7, ARYTM_1:def_1;
then 0 = x9 - x9 by A7, ARYTM_1:def_2;
hence + (x,y) = 0 by A6, Def1; ::_thesis: verum
end;
supposeA8: x in [:{0},REAL+:] ; ::_thesis: ex b1 being Element of REAL st + (x,b1) = 0
then consider a, b being set such that
A9: a in {0} and
A10: b in REAL+ and
A11: x = [a,b] by ZFMISC_1:84;
reconsider y = b as Element of REAL by A10, Th1;
take y ; ::_thesis: + (x,y) = 0
now__::_thesis:_(_(_x_in_REAL+_&_y_in_REAL+_&_ex_x9,_y9_being_Element_of_REAL+_st_
(_x_=_x9_&_y_=_y9_&_0_=_x9_+_y9_)_)_or_(_x_in_REAL+_&_y_in_[:{0},REAL+:]_&_ex_x9,_y9_being_Element_of_REAL+_st_
(_x_=_x9_&_y_=_[0,y9]_&_0_=_x9_-_y9_)_)_or_(_y_in_REAL+_&_x_in_[:{0},REAL+:]_&_ex_x9,_y9_being_Element_of_REAL+_st_
(_x_=_[0,x9]_&_y_=_y9_&_0_=_y9_-_x9_)_)_or_(_(_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]_&_0_=_[0,(y9_+_x9)]_)_)_)
percases ( ( x in REAL+ & y in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( y in REAL+ & x in [:{0},REAL+:] ) or ( ( 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+:] ) ) ) ;
case ( x in REAL+ & y in REAL+ ) ; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 )
hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by A8, Th5, XBOOLE_0:3; ::_thesis: verum
end;
case ( x in REAL+ & y in [:{0},REAL+:] ) ; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 0 = x9 - y9 )
hence ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 0 = x9 - y9 ) by A10, Th5, XBOOLE_0:3; ::_thesis: verum
end;
case ( y in REAL+ & x in [:{0},REAL+:] ) ; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & 0 = y9 - x9 )
reconsider x9 = b, y9 = y as Element of REAL+ by A10;
take x9 = x9; ::_thesis: ex y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & 0 = y9 - x9 )
take y9 = y9; ::_thesis: ( x = [0,x9] & y = y9 & 0 = y9 - x9 )
thus x = [0,x9] by A9, A11, TARSKI:def_1; ::_thesis: ( y = y9 & 0 = y9 - x9 )
thus y = y9 ; ::_thesis: 0 = y9 - x9
thus 0 = y9 - x9 by ARYTM_1:18; ::_thesis: verum
end;
case ( ( 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+:] ) ) ; ::_thesis: ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(y9 + x9)] )
hence ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(y9 + x9)] ) by A8, A10; ::_thesis: verum
end;
end;
end;
hence + (x,y) = 0 by Def1; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being Element of REAL st + (x,b1) = 0 & + (x,b2) = 0 holds
b1 = b2
proof
let y, z be Element of REAL ; ::_thesis: ( + (x,y) = 0 & + (x,z) = 0 implies y = z )
assume that
A12: + (x,y) = 0 and
A13: + (x,z) = 0 ; ::_thesis: y = z
percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & z in REAL+ & y in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( ( 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+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ) ;
suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; ::_thesis: y = z
then ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & z = y9 & 0 = x9 + y9 ) ) by A12, A13, Def1;
hence y = z by ARYTM_2:11; ::_thesis: verum
end;
supposethat A14: x in REAL+ and
A15: y in REAL+ and
A16: z in [:{0},REAL+:] ; ::_thesis: y = z
consider x99, y99 being Element of REAL+ such that
A17: x = x99 and
A18: ( z = [0,y99] & 0 = x99 - y99 ) by A13, A14, A16, Def1;
ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 0 = x9 + y9 ) by A12, A14, A15, Def1;
then A19: x99 = 0 by A17, ARYTM_2:5;
[0,0] in {[0,0]} by TARSKI:def_1;
then A20: not [0,0] in REAL by NUMBERS:def_1, XBOOLE_0:def_5;
z in REAL ;
hence y = z by A18, A19, A20, ARYTM_1:19; ::_thesis: verum
end;
supposethat A21: x in REAL+ and
A22: z in REAL+ and
A23: y in [:{0},REAL+:] ; ::_thesis: y = z
consider x99, y9 being Element of REAL+ such that
A24: x = x99 and
A25: ( y = [0,y9] & 0 = x99 - y9 ) by A12, A21, A23, Def1;
ex x9, z9 being Element of REAL+ st
( x = x9 & z = z9 & 0 = x9 + z9 ) by A13, A21, A22, Def1;
then A26: x99 = 0 by A24, ARYTM_2:5;
[0,0] in {[0,0]} by TARSKI:def_1;
then A27: not [0,0] in REAL by NUMBERS:def_1, XBOOLE_0:def_5;
y in REAL ;
hence y = z by A25, A26, A27, ARYTM_1:19; ::_thesis: verum
end;
supposethat A28: x in REAL+ and
A29: y in [:{0},REAL+:] and
A30: z in [:{0},REAL+:] ; ::_thesis: y = z
consider x99, z9 being Element of REAL+ such that
A31: x = x99 and
A32: z = [0,z9] and
A33: 0 = x99 - z9 by A13, A28, A30, Def1;
consider x9, y9 being Element of REAL+ such that
A34: x = x9 and
A35: y = [0,y9] and
A36: 0 = x9 - y9 by A12, A28, A29, Def1;
y9 = x9 by A36, Th6
.= z9 by A34, A31, A33, Th6 ;
hence y = z by A35, A32; ::_thesis: verum
end;
supposethat A37: z in REAL+ and
A38: y in REAL+ and
A39: x in [:{0},REAL+:] ; ::_thesis: y = z
consider x99, z9 being Element of REAL+ such that
A40: x = [0,x99] and
A41: z = z9 and
A42: 0 = z9 - x99 by A13, A37, A39, Def1;
consider x9, y9 being Element of REAL+ such that
A43: x = [0,x9] and
A44: y = y9 and
A45: 0 = y9 - x9 by A12, A38, A39, Def1;
x9 = x99 by A43, A40, XTUPLE_0:1;
then z9 = x9 by A42, Th6
.= y9 by A45, Th6 ;
hence y = z by A44, A41; ::_thesis: verum
end;
suppose ( ( 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+:] ) ) ; ::_thesis: y = z
then ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = [0,y9] & 0 = [0,(x9 + y9)] ) by A12, Def1;
hence y = z ; ::_thesis: verum
end;
suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] ) & ( not z in REAL+ or not x in [:{0},REAL+:] ) ) ; ::_thesis: y = z
then ex x9, z9 being Element of REAL+ st
( x = [0,x9] & z = [0,z9] & 0 = [0,(x9 + z9)] ) by A13, Def1;
hence y = z ; ::_thesis: verum
end;
end;
end;
involutiveness
for b1, b2 being Element of REAL st + (b2,b1) = 0 holds
+ (b1,b2) = 0 ;
func inv x -> Element of REAL means :Def4: :: ARYTM_0:def 4
* (x,it) = 1 if x <> 0
otherwise it = 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 ) )
proof
thus ( x <> 0 implies ex y being Element of REAL st * (x,y) = 1 ) ::_thesis: ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 )
proof
A46: x in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
assume A47: x <> 0 ; ::_thesis: ex y being Element of REAL st * (x,y) = 1
percases ( x in REAL+ or x in [:{0},REAL+:] ) by A46, XBOOLE_0:def_3;
suppose x in REAL+ ; ::_thesis: ex y being Element of REAL st * (x,y) = 1
then reconsider x9 = x as Element of REAL+ ;
consider y9 being Element of REAL+ such that
A48: x9 *' y9 = 1 by A47, ARYTM_2:14;
y9 in REAL+ ;
then reconsider y = y9 as Element of REAL by Th1;
take y ; ::_thesis: * (x,y) = 1
thus * (x,y) = 1 by A48, Def2; ::_thesis: verum
end;
supposeA49: x in [:{0},REAL+:] ; ::_thesis: ex y being Element of REAL st * (x,y) = 1
not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5;
then A50: x <> [0,0] by TARSKI:def_1;
consider x1, x2 being set such that
x1 in {0} and
A51: x2 in REAL+ and
A52: x = [x1,x2] by A49, ZFMISC_1:84;
reconsider x2 = x2 as Element of REAL+ by A51;
x1 in {0} by A49, A52, ZFMISC_1:87;
then x2 <> 0 by A52, A50, TARSKI:def_1;
then consider y2 being Element of REAL+ such that
A53: x2 *' y2 = 1 by ARYTM_2:14;
A54: now__::_thesis:_not_[0,y2]_in_{[0,0]}
assume [0,y2] in {[0,0]} ; ::_thesis: contradiction
then [0,y2] = [0,0] by TARSKI:def_1;
then y2 = 0 by XTUPLE_0:1;
hence contradiction by A53, ARYTM_2:4; ::_thesis: verum
end;
A55: [0,y2] in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then [0,y2] in REAL+ \/ [:{0},REAL+:] by XBOOLE_0:def_3;
then reconsider y = [0,y2] as Element of REAL by A54, NUMBERS:def_1, XBOOLE_0:def_5;
take y ; ::_thesis: * (x,y) = 1
consider x9, y9 being Element of REAL+ such that
A56: x = [0,x9] and
A57: y = [0,y9] and
A58: * (x,y) = y9 *' x9 by A49, A55, Def2;
y9 = y2 by A57, XTUPLE_0:1;
hence * (x,y) = 1 by A52, A53, A56, A58, XTUPLE_0:1; ::_thesis: verum
end;
end;
end;
thus ( not x <> 0 implies ex b1 being Element of REAL st b1 = 0 ) ; ::_thesis: verum
end;
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 ) )
proof
let y, z be Element of REAL ; ::_thesis: ( ( x <> 0 & * (x,y) = 1 & * (x,z) = 1 implies y = z ) & ( not x <> 0 & y = 0 & z = 0 implies y = z ) )
thus ( x <> 0 & * (x,y) = 1 & * (x,z) = 1 implies y = z ) ::_thesis: ( not x <> 0 & y = 0 & z = 0 implies y = z )
proof
assume that
A59: x <> 0 and
A60: * (x,y) = 1 and
A61: * (x,z) = 1 ; ::_thesis: y = z
A62: for x, y being Element of REAL st * (x,y) = 1 holds
x <> 0
proof
let x, y be Element of REAL ; ::_thesis: ( * (x,y) = 1 implies x <> 0 )
assume that
A63: * (x,y) = 1 and
A64: x = 0 ; ::_thesis: contradiction
A65: not x in [:{0},REAL+:] by A64, Th5, ARYTM_2:20, XBOOLE_0:3;
A66: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
percases ( y in REAL+ or y in [:{0},REAL+:] ) by A66, XBOOLE_0:def_3;
suppose y in REAL+ ; ::_thesis: contradiction
then ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 1 = x9 *' y9 ) by A63, A64, Def2, ARYTM_2:20;
hence contradiction by A64, ARYTM_2:4; ::_thesis: verum
end;
suppose y in [:{0},REAL+:] ; ::_thesis: contradiction
then not y in REAL+ by Th5, XBOOLE_0:3;
hence contradiction by A63, A64, A65, Def2; ::_thesis: verum
end;
end;
end;
then A67: y <> 0 by A60;
A68: z <> 0 by A61, A62;
percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in REAL+ ) or ( x in [:{0},REAL+:] & z in REAL+ ) or ( x in REAL+ & z in [:{0},REAL+:] ) or ( ( 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+:] ) ) or ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] or not x <> 0 ) & ( not z in REAL+ or not x in [:{0},REAL+:] or not z <> 0 ) & ( not x in [:{0},REAL+:] or not z in [:{0},REAL+:] ) ) ) ;
suppose ( x in REAL+ & y in REAL+ & z in REAL+ ) ; ::_thesis: y = z
then ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 1 = x9 *' y9 ) & ex x9, y9 being Element of REAL+ st
( x = x9 & z = y9 & 1 = x9 *' y9 ) ) by A60, A61, Def2;
hence y = z by A59, Th7; ::_thesis: verum
end;
supposethat A69: x in [:{0},REAL+:] and
A70: y in [:{0},REAL+:] and
A71: z in [:{0},REAL+:] ; ::_thesis: y = z
consider x9, y9 being Element of REAL+ such that
A72: x = [0,x9] and
A73: ( y = [0,y9] & 1 = y9 *' x9 ) by A60, A69, A70, Def2;
consider x99, z9 being Element of REAL+ such that
A74: x = [0,x99] and
A75: ( z = [0,z9] & 1 = z9 *' x99 ) by A61, A69, A71, Def2;
x9 = x99 by A72, A74, XTUPLE_0:1;
hence y = z by A72, A73, A75, Th3, Th7; ::_thesis: verum
end;
suppose ( x in REAL+ & y in [:{0},REAL+:] ) ; ::_thesis: y = z
then ex x9, y9 being Element of REAL+ st
( x = x9 & y = [0,y9] & 1 = [0,(x9 *' y9)] ) by A59, A60, Def2;
hence y = z by Lm2; ::_thesis: verum
end;
suppose ( x in [:{0},REAL+:] & y in REAL+ ) ; ::_thesis: y = z
then ex x9, y9 being Element of REAL+ st
( x = [0,x9] & y = y9 & 1 = [0,(y9 *' x9)] ) by A60, A67, Def2;
hence y = z by Lm2; ::_thesis: verum
end;
suppose ( x in [:{0},REAL+:] & z in REAL+ ) ; ::_thesis: y = z
then ex x9, z9 being Element of REAL+ st
( x = [0,x9] & z = z9 & 1 = [0,(z9 *' x9)] ) by A61, A68, Def2;
hence y = z by Lm2; ::_thesis: verum
end;
suppose ( x in REAL+ & z in [:{0},REAL+:] ) ; ::_thesis: y = z
then ex x9, z9 being Element of REAL+ st
( x = x9 & z = [0,z9] & 1 = [0,(x9 *' z9)] ) by A59, A61, Def2;
hence y = z by Lm2; ::_thesis: verum
end;
suppose ( ( 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+:] ) ) ; ::_thesis: y = z
hence y = z by A60, Def2; ::_thesis: verum
end;
suppose ( ( not x in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not z in [:{0},REAL+:] or not x <> 0 ) & ( not z in REAL+ or not x in [:{0},REAL+:] or not z <> 0 ) & ( not x in [:{0},REAL+:] or not z in [:{0},REAL+:] ) ) ; ::_thesis: y = z
hence y = z by A61, Def2; ::_thesis: verum
end;
end;
end;
thus ( not x <> 0 & y = 0 & z = 0 implies y = z ) ; ::_thesis: verum
end;
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 ) )
proof
let x, y be Element of REAL ; ::_thesis: ( ( y <> 0 implies * (y,x) = 1 ) & ( not y <> 0 implies x = 0 ) implies ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) ) )
assume that
A76: ( y <> 0 implies * (y,x) = 1 ) and
A77: ( y = 0 implies x = 0 ) ; ::_thesis: ( ( x <> 0 implies * (x,y) = 1 ) & ( not x <> 0 implies y = 0 ) )
thus ( x <> 0 implies * (x,y) = 1 ) by A76, A77; ::_thesis: ( not x <> 0 implies y = 0 )
assume A78: x = 0 ; ::_thesis: y = 0
A79: y in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
assume A80: y <> 0 ; ::_thesis: contradiction
percases ( y in REAL+ or y in [:{0},REAL+:] ) by A79, XBOOLE_0:def_3;
suppose y in REAL+ ; ::_thesis: contradiction
then ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & 1 = x9 *' y9 ) by A76, A78, A80, Def2, ARYTM_2:20;
hence contradiction by A78, ARYTM_2:4; ::_thesis: verum
end;
supposeA81: y in [:{0},REAL+:] ; ::_thesis: contradiction
A82: not x in [:{0},REAL+:] by A78, Th5, ARYTM_2:20, XBOOLE_0:3;
not y in REAL+ by A81, Th5, XBOOLE_0:3;
hence contradiction by A76, A78, A80, A82, Def2; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def3 defines opp ARYTM_0:def_3_:_
for x, b2 being Element of REAL holds
( b2 = opp x iff + (x,b2) = 0 );
:: deftheorem Def4 defines inv ARYTM_0:def_4_:_
for x, b2 being Element of REAL holds
( ( x <> 0 implies ( b2 = inv x iff * (x,b2) = 1 ) ) & ( not x <> 0 implies ( b2 = inv x iff b2 = 0 ) ) );
begin
Lm3: for x, y, z being set st [x,y] = {z} holds
( z = {x} & x = y )
proof
let x, y, z be set ; ::_thesis: ( [x,y] = {z} implies ( z = {x} & x = y ) )
assume [x,y] = {z} ; ::_thesis: ( z = {x} & x = y )
then A1: {{x,y},{x}} = {z} by TARSKI:def_5;
then {x} in {z} by TARSKI:def_2;
hence A2: z = {x} by TARSKI:def_1; ::_thesis: x = y
{x,y} in {z} by A1, TARSKI:def_2;
then {x,y} = z by TARSKI:def_1;
hence x = y by A2, ZFMISC_1:5; ::_thesis: verum
end;
theorem Th8: :: ARYTM_0:8
for a, b being Element of REAL holds not (0,1) --> (a,b) in REAL
proof
let a, b be Element of REAL ; ::_thesis: not (0,1) --> (a,b) in REAL
set IR = { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ;
set f = (0,1) --> (a,b);
A1: now__::_thesis:_not_(0,1)_-->_(a,b)_in_[:{{}},REAL+:]
(0,1) --> (a,b) = {[0,a],[1,b]} by FUNCT_4:67;
then A2: [1,b] in (0,1) --> (a,b) by TARSKI:def_2;
assume (0,1) --> (a,b) in [:{{}},REAL+:] ; ::_thesis: contradiction
then consider x, y being set such that
A3: x in {{}} and
y in REAL+ and
A4: (0,1) --> (a,b) = [x,y] by ZFMISC_1:84;
x = 0 by A3, TARSKI:def_1;
then (0,1) --> (a,b) = {{0,y},{0}} by A4, TARSKI:def_5;
then A5: ( [1,b] = {0} or [1,b] = {0,y} ) by A2, TARSKI:def_2;
percases ( {{1,b},{1}} = {0} or {{1,b},{1}} = {0,y} ) by A5, TARSKI:def_5;
suppose {{1,b},{1}} = {0} ; ::_thesis: contradiction
then 0 in {{1,b},{1}} by TARSKI:def_1;
hence contradiction by TARSKI:def_2; ::_thesis: verum
end;
suppose {{1,b},{1}} = {0,y} ; ::_thesis: contradiction
then 0 in {{1,b},{1}} by TARSKI:def_2;
hence contradiction by TARSKI:def_2; ::_thesis: verum
end;
end;
end;
A6: (0,1) --> (a,b) = {[0,a],[1,b]} by FUNCT_4:67;
now__::_thesis:_not_(0,1)_-->_(a,b)_in__{__[i,j]_where_i,_j_is_Element_of_NAT_:_(_i,j_are_relative_prime_&_j_<>_{}_)__}_
assume (0,1) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } ; ::_thesis: contradiction
then consider i, j being Element of NAT such that
A7: (0,1) --> (a,b) = [i,j] and
i,j are_relative_prime and
j <> {} ;
A8: (0,1) --> (a,b) = {{i,j},{i}} by A7, TARSKI:def_5;
then A9: ( {i} in (0,1) --> (a,b) & {i,j} in (0,1) --> (a,b) ) by TARSKI:def_2;
A10: now__::_thesis:_not_i_=_j
assume i = j ; ::_thesis: contradiction
then {i} = {i,j} by ENUMSET1:29;
then A11: [i,j] = {{i}} by A7, A8, ENUMSET1:29;
then [1,b] in {{i}} by A6, A7, TARSKI:def_2;
then A12: [1,b] = {i} by TARSKI:def_1;
[0,a] in {{i}} by A6, A7, A11, TARSKI:def_2;
then [0,a] = {i} by TARSKI:def_1;
hence contradiction by A12, XTUPLE_0:1; ::_thesis: verum
end;
A13: [1,b] = {{1,b},{1}} by TARSKI:def_5;
A14: [0,a] = {{0,a},{0}} by TARSKI:def_5;
percases ( ( {i,j} = [0,a] & {i} = [0,a] ) or ( {i,j} = [0,a] & {i} = [1,b] ) or ( {i,j} = [1,b] & {i} = [0,a] ) or ( {i,j} = [1,b] & {i} = [1,b] ) ) by A6, A9, TARSKI:def_2;
suppose ( {i,j} = [0,a] & {i} = [0,a] ) ; ::_thesis: contradiction
hence contradiction by A10, ZFMISC_1:5; ::_thesis: verum
end;
supposethat A15: {i,j} = [0,a] and
A16: {i} = [1,b] ; ::_thesis: contradiction
i in [0,a] by A15, TARSKI:def_2;
then ( i = {0,a} or i = {0} ) by A14, TARSKI:def_2;
then A17: 0 in i by TARSKI:def_1, TARSKI:def_2;
i = {1} by A16, Lm3;
hence contradiction by A17, TARSKI:def_1; ::_thesis: verum
end;
supposethat A18: {i,j} = [1,b] and
A19: {i} = [0,a] ; ::_thesis: contradiction
i in [1,b] by A18, TARSKI:def_2;
then ( i = {1,b} or i = {1} ) by A13, TARSKI:def_2;
then A20: 1 in i by TARSKI:def_1, TARSKI:def_2;
i = {0} by A19, Lm3;
hence contradiction by A20, TARSKI:def_1; ::_thesis: verum
end;
suppose ( {i,j} = [1,b] & {i} = [1,b] ) ; ::_thesis: contradiction
hence contradiction by A10, ZFMISC_1:5; ::_thesis: verum
end;
end;
end;
then A21: not (0,1) --> (a,b) in { [i,j] where i, j is Element of NAT : ( i,j are_relative_prime & j <> {} ) } \ { [k,1] where k is Element of NAT : verum } ;
for x, y being set holds not {[0,x],[1,y]} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) }
proof
given x, y being set such that A22: {[0,x],[1,y]} in { A where A is Subset of RAT+ : for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) } ; ::_thesis: contradiction
consider A being Subset of RAT+ such that
A23: {[0,x],[1,y]} = A and
A24: for r being Element of RAT+ st r in A holds
( ( for s being Element of RAT+ st s <=' r holds
s in A ) & ex s being Element of RAT+ st
( s in A & r < s ) ) by A22;
( [0,x] in A & ( for r, s being Element of RAT+ st r in A & s <=' r holds
s in A ) ) by A23, A24, TARSKI:def_2;
then consider r1, r2, r3 being Element of RAT+ such that
A25: r1 in A and
A26: r2 in A and
A27: ( r3 in A & r1 <> r2 & r2 <> r3 & r3 <> r1 ) by ARYTM_3:75;
A28: ( r2 = [0,x] or r2 = [1,y] ) by A23, A26, TARSKI:def_2;
( r1 = [0,x] or r1 = [1,y] ) by A23, A25, TARSKI:def_2;
hence contradiction by A23, A27, A28, TARSKI:def_2; ::_thesis: verum
end;
then A29: not (0,1) --> (a,b) in DEDEKIND_CUTS by A6, ARYTM_2:def_1;
now__::_thesis:_not_(0,1)_-->_(a,b)_in_omega
assume (0,1) --> (a,b) in omega ; ::_thesis: contradiction
then {} in (0,1) --> (a,b) by ORDINAL3:8;
hence contradiction by A6, TARSKI:def_2; ::_thesis: verum
end;
then not (0,1) --> (a,b) in RAT+ by A21, XBOOLE_0:def_3;
then not (0,1) --> (a,b) in REAL+ by A29, ARYTM_2:def_2, XBOOLE_0:def_3;
hence not (0,1) --> (a,b) in REAL by A1, NUMBERS:def_1, XBOOLE_0:def_3; ::_thesis: verum
end;
definition
let x, y be Element of REAL ;
func[*x,y*] -> Element of COMPLEX equals :Def5: :: ARYTM_0:def 5
x if y = 0
otherwise (0,1) --> (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,1) --> (x,y) is Element of COMPLEX ) )
proof
set z = (0,1) --> (x,y);
thus ( y = 0 implies x is Element of COMPLEX ) by NUMBERS:def_2, XBOOLE_0:def_3; ::_thesis: ( not y = 0 implies (0,1) --> (x,y) is Element of COMPLEX )
assume A1: y <> 0 ; ::_thesis: (0,1) --> (x,y) is Element of COMPLEX
A2: now__::_thesis:_not_(0,1)_-->_(x,y)_in__{__r_where_r_is_Element_of_Funcs_({0,1},REAL)_:_r_._1_=_0__}_
assume (0,1) --> (x,y) in { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 } ; ::_thesis: contradiction
then ex r being Element of Funcs ({0,1},REAL) st
( (0,1) --> (x,y) = r & r . 1 = 0 ) ;
hence contradiction by A1, FUNCT_4:63; ::_thesis: verum
end;
(0,1) --> (x,y) in Funcs ({0,1},REAL) by FUNCT_2:8;
then (0,1) --> (x,y) in (Funcs ({0,1},REAL)) \ { r where r is Element of Funcs ({0,1},REAL) : r . 1 = 0 } by A2, XBOOLE_0:def_5;
hence (0,1) --> (x,y) is Element of COMPLEX by NUMBERS:def_2, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines [* ARYTM_0:def_5_:_
for x, y being Element of REAL holds
( ( y = 0 implies [*x,y*] = x ) & ( not y = 0 implies [*x,y*] = (0,1) --> (x,y) ) );
theorem :: ARYTM_0:9
for c being Element of COMPLEX ex r, s being Element of REAL st c = [*r,s*]
proof
let c be Element of COMPLEX ; ::_thesis: ex r, s being Element of REAL st c = [*r,s*]
percases ( c in REAL or not c in REAL ) ;
suppose c in REAL ; ::_thesis: ex r, s being Element of REAL st c = [*r,s*]
then reconsider r = c, z = 0 as Element of REAL ;
take r ; ::_thesis: ex s being Element of REAL st c = [*r,s*]
take z ; ::_thesis: c = [*r,z*]
thus c = [*r,z*] by Def5; ::_thesis: verum
end;
suppose not c in REAL ; ::_thesis: ex r, s being Element of REAL st c = [*r,s*]
then A1: c in (Funcs ({0,1},REAL)) \ { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by NUMBERS:def_2, XBOOLE_0:def_3;
then consider f being Function such that
A2: c = f and
A3: dom f = {0,1} and
A4: rng f c= REAL by FUNCT_2:def_2;
1 in {0,1} by TARSKI:def_2;
then A5: f . 1 in rng f by A3, FUNCT_1:3;
0 in {0,1} by TARSKI:def_2;
then f . 0 in rng f by A3, FUNCT_1:3;
then reconsider r = f . 0, s = f . 1 as Element of REAL by A4, A5;
take r ; ::_thesis: ex s being Element of REAL st c = [*r,s*]
take s ; ::_thesis: c = [*r,s*]
A6: c = (0,1) --> (r,s) by A2, A3, FUNCT_4:66;
now__::_thesis:_not_s_=_0
assume s = 0 ; ::_thesis: contradiction
then ((0,1) --> (r,s)) . 1 = 0 by FUNCT_4:63;
then c in { x where x is Element of Funcs ({0,1},REAL) : x . 1 = 0 } by A1, A6;
hence contradiction by A1, XBOOLE_0:def_5; ::_thesis: verum
end;
hence c = [*r,s*] by A6, Def5; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_0:10
for x1, x2, y1, y2 being Element of REAL st [*x1,x2*] = [*y1,y2*] holds
( x1 = y1 & x2 = y2 )
proof
let x1, x2, y1, y2 be Element of REAL ; ::_thesis: ( [*x1,x2*] = [*y1,y2*] implies ( x1 = y1 & x2 = y2 ) )
assume A1: [*x1,x2*] = [*y1,y2*] ; ::_thesis: ( x1 = y1 & x2 = y2 )
percases ( x2 = 0 or x2 <> 0 ) ;
supposeA2: x2 = 0 ; ::_thesis: ( x1 = y1 & x2 = y2 )
then A3: [*x1,x2*] = x1 by Def5;
A4: now__::_thesis:_not_y2_<>_0
assume y2 <> 0 ; ::_thesis: contradiction
then x1 = (0,1) --> (y1,y2) by A1, A3, Def5;
hence contradiction by Th8; ::_thesis: verum
end;
hence x1 = y1 by A1, A3, Def5; ::_thesis: x2 = y2
thus x2 = y2 by A2, A4; ::_thesis: verum
end;
suppose x2 <> 0 ; ::_thesis: ( x1 = y1 & x2 = y2 )
then A5: [*y1,y2*] = (0,1) --> (x1,x2) by A1, Def5;
now__::_thesis:_not_y2_=_0
assume y2 = 0 ; ::_thesis: contradiction
then [*y1,y2*] = y1 by Def5;
hence contradiction by A5, Th8; ::_thesis: verum
end;
then [*y1,y2*] = (0,1) --> (y1,y2) by Def5;
hence ( x1 = y1 & x2 = y2 ) by A5, FUNCT_4:68; ::_thesis: verum
end;
end;
end;
set RR = [:{0},REAL+:] \ {[0,0]};
reconsider o = 0 as Element of REAL ;
theorem Th11: :: ARYTM_0:11
for x, o being Element of REAL st o = 0 holds
+ (x,o) = x
proof
reconsider y9 = 0 as Element of REAL+ by ARYTM_2:20;
let x, o be Element of REAL ; ::_thesis: ( o = 0 implies + (x,o) = x )
assume A1: o = 0 ; ::_thesis: + (x,o) = x
percases ( x in REAL+ or not x in REAL+ ) ;
suppose x in REAL+ ; ::_thesis: + (x,o) = x
then reconsider x9 = x as Element of REAL+ ;
x9 = x9 + y9 by ARYTM_2:def_8;
hence + (x,o) = x by A1, Def1; ::_thesis: verum
end;
supposeA2: not x in REAL+ ; ::_thesis: + (x,o) = x
x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
then A3: x in [:{{}},REAL+:] by A2, XBOOLE_0:def_3;
then consider x1, x2 being set such that
A4: x1 in {{}} and
A5: x2 in REAL+ and
A6: x = [x1,x2] by ZFMISC_1:84;
reconsider x9 = x2 as Element of REAL+ by A5;
A7: x1 = 0 by A4, TARSKI:def_1;
then x = y9 - x9 by A6, Th3, ARYTM_1:19;
hence + (x,o) = x by A1, A3, A6, A7, Def1; ::_thesis: verum
end;
end;
end;
theorem Th12: :: ARYTM_0:12
for x, o being Element of REAL st o = 0 holds
* (x,o) = 0
proof
let x, o be Element of REAL ; ::_thesis: ( o = 0 implies * (x,o) = 0 )
assume A1: o = 0 ; ::_thesis: * (x,o) = 0
percases ( x in REAL+ or not x in REAL+ ) ;
suppose x in REAL+ ; ::_thesis: * (x,o) = 0
then reconsider x9 = x, y9 = 0 as Element of REAL+ by ARYTM_2:20;
0 = x9 *' y9 by ARYTM_2:4;
hence * (x,o) = 0 by A1, Def2; ::_thesis: verum
end;
supposeA2: not x in REAL+ ; ::_thesis: * (x,o) = 0
not o in [:{{}},REAL+:] by A1, Th5, ARYTM_2:20, XBOOLE_0:3;
hence * (x,o) = 0 by A1, A2, Def2; ::_thesis: verum
end;
end;
end;
theorem Th13: :: ARYTM_0:13
for x, y, z being Element of REAL holds * (x,(* (y,z))) = * ((* (x,y)),z)
proof
let x, y, z be Element of REAL ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & z <> 0 ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & y <> 0 & z in REAL+ & z <> 0 ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & z <> 0 ) or ( x in REAL+ & x <> 0 & y in REAL+ & y <> 0 & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( y in REAL+ & y <> 0 & x in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or x = 0 or y = 0 or z = 0 or ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ) ;
supposethat A1: x in REAL+ and
A2: y in REAL+ and
A3: z in REAL+ ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
A4: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & * (x,y) = x99 *' y99 ) by A1, A2, Def2;
then A5: ex xy99, z99 being Element of REAL+ st
( * (x,y) = xy99 & z = z99 & * ((* (x,y)),z) = xy99 *' z99 ) by A3, Def2;
A6: ex y9, z9 being Element of REAL+ st
( y = y9 & z = z9 & * (y,z) = y9 *' z9 ) by A2, A3, Def2;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & * (y,z) = yz9 & * (x,(* (y,z))) = x9 *' yz9 ) by A1, Def2;
hence * (x,(* (y,z))) = * ((* (x,y)),z) by A6, A4, A5, ARYTM_2:12; ::_thesis: verum
end;
supposethat A7: ( x in REAL+ & x <> 0 ) and
A8: y in [:{0},REAL+:] \ {[0,0]} and
A9: ( z in REAL+ & z <> 0 ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
consider y9, z9 being Element of REAL+ such that
A10: y = [0,y9] and
A11: z = z9 and
A12: * (y,z) = [0,(z9 *' y9)] by A8, A9, Def2;
* (y,z) in [:{0},REAL+:] by A12, Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A13: x = x9 and
A14: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = [0,(x9 *' yz9)] ) by A7, Def2;
consider x99, y99 being Element of REAL+ such that
A15: x = x99 and
A16: y = [0,y99] and
A17: * (x,y) = [0,(x99 *' y99)] by A7, A8, Def2;
A18: y9 = y99 by A10, A16, XTUPLE_0:1;
* (x,y) in [:{0},REAL+:] by A17, Lm1, ZFMISC_1:87;
then consider xy99, z99 being Element of REAL+ such that
A19: * (x,y) = [0,xy99] and
A20: z = z99 and
A21: * ((* (x,y)),z) = [0,(z99 *' xy99)] by A9, Def2;
thus * (x,(* (y,z))) = [0,(x9 *' (y9 *' z9))] by A12, A14, XTUPLE_0:1
.= [0,((x99 *' y99) *' z99)] by A11, A13, A15, A20, A18, ARYTM_2:12
.= * ((* (x,y)),z) by A17, A19, A21, XTUPLE_0:1 ; ::_thesis: verum
end;
supposethat A22: x in [:{0},REAL+:] \ {[0,0]} and
A23: ( y in REAL+ & y <> 0 ) and
A24: ( z in REAL+ & z <> 0 ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
consider y9, z9 being Element of REAL+ such that
A25: ( y = y9 & z = z9 ) and
A26: * (y,z) = y9 *' z9 by A23, A24, Def2;
y9 *' z9 <> 0 by A23, A24, A25, ARYTM_1:2;
then consider x9, yz9 being Element of REAL+ such that
A27: x = [0,x9] and
A28: ( * (y,z) = yz9 & * (x,(* (y,z))) = [0,(yz9 *' x9)] ) by A22, A26, Def2;
consider x99, y99 being Element of REAL+ such that
A29: x = [0,x99] and
A30: y = y99 and
A31: * (x,y) = [0,(y99 *' x99)] by A22, A23, Def2;
* (x,y) in [:{0},REAL+:] by A31, Lm1, ZFMISC_1:87;
then consider xy99, z99 being Element of REAL+ such that
A32: * (x,y) = [0,xy99] and
A33: z = z99 and
A34: * ((* (x,y)),z) = [0,(z99 *' xy99)] by A24, Def2;
x9 = x99 by A27, A29, XTUPLE_0:1;
hence * (x,(* (y,z))) = [0,((x99 *' y99) *' z99)] by A25, A26, A28, A30, A33, ARYTM_2:12
.= * ((* (x,y)),z) by A31, A32, A34, XTUPLE_0:1 ;
::_thesis: verum
end;
supposethat A35: x in [:{0},REAL+:] \ {[0,0]} and
A36: y in [:{0},REAL+:] \ {[0,0]} and
A37: ( z in REAL+ & z <> 0 ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
consider x99, y99 being Element of REAL+ such that
A38: x = [0,x99] and
A39: y = [0,y99] and
A40: * (x,y) = y99 *' x99 by A35, A36, Def2;
consider y9, z9 being Element of REAL+ such that
A41: y = [0,y9] and
A42: z = z9 and
A43: * (y,z) = [0,(z9 *' y9)] by A36, A37, Def2;
A44: y9 = y99 by A41, A39, XTUPLE_0:1;
* (y,z) in [:{0},REAL+:] by A43, Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A45: x = [0,x9] and
A46: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = yz9 *' x9 ) by A35, Def2;
A47: x9 = x99 by A45, A38, XTUPLE_0:1;
A48: ex xy99, z99 being Element of REAL+ st
( * (x,y) = xy99 & z = z99 & * ((* (x,y)),z) = xy99 *' z99 ) by A37, A40, Def2;
thus * (x,(* (y,z))) = x9 *' (y9 *' z9) by A43, A46, XTUPLE_0:1
.= * ((* (x,y)),z) by A42, A40, A48, A47, A44, ARYTM_2:12 ; ::_thesis: verum
end;
supposethat A49: ( x in REAL+ & x <> 0 ) and
A50: ( y in REAL+ & y <> 0 ) and
A51: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
A52: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & * (x,y) = x99 *' y99 ) by A49, A50, Def2;
then * (x,y) <> 0 by A49, A50, ARYTM_1:2;
then consider xy99, z99 being Element of REAL+ such that
A53: * (x,y) = xy99 and
A54: z = [0,z99] and
A55: * ((* (x,y)),z) = [0,(xy99 *' z99)] by A51, A52, Def2;
consider y9, z9 being Element of REAL+ such that
A56: y = y9 and
A57: z = [0,z9] and
A58: * (y,z) = [0,(y9 *' z9)] by A50, A51, Def2;
A59: z9 = z99 by A57, A54, XTUPLE_0:1;
* (y,z) in [:{0},REAL+:] by A58, Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A60: x = x9 and
A61: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = [0,(x9 *' yz9)] ) by A49, Def2;
thus * (x,(* (y,z))) = [0,(x9 *' (y9 *' z9))] by A58, A61, XTUPLE_0:1
.= * ((* (x,y)),z) by A56, A60, A52, A53, A55, A59, ARYTM_2:12 ; ::_thesis: verum
end;
supposethat A62: ( x in REAL+ & x <> 0 ) and
A63: y in [:{0},REAL+:] \ {[0,0]} and
A64: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
consider y9, z9 being Element of REAL+ such that
A65: y = [0,y9] and
A66: z = [0,z9] and
A67: * (y,z) = z9 *' y9 by A63, A64, Def2;
A68: ex x9, yz9 being Element of REAL+ st
( x = x9 & * (y,z) = yz9 & * (x,(* (y,z))) = x9 *' yz9 ) by A62, A67, Def2;
consider x99, y99 being Element of REAL+ such that
A69: x = x99 and
A70: y = [0,y99] and
A71: * (x,y) = [0,(x99 *' y99)] by A62, A63, Def2;
A72: y9 = y99 by A65, A70, XTUPLE_0:1;
* (x,y) in [:{0},REAL+:] by A71, Lm1, ZFMISC_1:87;
then consider xy99, z99 being Element of REAL+ such that
A73: * (x,y) = [0,xy99] and
A74: z = [0,z99] and
A75: * ((* (x,y)),z) = z99 *' xy99 by A64, Def2;
z9 = z99 by A66, A74, XTUPLE_0:1;
hence * (x,(* (y,z))) = (x99 *' y99) *' z99 by A67, A68, A69, A72, ARYTM_2:12
.= * ((* (x,y)),z) by A71, A73, A75, XTUPLE_0:1 ;
::_thesis: verum
end;
supposethat A76: ( y in REAL+ & y <> 0 ) and
A77: x in [:{0},REAL+:] \ {[0,0]} and
A78: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
consider x99, y99 being Element of REAL+ such that
A79: x = [0,x99] and
A80: y = y99 and
A81: * (x,y) = [0,(y99 *' x99)] by A76, A77, Def2;
consider y9, z9 being Element of REAL+ such that
A82: y = y9 and
A83: z = [0,z9] and
A84: * (y,z) = [0,(y9 *' z9)] by A76, A78, Def2;
[0,(y9 *' z9)] in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A85: x = [0,x9] and
A86: ( * (y,z) = [0,yz9] & * (x,(* (y,z))) = yz9 *' x9 ) by A77, A84, Def2;
A87: x9 = x99 by A85, A79, XTUPLE_0:1;
* (x,y) in [:{0},REAL+:] by A81, Lm1, ZFMISC_1:87;
then consider xy99, z99 being Element of REAL+ such that
A88: * (x,y) = [0,xy99] and
A89: z = [0,z99] and
A90: * ((* (x,y)),z) = z99 *' xy99 by A78, Def2;
A91: z9 = z99 by A83, A89, XTUPLE_0:1;
thus * (x,(* (y,z))) = x9 *' (y9 *' z9) by A84, A86, XTUPLE_0:1
.= (x99 *' y99) *' z99 by A82, A80, A87, A91, ARYTM_2:12
.= * ((* (x,y)),z) by A81, A88, A90, XTUPLE_0:1 ; ::_thesis: verum
end;
supposethat A92: x in [:{0},REAL+:] \ {[0,0]} and
A93: y in [:{0},REAL+:] \ {[0,0]} and
A94: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
consider y9, z9 being Element of REAL+ such that
A95: y = [0,y9] and
A96: z = [0,z9] and
A97: * (y,z) = z9 *' y9 by A93, A94, Def2;
not y in {[0,0]} by A93, XBOOLE_0:def_5;
then A98: y9 <> 0 by A95, TARSKI:def_1;
not z in {[0,0]} by A94, XBOOLE_0:def_5;
then z9 <> 0 by A96, TARSKI:def_1;
then * (z,y) <> 0 by A97, A98, ARYTM_1:2;
then consider x9, yz9 being Element of REAL+ such that
A99: x = [0,x9] and
A100: ( * (y,z) = yz9 & * (x,(* (y,z))) = [0,(yz9 *' x9)] ) by A92, A97, Def2;
consider x99, y99 being Element of REAL+ such that
A101: x = [0,x99] and
A102: y = [0,y99] and
A103: * (x,y) = y99 *' x99 by A92, A93, Def2;
A104: x9 = x99 by A99, A101, XTUPLE_0:1;
A105: y9 = y99 by A95, A102, XTUPLE_0:1;
not y in {[0,0]} by A93, XBOOLE_0:def_5;
then A106: y9 <> 0 by A95, TARSKI:def_1;
not x in {[0,0]} by A92, XBOOLE_0:def_5;
then x9 <> 0 by A99, TARSKI:def_1;
then * (x,y) <> 0 by A103, A104, A105, A106, ARYTM_1:2;
then consider xy99, z99 being Element of REAL+ such that
A107: * (x,y) = xy99 and
A108: z = [0,z99] and
A109: * ((* (x,y)),z) = [0,(xy99 *' z99)] by A94, A103, Def2;
z9 = z99 by A96, A108, XTUPLE_0:1;
hence * (x,(* (y,z))) = * ((* (x,y)),z) by A97, A100, A103, A104, A105, A107, A109, ARYTM_2:12; ::_thesis: verum
end;
supposeA110: x = 0 ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
hence * (x,(* (y,z))) = 0 by Th12
.= * (o,z) by Th12
.= * ((* (x,y)),z) by A110, Th12 ;
::_thesis: verum
end;
supposeA111: y = 0 ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
hence * (x,(* (y,z))) = * (x,o) by Th12
.= 0 by Th12
.= * (o,z) by Th12
.= * ((* (x,y)),z) by A111, Th12 ;
::_thesis: verum
end;
supposeA112: z = 0 ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
hence * (x,(* (y,z))) = * (x,o) by Th12
.= 0 by Th12
.= * ((* (x,y)),z) by A112, Th12 ;
::_thesis: verum
end;
supposeA113: ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not y in REAL+ or not x in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ; ::_thesis: * (x,(* (y,z))) = * ((* (x,y)),z)
A114: not [0,0] in REAL+ by ARYTM_2:3;
REAL = (REAL+ \ {[{},{}]}) \/ ([:{{}},REAL+:] \ {[{},{}]}) by NUMBERS:def_1, XBOOLE_1:42
.= REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) by A114, ZFMISC_1:57 ;
hence * (x,(* (y,z))) = * ((* (x,y)),z) by A113, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
theorem Th14: :: ARYTM_0:14
for x, y, z being Element of REAL holds * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
proof
let x, y, z be Element of REAL ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
percases ( x = 0 or ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & x <> 0 & y in REAL+ & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & z in REAL+ & y in [:{0},REAL+:] \ {[0,0]} ) or ( x in REAL+ & x <> 0 & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & z in REAL+ ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in REAL+ & z in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & z in REAL+ & y in [:{0},REAL+:] \ {[0,0]} ) or ( x in [:{0},REAL+:] \ {[0,0]} & y in [:{0},REAL+:] \ {[0,0]} & z in [:{0},REAL+:] \ {[0,0]} ) or ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ) ;
supposeA1: x = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
hence * (x,(+ (y,z))) = 0 by Th12
.= + (o,o) by Th11
.= + ((* (x,y)),o) by A1, Th12
.= + ((* (x,y)),(* (x,z))) by A1, Th12 ;
::_thesis: verum
end;
supposethat A2: x in REAL+ and
A3: ( y in REAL+ & z in REAL+ ) ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
A4: ( ex x9, y9 being Element of REAL+ st
( x = x9 & y = y9 & * (x,y) = x9 *' y9 ) & ex x99, z9 being Element of REAL+ st
( x = x99 & z = z9 & * (x,z) = x99 *' z9 ) ) by A2, A3, Def2;
then A5: ex xy9, xz9 being Element of REAL+ st
( * (x,y) = xy9 & * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xy9 + xz9 ) by Def1;
A6: ex y99, z99 being Element of REAL+ st
( y = y99 & z = z99 & + (y,z) = y99 + z99 ) by A3, Def1;
then ex x999, yz9 being Element of REAL+ st
( x = x999 & + (y,z) = yz9 & * (x,(+ (y,z))) = x999 *' yz9 ) by A2, Def2;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) by A4, A5, A6, ARYTM_2:13; ::_thesis: verum
end;
supposethat A7: ( x in REAL+ & x <> 0 ) and
A8: y in REAL+ and
A9: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
consider y99, z99 being Element of REAL+ such that
A10: y = y99 and
A11: z = [0,z99] and
A12: + (y,z) = y99 - z99 by A8, A9, Def1;
consider x9, y9 being Element of REAL+ such that
A13: ( x = x9 & y = y9 ) and
A14: * (x,y) = x9 *' y9 by A7, A8, Def2;
consider x99, z9 being Element of REAL+ such that
A15: x = x99 and
A16: z = [0,z9] and
A17: * (x,z) = [0,(x99 *' z9)] by A7, A9, Def2;
* (x,z) in [:{0},REAL+:] by A17, Lm1, ZFMISC_1:87;
then A18: ex xy9, xz9 being Element of REAL+ st
( * (x,y) = xy9 & * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = xy9 - xz9 ) by A14, Def1;
A19: z9 = z99 by A16, A11, XTUPLE_0:1;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( z99 <=' y99 or not z99 <=' y99 ) ;
supposeA20: z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A21: + (y,z) = y99 -' z99 by A12, ARYTM_1:def_2;
then ex x999, yz9 being Element of REAL+ st
( x = x999 & + (y,z) = yz9 & * (x,(+ (y,z))) = x999 *' yz9 ) by A7, Def2;
hence * (x,(+ (y,z))) = (x9 *' y9) - (x99 *' z9) by A13, A15, A10, A19, A20, A21, ARYTM_1:26
.= + ((* (x,y)),(* (x,z))) by A14, A17, A18, XTUPLE_0:1 ;
::_thesis: verum
end;
supposeA22: not z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A23: + (y,z) = [0,(z99 -' y99)] by A12, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x999, yz9 being Element of REAL+ such that
A24: x = x999 and
A25: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = [0,(x999 *' yz9)] ) by A7, Def2;
thus * (x,(+ (y,z))) = [0,(x999 *' (z99 -' y99))] by A23, A25, XTUPLE_0:1
.= (x9 *' y9) - (x99 *' z9) by A7, A13, A15, A10, A19, A22, A24, ARYTM_1:27
.= + ((* (x,y)),(* (x,z))) by A14, A17, A18, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposethat A26: ( x in REAL+ & x <> 0 ) and
A27: z in REAL+ and
A28: y in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
consider z99, y99 being Element of REAL+ such that
A29: z = z99 and
A30: y = [0,y99] and
A31: + (z,y) = z99 - y99 by A27, A28, Def1;
consider x9, z9 being Element of REAL+ such that
A32: ( x = x9 & z = z9 ) and
A33: * (x,z) = x9 *' z9 by A26, A27, Def2;
consider x99, y9 being Element of REAL+ such that
A34: x = x99 and
A35: y = [0,y9] and
A36: * (x,y) = [0,(x99 *' y9)] by A26, A28, Def2;
* (x,y) in [:{0},REAL+:] by A36, Lm1, ZFMISC_1:87;
then A37: ex xz9, xy9 being Element of REAL+ st
( * (x,z) = xz9 & * (x,y) = [0,xy9] & + ((* (x,z)),(* (x,y))) = xz9 - xy9 ) by A33, Def1;
A38: y9 = y99 by A35, A30, XTUPLE_0:1;
now__::_thesis:_*_(x,(+_(z,y)))_=_+_((*_(x,z)),(*_(x,y)))
percases ( y99 <=' z99 or not y99 <=' z99 ) ;
supposeA39: y99 <=' z99 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))
then A40: + (z,y) = z99 -' y99 by A31, ARYTM_1:def_2;
then ex x999, zy9 being Element of REAL+ st
( x = x999 & + (z,y) = zy9 & * (x,(+ (z,y))) = x999 *' zy9 ) by A26, Def2;
hence * (x,(+ (z,y))) = (x9 *' z9) - (x99 *' y9) by A32, A34, A29, A38, A39, A40, ARYTM_1:26
.= + ((* (x,z)),(* (x,y))) by A33, A36, A37, XTUPLE_0:1 ;
::_thesis: verum
end;
supposeA41: not y99 <=' z99 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))
then A42: + (z,y) = [0,(y99 -' z99)] by A31, ARYTM_1:def_2;
then + (z,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x999, zy9 being Element of REAL+ such that
A43: x = x999 and
A44: ( + (z,y) = [0,zy9] & * (x,(+ (z,y))) = [0,(x999 *' zy9)] ) by A26, Def2;
thus * (x,(+ (z,y))) = [0,(x999 *' (y99 -' z99))] by A42, A44, XTUPLE_0:1
.= (x9 *' z9) - (x99 *' y9) by A26, A32, A34, A29, A38, A41, A43, ARYTM_1:27
.= + ((* (x,z)),(* (x,y))) by A33, A36, A37, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposethat A45: ( x in REAL+ & x <> 0 ) and
A46: y in [:{0},REAL+:] \ {[0,0]} and
A47: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
( ( not y in REAL+ or not z in [:{0},REAL+:] ) & ( not y in [:{0},REAL+:] or not z in REAL+ ) ) by A46, A47, Th5, XBOOLE_0:3;
then consider y99, z99 being Element of REAL+ such that
A48: y = [0,y99] and
A49: z = [0,z99] and
A50: + (y,z) = [0,(y99 + z99)] by A46, Def1;
+ (y,z) in [:{0},REAL+:] by A50, Lm1, ZFMISC_1:87;
then consider x999, yz9 being Element of REAL+ such that
A51: x = x999 and
A52: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = [0,(x999 *' yz9)] ) by A45, Def2;
consider x9, y9 being Element of REAL+ such that
A53: x = x9 and
A54: y = [0,y9] and
A55: * (x,y) = [0,(x9 *' y9)] by A45, A46, Def2;
A56: y9 = y99 by A54, A48, XTUPLE_0:1;
consider x99, z9 being Element of REAL+ such that
A57: x = x99 and
A58: z = [0,z9] and
A59: * (x,z) = [0,(x99 *' z9)] by A45, A47, Def2;
* (x,z) in [:{0},REAL+:] by A59, Lm1, ZFMISC_1:87;
then A60: ( not * (x,y) in [:{0},REAL+:] or not * (x,z) in REAL+ ) by Th5, XBOOLE_0:3;
* (x,y) in [:{0},REAL+:] by A55, Lm1, ZFMISC_1:87;
then ( not * (x,y) in REAL+ or not * (x,z) in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy9, xz9 being Element of REAL+ such that
A61: * (x,y) = [0,xy9] and
A62: ( * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = [0,(xy9 + xz9)] ) by A55, A60, Def1, Lm1, ZFMISC_1:87;
A63: xy9 = x9 *' y9 by A55, A61, XTUPLE_0:1;
A64: z9 = z99 by A58, A49, XTUPLE_0:1;
thus * (x,(+ (y,z))) = [0,(x999 *' (y99 + z99))] by A50, A52, XTUPLE_0:1
.= [0,((x9 *' y9) + (x9 *' z9))] by A53, A51, A56, A64, ARYTM_2:13
.= + ((* (x,y)),(* (x,z))) by A53, A57, A59, A62, A63, XTUPLE_0:1 ; ::_thesis: verum
end;
supposethat A65: x in [:{0},REAL+:] \ {[0,0]} and
A66: y in REAL+ and
A67: z in REAL+ ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
consider y99, z99 being Element of REAL+ such that
A68: y = y99 and
A69: z = z99 and
A70: + (y,z) = y99 + z99 by A66, A67, Def1;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( ( y <> 0 & z <> 0 ) or x = 0 or z = 0 or y = 0 ) ;
supposethat A71: y <> 0 and
A72: z <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
consider x99, z9 being Element of REAL+ such that
A73: x = [0,x99] and
A74: z = z9 and
A75: * (x,z) = [0,(z9 *' x99)] by A65, A67, A72, Def2;
y99 + z99 <> 0 by A69, A72, ARYTM_2:5;
then consider x999, yz9 being Element of REAL+ such that
A76: x = [0,x999] and
A77: ( + (y,z) = yz9 & * (x,(+ (y,z))) = [0,(yz9 *' x999)] ) by A65, A70, Def2;
consider x9, y9 being Element of REAL+ such that
A78: x = [0,x9] and
A79: y = y9 and
A80: * (x,y) = [0,(y9 *' x9)] by A65, A66, A71, Def2;
A81: x99 = x999 by A73, A76, XTUPLE_0:1;
* (x,z) in [:{0},REAL+:] by A75, Lm1, ZFMISC_1:87;
then A82: ( not * (x,y) in [:{0},REAL+:] or not * (x,z) in REAL+ ) by Th5, XBOOLE_0:3;
* (x,y) in [:{0},REAL+:] by A80, Lm1, ZFMISC_1:87;
then ( not * (x,y) in REAL+ or not * (x,z) in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy9, xz9 being Element of REAL+ such that
A83: * (x,y) = [0,xy9] and
A84: ( * (x,z) = [0,xz9] & + ((* (x,y)),(* (x,z))) = [0,(xy9 + xz9)] ) by A80, A82, Def1, Lm1, ZFMISC_1:87;
A85: xy9 = x9 *' y9 by A80, A83, XTUPLE_0:1;
x9 = x99 by A78, A73, XTUPLE_0:1;
hence * (x,(+ (y,z))) = [0,((x9 *' y9) + (x99 *' z9))] by A68, A69, A70, A79, A74, A77, A81, ARYTM_2:13
.= + ((* (x,y)),(* (x,z))) by A75, A84, A85, XTUPLE_0:1 ;
::_thesis: verum
end;
supposeA86: x = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
hence * (x,(+ (y,z))) = 0 by Th12
.= + (o,o) by Th11
.= + ((* (x,y)),o) by A86, Th12
.= + ((* (x,y)),(* (x,z))) by A86, Th12 ;
::_thesis: verum
end;
supposeA87: z = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
hence * (x,(+ (y,z))) = * (x,y) by Th11
.= + ((* (x,y)),(* (x,z))) by A87, Th11, Th12 ;
::_thesis: verum
end;
supposeA88: y = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
hence * (x,(+ (y,z))) = * (x,z) by Th11
.= + ((* (x,y)),(* (x,z))) by A88, Th11, Th12 ;
::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposethat A89: x in [:{0},REAL+:] \ {[0,0]} and
A90: y in REAL+ and
A91: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
consider x99, z9 being Element of REAL+ such that
A92: x = [0,x99] and
A93: z = [0,z9] and
A94: * (x,z) = z9 *' x99 by A89, A91, Def2;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( y <> 0 or y = 0 ) ;
suppose y <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then consider x9, y9 being Element of REAL+ such that
A95: x = [0,x9] and
A96: y = y9 and
A97: * (x,y) = [0,(y9 *' x9)] by A89, A90, Def2;
* (x,y) in [:{0},REAL+:] by A97, Lm1, ZFMISC_1:87;
then consider xy9, xz9 being Element of REAL+ such that
A98: * (x,y) = [0,xy9] and
A99: ( * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xz9 - xy9 ) by A94, Def1;
consider y99, z99 being Element of REAL+ such that
A100: y = y99 and
A101: z = [0,z99] and
A102: + (y,z) = y99 - z99 by A91, A96, Def1;
A103: z9 = z99 by A93, A101, XTUPLE_0:1;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( z99 <=' y99 or not z99 <=' y99 ) ;
supposeA104: z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A105: + (y,z) = y99 -' z99 by A102, ARYTM_1:def_2;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( + (y,z) <> 0 or + (y,z) = 0 ) ;
supposeA106: + (y,z) <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then consider x999, yz9 being Element of REAL+ such that
A107: x = [0,x999] and
A108: ( + (y,z) = yz9 & * (x,(+ (y,z))) = [0,(yz9 *' x999)] ) by A89, A105, Def2;
not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5;
then A109: x999 <> 0 by A107, TARSKI:def_1;
A110: z9 = z99 by A93, A101, XTUPLE_0:1;
A111: x9 = x99 by A92, A95, XTUPLE_0:1;
x99 = x999 by A92, A107, XTUPLE_0:1;
hence * (x,(+ (y,z))) = (x9 *' z9) - (x9 *' y9) by A96, A100, A104, A105, A106, A108, A111, A110, A109, ARYTM_1:28
.= + ((* (x,y)),(* (x,z))) by A94, A97, A98, A99, A111, XTUPLE_0:1 ;
::_thesis: verum
end;
supposeA112: + (y,z) = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A113: y99 = z99 by A104, A105, ARYTM_1:10;
A114: ( xy9 = x9 *' y9 & x9 = x99 ) by A92, A95, A97, A98, XTUPLE_0:1;
thus * (x,(+ (y,z))) = 0 by A112, Th12
.= + ((* (x,y)),(* (x,z))) by A94, A96, A100, A99, A103, A113, A114, ARYTM_1:18 ; ::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposeA115: not z99 <=' y99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A116: + (y,z) = [0,(z99 -' y99)] by A102, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x999, yz9 being Element of REAL+ such that
A117: x = [0,x999] and
A118: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = yz9 *' x999 ) by A89, Def2;
A119: x99 = x999 by A92, A117, XTUPLE_0:1;
A120: x9 = x99 by A92, A95, XTUPLE_0:1;
thus * (x,(+ (y,z))) = x999 *' (z99 -' y99) by A116, A118, XTUPLE_0:1
.= (x99 *' z9) - (x9 *' y9) by A96, A100, A103, A115, A120, A119, ARYTM_1:26
.= + ((* (x,y)),(* (x,z))) by A94, A97, A98, A99, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposeA121: y = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
hence * (x,(+ (y,z))) = * (x,z) by Th11
.= + ((* (x,y)),(* (x,z))) by A121, Th11, Th12 ;
::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposethat A122: x in [:{0},REAL+:] \ {[0,0]} and
A123: z in REAL+ and
A124: y in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
consider x99, y9 being Element of REAL+ such that
A125: x = [0,x99] and
A126: y = [0,y9] and
A127: * (x,y) = y9 *' x99 by A122, A124, Def2;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( z <> 0 or z = 0 ) ;
suppose z <> 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then consider x9, z9 being Element of REAL+ such that
A128: x = [0,x9] and
A129: z = z9 and
A130: * (x,z) = [0,(z9 *' x9)] by A122, A123, Def2;
* (x,z) in [:{0},REAL+:] by A130, Lm1, ZFMISC_1:87;
then consider xz9, xy9 being Element of REAL+ such that
A131: * (x,z) = [0,xz9] and
A132: ( * (x,y) = xy9 & + ((* (x,z)),(* (x,y))) = xy9 - xz9 ) by A127, Def1;
consider z99, y99 being Element of REAL+ such that
A133: z = z99 and
A134: y = [0,y99] and
A135: + (z,y) = z99 - y99 by A124, A129, Def1;
A136: y9 = y99 by A126, A134, XTUPLE_0:1;
now__::_thesis:_*_(x,(+_(y,z)))_=_+_((*_(x,y)),(*_(x,z)))
percases ( y99 <=' z99 or not y99 <=' z99 ) ;
supposeA137: y99 <=' z99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A138: + (z,y) = z99 -' y99 by A135, ARYTM_1:def_2;
now__::_thesis:_*_(x,(+_(z,y)))_=_+_((*_(x,z)),(*_(x,y)))
percases ( + (z,y) <> 0 or + (z,y) = 0 ) ;
supposeA139: + (z,y) <> 0 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))
then consider x999, zy9 being Element of REAL+ such that
A140: x = [0,x999] and
A141: ( + (z,y) = zy9 & * (x,(+ (z,y))) = [0,(zy9 *' x999)] ) by A122, A138, Def2;
not x in {[0,0]} by NUMBERS:def_1, XBOOLE_0:def_5;
then A142: x999 <> 0 by A140, TARSKI:def_1;
A143: y9 = y99 by A126, A134, XTUPLE_0:1;
A144: x9 = x99 by A125, A128, XTUPLE_0:1;
x99 = x999 by A125, A140, XTUPLE_0:1;
hence * (x,(+ (z,y))) = (x9 *' y9) - (x9 *' z9) by A129, A133, A137, A138, A139, A141, A144, A143, A142, ARYTM_1:28
.= + ((* (x,z)),(* (x,y))) by A127, A130, A131, A132, A144, XTUPLE_0:1 ;
::_thesis: verum
end;
supposeA145: + (z,y) = 0 ; ::_thesis: * (x,(+ (z,y))) = + ((* (x,z)),(* (x,y)))
then A146: z99 = y99 by A137, A138, ARYTM_1:10;
A147: ( xz9 = x9 *' z9 & x9 = x99 ) by A125, A128, A130, A131, XTUPLE_0:1;
thus * (x,(+ (z,y))) = 0 by A145, Th12
.= + ((* (x,z)),(* (x,y))) by A127, A129, A133, A132, A136, A146, A147, ARYTM_1:18 ; ::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposeA148: not y99 <=' z99 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
then A149: + (z,y) = [0,(y99 -' z99)] by A135, ARYTM_1:def_2;
then + (z,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x999, zy9 being Element of REAL+ such that
A150: x = [0,x999] and
A151: ( + (z,y) = [0,zy9] & * (x,(+ (z,y))) = zy9 *' x999 ) by A122, Def2;
A152: x99 = x999 by A125, A150, XTUPLE_0:1;
A153: x9 = x99 by A125, A128, XTUPLE_0:1;
thus * (x,(+ (y,z))) = x999 *' (y99 -' z99) by A149, A151, XTUPLE_0:1
.= (x99 *' y9) - (x9 *' z9) by A129, A133, A136, A148, A153, A152, ARYTM_1:26
.= + ((* (x,y)),(* (x,z))) by A127, A130, A131, A132, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposeA154: z = 0 ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
hence * (x,(+ (y,z))) = * (x,y) by Th11
.= + ((* (x,y)),(* (x,z))) by A154, Th11, Th12 ;
::_thesis: verum
end;
end;
end;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) ; ::_thesis: verum
end;
supposethat A155: x in [:{0},REAL+:] \ {[0,0]} and
A156: y in [:{0},REAL+:] \ {[0,0]} and
A157: z in [:{0},REAL+:] \ {[0,0]} ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
( ( not y in REAL+ or not z in [:{0},REAL+:] ) & ( not y in [:{0},REAL+:] or not z in REAL+ ) ) by A156, A157, Th5, XBOOLE_0:3;
then consider y99, z99 being Element of REAL+ such that
A158: y = [0,y99] and
A159: z = [0,z99] and
A160: + (y,z) = [0,(y99 + z99)] by A156, Def1;
consider x99, z9 being Element of REAL+ such that
A161: x = [0,x99] and
A162: z = [0,z9] and
A163: * (x,z) = z9 *' x99 by A155, A157, Def2;
A164: z9 = z99 by A162, A159, XTUPLE_0:1;
consider x9, y9 being Element of REAL+ such that
A165: x = [0,x9] and
A166: y = [0,y9] and
A167: * (x,y) = y9 *' x9 by A155, A156, Def2;
A168: y9 = y99 by A166, A158, XTUPLE_0:1;
+ (y,z) in [:{0},REAL+:] by A160, Lm1, ZFMISC_1:87;
then consider x999, yz9 being Element of REAL+ such that
A169: x = [0,x999] and
A170: ( + (y,z) = [0,yz9] & * (x,(+ (y,z))) = yz9 *' x999 ) by A155, Def2;
A171: x9 = x999 by A165, A169, XTUPLE_0:1;
A172: ( ex xy9, xz9 being Element of REAL+ st
( * (x,y) = xy9 & * (x,z) = xz9 & + ((* (x,y)),(* (x,z))) = xy9 + xz9 ) & x9 = x99 ) by A165, A167, A161, A163, Def1, XTUPLE_0:1;
thus * (x,(+ (y,z))) = x999 *' (y99 + z99) by A160, A170, XTUPLE_0:1
.= + ((* (x,y)),(* (x,z))) by A167, A163, A172, A171, A168, A164, ARYTM_2:13 ; ::_thesis: verum
end;
supposeA173: ( ( not x in REAL+ or not y in REAL+ or not z in REAL+ ) & ( not x in REAL+ or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in REAL+ or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in REAL+ or not z in [:{0},REAL+:] \ {[0,0]} ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in REAL+ ) & ( not x in [:{0},REAL+:] \ {[0,0]} or not y in [:{0},REAL+:] \ {[0,0]} or not z in [:{0},REAL+:] \ {[0,0]} ) ) ; ::_thesis: * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z)))
A174: not [0,0] in REAL+ by ARYTM_2:3;
REAL = (REAL+ \ {[0,0]}) \/ ([:{0},REAL+:] \ {[0,0]}) by NUMBERS:def_1, XBOOLE_1:42
.= REAL+ \/ ([:{0},REAL+:] \ {[0,0]}) by A174, ZFMISC_1:57 ;
hence * (x,(+ (y,z))) = + ((* (x,y)),(* (x,z))) by A173, XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_0:15
for x, y being Element of REAL holds * ((opp x),y) = opp (* (x,y))
proof
let x, y be Element of REAL ; ::_thesis: * ((opp x),y) = opp (* (x,y))
+ ((* ((opp x),y)),(* (x,y))) = * ((+ ((opp x),x)),y) by Th14
.= * (o,y) by Def3
.= 0 by Th12 ;
hence * ((opp x),y) = opp (* (x,y)) by Def3; ::_thesis: verum
end;
theorem Th16: :: ARYTM_0:16
for x being Element of REAL holds * (x,x) in REAL+
proof
let x be Element of REAL ; ::_thesis: * (x,x) in REAL+
A1: x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
percases ( x in REAL+ or x in [:{0},REAL+:] ) by A1, XBOOLE_0:def_3;
suppose x in REAL+ ; ::_thesis: * (x,x) in REAL+
then ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & * (x,x) = x9 *' y9 ) by Def2;
hence * (x,x) in REAL+ ; ::_thesis: verum
end;
suppose x in [:{0},REAL+:] ; ::_thesis: * (x,x) in REAL+
then ex x9, y9 being Element of REAL+ st
( x = [0,x9] & x = [0,y9] & * (x,x) = y9 *' x9 ) by Def2;
hence * (x,x) in REAL+ ; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_0:17
for x, y being Element of REAL st + ((* (x,x)),(* (y,y))) = 0 holds
x = 0
proof
let x, y be Element of REAL ; ::_thesis: ( + ((* (x,x)),(* (y,y))) = 0 implies x = 0 )
assume A1: + ((* (x,x)),(* (y,y))) = 0 ; ::_thesis: x = 0
( * (x,x) in REAL+ & * (y,y) in REAL+ ) by Th16;
then consider x9, y9 being Element of REAL+ such that
A2: * (x,x) = x9 and
* (y,y) = y9 and
A3: 0 = x9 + y9 by A1, Def1;
A4: x9 = 0 by A3, ARYTM_2:5;
A5: x in REAL+ \/ [:{{}},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
percases ( x in REAL+ or x in [:{0},REAL+:] ) by A5, XBOOLE_0:def_3;
suppose x in REAL+ ; ::_thesis: x = 0
then ex x9, y9 being Element of REAL+ st
( x = x9 & x = y9 & 0 = x9 *' y9 ) by A2, A4, Def2;
hence x = 0 by ARYTM_1:2; ::_thesis: verum
end;
suppose x in [:{0},REAL+:] ; ::_thesis: x = 0
then consider x9, y9 being Element of REAL+ such that
A6: x = [0,x9] and
A7: x = [0,y9] and
A8: 0 = y9 *' x9 by A2, A4, Def2;
x9 = y9 by A6, A7, XTUPLE_0:1;
then x9 = 0 by A8, ARYTM_1:2;
then x in {[0,0]} by A6, TARSKI:def_1;
hence x = 0 by NUMBERS:def_1, XBOOLE_0:def_5; ::_thesis: verum
end;
end;
end;
theorem Th18: :: ARYTM_0:18
for x, y, z being Element of REAL st x <> 0 & * (x,y) = 1 & * (x,z) = 1 holds
y = z
proof
let x, y, z be Element of REAL ; ::_thesis: ( x <> 0 & * (x,y) = 1 & * (x,z) = 1 implies y = z )
assume that
A1: x <> 0 and
A2: * (x,y) = 1 and
A3: * (x,z) = 1 ; ::_thesis: y = z
thus y = inv x by A1, A2, Def4
.= z by A1, A3, Def4 ; ::_thesis: verum
end;
theorem Th19: :: ARYTM_0:19
for x, y being Element of REAL st y = 1 holds
* (x,y) = x
proof
let x, y be Element of REAL ; ::_thesis: ( y = 1 implies * (x,y) = x )
assume A1: y = 1 ; ::_thesis: * (x,y) = x
percases ( x = 0 or x <> 0 ) ;
suppose x = 0 ; ::_thesis: * (x,y) = x
hence * (x,y) = x by Th12; ::_thesis: verum
end;
supposeA2: x <> 0 ; ::_thesis: * (x,y) = x
A3: now__::_thesis:_(_inv_x_=_0_implies_1_=_0_)
assume A4: inv x = 0 ; ::_thesis: 1 = 0
thus 1 = * (x,(inv x)) by A2, Def4
.= 0 by A4, Th12 ; ::_thesis: verum
end;
A5: ex x9, y9 being Element of REAL+ st
( y = x9 & y = y9 & * (y,y) = x9 *' y9 ) by A1, Def2, ARYTM_2:20;
A6: * (x,(inv x)) = 1 by A2, Def4;
* ((* (x,y)),(inv x)) = * ((* (x,(inv x))),y) by Th13
.= * (y,y) by A1, A2, Def4
.= 1 by A1, A5, ARYTM_2:15 ;
hence * (x,y) = x by A3, A6, Th18; ::_thesis: verum
end;
end;
end;
reconsider j = 1 as Element of REAL ;
theorem :: ARYTM_0:20
for x, y being Element of REAL st y <> 0 holds
* ((* (x,y)),(inv y)) = x
proof
let x, y be Element of REAL ; ::_thesis: ( y <> 0 implies * ((* (x,y)),(inv y)) = x )
assume A1: y <> 0 ; ::_thesis: * ((* (x,y)),(inv y)) = x
thus * ((* (x,y)),(inv y)) = * (x,(* (y,(inv y)))) by Th13
.= * (x,j) by A1, Def4
.= x by Th19 ; ::_thesis: verum
end;
theorem Th21: :: ARYTM_0:21
for x, y being Element of REAL holds
( not * (x,y) = 0 or x = 0 or y = 0 )
proof
let x, y be Element of REAL ; ::_thesis: ( not * (x,y) = 0 or x = 0 or y = 0 )
assume that
A1: * (x,y) = 0 and
A2: x <> 0 ; ::_thesis: y = 0
A3: * (x,(inv x)) = 1 by A2, Def4;
thus y = * (j,y) by Th19
.= * ((* (x,y)),(inv x)) by A3, Th13
.= 0 by A1, Th12 ; ::_thesis: verum
end;
theorem :: ARYTM_0:22
for x, y being Element of REAL holds inv (* (x,y)) = * ((inv x),(inv y))
proof
let x, y be Element of REAL ; ::_thesis: inv (* (x,y)) = * ((inv x),(inv y))
percases ( x = 0 or y = 0 or ( x <> 0 & y <> 0 ) ) ;
supposeA1: ( x = 0 or y = 0 ) ; ::_thesis: inv (* (x,y)) = * ((inv x),(inv y))
then A2: ( inv x = 0 or inv y = 0 ) by Def4;
* (x,y) = 0 by A1, Th12;
hence inv (* (x,y)) = 0 by Def4
.= * ((inv x),(inv y)) by A2, Th12 ;
::_thesis: verum
end;
supposethat A3: x <> 0 and
A4: y <> 0 ; ::_thesis: inv (* (x,y)) = * ((inv x),(inv y))
A5: * (x,y) <> 0 by A3, A4, Th21;
A6: * (x,(inv x)) = 1 by A3, Def4;
A7: * (y,(inv y)) = 1 by A4, Def4;
* ((* (x,y)),(* ((inv x),(inv y)))) = * ((* ((* (x,y)),(inv x))),(inv y)) by Th13
.= * ((* (j,y)),(inv y)) by A6, Th13
.= 1 by A7, Th19 ;
hence inv (* (x,y)) = * ((inv x),(inv y)) by A5, Def4; ::_thesis: verum
end;
end;
end;
theorem Th23: :: ARYTM_0:23
for x, y, z being Element of REAL holds + (x,(+ (y,z))) = + ((+ (x,y)),z)
proof
let x, y, z be Element of REAL ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A1: ( x in REAL+ \/ [:{0},REAL+:] & y in REAL+ \/ [:{0},REAL+:] ) by NUMBERS:def_1, XBOOLE_0:def_5;
A2: z in REAL+ \/ [:{0},REAL+:] by NUMBERS:def_1, XBOOLE_0:def_5;
percases ( ( x in REAL+ & y in REAL+ & z in REAL+ ) or ( x in REAL+ & y in REAL+ & z in [:{0},REAL+:] ) or ( x in REAL+ & y in [:{0},REAL+:] & z in REAL+ ) or ( x in REAL+ & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) or ( z in REAL+ & y in REAL+ & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in REAL+ & z in [:{0},REAL+:] ) or ( z in REAL+ & y in [:{0},REAL+:] & x in [:{0},REAL+:] ) or ( x in [:{0},REAL+:] & y in [:{0},REAL+:] & z in [:{0},REAL+:] ) ) by A1, A2, XBOOLE_0:def_3;
supposethat A3: x in REAL+ and
A4: y in REAL+ and
A5: z in REAL+ ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A6: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & + (x,y) = x99 + y99 ) by A3, A4, Def1;
then A7: ex xy99, z99 being Element of REAL+ st
( + (x,y) = xy99 & z = z99 & + ((+ (x,y)),z) = xy99 + z99 ) by A5, Def1;
A8: ex y9, z9 being Element of REAL+ st
( y = y9 & z = z9 & + (y,z) = y9 + z9 ) by A4, A5, Def1;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A3, Def1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A8, A6, A7, ARYTM_2:6; ::_thesis: verum
end;
supposethat A9: x in REAL+ and
A10: y in REAL+ and
A11: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A12: ex x99, y99 being Element of REAL+ st
( x = x99 & y = y99 & + (x,y) = x99 + y99 ) by A9, A10, Def1;
then consider xy99, z99 being Element of REAL+ such that
A13: + (x,y) = xy99 and
A14: z = [0,z99] and
A15: + ((+ (x,y)),z) = xy99 - z99 by A11, Def1;
consider y9, z9 being Element of REAL+ such that
A16: y = y9 and
A17: z = [0,z9] and
A18: + (y,z) = y9 - z9 by A10, A11, Def1;
A19: z9 = z99 by A17, A14, XTUPLE_0:1;
now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z)
percases ( z9 <=' y9 or not z9 <=' y9 ) ;
supposeA20: z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
then A21: + (y,z) = y9 -' z9 by A18, ARYTM_1:def_2;
then ex x9, yz9 being Element of REAL+ st
( x = x9 & + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A9, Def1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A16, A12, A13, A15, A19, A20, A21, ARYTM_1:20; ::_thesis: verum
end;
supposeA22: not z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
then A23: + (y,z) = [0,(z9 -' y9)] by A18, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A24: x = x9 and
A25: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A9, Def1;
thus + (x,(+ (y,z))) = x9 - (z9 -' y9) by A23, A25, XTUPLE_0:1
.= + ((+ (x,y)),z) by A16, A12, A13, A15, A19, A22, A24, ARYTM_1:21 ; ::_thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum
end;
supposethat A26: x in REAL+ and
A27: y in [:{0},REAL+:] and
A28: z in REAL+ ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
consider x99, y99 being Element of REAL+ such that
A29: x = x99 and
A30: y = [0,y99] and
A31: + (x,y) = x99 - y99 by A26, A27, Def1;
consider z9, y9 being Element of REAL+ such that
A32: z = z9 and
A33: y = [0,y9] and
A34: + (y,z) = z9 - y9 by A27, A28, Def1;
A35: y9 = y99 by A33, A30, XTUPLE_0:1;
now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z)
percases ( ( y9 <=' x99 & y9 <=' z9 ) or ( y9 <=' x99 & not y9 <=' z9 ) or ( not y9 <=' x99 & y9 <=' z9 ) or ( not y9 <=' x99 & not y9 <=' z9 ) ) ;
supposethat A36: y9 <=' x99 and
A37: y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A38: + (y,z) = z9 -' y9 by A34, A37, ARYTM_1:def_2;
then consider x9, yz9 being Element of REAL+ such that
A39: x = x9 and
A40: ( + (y,z) = yz9 & + (x,(+ (y,z))) = x9 + yz9 ) by A26, Def1;
A41: + (x,y) = x9 -' y9 by A29, A31, A35, A36, A39, ARYTM_1:def_2;
then ex z99, xy99 being Element of REAL+ st
( z = z99 & + (x,y) = xy99 & + (z,(+ (x,y))) = z99 + xy99 ) by A28, Def1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A32, A29, A36, A37, A38, A39, A40, A41, ARYTM_1:12; ::_thesis: verum
end;
supposethat A42: y9 <=' x99 and
A43: not y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A44: + (x,y) = x99 -' y9 by A31, A35, A42, ARYTM_1:def_2;
then A45: ex z99, xy99 being Element of REAL+ st
( z = z99 & + (x,y) = xy99 & + (z,(+ (x,y))) = z99 + xy99 ) by A28, Def1;
A46: + (y,z) = [0,(y9 -' z9)] by A34, A43, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A47: x = x9 and
A48: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A26, Def1;
thus + (x,(+ (y,z))) = x9 - (y9 -' z9) by A46, A48, XTUPLE_0:1
.= + ((+ (x,y)),z) by A32, A29, A42, A43, A47, A44, A45, ARYTM_1:22 ; ::_thesis: verum
end;
supposethat A49: not y9 <=' x99 and
A50: y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A51: + (y,x) = [0,(y9 -' x99)] by A31, A35, A49, ARYTM_1:def_2;
then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider z99, yx99 being Element of REAL+ such that
A52: z = z99 and
A53: ( + (y,x) = [0,yx99] & + (z,(+ (y,x))) = z99 - yx99 ) by A28, Def1;
A54: + (z,y) = z9 -' y9 by A34, A50, ARYTM_1:def_2;
then ex x9, zy99 being Element of REAL+ st
( x = x9 & + (z,y) = zy99 & + (x,(+ (z,y))) = x9 + zy99 ) by A26, Def1;
hence + (x,(+ (y,z))) = z99 - (y9 -' x99) by A32, A29, A49, A50, A52, A54, ARYTM_1:22
.= + ((+ (x,y)),z) by A51, A53, XTUPLE_0:1 ;
::_thesis: verum
end;
supposethat A55: not y9 <=' x99 and
A56: not y9 <=' z9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A57: + (y,z) = [0,(y9 -' z9)] by A34, A56, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A58: x = x9 and
A59: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = x9 - yz9 ) by A26, Def1;
A60: + (y,x) = [0,(y9 -' x99)] by A31, A35, A55, ARYTM_1:def_2;
then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider z99, yx99 being Element of REAL+ such that
A61: z = z99 and
A62: ( + (y,x) = [0,yx99] & + (z,(+ (y,x))) = z99 - yx99 ) by A28, Def1;
thus + (x,(+ (y,z))) = x9 - (y9 -' z9) by A57, A59, XTUPLE_0:1
.= z99 - (y9 -' x99) by A32, A29, A55, A56, A61, A58, ARYTM_1:23
.= + ((+ (x,y)),z) by A60, A62, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum
end;
supposethat A63: x in REAL+ and
A64: y in [:{0},REAL+:] and
A65: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
( ( not z in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not z in [:{0},REAL+:] ) ) by A64, A65, Th5, XBOOLE_0:3;
then consider y9, z9 being Element of REAL+ such that
A66: y = [0,y9] and
A67: z = [0,z9] and
A68: + (y,z) = [0,(y9 + z9)] by A64, Def1;
+ (y,z) in [:{0},REAL+:] by A68, Lm1, ZFMISC_1:87;
then consider x9, yz9 being Element of REAL+ such that
A69: x = x9 and
A70: + (y,z) = [0,yz9] and
A71: + (x,(+ (y,z))) = x9 - yz9 by A63, Def1;
consider x99, y99 being Element of REAL+ such that
A72: x = x99 and
A73: y = [0,y99] and
A74: + (x,y) = x99 - y99 by A63, A64, Def1;
A75: y9 = y99 by A66, A73, XTUPLE_0:1;
now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z)
percases ( y99 <=' x99 or not y99 <=' x99 ) ;
supposeA76: y99 <=' x99 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
then A77: + (x,y) = x99 -' y99 by A74, ARYTM_1:def_2;
then consider xy99, z99 being Element of REAL+ such that
A78: + (x,y) = xy99 and
A79: z = [0,z99] and
A80: + ((+ (x,y)),z) = xy99 - z99 by A65, Def1;
A81: z9 = z99 by A67, A79, XTUPLE_0:1;
thus + (x,(+ (y,z))) = x9 - (y9 + z9) by A68, A70, A71, XTUPLE_0:1
.= + ((+ (x,y)),z) by A72, A69, A75, A76, A77, A78, A80, A81, ARYTM_1:24 ; ::_thesis: verum
end;
supposeA82: not y99 <=' x99 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A83: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A65, Th5, XBOOLE_0:3;
A84: + (x,y) = [0,(y99 -' x99)] by A74, A82, ARYTM_1:def_2;
then + (x,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy99, z99 being Element of REAL+ such that
A85: + (x,y) = [0,xy99] and
A86: z = [0,z99] and
A87: + ((+ (x,y)),z) = [0,(xy99 + z99)] by A84, A83, Def1, Lm1, ZFMISC_1:87;
A88: z9 = z99 by A67, A86, XTUPLE_0:1;
A89: yz9 = z9 + y9 by A68, A70, XTUPLE_0:1;
then y99 <=' yz9 by A75, ARYTM_2:19;
then not yz9 <=' x9 by A72, A69, A82, ARYTM_1:3;
hence + (x,(+ (y,z))) = [0,((z9 + y9) -' x9)] by A71, A89, ARYTM_1:def_2
.= [0,(z99 + (y99 -' x99))] by A72, A69, A75, A82, A88, ARYTM_1:13
.= + ((+ (x,y)),z) by A84, A85, A87, XTUPLE_0:1 ;
::_thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum
end;
supposethat A90: z in REAL+ and
A91: y in REAL+ and
A92: x in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A93: ex z99, y99 being Element of REAL+ st
( z = z99 & y = y99 & + (z,y) = z99 + y99 ) by A90, A91, Def1;
then consider zy99, x99 being Element of REAL+ such that
A94: + (z,y) = zy99 and
A95: x = [0,x99] and
A96: + ((+ (z,y)),x) = zy99 - x99 by A92, Def1;
consider y9, x9 being Element of REAL+ such that
A97: y = y9 and
A98: x = [0,x9] and
A99: + (y,x) = y9 - x9 by A91, A92, Def1;
A100: x9 = x99 by A98, A95, XTUPLE_0:1;
now__::_thesis:_+_(z,(+_(y,x)))_=_+_((+_(z,y)),x)
percases ( x9 <=' y9 or not x9 <=' y9 ) ;
supposeA101: x9 <=' y9 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
then A102: + (y,x) = y9 -' x9 by A99, ARYTM_1:def_2;
then ex z9, yx9 being Element of REAL+ st
( z = z9 & + (y,x) = yx9 & + (z,(+ (y,x))) = z9 + yx9 ) by A90, Def1;
hence + (z,(+ (y,x))) = + ((+ (z,y)),x) by A97, A93, A94, A96, A100, A101, A102, ARYTM_1:20; ::_thesis: verum
end;
supposeA103: not x9 <=' y9 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
then A104: + (y,x) = [0,(x9 -' y9)] by A99, ARYTM_1:def_2;
then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then consider z9, yx9 being Element of REAL+ such that
A105: z = z9 and
A106: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = z9 - yx9 ) by A90, Def1;
thus + (z,(+ (y,x))) = z9 - (x9 -' y9) by A104, A106, XTUPLE_0:1
.= + ((+ (z,y)),x) by A97, A93, A94, A96, A100, A103, A105, ARYTM_1:21 ; ::_thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum
end;
supposethat A107: x in [:{0},REAL+:] and
A108: y in REAL+ and
A109: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
consider y9, z9 being Element of REAL+ such that
A110: y = y9 and
A111: z = [0,z9] and
A112: + (y,z) = y9 - z9 by A108, A109, Def1;
consider x99, y99 being Element of REAL+ such that
A113: x = [0,x99] and
A114: y = y99 and
A115: + (x,y) = y99 - x99 by A107, A108, Def1;
now__::_thesis:_+_(x,(+_(y,z)))_=_+_((+_(x,y)),z)
percases ( ( x99 <=' y99 & z9 <=' y9 ) or ( not x99 <=' y99 & z9 <=' y9 ) or ( not z9 <=' y9 & x99 <=' y99 ) or ( not x99 <=' y99 & not z9 <=' y9 ) ) ;
supposethat A116: x99 <=' y99 and
A117: z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A118: + (y,z) = y9 -' z9 by A112, A117, ARYTM_1:def_2;
then consider x9, yz9 being Element of REAL+ such that
A119: x = [0,x9] and
A120: ( + (y,z) = yz9 & + (x,(+ (y,z))) = yz9 - x9 ) by A107, Def1;
A121: x9 = x99 by A113, A119, XTUPLE_0:1;
then A122: + (x,y) = y9 -' x9 by A110, A114, A115, A116, ARYTM_1:def_2;
then consider z99, xy99 being Element of REAL+ such that
A123: z = [0,z99] and
A124: ( + (x,y) = xy99 & + (z,(+ (x,y))) = xy99 - z99 ) by A109, Def1;
z9 = z99 by A111, A123, XTUPLE_0:1;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) by A110, A114, A116, A117, A118, A120, A121, A122, A124, ARYTM_1:25; ::_thesis: verum
end;
supposethat A125: not x99 <=' y99 and
A126: z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A127: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A109, Th5, XBOOLE_0:3;
A128: + (y,x) = [0,(x99 -' y99)] by A115, A125, ARYTM_1:def_2;
then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider z99, yx9 being Element of REAL+ such that
A129: z = [0,z99] and
A130: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = [0,(z99 + yx9)] ) by A128, A127, Def1, Lm1, ZFMISC_1:87;
A131: z9 = z99 by A111, A129, XTUPLE_0:1;
A132: + (y,z) = y9 -' z9 by A112, A126, ARYTM_1:def_2;
then consider x9, yz9 being Element of REAL+ such that
A133: x = [0,x9] and
A134: + (y,z) = yz9 and
A135: + (x,(+ (y,z))) = yz9 - x9 by A107, Def1;
A136: x9 = x99 by A113, A133, XTUPLE_0:1;
yz9 <=' y9 by A132, A134, ARYTM_1:11;
then not x9 <=' yz9 by A110, A114, A125, A136, ARYTM_1:3;
hence + (x,(+ (y,z))) = [0,(x9 -' (y9 -' z9))] by A132, A134, A135, ARYTM_1:def_2
.= [0,((x99 -' y99) + z99)] by A110, A114, A125, A126, A136, A131, ARYTM_1:14
.= + ((+ (x,y)),z) by A128, A130, XTUPLE_0:1 ;
::_thesis: verum
end;
supposethat A137: not z9 <=' y9 and
A138: x99 <=' y99 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A139: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A107, Th5, XBOOLE_0:3;
A140: + (y,z) = [0,(z9 -' y9)] by A112, A137, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider x9, yz99 being Element of REAL+ such that
A141: x = [0,x9] and
A142: ( + (y,z) = [0,yz99] & + (x,(+ (y,z))) = [0,(x9 + yz99)] ) by A140, A139, Def1, Lm1, ZFMISC_1:87;
A143: x99 = x9 by A113, A141, XTUPLE_0:1;
A144: + (y,x) = y99 -' x99 by A115, A138, ARYTM_1:def_2;
then consider z99, yx99 being Element of REAL+ such that
A145: z = [0,z99] and
A146: + (y,x) = yx99 and
A147: + (z,(+ (y,x))) = yx99 - z99 by A109, Def1;
A148: z99 = z9 by A111, A145, XTUPLE_0:1;
yx99 <=' y99 by A144, A146, ARYTM_1:11;
then A149: not z99 <=' yx99 by A110, A114, A137, A148, ARYTM_1:3;
thus + (x,(+ (y,z))) = [0,((z9 -' y9) + x9)] by A140, A142, XTUPLE_0:1
.= [0,(z99 -' (y99 -' x99))] by A110, A114, A137, A138, A148, A143, ARYTM_1:14
.= + ((+ (x,y)),z) by A144, A146, A147, A149, ARYTM_1:def_2 ; ::_thesis: verum
end;
supposethat A150: not x99 <=' y99 and
A151: not z9 <=' y9 ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A152: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A107, Th5, XBOOLE_0:3;
A153: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A109, Th5, XBOOLE_0:3;
A154: + (y,x) = [0,(x99 -' y99)] by A115, A150, ARYTM_1:def_2;
then + (y,x) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider z99, yx9 being Element of REAL+ such that
A155: z = [0,z99] and
A156: ( + (y,x) = [0,yx9] & + (z,(+ (y,x))) = [0,(z99 + yx9)] ) by A154, A153, Def1, Lm1, ZFMISC_1:87;
A157: z9 = z99 by A111, A155, XTUPLE_0:1;
A158: + (y,z) = [0,(z9 -' y9)] by A112, A151, ARYTM_1:def_2;
then + (y,z) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider x9, yz99 being Element of REAL+ such that
A159: x = [0,x9] and
A160: ( + (y,z) = [0,yz99] & + (x,(+ (y,z))) = [0,(x9 + yz99)] ) by A158, A152, Def1, Lm1, ZFMISC_1:87;
A161: x9 = x99 by A113, A159, XTUPLE_0:1;
thus + (x,(+ (y,z))) = [0,((z9 -' y9) + x9)] by A158, A160, XTUPLE_0:1
.= [0,((x99 -' y99) + z99)] by A110, A114, A150, A151, A157, A161, ARYTM_1:15
.= + ((+ (x,y)),z) by A154, A156, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum
end;
supposethat A162: z in REAL+ and
A163: y in [:{0},REAL+:] and
A164: x in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
( ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) by A163, A164, Th5, XBOOLE_0:3;
then consider y9, x9 being Element of REAL+ such that
A165: y = [0,y9] and
A166: x = [0,x9] and
A167: + (y,x) = [0,(y9 + x9)] by A163, Def1;
+ (y,x) in [:{0},REAL+:] by A167, Lm1, ZFMISC_1:87;
then consider z9, yx9 being Element of REAL+ such that
A168: z = z9 and
A169: + (y,x) = [0,yx9] and
A170: + (z,(+ (y,x))) = z9 - yx9 by A162, Def1;
consider z99, y99 being Element of REAL+ such that
A171: z = z99 and
A172: y = [0,y99] and
A173: + (z,y) = z99 - y99 by A162, A163, Def1;
A174: y9 = y99 by A165, A172, XTUPLE_0:1;
now__::_thesis:_+_(z,(+_(y,x)))_=_+_((+_(z,y)),x)
percases ( y99 <=' z99 or not y99 <=' z99 ) ;
supposeA175: y99 <=' z99 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
then A176: + (z,y) = z99 -' y99 by A173, ARYTM_1:def_2;
then consider zy99, x99 being Element of REAL+ such that
A177: + (z,y) = zy99 and
A178: x = [0,x99] and
A179: + ((+ (z,y)),x) = zy99 - x99 by A164, Def1;
A180: x9 = x99 by A166, A178, XTUPLE_0:1;
thus + (z,(+ (y,x))) = z9 - (y9 + x9) by A167, A169, A170, XTUPLE_0:1
.= + ((+ (z,y)),x) by A171, A168, A174, A175, A176, A177, A179, A180, ARYTM_1:24 ; ::_thesis: verum
end;
supposeA181: not y99 <=' z99 ; ::_thesis: + (z,(+ (y,x))) = + ((+ (z,y)),x)
A182: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A164, Th5, XBOOLE_0:3;
A183: + (z,y) = [0,(y99 -' z99)] by A173, A181, ARYTM_1:def_2;
then + (z,y) in [:{0},REAL+:] by Lm1, ZFMISC_1:87;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider zy99, x99 being Element of REAL+ such that
A184: + (z,y) = [0,zy99] and
A185: x = [0,x99] and
A186: + ((+ (z,y)),x) = [0,(zy99 + x99)] by A183, A182, Def1, Lm1, ZFMISC_1:87;
A187: x9 = x99 by A166, A185, XTUPLE_0:1;
A188: yx9 = x9 + y9 by A167, A169, XTUPLE_0:1;
then y99 <=' yx9 by A174, ARYTM_2:19;
then not yx9 <=' z9 by A171, A168, A181, ARYTM_1:3;
hence + (z,(+ (y,x))) = [0,((x9 + y9) -' z9)] by A170, A188, ARYTM_1:def_2
.= [0,(x99 + (y99 -' z99))] by A171, A168, A174, A181, A187, ARYTM_1:13
.= + ((+ (z,y)),x) by A183, A184, A186, XTUPLE_0:1 ;
::_thesis: verum
end;
end;
end;
hence + (x,(+ (y,z))) = + ((+ (x,y)),z) ; ::_thesis: verum
end;
supposethat A189: x in [:{0},REAL+:] and
A190: y in [:{0},REAL+:] and
A191: z in [:{0},REAL+:] ; ::_thesis: + (x,(+ (y,z))) = + ((+ (x,y)),z)
A192: ( not x in REAL+ or not + (z,y) in [:{0},REAL+:] ) by A189, Th5, XBOOLE_0:3;
( ( not z in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not z in [:{0},REAL+:] ) ) by A190, A191, Th5, XBOOLE_0:3;
then consider y9, z9 being Element of REAL+ such that
A193: y = [0,y9] and
A194: z = [0,z9] and
A195: + (y,z) = [0,(y9 + z9)] by A190, Def1;
+ (z,y) in [:{0},REAL+:] by A195, Lm1, ZFMISC_1:87;
then ( not + (z,y) in REAL+ or not x in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider x9, yz9 being Element of REAL+ such that
A196: x = [0,x9] and
A197: ( + (y,z) = [0,yz9] & + (x,(+ (y,z))) = [0,(x9 + yz9)] ) by A195, A192, Def1, Lm1, ZFMISC_1:87;
A198: ( not z in REAL+ or not + (x,y) in [:{0},REAL+:] ) by A191, Th5, XBOOLE_0:3;
( ( not x in REAL+ or not y in [:{0},REAL+:] ) & ( not y in REAL+ or not x in [:{0},REAL+:] ) ) by A189, A190, Th5, XBOOLE_0:3;
then consider x99, y99 being Element of REAL+ such that
A199: x = [0,x99] and
A200: y = [0,y99] and
A201: + (x,y) = [0,(x99 + y99)] by A189, Def1;
A202: x9 = x99 by A199, A196, XTUPLE_0:1;
+ (x,y) in [:{0},REAL+:] by A201, Lm1, ZFMISC_1:87;
then ( not + (x,y) in REAL+ or not z in [:{0},REAL+:] ) by Th5, XBOOLE_0:3;
then consider xy99, z99 being Element of REAL+ such that
A203: + (x,y) = [0,xy99] and
A204: z = [0,z99] and
A205: + ((+ (x,y)),z) = [0,(xy99 + z99)] by A201, A198, Def1, Lm1, ZFMISC_1:87;
A206: z9 = z99 by A194, A204, XTUPLE_0:1;
A207: y9 = y99 by A193, A200, XTUPLE_0:1;
thus + (x,(+ (y,z))) = [0,((z9 + y9) + x9)] by A195, A197, XTUPLE_0:1
.= [0,(z99 + (y99 + x99))] by A206, A202, A207, ARYTM_2:6
.= + ((+ (x,y)),z) by A201, A203, A205, XTUPLE_0:1 ; ::_thesis: verum
end;
end;
end;
theorem :: ARYTM_0:24
for x, y being Element of REAL st [*x,y*] in REAL holds
y = 0
proof
let x, y be Element of REAL ; ::_thesis: ( [*x,y*] in REAL implies y = 0 )
assume A1: [*x,y*] in REAL ; ::_thesis: y = 0
assume y <> 0 ; ::_thesis: contradiction
then [*x,y*] = (0,1) --> (x,y) by Def5;
hence contradiction by A1, Th8; ::_thesis: verum
end;
theorem :: ARYTM_0:25
for x, y being Element of REAL holds opp (+ (x,y)) = + ((opp x),(opp y))
proof
let x, y be Element of REAL ; ::_thesis: opp (+ (x,y)) = + ((opp x),(opp y))
+ ((+ (x,y)),(+ ((opp x),(opp y)))) = + (x,(+ (y,(+ ((opp x),(opp y)))))) by Th23
.= + (x,(+ ((opp x),(+ (y,(opp y)))))) by Th23
.= + (x,(+ ((opp x),o))) by Def3
.= + (x,(opp x)) by Th11
.= 0 by Def3 ;
hence opp (+ (x,y)) = + ((opp x),(opp y)) by Def3; ::_thesis: verum
end;