arytm_0.miz
begin
Lm1: for x be
Element of
REAL+ holds
[
0 , x]
in
[:
{
0 },
REAL+ :]
proof
0
in
{
0 } by
TARSKI:def 1;
hence thesis by
ZFMISC_1: 87;
end;
theorem ::
ARYTM_0:1
Th1:
REAL+
c=
REAL
proof
REAL+
c= (
REAL+
\/
[:
{
{} },
REAL+ :]) by
XBOOLE_1: 7;
hence thesis by
ARYTM_2: 3,
ZFMISC_1: 34;
end;
theorem ::
ARYTM_0:2
Th2: for x be
Element of
REAL+ st x
<>
{} holds
[
{} , x]
in
REAL
proof
let x be
Element of
REAL+ such that
A1: x
<>
{} ;
A2:
now
assume
[
{} , x]
in
{
[
{} ,
{} ]};
then
[
{} , x]
=
[
{} ,
{} ] by
TARSKI:def 1;
hence contradiction by
A1,
XTUPLE_0: 1;
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 thesis by
A2,
XBOOLE_0:def 5;
end;
theorem ::
ARYTM_0:3
Th3: for y be
set st
[
{} , y]
in
REAL holds y
<>
{}
proof
let y be
set such that
A1:
[
{} , y]
in
REAL and
A2: y
=
{} ;
[
{} , y]
in
{
[
{} ,
{} ]} by
A2,
TARSKI:def 1;
hence contradiction by
A1,
XBOOLE_0:def 5;
end;
theorem ::
ARYTM_0:4
Th4: for x,y be
Element of
REAL+ holds (x
- y)
in
REAL
proof
let x,y be
Element of
REAL+ ;
per cases ;
suppose y
<=' x;
then (x
- y)
= (x
-' y) by
ARYTM_1:def 2;
then (x
- y)
in
REAL+ ;
hence thesis by
Th1;
end;
suppose
A1: not y
<=' x;
then (x
- y)
=
[
{} , (y
-' x)] by
ARYTM_1:def 2;
hence thesis by
A1,
Th2,
ARYTM_1: 9;
end;
end;
theorem ::
ARYTM_0:5
Th5:
REAL+
misses
[:
{
{} },
REAL+ :]
proof
assume
REAL+
meets
[:
{
{} },
REAL+ :];
then
consider x be
object such that
A1: x
in
REAL+ and
A2: x
in
[:
{
{} },
REAL+ :] by
XBOOLE_0: 3;
consider x1,x2 be
object 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;
end;
begin
registration
let x,y be
object;
cluster
[x, y] -> non
zero;
coherence ;
end
theorem ::
ARYTM_0:6
Th6: for x,y be
Element of
REAL+ st (x
- y)
=
{} holds x
= y
proof
let x,y be
Element of
REAL+ ;
assume
A1: (x
- y)
=
{} ;
0
<>
[
{} , (y
-' x)];
then y
<=' x & (x
-' y)
=
{} by
A1,
ARYTM_1:def 2;
hence thesis by
ARYTM_1: 10;
end;
Lm2: not ex a,b be
set st 1
=
[a, b]
proof
let a,b be
set;
assume
A1: 1
=
[a, b];
{a}
in
{
{a, b},
{a}} by
TARSKI:def 2;
hence contradiction by
A1,
ORDINAL3: 15,
TARSKI:def 1;
end;
theorem ::
ARYTM_0:7
Th7: for x,y,z be
Element of
REAL+ st x
<>
{} & (x
*' y)
= (x
*' z) holds y
= z
proof
let x,y,z be
Element of
REAL+ ;
assume that
A1: x
<>
{} and
A2: (x
*' y)
= (x
*' z);
per cases ;
suppose
A3: z
<=' y;
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 thesis by
Th6;
end;
suppose
A4: 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 thesis by
Th6;
end;
end;
begin
Lm3:
0
in
REAL by
NUMBERS: 19;
definition
let x,y be
Element of
REAL ;
::
ARYTM_0:def1
func
+ (x,y) ->
Element of
REAL means
:
Def1: ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & it
= (x9
+ y9) if x
in
REAL+ & y
in
REAL+ ,
ex x9,y9 be
Element of
REAL+ st x
= x9 & y
=
[
0 , y9] & it
= (x9
- y9) if x
in
REAL+ & y
in
[:
{
0 },
REAL+ :],
ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
= y9 & it
= (y9
- x9) if y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]
otherwise ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
=
[
0 , y9] & it
=
[
0 , (x9
+ y9)];
existence
proof
hereby
assume x
in
REAL+ & y
in
REAL+ ;
then
reconsider x9 = x, y9 = y as
Element of
REAL+ ;
reconsider IT = (x9
+ y9) as
Element of
REAL by
Th1;
take IT, x9, y9;
thus x
= x9 & y
= y9 & IT
= (x9
+ y9);
end;
A1: y
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
hereby
assume x
in
REAL+ ;
then
reconsider x9 = x as
Element of
REAL+ ;
assume y
in
[:
{
0 },
REAL+ :];
then
consider z,y9 be
object such that
A2: z
in
{
0 } and
A3: y9
in
REAL+ and
A4: y
=
[z, y9] by
ZFMISC_1: 84;
reconsider y9 as
Element of
REAL+ by
A3;
reconsider IT = (x9
- y9) as
Element of
REAL by
Th4;
take IT, x9, y9;
thus x
= x9 & y
=
[
0 , y9] & IT
= (x9
- y9) by
A2,
A4,
TARSKI:def 1;
end;
hereby
assume y
in
REAL+ ;
then
reconsider y9 = y as
Element of
REAL+ ;
assume x
in
[:
{
0 },
REAL+ :];
then
consider z,x9 be
object such that
A5: z
in
{
0 } and
A6: x9
in
REAL+ and
A7: x
=
[z, x9] by
ZFMISC_1: 84;
reconsider x9 as
Element of
REAL+ by
A6;
reconsider IT = (y9
- x9) as
Element of
REAL by
Th4;
take IT, x9, y9;
thus x
=
[
0 , x9] & y
= y9 & IT
= (y9
- x9) by
A5,
A7,
TARSKI:def 1;
end;
assume that
A8: not (x
in
REAL+ & y
in
REAL+ ) and
A9: not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :]) and
A10: not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]);
A11: x
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
then x
in
REAL+ or x
in
[:
{
0 },
REAL+ :] by
XBOOLE_0:def 3;
then
consider z1,x9 be
object 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 be
object 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 as
Element of
REAL+ by
A13;
reconsider 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, x9, y9;
thus thesis by
A12,
A14,
A15,
A17,
TARSKI:def 1;
end;
uniqueness
proof
let IT1,IT2 be
Element of
REAL ;
thus x
in
REAL+ & y
in
REAL+ & (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & IT1
= (x9
+ y9)) & (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & IT2
= (x9
+ y9)) implies IT1
= IT2;
thus x
in
REAL+ & y
in
[:
{
0 },
REAL+ :] & (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
=
[
0 , y9] & IT1
= (x9
- y9)) & (ex x99,y99 be
Element of
REAL+ st x
= x99 & y
=
[
0 , y99] & IT2
= (x99
- y99)) implies IT1
= IT2 by
XTUPLE_0: 1;
thus y
in
REAL+ & x
in
[:
{
0 },
REAL+ :] & (ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
= y9 & IT1
= (y9
- x9)) & (ex x99,y99 be
Element of
REAL+ st x
=
[
0 , x99] & y
= y99 & IT2
= (y99
- x99)) implies IT1
= IT2 by
XTUPLE_0: 1;
assume that not (x
in
REAL+ & y
in
REAL+ ) and not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :]) and not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]);
given x9,y9 be
Element of
REAL+ such that
A18: x
=
[
0 , x9] and
A19: y
=
[
0 , y9] & IT1
=
[
0 , (x9
+ y9)];
given x99,y99 be
Element of
REAL+ such that
A20: x
=
[
0 , x99] and
A21: y
=
[
0 , y99] & IT2
=
[
0 , (x99
+ y99)];
x9
= x99 by
A18,
A20,
XTUPLE_0: 1;
hence thesis by
A19,
A21,
XTUPLE_0: 1;
end;
consistency by
Th5,
XBOOLE_0: 3;
commutativity ;
::
ARYTM_0:def2
func
* (x,y) ->
Element of
REAL means
:
Def2: ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & it
= (x9
*' y9) if x
in
REAL+ & y
in
REAL+ ,
ex x9,y9 be
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 be
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 be
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
proof
hereby
assume x
in
REAL+ & y
in
REAL+ ;
then
reconsider x9 = x, y9 = y as
Element of
REAL+ ;
reconsider IT = (x9
*' y9) as
Element of
REAL by
Th1;
take IT, x9, y9;
thus x
= x9 & y
= y9 & IT
= (x9
*' y9);
end;
hereby
assume x
in
REAL+ ;
then
reconsider x9 = x as
Element of
REAL+ ;
assume y
in
[:
{
0 },
REAL+ :];
then
consider z,y9 be
object such that
A22: z
in
{
0 } and
A23: y9
in
REAL+ and
A24: y
=
[z, y9] by
ZFMISC_1: 84;
reconsider 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 ;
then
reconsider IT =
[
0 , (x9
*' y9)] as
Element of
REAL by
A25,
Th2,
ARYTM_1: 2;
take IT, x9, y9;
thus x
= x9 & y
=
[
0 , y9] & IT
=
[
0 , (x9
*' y9)] by
A22,
A24,
TARSKI:def 1;
end;
hereby
assume y
in
REAL+ ;
then
reconsider y9 = y as
Element of
REAL+ ;
assume x
in
[:
{
0 },
REAL+ :];
then
consider z,x9 be
object such that
A26: z
in
{
0 } and
A27: x9
in
REAL+ and
A28: x
=
[z, x9] by
ZFMISC_1: 84;
reconsider 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 ;
then
reconsider IT =
[
0 , (y9
*' x9)] as
Element of
REAL by
A29,
Th2,
ARYTM_1: 2;
take IT, x9, y9;
thus x
=
[
0 , x9] & y
= y9 & IT
=
[
0 , (y9
*' x9)] by
A26,
A28,
TARSKI:def 1;
end;
hereby
assume x
in
[:
{
0 },
REAL+ :];
then
consider z1,x9 be
object such that
A30: z1
in
{
0 } and
A31: x9
in
REAL+ and
A32: x
=
[z1, x9] by
ZFMISC_1: 84;
reconsider x9 as
Element of
REAL+ by
A31;
assume y
in
[:
{
0 },
REAL+ :];
then
consider z2,y9 be
object such that
A33: z2
in
{
0 } and
A34: y9
in
REAL+ and
A35: y
=
[z2, y9] by
ZFMISC_1: 84;
reconsider y9 as
Element of
REAL+ by
A34;
reconsider IT = (y9
*' x9) as
Element of
REAL by
Th1;
take IT, x9, y9;
thus x
=
[
0 , x9] & y
=
[
0 , y9] & IT
= (y9
*' x9) by
A30,
A32,
A33,
A35,
TARSKI:def 1;
end;
thus thesis by
Lm3;
end;
uniqueness
proof
let IT1,IT2 be
Element of
REAL ;
thus x
in
REAL+ & y
in
REAL+ & (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & IT1
= (x9
*' y9)) & (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & IT2
= (x9
*' y9)) implies IT1
= IT2;
thus x
in
REAL+ & y
in
[:
{
0 },
REAL+ :] & x
<>
0 & (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
=
[
0 , y9] & IT1
=
[
0 , (x9
*' y9)]) & (ex x99,y99 be
Element of
REAL+ st x
= x99 & y
=
[
0 , y99] & IT2
=
[
0 , (x99
*' y99)]) implies IT1
= IT2 by
XTUPLE_0: 1;
thus y
in
REAL+ & x
in
[:
{
0 },
REAL+ :] & y
<>
0 & (ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
= y9 & IT1
=
[
0 , (y9
*' x9)]) & (ex x99,y99 be
Element of
REAL+ st x
=
[
0 , x99] & y
= y99 & IT2
=
[
0 , (y99
*' x99)]) implies IT1
= IT2 by
XTUPLE_0: 1;
hereby
assume that x
in
[:
{
0 },
REAL+ :] and y
in
[:
{
0 },
REAL+ :];
given x9,y9 be
Element of
REAL+ such that
A36: x
=
[
0 , x9] and
A37: y
=
[
0 , y9] & IT1
= (y9
*' x9);
given x99,y99 be
Element of
REAL+ such that
A38: x
=
[
0 , x99] and
A39: y
=
[
0 , y99] & IT2
= (y99
*' x99);
x9
= x99 by
A36,
A38,
XTUPLE_0: 1;
hence IT1
= IT2 by
A37,
A39,
XTUPLE_0: 1;
end;
thus thesis;
end;
consistency by
Th5,
XBOOLE_0: 3;
commutativity ;
end
reserve x,y for
Element of
REAL ;
definition
let x be
Element of
REAL ;
::
ARYTM_0:def3
func
opp x ->
Element of
REAL means
:
Def3: (
+ (x,it ))
=
0 ;
existence
proof
reconsider z9 =
0 as
Element of
REAL+ by
ARYTM_2: 20;
A1: x
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
per cases by
A1,
XBOOLE_0:def 3;
suppose
A2: x
=
0 ;
then
reconsider x9 = x as
Element of
REAL+ by
ARYTM_2: 20;
take x;
(x9
+ x9)
=
0 by
A2,
ARYTM_2:def 8;
hence thesis by
Def1,
Lm3;
end;
suppose that
A3: x
in
REAL+ and
A4: x
<>
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,
ZFMISC_1: 56;
reconsider x9 = x as
Element of
REAL+ by
A3;
A7: x9
<=' x9;
take y;
(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 thesis by
A6,
Def1,
Lm3;
end;
suppose
A8: x
in
[:
{
0 },
REAL+ :];
then
consider a,b be
object 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;
now
per cases ;
case x
in
REAL+ & y
in
REAL+ ;
hence ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 &
0
= (x9
+ y9) by
A8,
Th5,
XBOOLE_0: 3;
end;
case x
in
REAL+ & y
in
[:
{
0 },
REAL+ :];
hence ex x9,y9 be
Element of
REAL+ st x
= x9 & y
=
[
0 , y9] &
0
= (x9
- y9) by
A10,
Th5,
XBOOLE_0: 3;
end;
case y
in
REAL+ & x
in
[:
{
0 },
REAL+ :];
reconsider x9 = b, y9 = y as
Element of
REAL+ by
A10;
take x9, y9;
thus x
=
[
0 , x9] by
A9,
A11,
TARSKI:def 1;
thus y
= y9;
thus
0
= (y9
- x9) by
ARYTM_1: 18;
end;
case not (x
in
REAL+ & y
in
REAL+ ) & not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :]) & not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]);
hence ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
=
[
0 , y9] &
0
=
[
0 , (y9
+ x9)] by
A8,
A10;
end;
end;
hence thesis by
Def1,
Lm3;
end;
end;
uniqueness
proof
let y,z be
Element of
REAL such that
A12: (
+ (x,y))
=
0 and
A13: (
+ (x,z))
=
0 ;
per cases ;
suppose x
in
REAL+ & y
in
REAL+ & z
in
REAL+ ;
then (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 &
0
= (x9
+ y9)) & ex x9,y9 be
Element of
REAL+ st x
= x9 & z
= y9 &
0
= (x9
+ y9) by
A12,
A13,
Def1;
hence thesis by
ARYTM_2: 11;
end;
suppose that
A14: x
in
REAL+ and
A15: y
in
REAL+ and
A16: z
in
[:
{
0 },
REAL+ :];
consider x99,y99 be
Element of
REAL+ such that
A17: x
= x99 and
A18: z
=
[
0 , y99] &
0
= (x99
- y99) by
A13,
A14,
A16,
Def1;
ex x9,y9 be
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
XBOOLE_0:def 5;
z
in
REAL ;
hence thesis by
A18,
A19,
A20,
ARYTM_1: 19;
end;
suppose that
A21: x
in
REAL+ and
A22: z
in
REAL+ and
A23: y
in
[:
{
0 },
REAL+ :];
consider x99,y9 be
Element of
REAL+ such that
A24: x
= x99 and
A25: y
=
[
0 , y9] &
0
= (x99
- y9) by
A12,
A21,
A23,
Def1;
ex x9,z9 be
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
XBOOLE_0:def 5;
y
in
REAL ;
hence thesis by
A25,
A26,
A27,
ARYTM_1: 19;
end;
suppose that
A28: x
in
REAL+ and
A29: y
in
[:
{
0 },
REAL+ :] and
A30: z
in
[:
{
0 },
REAL+ :];
consider x99,z9 be
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 be
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 thesis by
A35,
A32;
end;
suppose that
A37: z
in
REAL+ and
A38: y
in
REAL+ and
A39: x
in
[:
{
0 },
REAL+ :];
consider x99,z9 be
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 be
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 thesis by
A44,
A41;
end;
suppose not (x
in
REAL+ & y
in
REAL+ ) & not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :]) & not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]);
then ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
=
[
0 , y9] &
0
=
[
0 , (x9
+ y9)] by
A12,
Def1;
hence thesis;
end;
suppose not (x
in
REAL+ & z
in
REAL+ ) & not (x
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) & not (z
in
REAL+ & x
in
[:
{
0 },
REAL+ :]);
then ex x9,z9 be
Element of
REAL+ st x
=
[
0 , x9] & z
=
[
0 , z9] &
0
=
[
0 , (x9
+ z9)] by
A13,
Def1;
hence thesis;
end;
end;
involutiveness ;
::
ARYTM_0:def4
func
inv x ->
Element of
REAL means
:
Def4: (
* (x,it ))
= 1 if x
<>
0
otherwise it
=
0 ;
existence
proof
thus x
<>
0 implies ex y st (
* (x,y))
= 1
proof
A46: x
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
assume
A47: x
<>
0 ;
per cases by
A46,
XBOOLE_0:def 3;
suppose x
in
REAL+ ;
then
reconsider x9 = x as
Element of
REAL+ ;
reconsider jj = 1 as
Element of
REAL by
NUMBERS: 19;
consider y9 be
Element of
REAL+ such that
A48: (x9
*' y9)
= jj by
A47,
ARYTM_2: 14;
reconsider y = y9 as
Element of
REAL by
Th1;
take y;
thus thesis by
A48,
Def2;
end;
suppose
A49: x
in
[:
{
0 },
REAL+ :];
not x
in
{
[
0 ,
0 ]} by
XBOOLE_0:def 5;
then
A50: x
<>
[
0 ,
0 ] by
TARSKI:def 1;
consider x1,x2 be
object such that x1
in
{
0 } and
A51: x2
in
REAL+ and
A52: x
=
[x1, x2] by
A49,
ZFMISC_1: 84;
reconsider 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 be
Element of
REAL+ such that
A53: (x2
*' y2)
= 1 by
ARYTM_2: 14;
A54:
now
assume
[
0 , y2]
in
{
[
0 ,
0 ]};
then
[
0 , y2]
=
[
0 ,
0 ] by
TARSKI:def 1;
then y2
=
0 by
XTUPLE_0: 1;
hence contradiction by
A53,
ARYTM_2: 4;
end;
A55:
[
0 , y2]
in
[:
{
0 },
REAL+ :] by
Lm1;
then
[
0 , y2]
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 3;
then
reconsider y =
[
0 , y2] as
Element of
REAL by
A54,
XBOOLE_0:def 5;
take y;
consider x9,y9 be
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 thesis by
A52,
A53,
A56,
A58,
XTUPLE_0: 1;
end;
end;
thus thesis;
end;
uniqueness
proof
let y,z be
Element of
REAL ;
thus x
<>
0 & (
* (x,y))
= 1 & (
* (x,z))
= 1 implies y
= z
proof
assume that
A59: x
<>
0 and
A60: (
* (x,y))
= 1 and
A61: (
* (x,z))
= 1;
A62: for x,y be
Element of
REAL st (
* (x,y))
= 1 holds x
<>
0
proof
let x,y be
Element of
REAL such that
A63: (
* (x,y))
= 1 and
A64: x
=
0 ;
A65: not x
in
[:
{
0 },
REAL+ :] by
A64,
Th5,
ARYTM_2: 20,
XBOOLE_0: 3;
A66: y
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
per cases by
A66,
XBOOLE_0:def 3;
suppose y
in
REAL+ ;
then ex x9,y9 be
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;
end;
suppose y
in
[:
{
0 },
REAL+ :];
then not y
in
REAL+ by
Th5,
XBOOLE_0: 3;
hence contradiction by
A63,
A64,
A65,
Def2;
end;
end;
then
A67: y
<>
0 by
A60;
A68: z
<>
0 by
A61,
A62;
per cases ;
suppose x
in
REAL+ & y
in
REAL+ & z
in
REAL+ ;
then (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & 1
= (x9
*' y9)) & ex x9,y9 be
Element of
REAL+ st x
= x9 & z
= y9 & 1
= (x9
*' y9) by
A60,
A61,
Def2;
hence thesis by
A59,
Th7;
end;
suppose that
A69: x
in
[:
{
0 },
REAL+ :] and
A70: y
in
[:
{
0 },
REAL+ :] and
A71: z
in
[:
{
0 },
REAL+ :];
consider x9,y9 be
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 be
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 thesis by
A72,
A73,
A75,
Th3,
Th7;
end;
suppose x
in
REAL+ & y
in
[:
{
0 },
REAL+ :];
then ex x9,y9 be
Element of
REAL+ st x
= x9 & y
=
[
0 , y9] & 1
=
[
0 , (x9
*' y9)] by
A59,
A60,
Def2;
hence thesis by
Lm2;
end;
suppose x
in
[:
{
0 },
REAL+ :] & y
in
REAL+ ;
then ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & y
= y9 & 1
=
[
0 , (y9
*' x9)] by
A60,
A67,
Def2;
hence thesis by
Lm2;
end;
suppose x
in
[:
{
0 },
REAL+ :] & z
in
REAL+ ;
then ex x9,z9 be
Element of
REAL+ st x
=
[
0 , x9] & z
= z9 & 1
=
[
0 , (z9
*' x9)] by
A61,
A68,
Def2;
hence thesis by
Lm2;
end;
suppose x
in
REAL+ & z
in
[:
{
0 },
REAL+ :];
then ex x9,z9 be
Element of
REAL+ st x
= x9 & z
=
[
0 , z9] & 1
=
[
0 , (x9
*' z9)] by
A59,
A61,
Def2;
hence thesis by
Lm2;
end;
suppose not (x
in
REAL+ & y
in
REAL+ ) & not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :] & x
<>
0 ) & not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :] & y
<>
0 ) & not (x
in
[:
{
0 },
REAL+ :] & y
in
[:
{
0 },
REAL+ :]);
hence thesis by
A60,
Def2;
end;
suppose not (x
in
REAL+ & z
in
REAL+ ) & not (x
in
REAL+ & z
in
[:
{
0 },
REAL+ :] & x
<>
0 ) & not (z
in
REAL+ & x
in
[:
{
0 },
REAL+ :] & z
<>
0 ) & not (x
in
[:
{
0 },
REAL+ :] & z
in
[:
{
0 },
REAL+ :]);
hence thesis by
A61,
Def2;
end;
end;
thus thesis;
end;
consistency ;
involutiveness
proof
let x,y be
Element of
REAL ;
assume that
A76: y
<>
0 implies (
* (y,x))
= 1 and
A77: y
=
0 implies x
=
0 ;
thus x
<>
0 implies (
* (x,y))
= 1 by
A76,
A77;
assume
A78: x
=
0 ;
A79: y
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
assume
A80: y
<>
0 ;
per cases by
A79,
XBOOLE_0:def 3;
suppose y
in
REAL+ ;
then ex x9,y9 be
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;
end;
suppose
A81: y
in
[:
{
0 },
REAL+ :];
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;
end;
end;
end
begin
Lm4: for x,y,z be
set st
[x, y]
=
{z} holds z
=
{x} & x
= y
proof
let x,y,z be
set;
assume
A1:
[x, y]
=
{z};
then
{x}
in
{z} by
TARSKI:def 2;
hence
A2: z
=
{x} by
TARSKI:def 1;
{x, y}
in
{z} by
A1,
TARSKI:def 2;
then
{x, y}
= z by
TARSKI:def 1;
hence thesis by
A2,
ZFMISC_1: 5;
end;
reserve i,j,k for
Element of
NAT ;
reserve a,b for
Element of
REAL ;
theorem ::
ARYTM_0:8
Th8: not ((
0 ,1)
--> (a,b))
in
REAL
proof
set IR = { A where A be
Subset of
RAT+ : for r be
Element of
RAT+ st r
in A holds (for s be
Element of
RAT+ st s
<=' r holds s
in A) & ex s be
Element of
RAT+ st s
in A & r
< s };
set f = ((
0 ,1)
--> (a,b));
A1:
now
f
=
{
[
0 , a],
[1, b]} by
FUNCT_4: 67;
then
A2:
[1, b]
in f by
TARSKI:def 2;
assume f
in
[:
{
{} },
REAL+ :];
then
consider x,y be
object such that
A3: x
in
{
{} } and y
in
REAL+ and
A4: f
=
[x, y] by
ZFMISC_1: 84;
x
=
0 by
A3,
TARSKI:def 1;
per cases by
A4,
A2,
TARSKI:def 2;
suppose
{
{1, b},
{1}}
=
{
0 };
then
0
in
{
{1, b},
{1}} by
TARSKI:def 1;
hence contradiction by
TARSKI:def 2;
end;
suppose
{
{1, b},
{1}}
=
{
0 , y};
then
0
in
{
{1, b},
{1}} by
TARSKI:def 2;
hence contradiction by
TARSKI:def 2;
end;
end;
A5: f
=
{
[
0 , a],
[1, b]} by
FUNCT_4: 67;
now
assume f
in {
[i, j] : (i,j)
are_coprime & j
<>
{} };
then
consider i, j such that
A6: f
=
[i, j] and (i,j)
are_coprime and j
<>
{} ;
A7:
{i}
in f &
{i, j}
in f by
A6,
TARSKI:def 2;
A8:
now
assume i
= j;
then
{i}
=
{i, j} by
ENUMSET1: 29;
then
A9:
[i, j]
=
{
{i}} by
ENUMSET1: 29;
then
[1, b]
in
{
{i}} by
A5,
A6,
TARSKI:def 2;
then
A10:
[1, b]
=
{i} by
TARSKI:def 1;
[
0 , a]
in
{
{i}} by
A5,
A6,
A9,
TARSKI:def 2;
then
[
0 , a]
=
{i} by
TARSKI:def 1;
hence contradiction by
A10,
XTUPLE_0: 1;
end;
per cases by
A5,
A7,
TARSKI:def 2;
suppose
{i, j}
=
[
0 , a] &
{i}
=
[
0 , a];
hence contradiction by
A8,
ZFMISC_1: 5;
end;
suppose that
A11:
{i, j}
=
[
0 , a] and
A12:
{i}
=
[1, b];
i
in
{i, j} by
TARSKI:def 2;
then i
=
{
0 , a} or i
=
{
0 } by
A11,
TARSKI:def 2;
then
A13:
0
in i by
TARSKI:def 1,
TARSKI:def 2;
i
=
{1} by
A12,
Lm4;
hence contradiction by
A13,
TARSKI:def 1;
end;
suppose that
A14:
{i, j}
=
[1, b] and
A15:
{i}
=
[
0 , a];
i
in
{i, j} by
TARSKI:def 2;
then i
=
{1, b} or i
=
{1} by
A14,
TARSKI:def 2;
then
A16: 1
in i by
TARSKI:def 1,
TARSKI:def 2;
i
=
{
0 } by
A15,
Lm4;
hence contradiction by
A16,
TARSKI:def 1;
end;
suppose
{i, j}
=
[1, b] &
{i}
=
[1, b];
hence contradiction by
A8,
ZFMISC_1: 5;
end;
end;
then
A17: not f
in ({
[i, j] : (i,j)
are_coprime & j
<>
{} }
\ the set of all
[k, 1]);
not ex x,y be
set st
{
[
0 , x],
[1, y]}
in IR
proof
given x,y be
set such that
A18:
{
[
0 , x],
[1, y]}
in IR;
consider A be
Subset of
RAT+ such that
A19:
{
[
0 , x],
[1, y]}
= A and
A20: for r be
Element of
RAT+ st r
in A holds (for s be
Element of
RAT+ st s
<=' r holds s
in A) & ex s be
Element of
RAT+ st s
in A & r
< s by
A18;
[
0 , x]
in A & for r,s be
Element of
RAT+ st r
in A & s
<=' r holds s
in A by
A19,
A20,
TARSKI:def 2;
then
consider r1,r2,r3 be
Element of
RAT+ such that
A21: r1
in A and
A22: r2
in A and
A23: r3
in A & r1
<> r2 & r2
<> r3 & r3
<> r1 by
ARYTM_3: 75;
A24: r2
=
[
0 , x] or r2
=
[1, y] by
A19,
A22,
TARSKI:def 2;
r1
=
[
0 , x] or r1
=
[1, y] by
A19,
A21,
TARSKI:def 2;
hence contradiction by
A19,
A23,
A24,
TARSKI:def 2;
end;
then
A25: not f
in
DEDEKIND_CUTS by
A5,
ARYTM_2:def 1;
now
assume f
in
omega ;
then
{}
in f by
ORDINAL3: 8;
hence contradiction by
A5,
TARSKI:def 2;
end;
then not f
in
RAT+ by
A17,
XBOOLE_0:def 3;
then not f
in
REAL+ by
A25,
ARYTM_2:def 2,
XBOOLE_0:def 3;
hence thesis by
A1,
XBOOLE_0:def 3;
end;
definition
let x,y be
Element of
REAL ;
::
ARYTM_0:def5
func
[*x,y*] ->
Element of
COMPLEX equals
:
Def5: x if y
=
0
otherwise ((
0 ,1)
--> (x,y));
consistency ;
coherence
proof
set z = ((
0 ,1)
--> (x,y));
thus y
=
0 implies x is
Element of
COMPLEX by
XBOOLE_0:def 3;
assume
A1: y
<>
0 ;
A2:
now
assume z
in { r where r be
Element of (
Funcs (
{
0 , 1},
REAL )) : (r
. 1)
=
0 };
then ex r be
Element of (
Funcs (
{
0 , 1},
REAL )) st z
= r & (r
. 1)
=
0 ;
hence contradiction by
A1,
FUNCT_4: 63;
end;
z
in (
Funcs (
{
0 , 1},
REAL )) by
FUNCT_2: 8;
then z
in ((
Funcs (
{
0 , 1},
REAL ))
\ { r where r be
Element of (
Funcs (
{
0 , 1},
REAL )) : (r
. 1)
=
0 }) by
A2,
XBOOLE_0:def 5;
hence thesis by
XBOOLE_0:def 3;
end;
end
theorem ::
ARYTM_0:9
for c be
Element of
COMPLEX holds ex r,s be
Element of
REAL st c
=
[*r, s*]
proof
let c be
Element of
COMPLEX ;
per cases ;
suppose c
in
REAL ;
then
reconsider r = c, z =
0 as
Element of
REAL by
Lm3;
take r, z;
thus thesis by
Def5;
end;
suppose not c
in
REAL ;
then
A1: c
in ((
Funcs (
{
0 , 1},
REAL ))
\ { x where x be
Element of (
Funcs (
{
0 , 1},
REAL )) : (x
. 1)
=
0 }) by
XBOOLE_0:def 3;
then
consider f be
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, s;
A6: c
= ((
0 ,1)
--> (r,s)) by
A2,
A3,
FUNCT_4: 66;
now
assume s
=
0 ;
then (((
0 ,1)
--> (r,s))
. 1)
=
0 by
FUNCT_4: 63;
then c
in { x where x be
Element of (
Funcs (
{
0 , 1},
REAL )) : (x
. 1)
=
0 } by
A1,
A6;
hence contradiction by
A1,
XBOOLE_0:def 5;
end;
hence thesis by
A6,
Def5;
end;
end;
theorem ::
ARYTM_0:10
for x1,x2,y1,y2 be
Element of
REAL st
[*x1, x2*]
=
[*y1, y2*] holds x1
= y1 & x2
= y2
proof
let x1,x2,y1,y2 be
Element of
REAL such that
A1:
[*x1, x2*]
=
[*y1, y2*];
per cases ;
suppose
A2: x2
=
0 ;
then
A3:
[*x1, x2*]
= x1 by
Def5;
A4:
now
assume y2
<>
0 ;
then x1
= ((
0 ,1)
--> (y1,y2)) by
A1,
A3,
Def5;
hence contradiction by
Th8;
end;
hence x1
= y1 by
A1,
A3,
Def5;
thus thesis by
A2,
A4;
end;
suppose x2
<>
0 ;
then
A5:
[*y1, y2*]
= ((
0 ,1)
--> (x1,x2)) by
A1,
Def5;
now
assume y2
=
0 ;
then
[*y1, y2*]
= y1 by
Def5;
hence contradiction by
A5,
Th8;
end;
then
[*y1, y2*]
= ((
0 ,1)
--> (y1,y2)) by
Def5;
hence thesis by
A5,
FUNCT_4: 68;
end;
end;
set RR = (
[:
{
0 },
REAL+ :]
\
{
[
0 ,
0 ]});
theorem ::
ARYTM_0:11
Th11: for x,o be
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 such that
A1: o
=
0 ;
per cases ;
suppose x
in
REAL+ ;
then
reconsider x9 = x as
Element of
REAL+ ;
x9
= (x9
+ y9) by
ARYTM_2:def 8;
hence thesis by
A1,
Def1;
end;
suppose
A2: not x
in
REAL+ ;
x
in (
REAL+
\/
[:
{
{} },
REAL+ :]) by
XBOOLE_0:def 5;
then
A3: x
in
[:
{
{} },
REAL+ :] by
A2,
XBOOLE_0:def 3;
then
consider x1,x2 be
object 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 thesis by
A1,
A3,
A6,
A7,
Def1;
end;
end;
theorem ::
ARYTM_0:12
Th12: for x,o be
Element of
REAL st o
=
0 holds (
* (x,o))
=
0
proof
let x,o be
Element of
REAL such that
A1: o
=
0 ;
per cases ;
suppose x
in
REAL+ ;
then
reconsider x9 = x, y9 =
0 as
Element of
REAL+ by
ARYTM_2: 20;
0
= (x9
*' y9) by
ARYTM_2: 4;
hence thesis by
A1,
Def2;
end;
suppose
A2: not x
in
REAL+ ;
not o
in
[:
{
{} },
REAL+ :] by
A1,
Th5,
ARYTM_2: 20,
XBOOLE_0: 3;
hence thesis by
A1,
A2,
Def2;
end;
end;
theorem ::
ARYTM_0:13
Th13: for x,y,z be
Element of
REAL holds (
* (x,(
* (y,z))))
= (
* ((
* (x,y)),z))
proof
let x,y,z be
Element of
REAL ;
reconsider o =
0 as
Element of
REAL by
Lm3;
per cases ;
suppose that
A1: x
in
REAL+ and
A2: y
in
REAL+ and
A3: z
in
REAL+ ;
A4: ex x99,y99 be
Element of
REAL+ st x
= x99 & y
= y99 & (
* (x,y))
= (x99
*' y99) by
A1,
A2,
Def2;
then
A5: ex xy99,z99 be
Element of
REAL+ st (
* (x,y))
= xy99 & z
= z99 & (
* ((
* (x,y)),z))
= (xy99
*' z99) by
A3,
Def2;
A6: ex y9,z9 be
Element of
REAL+ st y
= y9 & z
= z9 & (
* (y,z))
= (y9
*' z9) by
A2,
A3,
Def2;
then ex x9,yz9 be
Element of
REAL+ st x
= x9 & (
* (y,z))
= yz9 & (
* (x,(
* (y,z))))
= (x9
*' yz9) by
A1,
Def2;
hence thesis by
A6,
A4,
A5,
ARYTM_2: 12;
end;
suppose that
A7: x
in
REAL+ & x
<>
0 and
A8: y
in RR and
A9: z
in
REAL+ & z
<>
0 ;
consider y9,z9 be
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;
then
consider x9,yz9 be
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 be
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;
then
consider xy99,z99 be
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;
end;
suppose that
A22: x
in RR and
A23: y
in
REAL+ & y
<>
0 and
A24: z
in
REAL+ & z
<>
0 ;
consider y9,z9 be
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 be
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 be
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;
then
consider xy99,z99 be
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;
end;
suppose that
A35: x
in RR and
A36: y
in RR and
A37: z
in
REAL+ & z
<>
0 ;
consider x99,y99 be
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 be
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;
then
consider x9,yz9 be
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 be
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;
end;
suppose that
A49: x
in
REAL+ & x
<>
0 and
A50: y
in
REAL+ & y
<>
0 and
A51: z
in RR;
A52: ex x99,y99 be
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 be
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 be
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;
then
consider x9,yz9 be
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;
end;
suppose that
A62: x
in
REAL+ & x
<>
0 and
A63: y
in RR and
A64: z
in RR;
consider y9,z9 be
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 be
Element of
REAL+ st x
= x9 & (
* (y,z))
= yz9 & (
* (x,(
* (y,z))))
= (x9
*' yz9) by
A62,
A67,
Def2;
consider x99,y99 be
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;
then
consider xy99,z99 be
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;
end;
suppose that
A76: y
in
REAL+ & y
<>
0 and
A77: x
in RR and
A78: z
in RR;
consider x99,y99 be
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 be
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;
then
consider x9,yz9 be
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;
then
consider xy99,z99 be
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;
end;
suppose that
A92: x
in RR and
A93: y
in RR and
A94: z
in RR;
consider y9,z9 be
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
XBOOLE_0:def 5;
then
A98: y9
<>
0 by
A95,
TARSKI:def 1;
not z
in
{
[
0 ,
0 ]} by
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 be
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 be
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
XBOOLE_0:def 5;
then
A106: y9
<>
0 by
A95,
TARSKI:def 1;
not x
in
{
[
0 ,
0 ]} by
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 be
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 thesis by
A97,
A100,
A103,
A104,
A105,
A107,
A109,
ARYTM_2: 12;
end;
suppose
A110: x
=
0 ;
hence (
* (x,(
* (y,z))))
=
0 by
Th12
.= (
* (o,z)) by
Th12
.= (
* ((
* (x,y)),z)) by
A110,
Th12;
end;
suppose
A111: y
=
0 ;
hence (
* (x,(
* (y,z))))
= (
* (x,o)) by
Th12
.=
0 by
Th12
.= (
* (o,z)) by
Th12
.= (
* ((
* (x,y)),z)) by
A111,
Th12;
end;
suppose
A112: z
=
0 ;
hence (
* (x,(
* (y,z))))
= (
* (x,o)) by
Th12
.=
0 by
Th12
.= (
* ((
* (x,y)),z)) by
A112,
Th12;
end;
suppose
A113: not (x
in
REAL+ & y
in
REAL+ & z
in
REAL+ ) & not (x
in
REAL+ & y
in RR & z
in
REAL+ ) & not (y
in
REAL+ & x
in RR & z
in
REAL+ ) & not (x
in RR & y
in RR & z
in
REAL+ ) & not (x
in
REAL+ & y
in
REAL+ & z
in RR) & not (x
in
REAL+ & y
in RR & z
in RR) & not (y
in
REAL+ & x
in RR & z
in RR) & not (x
in RR & y
in RR & z
in RR);
REAL
= ((
REAL+
\
{
[
{} ,
{} ]})
\/ (
[:
{
{} },
REAL+ :]
\
{
[
{} ,
{} ]})) by
XBOOLE_1: 42
.= (
REAL+
\/ RR) by
ARYTM_2: 3,
ZFMISC_1: 57;
hence thesis by
A113,
XBOOLE_0:def 3;
end;
end;
theorem ::
ARYTM_0:14
Th14: for x,y,z be
Element of
REAL holds (
* (x,(
+ (y,z))))
= (
+ ((
* (x,y)),(
* (x,z))))
proof
let x,y,z be
Element of
REAL ;
reconsider o =
0 as
Element of
REAL by
Lm3;
per cases ;
suppose
A1: x
=
0 ;
hence (
* (x,(
+ (y,z))))
=
0 by
Th12
.= (
+ (o,o)) by
Th11
.= (
+ ((
* (x,y)),o)) by
A1,
Th12
.= (
+ ((
* (x,y)),(
* (x,z)))) by
A1,
Th12;
end;
suppose that
A2: x
in
REAL+ and
A3: y
in
REAL+ & z
in
REAL+ ;
A4: (ex x9,y9 be
Element of
REAL+ st x
= x9 & y
= y9 & (
* (x,y))
= (x9
*' y9)) & ex x99,z9 be
Element of
REAL+ st x
= x99 & z
= z9 & (
* (x,z))
= (x99
*' z9) by
A2,
A3,
Def2;
then
A5: ex xy9,xz9 be
Element of
REAL+ st (
* (x,y))
= xy9 & (
* (x,z))
= xz9 & (
+ ((
* (x,y)),(
* (x,z))))
= (xy9
+ xz9) by
Def1;
A6: ex y99,z99 be
Element of
REAL+ st y
= y99 & z
= z99 & (
+ (y,z))
= (y99
+ z99) by
A3,
Def1;
then ex x999,yz9 be
Element of
REAL+ st x
= x999 & (
+ (y,z))
= yz9 & (
* (x,(
+ (y,z))))
= (x999
*' yz9) by
A2,
Def2;
hence thesis by
A4,
A5,
A6,
ARYTM_2: 13;
end;
suppose that
A7: x
in
REAL+ & x
<>
0 and
A8: y
in
REAL+ and
A9: z
in RR;
consider y99,z99 be
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 be
Element of
REAL+ such that
A13: x
= x9 & y
= y9 and
A14: (
* (x,y))
= (x9
*' y9) by
A7,
A8,
Def2;
consider x99,z9 be
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;
then
A18: ex xy9,xz9 be
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
per cases ;
suppose
A20: z99
<=' y99;
then
A21: (
+ (y,z))
= (y99
-' z99) by
A12,
ARYTM_1:def 2;
then ex x999,yz9 be
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;
end;
suppose
A22: not z99
<=' y99;
then
A23: (
+ (y,z))
=
[
0 , (z99
-' y99)] by
A12,
ARYTM_1:def 2;
then (
+ (y,z))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider x999,yz9 be
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;
end;
end;
hence thesis;
end;
suppose that
A26: x
in
REAL+ & x
<>
0 and
A27: z
in
REAL+ and
A28: y
in RR;
consider z99,y99 be
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 be
Element of
REAL+ such that
A32: x
= x9 & z
= z9 and
A33: (
* (x,z))
= (x9
*' z9) by
A26,
A27,
Def2;
consider x99,y9 be
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;
then
A37: ex xz9,xy9 be
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
per cases ;
suppose
A39: y99
<=' z99;
then
A40: (
+ (z,y))
= (z99
-' y99) by
A31,
ARYTM_1:def 2;
then ex x999,zy9 be
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;
end;
suppose
A41: not y99
<=' z99;
then
A42: (
+ (z,y))
=
[
0 , (y99
-' z99)] by
A31,
ARYTM_1:def 2;
then (
+ (z,y))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider x999,zy9 be
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;
end;
end;
hence thesis;
end;
suppose that
A45: x
in
REAL+ & x
<>
0 and
A46: y
in RR and
A47: z
in RR;
( not (y
in
REAL+ & z
in
[:
{
0 },
REAL+ :])) & not (y
in
[:
{
0 },
REAL+ :] & z
in
REAL+ ) by
A46,
A47,
Th5,
XBOOLE_0: 3;
then
consider y99,z99 be
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;
then
consider x999,yz9 be
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 be
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 be
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;
then
A60: not ((
* (x,y))
in
[:
{
0 },
REAL+ :] & (
* (x,z))
in
REAL+ ) by
Th5,
XBOOLE_0: 3;
(
* (x,y))
in
[:
{
0 },
REAL+ :] by
A55,
Lm1;
then not ((
* (x,y))
in
REAL+ & (
* (x,z))
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider xy9,xz9 be
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;
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;
end;
suppose that
A65: x
in RR and
A66: y
in
REAL+ and
A67: z
in
REAL+ ;
consider y99,z99 be
Element of
REAL+ such that
A68: y
= y99 and
A69: z
= z99 and
A70: (
+ (y,z))
= (y99
+ z99) by
A66,
A67,
Def1;
now
per cases ;
suppose that
A71: y
<>
0 and
A72: z
<>
0 ;
consider x99,z9 be
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 be
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 be
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;
then
A82: not ((
* (x,y))
in
[:
{
0 },
REAL+ :] & (
* (x,z))
in
REAL+ ) by
Th5,
XBOOLE_0: 3;
(
* (x,y))
in
[:
{
0 },
REAL+ :] by
A80,
Lm1;
then not ((
* (x,y))
in
REAL+ & (
* (x,z))
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider xy9,xz9 be
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;
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;
end;
suppose
A86: x
=
0 ;
hence (
* (x,(
+ (y,z))))
=
0 by
Th12
.= (
+ (o,o)) by
Th11
.= (
+ ((
* (x,y)),o)) by
A86,
Th12
.= (
+ ((
* (x,y)),(
* (x,z)))) by
A86,
Th12;
end;
suppose
A87: z
=
0 ;
hence (
* (x,(
+ (y,z))))
= (
* (x,y)) by
Th11
.= (
+ ((
* (x,y)),(
* (x,z)))) by
A87,
Th11,
Th12;
end;
suppose
A88: y
=
0 ;
hence (
* (x,(
+ (y,z))))
= (
* (x,z)) by
Th11
.= (
+ ((
* (x,y)),(
* (x,z)))) by
A88,
Th11,
Th12;
end;
end;
hence thesis;
end;
suppose that
A89: x
in RR and
A90: y
in
REAL+ and
A91: z
in RR;
consider x99,z9 be
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
per cases ;
suppose y
<>
0 ;
then
consider x9,y9 be
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;
then
consider xy9,xz9 be
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 be
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
per cases ;
suppose
A104: z99
<=' y99;
then
A105: (
+ (y,z))
= (y99
-' z99) by
A102,
ARYTM_1:def 2;
now
per cases ;
suppose
A106: (
+ (y,z))
<>
0 ;
then
consider x999,yz9 be
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
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;
end;
suppose
A112: (
+ (y,z))
=
0 ;
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;
end;
end;
hence thesis;
end;
suppose
A115: not z99
<=' y99;
then
A116: (
+ (y,z))
=
[
0 , (z99
-' y99)] by
A102,
ARYTM_1:def 2;
then (
+ (y,z))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider x999,yz9 be
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;
end;
end;
hence thesis;
end;
suppose
A121: y
=
0 ;
hence (
* (x,(
+ (y,z))))
= (
* (x,z)) by
Th11
.= (
+ ((
* (x,y)),(
* (x,z)))) by
A121,
Th11,
Th12;
end;
end;
hence thesis;
end;
suppose that
A122: x
in RR and
A123: z
in
REAL+ and
A124: y
in RR;
consider x99,y9 be
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
per cases ;
suppose z
<>
0 ;
then
consider x9,z9 be
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;
then
consider xz9,xy9 be
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 be
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
per cases ;
suppose
A137: y99
<=' z99;
then
A138: (
+ (z,y))
= (z99
-' y99) by
A135,
ARYTM_1:def 2;
now
per cases ;
suppose
A139: (
+ (z,y))
<>
0 ;
then
consider x999,zy9 be
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
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;
end;
suppose
A145: (
+ (z,y))
=
0 ;
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;
end;
end;
hence thesis;
end;
suppose
A148: not y99
<=' z99;
then
A149: (
+ (z,y))
=
[
0 , (y99
-' z99)] by
A135,
ARYTM_1:def 2;
then (
+ (z,y))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider x999,zy9 be
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;
end;
end;
hence thesis;
end;
suppose
A154: z
=
0 ;
hence (
* (x,(
+ (y,z))))
= (
* (x,y)) by
Th11
.= (
+ ((
* (x,y)),(
* (x,z)))) by
A154,
Th11,
Th12;
end;
end;
hence thesis;
end;
suppose that
A155: x
in RR and
A156: y
in RR and
A157: z
in RR;
( not (y
in
REAL+ & z
in
[:
{
0 },
REAL+ :])) & not (y
in
[:
{
0 },
REAL+ :] & z
in
REAL+ ) by
A156,
A157,
Th5,
XBOOLE_0: 3;
then
consider y99,z99 be
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 be
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 be
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;
then
consider x999,yz9 be
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 be
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;
end;
suppose
A173: not (x
in
REAL+ & y
in
REAL+ & z
in
REAL+ ) & not (x
in
REAL+ & y
in
REAL+ & z
in RR) & not (x
in
REAL+ & y
in RR & z
in
REAL+ ) & not (x
in
REAL+ & y
in RR & z
in RR) & not (x
in RR & y
in
REAL+ & z
in
REAL+ ) & not (x
in RR & y
in
REAL+ & z
in RR) & not (x
in RR & y
in RR & z
in
REAL+ ) & not (x
in RR & y
in RR & z
in RR);
REAL
= ((
REAL+
\
{
[
0 ,
0 ]})
\/ (
[:
{
0 },
REAL+ :]
\
{
[
0 ,
0 ]})) by
XBOOLE_1: 42
.= (
REAL+
\/ RR) by
ARYTM_2: 3,
ZFMISC_1: 57;
hence thesis by
A173,
XBOOLE_0:def 3;
end;
end;
theorem ::
ARYTM_0:15
for x,y be
Element of
REAL holds (
* ((
opp x),y))
= (
opp (
* (x,y)))
proof
let x,y be
Element of
REAL ;
(
+ ((
* ((
opp x),y)),(
* (x,y))))
= (
* ((
+ ((
opp x),x)),y)) by
Th14
.=
0 by
Th12,
Def3;
hence thesis by
Def3;
end;
theorem ::
ARYTM_0:16
Th16: for x be
Element of
REAL holds (
* (x,x))
in
REAL+
proof
let x be
Element of
REAL ;
A1: x
in (
REAL+
\/
[:
{
{} },
REAL+ :]) by
XBOOLE_0:def 5;
per cases by
A1,
XBOOLE_0:def 3;
suppose x
in
REAL+ ;
then ex x9,y9 be
Element of
REAL+ st x
= x9 & x
= y9 & (
* (x,x))
= (x9
*' y9) by
Def2;
hence thesis;
end;
suppose x
in
[:
{
0 },
REAL+ :];
then ex x9,y9 be
Element of
REAL+ st x
=
[
0 , x9] & x
=
[
0 , y9] & (
* (x,x))
= (y9
*' x9) by
Def2;
hence thesis;
end;
end;
theorem ::
ARYTM_0:17
for x, y st (
+ ((
* (x,x)),(
* (y,y))))
=
0 holds x
=
0
proof
let x, y such that
A1: (
+ ((
* (x,x)),(
* (y,y))))
=
0 ;
(
* (x,x))
in
REAL+ & (
* (y,y))
in
REAL+ by
Th16;
then
consider x9,y9 be
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
XBOOLE_0:def 5;
per cases by
A5,
XBOOLE_0:def 3;
suppose x
in
REAL+ ;
then ex x9,y9 be
Element of
REAL+ st x
= x9 & x
= y9 &
0
= (x9
*' y9) by
A2,
A4,
Def2;
hence thesis by
ARYTM_1: 2;
end;
suppose x
in
[:
{
0 },
REAL+ :];
then
consider x9,y9 be
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 thesis by
XBOOLE_0:def 5;
end;
end;
theorem ::
ARYTM_0:18
Th18: for x,y,z be
Element of
REAL st x
<>
0 & (
* (x,y))
= 1 & (
* (x,z))
= 1 holds y
= z
proof
let x,y,z be
Element of
REAL ;
assume that
A1: x
<>
0 and
A2: (
* (x,y))
= 1 and
A3: (
* (x,z))
= 1;
thus y
= (
inv x) by
A1,
A2,
Def4
.= z by
A1,
A3,
Def4;
end;
theorem ::
ARYTM_0:19
Th19: for x, y st y
= 1 holds (
* (x,y))
= x
proof
let x, y such that
A1: y
= 1;
per cases ;
suppose x
=
0 ;
hence thesis by
Th12;
end;
suppose
A2: x
<>
0 ;
A3:
now
assume
A4: (
inv x)
=
0 ;
thus 1
= (
* (x,(
inv x))) by
A2,
Def4
.=
0 by
A4,
Th12;
end;
A5: ex x9,y9 be
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 thesis by
A3,
A6,
Th18;
end;
end;
theorem ::
ARYTM_0:20
for x, y st y
<>
0 holds (
* ((
* (x,y)),(
inv y)))
= x
proof
reconsider jj = 1 as
Element of
REAL by
NUMBERS: 19;
let x, y such that
A1: y
<>
0 ;
thus (
* ((
* (x,y)),(
inv y)))
= (
* (x,(
* (y,(
inv y))))) by
Th13
.= (
* (x,jj)) by
A1,
Def4
.= x by
Th19;
end;
theorem ::
ARYTM_0:21
Th21: for x, y st (
* (x,y))
=
0 holds x
=
0 or y
=
0
proof
reconsider jj = 1 as
Element of
REAL by
NUMBERS: 19;
let x, y such that
A1: (
* (x,y))
=
0 and
A2: x
<>
0 ;
A3: (
* (x,(
inv x)))
= 1 by
A2,
Def4;
thus y
= (
* (jj,y)) by
Th19
.= (
* ((
* (x,y)),(
inv x))) by
A3,
Th13
.=
0 by
A1,
Th12;
end;
theorem ::
ARYTM_0:22
for x, y holds (
inv (
* (x,y)))
= (
* ((
inv x),(
inv y)))
proof
reconsider jj = 1 as
Element of
REAL by
NUMBERS: 19;
let x, y;
per cases ;
suppose
A1: x
=
0 or y
=
0 ;
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;
end;
suppose that
A3: x
<>
0 and
A4: y
<>
0 ;
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
.= (
* ((
* (jj,y)),(
inv y))) by
A6,
Th13
.= 1 by
A7,
Th19;
hence thesis by
A5,
Def4;
end;
end;
theorem ::
ARYTM_0:23
Th23: for x,y,z be
Element of
REAL holds (
+ (x,(
+ (y,z))))
= (
+ ((
+ (x,y)),z))
proof
let x,y,z be
Element of
REAL ;
A1: x
in (
REAL+
\/
[:
{
0 },
REAL+ :]) & y
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
A2: z
in (
REAL+
\/
[:
{
0 },
REAL+ :]) by
XBOOLE_0:def 5;
per cases by
A1,
A2,
XBOOLE_0:def 3;
suppose that
A3: x
in
REAL+ and
A4: y
in
REAL+ and
A5: z
in
REAL+ ;
A6: ex x99,y99 be
Element of
REAL+ st x
= x99 & y
= y99 & (
+ (x,y))
= (x99
+ y99) by
A3,
A4,
Def1;
then
A7: ex xy99,z99 be
Element of
REAL+ st (
+ (x,y))
= xy99 & z
= z99 & (
+ ((
+ (x,y)),z))
= (xy99
+ z99) by
A5,
Def1;
A8: ex y9,z9 be
Element of
REAL+ st y
= y9 & z
= z9 & (
+ (y,z))
= (y9
+ z9) by
A4,
A5,
Def1;
then ex x9,yz9 be
Element of
REAL+ st x
= x9 & (
+ (y,z))
= yz9 & (
+ (x,(
+ (y,z))))
= (x9
+ yz9) by
A3,
Def1;
hence thesis by
A8,
A6,
A7,
ARYTM_2: 6;
end;
suppose that
A9: x
in
REAL+ and
A10: y
in
REAL+ and
A11: z
in
[:
{
0 },
REAL+ :];
A12: ex x99,y99 be
Element of
REAL+ st x
= x99 & y
= y99 & (
+ (x,y))
= (x99
+ y99) by
A9,
A10,
Def1;
then
consider xy99,z99 be
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 be
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
per cases ;
suppose
A20: z9
<=' y9;
then
A21: (
+ (y,z))
= (y9
-' z9) by
A18,
ARYTM_1:def 2;
then ex x9,yz9 be
Element of
REAL+ st x
= x9 & (
+ (y,z))
= yz9 & (
+ (x,(
+ (y,z))))
= (x9
+ yz9) by
A9,
Def1;
hence thesis by
A16,
A12,
A13,
A15,
A19,
A20,
A21,
ARYTM_1: 20;
end;
suppose
A22: not z9
<=' y9;
then
A23: (
+ (y,z))
=
[
0 , (z9
-' y9)] by
A18,
ARYTM_1:def 2;
then (
+ (y,z))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider x9,yz9 be
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;
end;
end;
hence thesis;
end;
suppose that
A26: x
in
REAL+ and
A27: y
in
[:
{
0 },
REAL+ :] and
A28: z
in
REAL+ ;
consider x99,y99 be
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 be
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
per cases ;
suppose that
A36: y9
<=' x99 and
A37: y9
<=' z9;
A38: (
+ (y,z))
= (z9
-' y9) by
A34,
A37,
ARYTM_1:def 2;
then
consider x9,yz9 be
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 be
Element of
REAL+ st z
= z99 & (
+ (x,y))
= xy99 & (
+ (z,(
+ (x,y))))
= (z99
+ xy99) by
A28,
Def1;
hence thesis by
A32,
A29,
A36,
A37,
A38,
A39,
A40,
A41,
ARYTM_1: 12;
end;
suppose that
A42: y9
<=' x99 and
A43: not y9
<=' z9;
A44: (
+ (x,y))
= (x99
-' y9) by
A31,
A35,
A42,
ARYTM_1:def 2;
then
A45: ex z99,xy99 be
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;
then
consider x9,yz9 be
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;
end;
suppose that
A49: not y9
<=' x99 and
A50: y9
<=' z9;
A51: (
+ (y,x))
=
[
0 , (y9
-' x99)] by
A31,
A35,
A49,
ARYTM_1:def 2;
then (
+ (y,x))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider z99,yx99 be
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 be
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;
end;
suppose that
A55: not y9
<=' x99 and
A56: not y9
<=' z9;
A57: (
+ (y,z))
=
[
0 , (y9
-' z9)] by
A34,
A56,
ARYTM_1:def 2;
then (
+ (y,z))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider x9,yz9 be
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;
then
consider z99,yx99 be
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;
end;
end;
hence thesis;
end;
suppose that
A63: x
in
REAL+ and
A64: y
in
[:
{
0 },
REAL+ :] and
A65: z
in
[:
{
0 },
REAL+ :];
( not (z
in
REAL+ & y
in
[:
{
0 },
REAL+ :])) & not (y
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) by
A64,
A65,
Th5,
XBOOLE_0: 3;
then
consider y9,z9 be
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;
then
consider x9,yz9 be
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 be
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
per cases ;
suppose
A76: y99
<=' x99;
then
A77: (
+ (x,y))
= (x99
-' y99) by
A74,
ARYTM_1:def 2;
then
consider xy99,z99 be
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;
end;
suppose
A82: not y99
<=' x99;
A83: not (z
in
REAL+ & (
+ (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;
then not ((
+ (x,y))
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider xy99,z99 be
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;
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;
end;
end;
hence thesis;
end;
suppose that
A90: z
in
REAL+ and
A91: y
in
REAL+ and
A92: x
in
[:
{
0 },
REAL+ :];
A93: ex z99,y99 be
Element of
REAL+ st z
= z99 & y
= y99 & (
+ (z,y))
= (z99
+ y99) by
A90,
A91,
Def1;
then
consider zy99,x99 be
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 be
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
per cases ;
suppose
A101: x9
<=' y9;
then
A102: (
+ (y,x))
= (y9
-' x9) by
A99,
ARYTM_1:def 2;
then ex z9,yx9 be
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;
end;
suppose
A103: not x9
<=' y9;
then
A104: (
+ (y,x))
=
[
0 , (x9
-' y9)] by
A99,
ARYTM_1:def 2;
then (
+ (y,x))
in
[:
{
0 },
REAL+ :] by
Lm1;
then
consider z9,yx9 be
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;
end;
end;
hence thesis;
end;
suppose that
A107: x
in
[:
{
0 },
REAL+ :] and
A108: y
in
REAL+ and
A109: z
in
[:
{
0 },
REAL+ :];
consider y9,z9 be
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 be
Element of
REAL+ such that
A113: x
=
[
0 , x99] and
A114: y
= y99 and
A115: (
+ (x,y))
= (y99
- x99) by
A107,
A108,
Def1;
now
per cases ;
suppose that
A116: x99
<=' y99 and
A117: z9
<=' y9;
A118: (
+ (y,z))
= (y9
-' z9) by
A112,
A117,
ARYTM_1:def 2;
then
consider x9,yz9 be
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 be
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 thesis by
A110,
A114,
A116,
A117,
A118,
A120,
A121,
A122,
A124,
ARYTM_1: 25;
end;
suppose that
A125: not x99
<=' y99 and
A126: z9
<=' y9;
A127: not (z
in
REAL+ & (
+ (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;
then not ((
+ (x,y))
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider z99,yx9 be
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;
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 be
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;
end;
suppose that
A137: not z9
<=' y9 and
A138: x99
<=' y99;
A139: not (x
in
REAL+ & (
+ (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;
then not ((
+ (z,y))
in
REAL+ & x
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider x9,yz99 be
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;
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 be
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;
end;
suppose that
A150: not x99
<=' y99 and
A151: not z9
<=' y9;
A152: not (x
in
REAL+ & (
+ (z,y))
in
[:
{
0 },
REAL+ :]) by
A107,
Th5,
XBOOLE_0: 3;
A153: not (z
in
REAL+ & (
+ (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;
then not ((
+ (x,y))
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider z99,yx9 be
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;
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;
then not ((
+ (z,y))
in
REAL+ & x
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider x9,yz99 be
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;
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;
end;
end;
hence thesis;
end;
suppose that
A162: z
in
REAL+ and
A163: y
in
[:
{
0 },
REAL+ :] and
A164: x
in
[:
{
0 },
REAL+ :];
( not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :])) & not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]) by
A163,
A164,
Th5,
XBOOLE_0: 3;
then
consider y9,x9 be
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;
then
consider z9,yx9 be
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 be
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
per cases ;
suppose
A175: y99
<=' z99;
then
A176: (
+ (z,y))
= (z99
-' y99) by
A173,
ARYTM_1:def 2;
then
consider zy99,x99 be
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;
end;
suppose
A181: not y99
<=' z99;
A182: not (x
in
REAL+ & (
+ (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;
then not ((
+ (z,y))
in
REAL+ & x
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider zy99,x99 be
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;
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;
end;
end;
hence thesis;
end;
suppose that
A189: x
in
[:
{
0 },
REAL+ :] and
A190: y
in
[:
{
0 },
REAL+ :] and
A191: z
in
[:
{
0 },
REAL+ :];
A192: not (x
in
REAL+ & (
+ (z,y))
in
[:
{
0 },
REAL+ :]) by
A189,
Th5,
XBOOLE_0: 3;
( not (z
in
REAL+ & y
in
[:
{
0 },
REAL+ :])) & not (y
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) by
A190,
A191,
Th5,
XBOOLE_0: 3;
then
consider y9,z9 be
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;
then not ((
+ (z,y))
in
REAL+ & x
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider x9,yz9 be
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;
A198: not (z
in
REAL+ & (
+ (x,y))
in
[:
{
0 },
REAL+ :]) by
A191,
Th5,
XBOOLE_0: 3;
( not (x
in
REAL+ & y
in
[:
{
0 },
REAL+ :])) & not (y
in
REAL+ & x
in
[:
{
0 },
REAL+ :]) by
A189,
A190,
Th5,
XBOOLE_0: 3;
then
consider x99,y99 be
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;
then not ((
+ (x,y))
in
REAL+ & z
in
[:
{
0 },
REAL+ :]) by
Th5,
XBOOLE_0: 3;
then
consider xy99,z99 be
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;
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;
end;
end;
theorem ::
ARYTM_0:24
[*x, y*]
in
REAL implies y
=
0
proof
assume
A1:
[*x, y*]
in
REAL ;
assume y
<>
0 ;
then
[*x, y*]
= ((
0 ,1)
--> (x,y)) by
Def5;
hence contradiction by
A1,
Th8;
end;
theorem ::
ARYTM_0:25
for x,y be
Element of
REAL holds (
opp (
+ (x,y)))
= (
+ ((
opp x),(
opp y)))
proof
reconsider o =
0 as
Element of
REAL by
Lm3;
let x,y be
Element of
REAL ;
(
+ ((
+ (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 thesis by
Def3;
end;