:: Complex Numbers - Basic Definitions
:: by Library Committee
::
:: Received March 7, 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 CARD_1, FUNCOP_1, ORDINAL1, NUMBERS, SUBSET_1, FUNCT_2, FUNCT_1,
XBOOLE_0, ARYTM_0, ARYTM_3, RELAT_1, ARYTM_2, ZFMISC_1, ARYTM_1, TARSKI,
XCMPLX_0, FUNCT_7;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, RELAT_1, RELSET_1, FUNCT_1,
FUNCT_2, FUNCT_4, ORDINAL1, ARYTM_2, ARYTM_1, NUMBERS, ARYTM_0;
constructors FUNCT_4, ARYTM_1, ARYTM_0, FUNCOP_1, RELSET_1, NUMBERS;
registrations FUNCT_1, FUNCT_2, NUMBERS, XBOOLE_0, FUNCT_4, ORDINAL1, ARYTM_0,
SUBSET_1;
requirements BOOLE, SUBSET, NUMERALS;
definitions ORDINAL1;
equalities ORDINAL1;
expansions ORDINAL1;
theorems ARYTM_0, XBOOLE_0, FUNCT_4, FUNCT_2, ZFMISC_1, ARYTM_2, TARSKI,
ARYTM_1, XBOOLE_1, NUMBERS, XTUPLE_0, RELSET_1, SUBSET_1;
begin
definition
func <i> -> Number equals
(0,1) --> (0,1);
coherence;
let c be Number;
attr c is complex means
:Def2:
c in COMPLEX;
end;
0 in NAT;
then 0 in REAL by NUMBERS:19;
then
Lm1: In(0,REAL) = 0 by SUBSET_1:def 8;
1 in NAT;
then
Lm2: 1 in REAL by NUMBERS:19;
registration
cluster <i> -> complex;
coherence
proof
set X = { x where x is Element of Funcs({0,1},REAL): x.1 = 0};
A1: now
assume <i> in X;
then ex x being Element of Funcs({0,1},REAL) st <i> = x & x.1 = 0;
hence contradiction by FUNCT_4:63;
end;
A2: {In(0,REAL),1} c= REAL by ZFMISC_1:32,Lm2;
rng (0,1) --> (0,1) c= {In(0,REAL),1} by FUNCT_4:62,Lm1;
then rng (0,1) --> (0,1) c= REAL by A2,XBOOLE_1:1;
then <i> is Relation of {0,1}, REAL by RELSET_1:6;
then <i> in Funcs({0,1},REAL) by FUNCT_2:8;
then <i> in Funcs({0,1},REAL) \ X by A1,XBOOLE_0:def 5;
hence <i> in COMPLEX by NUMBERS:def 2,XBOOLE_0:def 3;
end;
end;
registration
cluster complex for Number;
existence
proof
take <i>;
thus thesis;
end;
cluster complex for number;
existence
proof
take <i>;
thus thesis;
end;
end;
definition
mode Complex is complex Number;
end;
registration
sethood of Complex
proof
take COMPLEX;
thus thesis by Def2;
end;
end;
registration
let c be Complex;
reduce In(c,COMPLEX) to c;
reducibility by Def2,SUBSET_1:def 8;
end;
registration
let c,d be Complex;
reduce In([c,d],[:COMPLEX,COMPLEX:]) to [c,d];
reducibility
proof
[In(c,COMPLEX),In(d,COMPLEX)] in [:COMPLEX,COMPLEX:] by ZFMISC_1:87;
hence thesis;
end;
end;
::$CD
definition
let x,y be Complex;
x in COMPLEX by Def2;
then consider x1,x2 being Element of REAL such that
A1: x = [*x1,x2*] by ARYTM_0:9;
y in COMPLEX by Def2;
then consider y1,y2 being Element of REAL such that
A2: y = [*y1,y2*] by ARYTM_0:9;
func x+y -> number means
:Def3:
ex x1,x2,y1,y2 being Element of REAL st
x = [*x1,x2*] & y = [*y1,y2*] & it = [*+(x1,y1),+(x2,y2)*];
existence
proof
take IT=[*+(x1,y1),+(x2,y2)*];
thus thesis by A1,A2;
end;
uniqueness
proof
let c1,c2 be number;
given x1,x2,y1,y2 being Element of REAL such that
A3: x = [*x1,x2*] and
A4: y = [*y1,y2*] and
A5: c1 = [*+(x1,y1),+(x2,y2)*];
given x19,x29,y19,y29 being Element of REAL such that
A6: x = [*x19,x29*] and
A7: y = [*y19,y29*] and
A8: c2 = [*+(x19,y19),+(x29,y29)*];
A9: x1 = x19 & x2 = x29 by A3,A6,ARYTM_0:10;
y1 = y19 by A4,A7,ARYTM_0:10;
hence thesis by A4,A5,A7,A8,A9,ARYTM_0:10;
end;
commutativity;
func x*y -> number means
:Def4:
ex x1,x2,y1,y2 being Element of REAL st x = [*x1,x2*] & y = [*y1,y2*] &
it = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *];
existence
proof
take IT=[* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *];
thus thesis by A1,A2;
end;
uniqueness
proof
let c1,c2 be number;
given x1,x2,y1,y2 being Element of REAL such that
A10: x = [*x1,x2*] and
A11: y = [*y1,y2*] and
A12: c1 = [*+(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1))*];
given x19,x29,y19,y29 being Element of REAL such that
A13: x = [*x19,x29*] and
A14: y = [*y19,y29*] and
A15: c2 = [*+(*(x19,y19),opp*(x29,y29)), +(*(x19,y29),*(x29,y19))*];
A16: x1 = x19 & x2 = x29 by A10,A13,ARYTM_0:10;
y1 = y19 & y2 = y29 by A11,A14,ARYTM_0:10;
hence thesis by A12,A15,A16;
end;
commutativity;
end;
Lm4: for x,y,z being Element of REAL st +(x,y) = 0 & +(x,z) = 0 holds y = z
proof
let x,y,z be Element of REAL such that
A1: +(x,y) = 0 and
A2: +(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 A1,A2,
ARYTM_0:def 1;
hence thesis by ARYTM_2:11;
end;
suppose that
A3: x in REAL+ and
A4: y in REAL+ and
A5: z in [:{0},REAL+:];
A6: ex x9,y9 being Element of REAL+ st x = x9 & y = y9 & 0 =
x9 + y9 by A1,A3,A4,ARYTM_0:def 1;
consider x99,y99 being Element of REAL+ such that
A7: x = x99 and
A8: z = [0,y99] & 0 = x99 - y99 by A2,A3,A5,ARYTM_0:def 1;
A9: x99 = 0 by A6,A7,ARYTM_2:5;
[{},{}] in {[{},{}]} by TARSKI:def 1;
then A10: not [{},{}] in REAL by NUMBERS:def 1,XBOOLE_0:def 5;
z in REAL;
hence thesis by A8,A9,A10,ARYTM_1:19;
end;
suppose that
A11: x in REAL+ and
A12: z in REAL+ and
A13: y in [:{0},REAL+:];
A14: ex x9,z9 being Element of REAL+ st x = x9 & z = z9 & 0 =
x9 + z9 by A2,A11,A12,ARYTM_0:def 1;
consider x99,y9 being Element of REAL+ such that
A15: x = x99 and
A16: y = [0,y9] & 0 = x99 - y9 by A1,A11,A13,ARYTM_0:def 1;
A17: x99 = 0 by A14,A15,ARYTM_2:5;
[0,0] in {[0,0]} by TARSKI:def 1;
then A18: not [0,0] in REAL by NUMBERS:def 1,XBOOLE_0:def 5;
y in REAL;
hence thesis by A16,A17,A18,ARYTM_1:19;
end;
suppose that
A19: x in REAL+ and
A20: y in [:{0},REAL+:] and
A21: z in [:{0},REAL+:];
consider x9,y9 being Element of REAL+ such that
A22: x = x9 and
A23: y = [0,y9] and
A24: 0 = x9 - y9 by A1,A19,A20,ARYTM_0:def 1;
consider x99,z9 being Element of REAL+ such that
A25: x = x99 and
A26: z = [0,z9] and
A27: 0 = x99 - z9 by A2,A19,A21,ARYTM_0:def 1;
y9 = x9 by A24,ARYTM_0:6
.= z9 by A22,A25,A27,ARYTM_0:6;
hence thesis by A23,A26;
end;
suppose that
A28: z in REAL+ and
A29: y in REAL+ and
A30: x in [:{0},REAL+:];
consider x9,y9 being Element of REAL+ such that
A31: x = [0,x9] and
A32: y = y9 and
A33: 0 = y9 - x9 by A1,A29,A30,ARYTM_0:def 1;
consider x99,z9 being Element of REAL+ such that
A34: x = [0,x99] and
A35: z = z9 and
A36: 0 = z9 - x99 by A2,A28,A30,ARYTM_0:def 1;
x9 = x99 by A31,A34,XTUPLE_0:1;
then z9 = x9 by A36,ARYTM_0:6
.= y9 by A33,ARYTM_0:6;
hence thesis by A32,A35;
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 A1,ARYTM_0:def 1;
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 A2,ARYTM_0:def 1;
hence thesis;
end;
end;
registration
let z,z9 be Complex;
cluster z+z9 -> complex;
coherence
proof
ex x1,x2,y1,y2 being Element of REAL st
z = [*x1,x2*] & z9 = [*y1,y2*] & z+z9 = [*+(x1,y1),+(x2,y2)*] by Def3;
hence z+z9 in COMPLEX;
end;
cluster z*z9 -> complex;
coherence
proof
ex
x1,x2,y1,y2 being Element of REAL st z = [*x1,x2*] & z9 = [*y1,y2*] &
z*z9 = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by Def4;
hence z*z9 in COMPLEX;
end;
end;
definition
let z be Complex;
z in COMPLEX by Def2;
then consider x,y being Element of REAL such that
A1: z = [*x,y*] by ARYTM_0:9;
func -z -> Complex means
:Def5:
z + it = 0;
existence
proof
reconsider z9 = [*opp x, opp y*] as Complex by Def2;
take z9;
A2: 0 = +(x,opp x) & 0 = +(y,opp y) by ARYTM_0:def 3;
0 in NAT;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
0 = [*zz,zz*] by ARYTM_0:def 5;
hence thesis by A1,Def3,A2;
end;
uniqueness
proof
let c1,c2 be Complex such that
A2: z+c1 = 0 and
A3: z+c2 = 0;
consider x1,x2,y1,y2 being Element of REAL such that
A4: z = [*x1,x2*] and
A5: c1 = [*y1,y2*] and
A6: 0 = [*+(x1,y1),+(x2,y2)*] by A2,Def3;
consider x19,x29,y19,y29 being Element of REAL such that
A7: z = [*x19,x29*] and
A8: c2 = [*y19,y29*] and
A9: 0 = [*+(x19,y19),+(x29,y29)*] by A3,Def3;
A10: x1 = x19 by A4,A7,ARYTM_0:10;
A11: x2 = x29 by A4,A7,ARYTM_0:10;
0 in NAT;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
Lm3: 0 = [*zz,zz*] by ARYTM_0:def 5;
A12: +(x1,y1) = 0 by A6,Lm3,ARYTM_0:10;
+(x1,y19) = 0 by A9,A10,Lm3,ARYTM_0:10;
then A13: y1 = y19 by A12,Lm4;
A14: +(x2,y2) = 0 by A6,Lm3,ARYTM_0:10;
+(x2,y29) = 0 by A9,A11,Lm3,ARYTM_0:10;
hence thesis by A5,A8,A13,A14,Lm4;
end;
involutiveness;
func z" -> Complex means
:Def6:
z*it = 1 if z <> 0 otherwise it = 0;
existence
proof
thus z <> 0 implies ex z9 being Complex st z*z9 = 1
proof
set y1 = *(x,inv +(*(x,x),*(y,y))), y2 = *(opp y,inv +(*(x,x),*(y,y)));
set z9 = [* y1, y2 *];
reconsider z9 as Complex by Def2;
assume
A15: z <> 0;
take z9;
A16: opp *(y,y2) = opp *(y,opp *(y,inv +(*(x,x),*(y,y)))) by ARYTM_0:15
.= opp opp *(y,*(y,inv +(*(x,x),*(y,y)))) by ARYTM_0:15
.= *(*(y,y),inv +(*(x,x),*(y,y))) by ARYTM_0:13;
A17: *(x,y1) = *(*(x,x),inv +(*(x,x),*(y,y))) by ARYTM_0:13;
A18: now
assume +(*(x,x),*(y,y)) = 0;
then x = 0 & y = 0 by ARYTM_0:17;
hence contradiction by A1,A15,ARYTM_0:def 5;
end;
*(x,y2) = *(opp y,y1) by ARYTM_0:13
.= opp *(y,y1) by ARYTM_0:15;
then +(*(x,y2),*(y,y1)) = 0 by ARYTM_0:def 3;
then [* +(*(x,y1),opp*(y,y2)), +(*(x,y2),*(y,y1)) *]
= +(*(x,y1),opp*(y,y2)) by ARYTM_0:def 5
.=*(+(*(x,x),*(y,y)),inv +(*(x,x),*(y,y))) by A16,A17,ARYTM_0:14
.= 1 by A18,ARYTM_0:def 4;
hence thesis by A1,Def4;
end;
assume z = 0;
hence thesis;
end;
uniqueness
proof
let c1,c2 be Complex;
0 in NAT;
then reconsider zz = 0,j=1 as Element of REAL by Lm2,NUMBERS:19;
thus z <> 0 & z*c1 = 1 & z*c2 = 1 implies c1 = c2
proof
assume that
A19: z <> 0 and
A20: z*c1 = 1 and
A21: z*c2 = 1;
A22: for z9 being Complex st z*z9 = 1
holds z9 = [* *(x,inv +(*(x,x),*(y,y))) , *(opp y,inv +(*(x,x),*(y,y))) *]
proof
let z9 being Complex such that
A23: z*z9 = 1;
consider x1,x2,x9,y9 being Element of REAL such that
A24: z = [*x1,x2*] and
A25: z9 = [*x9,y9*] and
A26: 1 = [* +(*(x1,x9),opp*(x2,y9)), +(*(x1,y9),*(x2,x9)) *] by A23,Def4;
A27: x = x1 & y = x2 by A1,A24,ARYTM_0:10;
per cases by A1,A19,ARYTM_0:def 5;
suppose that
A28: x = 0 and
A29: y <> 0;
+(y, opp y) = 0 by ARYTM_0:def 3;
then A30: opp y <> 0 by A29,ARYTM_0:11;
*(x,y9) = 0 & *(x,x9) = 0 by A28,ARYTM_0:12;
then A31: 1 = [* opp*(y,y9), +(zz,*(y,x9)) *] by A26,A27,ARYTM_0:11
.= [* opp*(y,y9), *(y,x9) *] by ARYTM_0:11;
A32: 1 = [*j,zz*] by ARYTM_0:def 5;
*(opp y,y9) = opp*(y,y9) by ARYTM_0:15
.= 1 by A31,A32,ARYTM_0:10;
then A33: y9 = inv opp y by A30,ARYTM_0:def 4;
A34: *(x,x) = 0 by A28,ARYTM_0:12;
*(opp y,opp inv y) = opp *(y,opp inv y) by ARYTM_0:15
.= opp opp *(y,inv y) by ARYTM_0:15
.= 1 by A29,ARYTM_0:def 4;
then A35: inv opp y = opp inv y by A30,ARYTM_0:def 4;
*(y,x9) = 0 by A31,A32,ARYTM_0:10;
hence z9 = [*zz,inv opp y*] by A25,A29,A33,ARYTM_0:21
.= [* zz , opp *(j,inv y) *] by A35,ARYTM_0:19
.= [* zz , opp *(*(y,inv y),inv y) *] by A29,ARYTM_0:def 4
.= [* zz , opp *(y,*(inv y,inv y)) *] by ARYTM_0:13
.= [* zz , *(opp y,*(inv y,inv y)) *] by ARYTM_0:15
.= [* zz , *(opp y,inv *(y,y)) *] by ARYTM_0:22
.= [* zz , *(opp y,inv +(zz,*(y,y))) *] by ARYTM_0:11
.= [* *(x,inv +(*(x,x),*(y,y))) , *(opp y,inv +(*(x,x),*(y,y))) *]
by A28,A34,ARYTM_0:12;
end;
suppose that
A36: opp y = 0 and
A37: x <> 0;
+(y,opp y) = 0 by ARYTM_0:def 3;
then A38: y = 0 by A36,ARYTM_0:11;
then A39: *(y,x9) = 0 by ARYTM_0:12;
opp*(y,y9) = *(opp y,y9) by ARYTM_0:15
.= 0 by A36,ARYTM_0:12;
then A40: 1 = [* *(x,x9), +(*(x,y9),zz) *] by A26,A27,A39,ARYTM_0:11
.= [* *(x,x9), *(x,y9) *] by ARYTM_0:11;
A41: 1 = [*j,zz*] by ARYTM_0:def 5;
then *(x,x9) = 1 by A40,ARYTM_0:10;
then A42: x9 = inv x by A37,ARYTM_0:def 4;
*(x,y9) = 0 by A40,A41,ARYTM_0:10;
then A43: y9 = 0 by A37,ARYTM_0:21;
A44: *(y,y) = 0 by A38,ARYTM_0:12;
x9 = *(j,inv x) by A42,ARYTM_0:19
.= *(*(x,inv x),inv x) by A37,ARYTM_0:def 4
.= *(x,*(inv x,inv x)) by ARYTM_0:13
.= *(x,inv *(x,x)) by ARYTM_0:22
.= *(x,inv +(*(x,x),zz)) by ARYTM_0:11;
hence thesis by A25,A36,A43,A44,ARYTM_0:12;
end;
suppose that
A45: opp y <> 0 and
A46: x <> 0;
A47: now
assume +(*(*(x,x), inv opp y),opp y) = 0;
then +(*(*(x,x), inv opp y),*(opp y,j)) = 0 by ARYTM_0:19;
then +(*(*(x,x), inv opp y),*(opp y,*(opp y, inv opp y))) = 0
by A45,ARYTM_0:def 4;
then +(*(*(x,x), inv opp y),*(*(opp y,opp y), inv opp y)) = 0
by ARYTM_0:13;
then A48: *(inv opp y, +(*(x,x),*(opp y,opp y))) = 0 by ARYTM_0:14;
+(*(x,x),*(opp y,opp y)) <> 0 by A46,ARYTM_0:17;
then A49: inv opp y = 0 by A48,ARYTM_0:21;
*(opp y,inv opp y) = 1 by A45,ARYTM_0:def 4;
hence contradiction by A49,ARYTM_0:12;
end;
A50: 1 = [*j,zz*] by ARYTM_0:def 5;
then +(*(x1,y9),*(x2,x9)) = 0 by A26,ARYTM_0:10;
then *(x,y9) = opp*(y,x9) by A27,ARYTM_0:def 3;
then *(x,y9) = *(opp y,x9) by ARYTM_0:15;
then A51: x9 = *(*(x,y9), inv opp y) by A45,ARYTM_0:20
.= *(x,*(y9, inv opp y)) by ARYTM_0:13;
then +
(*(x,*(x,*(y9, inv opp y))),opp*(y,y9)) = 1 by A26,A27,A50,ARYTM_0:10;
then +(*(*(x,x),*(y9, inv opp y)),opp*(y,y9)) = 1 by ARYTM_0:13;
then +(*(*(x,x),*(y9, inv opp y)),*(opp y,y9)) = 1 by ARYTM_0:15;
then +(*(y9,*(*(x,x), inv opp y)),*(opp y,y9)) = 1 by ARYTM_0:13;
then *(y9,+(*(*(x,x), inv opp y),opp y)) = 1 by ARYTM_0:14;
then A52: y9 = inv +(*(*(x,x), inv opp y),opp y) by A47,ARYTM_0:def 4;
then A53: x9 = *(x,inv *(+(*(*(x,x), inv opp y),opp y), opp y)) by A51,
ARYTM_0:22
.= *(x,inv +(*(*(*(x,x), inv opp y),opp y),*(opp y, opp y))) by ARYTM_0:14
.= *(x,inv +(*(*(*(x,x), inv opp y),opp y),opp*(y, opp y))) by ARYTM_0:15
.= *(x,inv +(*(*(*(x,x), inv opp y),opp y),opp opp*(y,y))) by ARYTM_0:15
.= *(x,inv +(*(*(x,x), *(inv opp y,opp y)),*(y,y))) by ARYTM_0:13
.= *(x,inv +(*(*(x,x), j),*(y,y))) by A45,ARYTM_0:def 4
.= *(x,inv +(*(x,x),*(y,y))) by ARYTM_0:19;
y9 = *(j,inv +(*(*(x,x), inv opp y),opp y)) by A52,ARYTM_0:19
.= *(*(opp y, inv opp y),inv +(*(*(x,x), inv opp y),opp y))
by A45,ARYTM_0:def 4
.= *(opp y, *(inv opp y,inv +(*(*(x,x), inv opp y),opp y))) by ARYTM_0:13
.= *(opp y, inv *(opp y,+(*(*(x,x), inv opp y),opp y))) by ARYTM_0:22
.= *(opp y, inv +(*(opp y,*(*(x,x), inv opp y)),*(opp y,opp y)))
by ARYTM_0:14
.= *(opp y, inv +(*(*(x,x),*(opp y, inv opp y)),*(opp y,opp y)))
by ARYTM_0:13
.= *(opp y, inv +(*(*(x,x),j),*(opp y,opp y))) by A45,ARYTM_0:def 4
.= *(opp y, inv +(*(x,x),*(opp y,opp y))) by ARYTM_0:19
.= *(opp y, inv +(*(x,x),opp *(y,opp y))) by ARYTM_0:15
.= *(opp y, inv +(*(x,x),opp opp *(y,y))) by ARYTM_0:15
.= *(opp y, inv +(*(x,x),*(y,y)));
hence thesis by A25,A53;
end;
end;
thus
then c1 = [* *(x,inv +(*(x,x),*(y,y))) , *(opp y,inv +(*(x,x),*(y,y)))
*] by A20
.= c2 by A21,A22;
end;
thus thesis;
end;
consistency;
involutiveness
proof
let z,z9 be Complex;
0 in NAT;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
assume that
A54: z9 <> 0 implies z9*z = 1 and
A55: z9 = 0 implies z = 0;
thus z <> 0 implies z*z9 = 1 by A54,A55;
assume
A56: z = 0;
assume z9 <> 0;
then consider x1,x2,y1,y2 being Element of REAL such that
A57: z = [*x1,x2*] and z9 = [*y1,y2*] and
A58: 1 = [*+(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1))*] by A54,Def4;
A59: z = [*zz,zz*] by A56,ARYTM_0:def 5;
then A60: x1 = 0 by A57,ARYTM_0:10;
A61: x2 = 0 by A57,A59,ARYTM_0:10;
A62: *(x1,y1) = 0 by A60,ARYTM_0:12;
*(x2,y2) = 0 by A61,ARYTM_0:12;
then A63: +(*(x1,y1),opp*(x2,y2)) = 0 by A62,ARYTM_0:def 3;
A64: *(x1,y2) = 0 by A60,ARYTM_0:12;
*(x2,y1) = 0 by A61,ARYTM_0:12;
then +(*(x1,y2),*(x2,y1)) = 0 by A64,ARYTM_0:11;
hence contradiction by A58,A63,ARYTM_0:def 5;
end;
end;
definition
let x,y be Complex;
func x-y -> number equals
x+(-y);
coherence;
func x/y -> number equals
x * y";
coherence;
end;
registration
let x,y be Complex;
cluster x-y -> complex;
coherence;
cluster x/y -> complex;
coherence;
end;
Lm5: for x, y, z being Complex holds x * (y * z) = (x * y) * z
proof
let x, y, z be Complex;
consider x1,x2,y1,y2 being Element of REAL such that
A1: x = [*x1,x2*] and
A2: y = [*y1,y2*] and
A3: x*y = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by Def4;
consider y3,y4,z1,z2 being Element of REAL such that
A4: y = [*y3,y4*] and
A5: z = [*z1,z2*] and
A6: y*z = [* +(*(y3,z1),opp*(y4,z2)), +(*(y3,z2),*(y4,z1)) *] by Def4;
A7: y1 = y3 by A2,A4,ARYTM_0:10;
A8: y2 = y4 by A2,A4,ARYTM_0:10;
consider x3,x4,yz1,yz2 being Element of REAL such that
A9: x = [*x3,x4*] and
A10: y*z = [*yz1,yz2*] and
A11: x*(y*z) = [* +(*(x3,yz1),opp*(x4,yz2)), +(*(x3,yz2),*(x4,yz1)) *] by Def4;
A12: x1 = x3 by A1,A9,ARYTM_0:10;
A13: x2 = x4 by A1,A9,ARYTM_0:10;
consider xy1,xy2,z3,z4 being Element of REAL such that
A14: x*y = [*xy1,xy2*] and
A15: z = [*z3,z4*] and
A16: (x*y)*z = [* +(*(xy1,z3),opp*(xy2,z4)), +(*(xy1,z4),*(xy2,z3)) *] by Def4;
A17: z1 = z3 by A5,A15,ARYTM_0:10;
A18: z2 = z4 by A5,A15,ARYTM_0:10;
A19: xy1 = +(*(x1,y1),opp*(x2,y2)) by A3,A14,ARYTM_0:10;
A20: xy2 = +(*(x1,y2),*(x2,y1)) by A3,A14,ARYTM_0:10;
A21: yz1 = +(*(y3,z1),opp*(y4,z2)) by A6,A10,ARYTM_0:10;
A22: yz2 = +(*(y3,z2),*(y4,z1)) by A6,A10,ARYTM_0:10;
+(*(opp x4,*(y3,z2)),*(opp x4,*(y4,z1)))
= +(*(opp x4,*(y4,z1)),*(*(opp x2,y1),z4)) by A7,A13,A18,ARYTM_0:13
.= +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4)) by A8,A13,A17,ARYTM_0:13;
then A23: +(*(x3,*(opp y4,z2)),+(*(opp x4,*(y3,z2)),*(opp x4,*(y4,z1)) ))
= +(*(*(x1,opp y2),z4), +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4)))
by A8,A12,A18,ARYTM_0:13
.= +(*(opp *(x1,y2),z4), +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4)))
by ARYTM_0:15
.= +(*(*(opp x1,y2),z4), +(*(*(opp x2,y2),z3),*(*(opp x2,y1),z4)))
by ARYTM_0:15
.= +(*(*(opp x2,y2),z3), +(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4)))
by ARYTM_0:23;
A24: +(*(x3,yz1),opp*(x4,yz2)) = +(*(x3,yz1),*(opp x4,yz2)) by ARYTM_0:15
.= +(*(x3,+(*(y3,z1),*(opp y4,z2))),*(opp x4,yz2)) by A21,ARYTM_0:15
.= +(+(*(x3,*(y3,z1)),*(x3,*(opp y4,z2))),
*(opp x4,+(*(y3,z2),*(y4,z1)))) by A22,ARYTM_0:14
.= +(+(*(x3,*(y3,z1)),*(x3,*(opp y4,z2))),
+(*(opp x4,*(y3,z2)),*(opp x4,*(y4,z1)))) by ARYTM_0:14
.= +(*(x3,*(y3,z1)),+(*(*(opp x2,y2),z3),
+(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4)))) by A23,ARYTM_0:23
.= +(+(*(x3,*(y3,z1)),*(*(opp x2,y2),z3)),
+(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by ARYTM_0:23
.= +(+(*(*(x1,y1),z3),*(*(opp x2,y2),z3)),
+(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by A7,A12,A17,ARYTM_0:13
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
+(*(*(opp x1,y2),z4),*(*(opp x2,y1),z4))) by ARYTM_0:14
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
+(*(*(opp x1,y2),z4),*(opp *(x2,y1),z4))) by ARYTM_0:15
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
+(*(*(opp x1,y2),z4),opp *(*(x2,y1),z4))) by ARYTM_0:15
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
+(*(opp *(x1,y2),z4),opp *(*(x2,y1),z4))) by ARYTM_0:15
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
+(opp *(*(x1,y2),z4),opp *(*(x2,y1),z4))) by ARYTM_0:15
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
opp +(*(*(x1,y2),z4),*(*(x2,y1),z4))) by ARYTM_0:25
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),
opp*( +(*(x1,y2),*(x2,y1)),z4)) by ARYTM_0:14
.= +(*(+(*(x1,y1),*(opp x2,y2)),z3),*(opp xy2,z4)) by A20,ARYTM_0:15
.= +(*(xy1,z3),*(opp xy2,z4)) by A19,ARYTM_0:15
.= +(*(xy1,z3),opp*(xy2,z4)) by ARYTM_0:15;
A25: +(*(opp*(x2,y2),z4),*(*(x2,y1),z3))
= +(opp*(*(x2,y2),z4),*(*(x2,y1),z3)) by ARYTM_0:15
.= +(*(x4,*(y3,z1)),opp*(*(x2,y2),z4)) by A7,A13,A17,ARYTM_0:13
.= +(*(x4,*(y3,z1)),opp*(x4,*(y4,z2))) by A8,A13,A18,ARYTM_0:13
.= +(*(x4,*(y3,z1)),*(x4,opp*(y4,z2))) by ARYTM_0:15;
A26: +(*(opp*(x2,y2),z4),*(xy2,z3))
= +(*(opp*(x2,y2),z4),+(*(*(x1,y2),z3),*(*(x2,y1),z3))) by A20,ARYTM_0:14
.= +(*(*(x1,y2),z3),+(*(opp*(x2,y2),z4),*(*(x2,y1),z3))) by ARYTM_0:23
.= +(*(x3,*(y4,z1)),+(*(x4,*(y3,z1)),*(x4,opp*(y4,z2))))
by A8,A12,A17,A25,ARYTM_0:13
.= +(*(x3,*(y4,z1)),*(x4,yz1)) by A21,ARYTM_0:14;
+(*(xy1,z4),*(xy2,z3))
= +(+(*(*(x1,y1),z4),*(opp*(x2,y2),z4)),*(xy2,z3)) by A19,ARYTM_0:14
.= +(*(*(x1,y1),z4),+(*(opp*(x2,y2),z4),*(xy2,z3))) by ARYTM_0:23
.= +(*(x3,*(y3,z2)),+(*(x3,*(y4,z1)),*(x4,yz1)))
by A7,A12,A18,A26,ARYTM_0:13
.= +(+(*(x3,*(y3,z2)),*(x3,*(y4,z1))),*(x4,yz1)) by ARYTM_0:23
.= +(*(x3,yz2),*(x4,yz1)) by A22,ARYTM_0:14;
hence thesis by A11,A16,A24;
end;
registration
cluster natural -> complex for object;
coherence by NUMBERS:20;
end;
Lm: 1 is Complex;
registration
cluster zero for Complex;
existence
proof
take 0;
thus thesis;
end;
cluster non zero for Complex;
existence by Lm;
cluster non zero for Complex;
existence by Lm;
end;
Lm6: REAL c= COMPLEX by NUMBERS:def 2,XBOOLE_1:7;
registration
let x be non zero Complex;
cluster -x -> non zero;
coherence
proof
assume
A1: -x = 0;
x + -x = 0 by Def5;
then consider x1,x2,y1,y2 being Element of REAL such that
A2: x = [*x1,x2*] and
A3: -x = [*y1,y2*] and
A4: In(0,REAL) = [*+(x1,y1),+(x2,y2)*] by Def3,Lm1;
A5: +(x2,y2) = 0 by A4,ARYTM_0:24;
then A6: +(x1,y1) = 0 by A4,ARYTM_0:def 5;
y2 = In(0,REAL) by A1,A3,ARYTM_0:24,Lm1;
then A7: y1 = 0 by A1,A3,ARYTM_0:def 5,Lm1;
x2 = 0 by A1,A3,A5,ARYTM_0:11,24;
then x = x1 by A2,ARYTM_0:def 5
.= 0 by A6,A7,ARYTM_0:11;
hence contradiction;
end;
cluster x" -> non zero;
coherence
proof
assume
A8: x" = 0;
then
A9: x" = In(0,REAL) by Lm1;
x*x" = 1 by Def6;
then consider x1,x2,y1,y2 being Element of REAL such that
x = [*x1,x2*] and
A10: x" = [*y1,y2*] and
A11: 1 = [* +(*(x1,y1),opp*(x2,y2)), +(*(x1,y2),*(x2,y1)) *] by Def4;
y2 = In(0,REAL) by A8,A10,ARYTM_0:24,Lm1;
then A12: y1 = 0 by A8,A10,ARYTM_0:def 5,Lm1;
+(*(x1,y2),*(x2,y1)) = 0 by A11,ARYTM_0:24,Lm2;
then 1 = +(*(x1,y1),opp*(x2,y2)) by A11,ARYTM_0:def 5
.= +(*(x1,y1),*(opp x2,y2)) by ARYTM_0:15
.= *(opp x2,y2) by A12,ARYTM_0:11,12;
hence contradiction by A10,ARYTM_0:12,24,A9;
end;
let y be non zero Complex;
cluster x*y -> non zero;
coherence
proof
set j = 1;
0 in NAT;
then reconsider zz = 0 as Element of REAL by NUMBERS:19;
consider u1,u2,v1,v2 being Element of REAL such that
A13: j = [*u1,u2*] and
A14: y
= [*v1,v2*] & j*y = [* +(*(u1,v1),opp*(u2,v2)), +(*(u1,v2),*(u2,v1)) *]
by Def4;
A15: u2 = 0 by A13,ARYTM_0:24,Lm2;
then A16: +(*(u1,v2),*(u2,v1)) = *(u1,v2) by ARYTM_0:11,12;
A17: u1 = 1 by A13,A15,ARYTM_0:def 5;
+(zz,opp zz) = 0 by ARYTM_0:def 3;
then A18: opp zz = 0 by ARYTM_0:11;
A19: +(*(u1,v1),opp*(u2,v2)) = +(v1,opp*(u2,v2)) by A17,ARYTM_0:19
.= +(v1,*(opp u2,v2)) by ARYTM_0:15
.= +(v1,*(zz,v2)) by A13,A18,ARYTM_0:24,Lm2
.= v1 by ARYTM_0:11,12;
set z = 0;
consider u1,u2,v1,v2 being Element of REAL such that
x" = [*u1,u2*] and
A20: z = [*v1,v2*] and
A21: x"*z = [* +(*(u1,v1),opp*(u2,v2)), +(*(u1,v2),*(u2,v1)) *] by Def4;
v2 = zz by A20,ARYTM_0:24;
then A22: v1 = 0 by A20,ARYTM_0:def 5;
then A23: +(*(u1,v1),opp*(u2,v2)) = opp*(u2,v2) by ARYTM_0:11,12
.= 0 by A18,A20,ARYTM_0:12,24;
A24: +(*(u1,v2),*(u2,v1)) = +(zz,*(u2,v1)) by A20,ARYTM_0:12,24
.= *(u2,v1) by ARYTM_0:11
.= 0 by A22,ARYTM_0:12;
assume
A25: x*y = 0;
A26: x"*x*y = x"*(x*y) by Lm5
.= 0 by A21,A23,A24,A25,ARYTM_0:def 5;
x"*x*y = j * y by Def6
.= y by A14,A16,A17,A19,ARYTM_0:19;
hence contradiction by A26;
end;
end;
registration
let x,y be non zero Complex;
cluster x/y -> non zero;
coherence;
end;
registration
cluster -> complex for Element of REAL;
coherence
proof
let n be Element of REAL;
n in REAL;
hence thesis by Lm6;
end;
end;
registration
cluster -> complex for Element of COMPLEX;
coherence;
end;