:: Introduction to Arithmetics
:: by Andrzej Trybulec
::
:: Received January 9, 2003
:: Copyright (c) 2003-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, ARYTM_2, TARSKI, NUMBERS, ZFMISC_1, SUBSET_1, ARYTM_1,
ARYTM_3, CARD_1, RELAT_1, FUNCOP_1, ORDINAL1, FUNCT_2, FUNCT_1, ARYTM_0,
XCMPLX_0;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2,
FUNCT_4, ORDINAL1, ARYTM_3, ARYTM_2, ARYTM_1, NUMBERS;
constructors FUNCT_4, ARYTM_1, NUMBERS, XTUPLE_0;
registrations XBOOLE_0, ORDINAL1, FUNCT_2, FUNCT_4, ARYTM_2, FUNCT_1, NUMBERS;
requirements BOOLE, SUBSET, NUMERALS;
equalities NUMBERS, TARSKI, ARYTM_3, ORDINAL1;
expansions TARSKI, ORDINAL1;
theorems XBOOLE_0, ARYTM_1, ZFMISC_1, TARSKI, ARYTM_2, XBOOLE_1, ORDINAL3,
ARYTM_3, FUNCT_2, FUNCT_4, FUNCT_1, ENUMSET1, NUMBERS, XTUPLE_0;
begin :: Arithmetics
Lm1: for x being 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 Th1:
REAL+ c= REAL
proof
REAL+ c= REAL+ \/ [:{{}},REAL+:] by XBOOLE_1:7;
hence thesis by ARYTM_2:3,ZFMISC_1:34;
end;
theorem Th2:
for x being 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 Th3:
for y being 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 Th4:
for x,y being 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 Th5:
REAL+ misses [:{{}},REAL+:]
proof
assume REAL+ meets [:{{}},REAL+:];
then consider x being object such that
A1: x in REAL+ and
A2: x in [:{{}},REAL+:] by XBOOLE_0:3;
consider x1,x2 being 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 :: Real numbers
registration let x,y be object;
cluster [x,y] -> non zero;
coherence;
end;
theorem Th6:
for x,y being 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 being 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 Th7:
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+;
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;
func +(x,y) -> Element of REAL means
:Def1:
ex x9,y9 being Element of REAL+
st x = x9 & y = y9 & it = x9 + y9 if x in REAL+ & y in REAL+, ex x9,y9 being
Element of REAL+ st x = x9 & y = [0,y9] & it = x9 - y9 if x in REAL+ & y in [:{
0},REAL+:], ex x9,y9 being Element of REAL+ st x = [0,x9] & y = y9 & it = y9 -
x9 if y in REAL+ & x in [:{0},REAL+:] otherwise ex x9,y9 being Element of REAL+
st x = [0,x9] & y = [0,y9] & it = [0,x9+y9];
existence
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 being 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 being 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 being 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 being 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 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;
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;
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;
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 being Element of REAL+ such that
A18: x = [0,x9] and
A19: y = [0,y9] & IT1 = [0,x9+y9];
given x99,y99 being 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;
func *(x,y) -> Element of REAL means
:Def2:
ex x9,y9 being Element of REAL+
st x = x9 & y = y9 & it = x9 *' y9 if x in REAL+ & y in REAL+, ex x9,y9 being
Element of REAL+ st x = x9 & y = [0,y9] & it = [0,x9 *' y9] if x in REAL+ & y
in [:{0},REAL+:] & x <> 0, ex x9,y9 being Element of REAL+ st x = [0,x9] & y =
y9 & it = [0,y9 *' x9] if y in REAL+ & x in [:{0},REAL+:] & y <> 0, ex x9,y9
being Element of REAL+ st x = [0,x9] & y = [0,y9] & it = y9 *' x9 if x in [:{0}
,REAL+:] & y in [:{0},REAL+:] otherwise it = 0;
existence
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 being 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 being 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 being 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 being 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 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;
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;
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;
hereby
assume that
x in [:{0},REAL+:] and
y in [:{0},REAL+:];
given x9,y9 being Element of REAL+ such that
A36: x = [0,x9] and
A37: y = [0,y9] & IT1 = y9 *' x9;
given x99,y99 being 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;
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 being 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 being 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 being 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 being 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 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 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 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 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 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 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 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 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 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 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 being 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 being Element of REAL+ st x = [0,x9] & z = [0,z9] & 0 = [0
,x9+z9] by A13,Def1;
hence thesis;
end;
end;
involutiveness;
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 being 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 being 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 being 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 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 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 being 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 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;
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 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 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 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 thesis by A72,A73,A75,Th3,Th7;
end;
suppose
x in REAL+ & y in [:{0},REAL+:];
then ex x9,y9 being 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 being 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 being 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 being 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 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;
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 :: from COMPLEX1
Lm4: for x,y,z being 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 Th8:
not (0,1)-->(a,b) in REAL
proof
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
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 being 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;
then 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,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,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 being set st {[0,x],[1,y]} in IR
proof
given x,y being set such that
A18: {[0,x],[1,y]} in IR;
consider A being Subset of RAT+ such that
A19: {[0,x],[1,y]} = A and
A20: 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 A18;
[0,x] in A & for r,s being Element of RAT+ st r in A & s <=' r holds
s in A by A19,A20,TARSKI:def 2;
then consider r1,r2,r3 being 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;
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 is Element of Funcs({0,1},REAL): r.1 = 0 };
then ex r being 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 is 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
for c being Element of COMPLEX ex r,s being 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 is Element of Funcs({0,1},REAL):
x.1 = 0} by 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,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 is 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
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 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 Th11:
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 being 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 being 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 Th12:
for x,o being Element of REAL st o = 0 holds *(x,o) = 0
proof
let x,o being 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 Th13:
for x,y,z being 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 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 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 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;
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;
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;
end;
suppose that
A22: x in RR and
A23: y in REAL+ & y <> 0 and
A24: z in REAL+ & z <> 0;
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;
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;
end;
suppose that
A35: x in RR and
A36: y in RR and
A37: z in REAL+ & z <> 0;
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;
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;
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 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;
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;
end;
suppose that
A62: x in REAL+ & x <> 0 and
A63: y in RR and
A64: z in RR;
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;
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;
end;
suppose that
A76: y in REAL+ & y <> 0 and
A77: x in RR and
A78: z in RR;
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;
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;
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;
end;
suppose that
A92: x in RR and
A93: y in RR and
A94: z in RR;
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 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 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 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 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 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 Th14:
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;
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 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 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 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;
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
per cases;
suppose
A20: z99 <=' y99;
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;
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 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;
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 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;
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
per cases;
suppose
A39: y99 <=' z99;
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;
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 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;
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 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;
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;
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 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;
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 being 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 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;
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 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;
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 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
per cases;
suppose
y <> 0;
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;
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
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 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 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 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;
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 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
per cases;
suppose
z <> 0;
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;
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
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 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 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 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;
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 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;
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;
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
for x,y being 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 Th16:
for x being 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 being 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 being Element of REAL+ st x = [0,x9] & x = [0,y9] & *(x,x) =
y9 *' x9 by Def2;
hence thesis;
end;
end;
theorem
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 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 XBOOLE_0:def 5;
per cases by A5,XBOOLE_0:def 3;
suppose
x in REAL+;
then ex x9,y9 being 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 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 thesis by XBOOLE_0:def 5;
end;
end;
theorem Th18:
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;
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 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 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 thesis by A3,A6,Th18;
end;
end;
theorem
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 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
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 Th23:
for x,y,z being 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 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 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 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
per cases;
suppose
A20: z9 <=' y9;
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 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 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;
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 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
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 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 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 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;
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;
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 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;
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 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;
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;
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 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;
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
per cases;
suppose
A76: y99 <=' x99;
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;
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 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;
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 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
per cases;
suppose
A101: x9 <=' y9;
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;
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 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;
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 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
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 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 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 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;
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;
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 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;
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;
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 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;
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 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;
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 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;
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
per cases;
suppose
A175: y99 <=' z99;
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;
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 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;
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 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;
then not(+(z,y) in REAL+ & 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;
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 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;
then not(+(x,y) in REAL+ & 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;
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
[*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
for x,y being 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;