Copyright (c) 1990 Association of Mizar Users
environ
vocabulary COMPLEX1, FUNCT_1, BINOP_1, SETWISEO, ARYTM_1, FINSEQOP, FUNCOP_1,
FINSEQ_1, RELAT_1, ABSVALUE, FINSEQ_2, SQUARE_1, RLVECT_1, RVSUM_1,
PRE_TOPC, BOOLE, SETFAM_1, TARSKI, METRIC_1, SEQ_4, ARYTM, SEQ_2,
ARYTM_3, SUBSET_1, COMPTS_1, COMPLSP1;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
XREAL_0, NAT_1, SETFAM_1, REAL_1, SQUARE_1, COMPLEX1, FUNCT_1, PARTFUN1,
FUNCT_2, BINOP_1, STRUCT_0, PRE_TOPC, COMPTS_1, FINSEQ_1, FUNCOP_1,
SETWISEO, FINSEQ_2, FINSEQOP, RVSUM_1, SEQ_4;
constructors REAL_1, SQUARE_1, COMPLEX1, BINOP_1, COMPTS_1, SETWISEO,
FINSEQOP, RVSUM_1, SEQ_4, SEQ_1, MEMBERED, PARTFUN1, XBOOLE_0;
clusters SUBSET_1, PRE_TOPC, RELSET_1, FINSEQ_2, XREAL_0, COMPLEX1, ARYTM_3,
SEQ_1, MEMBERED, ZFMISC_1, PARTFUN1, FUNCT_1, FUNCT_2, XBOOLE_0;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, BINOP_1, COMPTS_1, PRE_TOPC, FINSEQOP, SEQ_4, STRUCT_0,
XBOOLE_0;
theorems AXIOMS, TARSKI, SUBSET_1, FUNCT_1, FINSEQ_1, FUNCOP_1, REAL_1,
SQUARE_1, FUNCT_2, BINOP_1, PRE_TOPC, SEQ_2, COMPLEX1, SETWISEO,
FINSEQ_2, FINSEQOP, RVSUM_1, SEQ_4, RELAT_1, SETFAM_1, ZFMISC_1,
XBOOLE_0, XCMPLX_0, XCMPLX_1;
schemes BINOP_1, FUNCT_2, FRAENKEL;
begin
reserve i,j,k,n for Nat, r,r',r1,r2 for Real;
reserve c,c',c1,c2,c3 for Element of COMPLEX;
scheme FuncDefUniq{C, D()->non empty set,
F((Element of C()))->set}:
for f1,f2 being Function of C(),D() st
(for x being Element of C() holds f1.x = F(x)) &
(for x being Element of C() holds f2.x = F(x))
holds f1 = f2
proof let f1,f2 be Function of C(),D() such that
A1: for x being Element of C() holds f1.x = F(x) and
A2: for x being Element of C() holds f2.x = F(x);
now let x be Element of C();
thus f1.x = F(x) by A1 .= f2.x by A2;
end;
hence thesis by FUNCT_2:113;
end;
scheme BinOpDefuniq{A()->non empty set,
O((Element of A()),Element of A())->set}:
for o1,o2 being BinOp of A() st
(for a,b being Element of A() holds o1.(a,b) = O(a,b)) &
(for a,b being Element of A() holds o2.(a,b) = O(a,b))
holds o1 = o2
proof let o1,o2 be BinOp of A() such that
A1: for a,b being Element of A() holds o1.(a,b) = O(a,b) and
A2: for a,b being Element of A() holds o2.(a,b) = O(a,b);
now let a,b be Element of A();
thus o1.(a,b) = O(a,b) by A1 .= o2.(a,b) by A2;
end;
hence thesis by BINOP_1:2;
end;
definition
deffunc O(Element of COMPLEX,Element of COMPLEX) = $1+$2;
func addcomplex -> BinOp of COMPLEX means
:Def1: for c1,c2 holds it.(c1,c2) = c1 + c2;
existence
proof
thus ex o being BinOp of COMPLEX st
for a,b being Element of COMPLEX holds o.(a,b) = O(a,b) from BinOpLambda;
end;
uniqueness
proof
thus for o1,o2 being BinOp of COMPLEX st
(for a,b being Element of COMPLEX holds o1.(a,b) = O(a,b)) &
(for a,b being Element of COMPLEX holds o2.(a,b) = O(a,b))
holds o1 = o2 from BinOpDefuniq;
end;
end;
theorem Th1:
addcomplex is commutative
proof let c1,c2;
thus addcomplex.(c1,c2) = c1 + c2 by Def1
.= addcomplex.(c2,c1) by Def1;
end;
theorem Th2:
addcomplex is associative
proof let c1,c2,c3;
thus addcomplex.(c1,addcomplex.(c2,c3))
= addcomplex.(c1,c2+c3) by Def1
.= c1+(c2+c3) by Def1
.= c1+c2+c3 by XCMPLX_1:1
.= (addcomplex.(c1,c2))+c3 by Def1
.= addcomplex.(addcomplex.(c1,c2),c3) by Def1;
end;
theorem Th3:
0c is_a_unity_wrt addcomplex
proof
thus for c holds addcomplex.(0c,c) = c
proof let c;
thus addcomplex.(0c,c) = 0c + c by Def1 .= c by COMPLEX1:22;
end;
let c;
thus addcomplex.(c,0c) = c + 0c by Def1 .= c by COMPLEX1:22;
end;
theorem Th4:
the_unity_wrt addcomplex = 0c by Th3,BINOP_1:def 8;
theorem Th5:
addcomplex has_a_unity by Th3,SETWISEO:def 2;
definition
deffunc F(Element of COMPLEX) = -$1;
func compcomplex -> UnOp of COMPLEX means
:Def2: for c holds it.c = -c;
existence
proof
thus ex f being Function of COMPLEX,COMPLEX st
for x being Element of COMPLEX holds f.x = F(x) from LambdaD;
end;
uniqueness
proof
thus for f1,f2 being Function of COMPLEX,COMPLEX st
(for x being Element of COMPLEX holds f1.x = F(x)) &
(for x being Element of COMPLEX holds f2.x = F(x))
holds f1 = f2 from FuncDefUniq;
end;
end;
theorem Th6:
compcomplex is_an_inverseOp_wrt addcomplex
proof let c;
thus addcomplex.(c,compcomplex.c) = c+compcomplex.c by Def1
.= c+-c by Def2
.= the_unity_wrt addcomplex by Th4,XCMPLX_0:def 6;
thus addcomplex.(compcomplex.c,c) = compcomplex.c+c by Def1
.= -c+c by Def2
.= the_unity_wrt addcomplex by Th4,XCMPLX_0:def 6
;
end;
theorem Th7:
addcomplex has_an_inverseOp by Th6,FINSEQOP:def 2;
theorem Th8:
the_inverseOp_wrt addcomplex = compcomplex by Th2,Th5,Th6,Th7,FINSEQOP:def 3;
definition
func diffcomplex -> BinOp of COMPLEX equals
:Def3: addcomplex*(id COMPLEX,compcomplex);
correctness;
end;
theorem Th9:
diffcomplex.(c1,c2) = c1 - c2
proof
thus diffcomplex.(c1,c2) = addcomplex.(c1,compcomplex.c2) by Def3,FINSEQOP:87
.= addcomplex.(c1,-c2) by Def2
.= c1 + - c2 by Def1
.= c1 - c2 by XCMPLX_0:def 8;
end;
definition
deffunc O(Element of COMPLEX,Element of COMPLEX) = $1*$2;
func multcomplex -> BinOp of COMPLEX means
:Def4: for c1,c2 holds it.(c1,c2) = c1 * c2;
existence
proof
thus ex o being BinOp of COMPLEX st
for a,b being Element of COMPLEX holds o.(a,b) = O(a,b) from BinOpLambda;
end;
uniqueness
proof
thus for o1,o2 being BinOp of COMPLEX st
(for a,b being Element of COMPLEX holds o1.(a,b) = O(a,b)) &
(for a,b being Element of COMPLEX holds o2.(a,b) = O(a,b))
holds o1 = o2 from BinOpDefuniq;
end;
end;
theorem
multcomplex is commutative
proof let c1,c2;
thus multcomplex.(c1,c2) = c1 * c2 by Def4
.= multcomplex.(c2,c1) by Def4;
end;
theorem Th11:
multcomplex is associative
proof let c1,c2,c3;
thus multcomplex.(c1,multcomplex.(c2,c3))
= multcomplex.(c1,c2*c3) by Def4
.= c1*(c2*c3) by Def4
.= c1*c2*c3 by XCMPLX_1:4
.= (multcomplex.(c1,c2))*c3 by Def4
.= multcomplex.(multcomplex.(c1,c2),c3) by Def4;
end;
theorem Th12:
1r is_a_unity_wrt multcomplex
proof
thus for c holds multcomplex.(1r,c) = c
proof let c;
thus multcomplex.(1r,c) = 1r * c by Def4 .= c by COMPLEX1:29;
end;
let c;
thus multcomplex.(c,1r) = c * 1r by Def4 .= c by COMPLEX1:29;
end;
theorem Th13:
the_unity_wrt multcomplex = 1r by Th12,BINOP_1:def 8;
theorem Th14:
multcomplex has_a_unity by Th12,SETWISEO:def 2;
theorem Th15:
multcomplex is_distributive_wrt addcomplex
proof
now let c1,c2,c3;
thus multcomplex.(c1,addcomplex.(c2,c3))
= multcomplex.(c1,c2+c3) by Def1
.= c1*(c2+c3) by Def4
.= c1*c2+c1*c3 by XCMPLX_1:8
.= addcomplex.(c1*c2,c1*c3) by Def1
.= addcomplex.(multcomplex.(c1,c2),c1*c3) by Def4
.= addcomplex.(multcomplex.(c1,c2),multcomplex.(c1,c3)) by Def4;
thus multcomplex.(addcomplex.(c1,c2),c3)
= multcomplex.(c1+c2,c3) by Def1
.= (c1+c2)*c3 by Def4
.= c1*c3+c2*c3 by XCMPLX_1:8
.= addcomplex.(c1*c3,c2*c3) by Def1
.= addcomplex.(multcomplex.(c1,c3),c2*c3) by Def4
.= addcomplex.(multcomplex.(c1,c3),multcomplex.(c2,c3)) by Def4;
end;
hence thesis by BINOP_1:23;
end;
definition let c;
func c multcomplex -> UnOp of COMPLEX equals
:Def5: multcomplex[;](c,id COMPLEX);
coherence;
end;
Lm1:
(multcomplex[;](c,id COMPLEX)).c' = c*c'
proof
thus (multcomplex[;](c,id COMPLEX)).c'
= multcomplex.(c,(id COMPLEX).c') by FUNCOP_1:66
.= multcomplex.(c,c') by FUNCT_1:35
.= c*c' by Def4;
end;
theorem Th16:
(c multcomplex).c' = c*c'
proof c multcomplex = multcomplex[;](c,id COMPLEX) by Def5;
hence thesis by Lm1;
end;
theorem Th17:
c multcomplex is_distributive_wrt addcomplex
proof c multcomplex = multcomplex[;](c,id COMPLEX) by Def5;
hence thesis by Th15,FINSEQOP:55;
end;
definition
deffunc F(Element of COMPLEX) = |.$1.|;
func abscomplex -> Function of COMPLEX,REAL means
:Def6: for c holds it.c = |.c.|;
existence
proof
thus ex f being Function of COMPLEX,REAL st
for x being Element of COMPLEX holds f.x = F(x) from LambdaD;
end;
uniqueness
proof
thus for f1,f2 being Function of COMPLEX,REAL st
(for x being Element of COMPLEX holds f1.x = F(x)) &
(for x being Element of COMPLEX holds f2.x = F(x))
holds f1 = f2 from FuncDefUniq;
end;
end;
reserve z,z1,z2 for FinSequence of COMPLEX;
definition let z1,z2;
func z1 + z2 -> FinSequence of COMPLEX equals
:Def7: addcomplex.:(z1,z2);
correctness;
func z1 - z2 -> FinSequence of COMPLEX equals
:Def8: diffcomplex.:(z1,z2);
correctness;
end;
definition let z;
func -z -> FinSequence of COMPLEX equals
:Def9: compcomplex*z;
correctness;
end;
definition let c,z;
func c*z -> FinSequence of COMPLEX equals
:Def10: (c multcomplex)*z;
correctness;
end;
Lm2: c*z = (multcomplex[;](c,id COMPLEX))*z
proof multcomplex[;](c,id COMPLEX) = c multcomplex by Def5;
hence thesis by Def10;
end;
definition let z;
func abs z -> FinSequence of REAL equals
:Def11: abscomplex*z;
correctness;
end;
definition let n;
func COMPLEX n -> FinSequence-DOMAIN of COMPLEX equals
:Def12: n-tuples_on COMPLEX;
correctness;
end;
definition let n;
cluster COMPLEX n -> non empty;
coherence;
end;
reserve x,z,z1,z2,z3 for Element of COMPLEX n,
A,B for Subset of COMPLEX n;
theorem Th18:
len z = n
proof n-tuples_on COMPLEX = COMPLEX n by Def12;
hence thesis by FINSEQ_2:109;
end;
Lm3: dom z = Seg n
proof len z = n by Th18; hence thesis by FINSEQ_1:def 3; end;
theorem
for z being Element of COMPLEX 0 holds z = <*>COMPLEX
proof let z be Element of COMPLEX 0;
0-tuples_on COMPLEX = COMPLEX 0 by Def12;
hence thesis by FINSEQ_2:113;
end;
theorem
<*>COMPLEX is Element of COMPLEX 0
proof 0-tuples_on COMPLEX = COMPLEX 0 by Def12;
hence thesis by FINSEQ_2:114;
end;
theorem Th21:
k in Seg n implies z.k in COMPLEX
proof len z = n by Th18;
then Seg n = dom z by FINSEQ_1:def 3;
hence thesis by FINSEQ_2:13;
end;
canceled;
theorem Th23:
(for k st k in Seg n holds z1.k = z2.k) implies z1 = z2
proof n-tuples_on COMPLEX = COMPLEX n by Def12;
hence thesis by FINSEQ_2:139;
end;
definition let n,z1,z2;
redefine
func z1 + z2 -> Element of COMPLEX n;
coherence
proof z1 + z2 = addcomplex.:(z1,z2) & n-tuples_on COMPLEX = COMPLEX n
by Def7,Def12;
hence thesis by FINSEQ_2:140;
end;
end;
theorem Th24:
k in Seg n & c1 = z1.k & c2 = z2.k implies (z1 + z2).k = c1 + c2
proof assume that
A1: k in Seg n and
A2: c1 = z1.k & c2 = z2.k;
z1 + z2 = addcomplex.:(z1,z2) & k in dom(z1+z2) by A1,Def7,Lm3;
hence (z1 + z2).k = addcomplex.(c1,c2) by A2,FUNCOP_1:28
.= c1 + c2 by Def1;
end;
theorem Th25:
z1 + z2 = z2 + z1
proof
A1: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus z1 + z2 = addcomplex.:(z1,z2) by Def7
.= addcomplex.:(z2,z1) by A1,Th1,FINSEQOP:34
.= z2 + z1 by Def7;
end;
theorem Th26:
z1 + (z2 + z3) = z1 + z2 + z3
proof
A1: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus z1 + (z2 + z3)
= addcomplex.:(z1,z2+z3) by Def7
.= addcomplex.:(z1,addcomplex.:(z2,z3)) by Def7
.= addcomplex.:(addcomplex.:(z1,z2),z3) by A1,Th2,FINSEQOP:29
.= addcomplex.:(z1+z2,z3) by Def7
.= z1 + z2 + z3 by Def7;
end;
definition let n;
func 0c n -> FinSequence of COMPLEX equals
:Def13: n |-> 0c;
correctness;
end;
definition let n;
redefine func 0c n -> Element of COMPLEX n;
coherence
proof 0c n = n |-> 0c & n-tuples_on COMPLEX = COMPLEX n by Def12,Def13;
hence thesis;
end;
end;
theorem
k in Seg n implies (0c n).k = 0c
proof 0c n = n |-> 0c by Def13;
hence thesis by FINSEQ_2:70;
end;
Lm4: z + 0c n = z
proof
A1: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus z + 0c n = z + (n|->0c) by Def13
.= addcomplex.:(z,n|->0c) by Def7
.= z by A1,Th4,Th5,FINSEQOP:57;
end;
theorem Th28:
z + 0c n = z & z = 0c n + z
proof thus z + 0c n = z by Lm4; hence thesis by Th25; end;
definition let n,z;
redefine func -z -> Element of COMPLEX n;
coherence
proof -z = compcomplex*z & n-tuples_on COMPLEX = COMPLEX n by Def9,Def12;
hence thesis by FINSEQ_2:133;
end;
end;
theorem Th29:
k in Seg n & c = z.k implies (-z).k = -c
proof assume that
A1: k in Seg n and
A2: c = z.k;
-z = compcomplex*z & k in dom(-z) by A1,Def9,Lm3;
hence (-z).k = compcomplex.c by A2,FUNCT_1:22 .= -c by Def2;
end;
Lm5: z + -z = 0c n
proof
A1: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus z + -z = addcomplex.:(z,-z) by Def7
.= addcomplex.:(z,compcomplex*z) by Def9
.= n|->0c by A1,Th2,Th4,Th5,Th7,Th8,FINSEQOP:77
.= 0c n by Def13;
end;
Lm6: -0c n = 0c n
proof
thus -0c n = -(n|->0c) by Def13
.= compcomplex*(n|->0c) by Def9
.= n|->(compcomplex.0c) by FINSEQOP:17
.= n|->0c by Def2,REAL_1:26
.= 0c n by Def13;
end;
theorem Th30:
z + -z = 0c n & -z + z = 0c n
proof thus z + -z = 0c n by Lm5; hence -z + z = 0c n by Th25; end;
theorem Th31:
z1 + z2 = 0c n implies z1 = -z2 & z2 = -z1
proof
n-tuples_on COMPLEX = COMPLEX n & 0c n = n |-> 0c &
z1 + z2 = addcomplex.:(z1,z2) & -z1 = compcomplex*z1 & -z2 = compcomplex*z2
by Def7,Def9,Def12,Def13;
hence thesis by Th2,Th4,Th5,Th7,Th8,FINSEQOP:78;
end;
theorem Th32:
--z = z
proof z + -z = 0c n by Lm5; hence thesis by Th31; end;
theorem
-z1 = -z2 implies z1 = z2
proof assume -z1 = -z2; hence z1 = --z2 by Th32 .= z2 by Th32; end;
Lm7: z1 + z = z2 + z implies z1 = z2
proof assume z1 + z = z2 + z;
then z1 + (z + -z)= (z2 + z) + -z by Th26;
then z1 + (z + -z)= z2 + (z + -z) & z + -z = 0c n by Lm5,Th26;
then z1 = z2 + 0c n by Lm4;
hence z1 = z2 by Lm4;
end;
theorem
z1 + z = z2 + z or z1 + z = z + z2 implies z1 = z2
proof z1 + z = z2 + z iff z1 + z = z + z2 by Th25;
hence thesis by Lm7;
end;
theorem Th35:
-(z1 + z2) = -z1 + -z2
proof
(z1 + z2) + (-z1 + -z2) = z1 + z2 + -z1 + -z2 by Th26
.= z2 + z1 + -z1 + -z2 by Th25
.= z2 + (z1 + -z1) + -z2 by Th26
.= z2 + 0c n + -z2 by Lm5
.= z2 + -z2 by Lm4
.= 0c n by Lm5;
hence thesis by Th31;
end;
definition let n,z1,z2;
redefine func z1 - z2 -> Element of COMPLEX n;
coherence
proof n-tuples_on COMPLEX = COMPLEX n & z1 - z2 = diffcomplex.:(z1,z2)
by Def8,Def12;
hence thesis by FINSEQ_2:140;
end;
end;
theorem
k in Seg n & c1 = z1.k & c2 = z2.k implies (z1 - z2).k = c1 - c2
proof assume that
A1: k in Seg n and
A2: c1 = z1.k & c2 = z2.k;
z1 - z2 = diffcomplex.:(z1,z2) & k in dom(z1 - z2) by A1,Def8,Lm3;
hence (z1 - z2).k = diffcomplex.(c1,c2) by A2,FUNCOP_1:28
.= c1 - c2 by Th9;
end;
theorem Th37:
z1 - z2 = z1 + - z2
proof
A1: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus z1 - z2 = diffcomplex.:(z1,z2) by Def8
.= addcomplex.:(z1,compcomplex*z2) by A1,Def3,FINSEQOP:89
.= addcomplex.:(z1,-z2) by Def9
.= z1 + -z2 by Def7;
end;
theorem
z - 0c n = z
proof
thus z - 0c n = z + -0c n by Th37 .= z + 0c n by Lm6 .= z by Lm4;
end;
theorem
0c n - z = -z
proof thus 0c n - z = 0c n + -z by Th37 .= -z by Th28; end;
theorem
z1 - -z2 = z1 + z2
proof thus z1 - -z2 = z1 + --z2 by Th37 .= z1 + z2 by Th32; end;
theorem Th41:
-(z1 - z2) = z2 - z1
proof
thus -(z1 - z2) = -(z1 + -z2) by Th37
.= -z1 + --z2 by Th35
.= -z1 + z2 by Th32
.= z2 + -z1 by Th25
.= z2 - z1 by Th37;
end;
theorem Th42:
-(z1 - z2) = -z1 + z2
proof
thus -(z1 - z2) = -(z1+ -z2) by Th37
.= -z1 + --z2 by Th35
.= -z1 + z2 by Th32;
end;
theorem Th43:
z - z = 0c n
proof thus z - z = z + -z by Th37 .= 0c n by Lm5; end;
theorem Th44:
z1 - z2 = 0c n implies z1 = z2
proof assume z1 - z2 = 0c n;
then z1 + - z2 = 0c n by Th37;
then z1 = --z2 by Th31;
hence thesis by Th32;
end;
theorem Th45:
z1 - z2 - z3 = z1 - (z2 + z3)
proof
thus z1 - z2 - z3 = z1 - z2 + -z3 by Th37
.= z1 + -z2 + -z3 by Th37
.= z1 + (- z2 + -z3) by Th26
.= z1 + -(z2 + z3) by Th35
.= z1 - (z2 + z3) by Th37;
end;
theorem Th46:
z1 + (z2 - z3) = z1 + z2 - z3
proof
thus z1 + (z2 - z3) = z1 + (z2 + -z3) by Th37
.= z1 + z2 + -z3 by Th26
.= z1 + z2 - z3 by Th37;
end;
theorem Th47:
z1 - (z2 - z3) = z1 - z2 + z3
proof
thus z1 - (z2 - z3) = z1 + - (z2 - z3) by Th37
.= z1 + (-z2 + z3) by Th42
.= z1 + -z2 + z3 by Th26
.= z1 - z2 + z3 by Th37;
end;
theorem Th48:
z1 - z2 + z3 = z1 + z3 - z2
proof
thus z1 - z2 + z3 = z1 - (z2 - z3) by Th47
.= z1 + -(z2 - z3) by Th37
.= z1 + (z3 - z2) by Th41
.= z1 + z3 - z2 by Th46;
end;
theorem Th49:
z1 = z1 + z - z
proof
thus z1 = z1 + 0c n by Lm4
.= z1 + (z - z) by Th43
.= z1 + z - z by Th46;
end;
theorem Th50:
z1 + (z2 - z1) = z2
proof
thus z1 + (z2 - z1) = z2 - z1 + z1 by Th25
.= z2 + -z1 + z1 by Th37
.= z2 + (-z1 + z1) by Th26
.= z2 + 0c n by Th30
.= z2 by Th28;
end;
theorem Th51:
z1 = z1 - z + z
proof
thus z1 = z1 + 0c n by Lm4
.= z1 + (-z + z) by Th30
.= z1 + -z + z by Th26
.= z1 - z + z by Th37;
end;
definition let n,c,z;
redefine func c*z -> Element of COMPLEX n;
coherence
proof n-tuples_on COMPLEX = COMPLEX n & c*z = (multcomplex[;](c,id COMPLEX))*
z
by Def12,Lm2;
hence thesis by FINSEQ_2:133;
end;
end;
theorem Th52:
k in Seg n & c' = z.k implies (c*z).k = c*c'
proof assume that
A1: k in Seg n and
A2: c' = z.k;
c*z = (c multcomplex)*z & k in dom(c*z) by A1,Def10,Lm3;
hence (c*z).k = (c multcomplex).c' by A2,FUNCT_1:22 .= c*c' by Th16;
end;
theorem
c1*(c2*z) = (c1*c2)*z
proof
thus (c1*c2)*z
= (multcomplex[;](c1*c2,id COMPLEX))*z by Lm2
.= multcomplex[;](multcomplex.(c1,c2),id COMPLEX)*z by Def4
.= multcomplex[;](c1,multcomplex[;](c2,id COMPLEX))*z by Th11,FUNCOP_1:77
.= (multcomplex[;](c1,id COMPLEX)*multcomplex[;](c2,id COMPLEX))*z
by FUNCOP_1:69
.= (multcomplex[;](c1,id COMPLEX))*(multcomplex[;](c2,id COMPLEX)*z)
by RELAT_1:55
.= (multcomplex[;](c1,id COMPLEX))*(c2*z) by Lm2
.= c1*(c2*z) by Lm2;
end;
theorem
(c1 + c2)*z = c1*z + c2*z
proof
set c1M = multcomplex[;](c1,id COMPLEX), c2M = multcomplex[;](c2,id COMPLEX);
thus (c1 + c2)*z
= (multcomplex[;](c1 + c2,id COMPLEX))*z by Lm2
.= multcomplex[;](addcomplex.(c1,c2),id COMPLEX)*z by Def1
.= addcomplex.:(c1M,c2M)*z by Th15,FINSEQOP:36
.= addcomplex.:(c1M*z,c2M*z) by FUNCOP_1:31
.= c1M*z + c2M*z by Def7
.= c1*z + c2M*z by Lm2
.= c1*z + c2*z by Lm2;
end;
theorem
c*(z1+z2) = c*z1 + c*z2
proof set cM = c multcomplex;
A1: cM is_distributive_wrt addcomplex by Th17;
A2: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus c*(z1+z2)
= cM*(z1 + z2) by Def10
.= cM*(addcomplex.:(z1,z2)) by Def7
.= addcomplex.:(cM*z1,cM*z2) by A1,A2,FINSEQOP:52
.= cM*z1 + cM*z2 by Def7
.= c*z1 + cM*z2 by Def10
.= c*z1 + c*z2 by Def10;
end;
theorem
1r*z = z
proof
A1: rng z c= COMPLEX by FINSEQ_1:def 4;
thus 1r*z = multcomplex[;](1r,id COMPLEX)*z by Lm2
.= (id COMPLEX)*z by Th13,Th14,FINSEQOP:45
.= z by A1,RELAT_1:79;
end;
theorem
0c*z = 0c n
proof
A1: rng z c= COMPLEX by FINSEQ_1:def 4;
A2: n-tuples_on COMPLEX = COMPLEX n by Def12;
thus 0c*z = multcomplex[;](0c,id COMPLEX)*z by Lm2
.= multcomplex[;](0c,(id COMPLEX)*z) by FUNCOP_1:44
.= multcomplex[;](0c,z) by A1,RELAT_1:79
.= n|->0c by A2,Th2,Th4,Th5,Th7,Th15,FINSEQOP:80
.= 0c n by Def13;
end;
theorem
(-1r)*z = -z
proof
A1: compcomplex.1r = -1r by Def2;
thus (-1r)*z
= multcomplex[;](-1r,id COMPLEX)*z by Lm2
.= compcomplex*z by A1,Th2,Th5,Th7,Th8,Th13,Th14,Th15,FINSEQOP:72
.= -z by Def9;
end;
definition let n,z;
redefine func abs z -> Element of n-tuples_on REAL;
correctness
proof n-tuples_on COMPLEX = COMPLEX n & abs z = abscomplex*z by Def11,Def12;
hence thesis by FINSEQ_2:133;
end;
end;
theorem Th59:
k in Seg n & c = z.k implies (abs z).k = |.c.|
proof assume that
A1: k in Seg n and
A2: c = z.k;
len abs z = n by FINSEQ_2:109;
then abscomplex*z = abs z & k in dom abs z by A1,Def11,FINSEQ_1:def 3;
hence (abs z).k = abscomplex.c by A2,FUNCT_1:22 .= |.c.| by Def6;
end;
theorem Th60:
abs 0c n = n |-> 0
proof
thus abs 0c n = abs(n |-> 0c) by Def13
.= abscomplex*(n |-> 0c) by Def11
.= n |-> abscomplex.0c by FINSEQOP:17
.= n |-> 0 by Def6,COMPLEX1:130;
end;
theorem Th61:
abs -z = abs z
proof
now let j; assume
A1: j in Seg n;
then reconsider c = z.j, c' = (-z).j as Element of COMPLEX by Th21;
thus (abs -z).j = |.c'.| by A1,Th59
.= |.-c.| by A1,Th29
.= |.c.| by COMPLEX1:138
.= (abs z).j by A1,Th59;
end;
hence thesis by FINSEQ_2:139;
end;
theorem Th62:
abs(c*z) = |.c.|*(abs z)
proof
now let j; assume
A1: j in Seg n;
then reconsider c' = z.j, cc = (c*z).j as Element of COMPLEX by Th21;
len (abs z) = n by FINSEQ_2:109;
then Seg n = dom abs z by FINSEQ_1:def 3;
then reconsider ac = (abs z).j as Real by A1,FINSEQ_2:13;
thus (abs(c*z)).j = |.cc.| by A1,Th59
.= |.c*c'.| by A1,Th52
.= |.c.|*|.c'.| by COMPLEX1:151
.= |.c.|*ac by A1,Th59
.= (|.c.|*(abs z)).j by RVSUM_1:67;
end;
hence thesis by FINSEQ_2:139;
end;
definition let z be FinSequence of COMPLEX;
func |.z.| -> Real equals
:Def14: sqrt Sum sqr abs z;
correctness;
end;
theorem Th63:
|.0c n.| = 0
proof
thus |.0c n .| = sqrt Sum sqr abs 0c n by Def14
.= sqrt Sum sqr (n |-> (0 qua Real)) by Th60
.= sqrt Sum (n |-> (0 qua Real)) by RVSUM_1:82,SQUARE_1:60
.= sqrt (n*0) by RVSUM_1:110
.= 0 by SQUARE_1:82;
end;
theorem Th64:
|.z.| = 0 implies z = 0c n
proof assume
A1: |.z.| = 0;
A2: n-tuples_on COMPLEX = COMPLEX n by Def12;
now let j; assume
A3: j in Seg n;
then reconsider c = z.j as Element of COMPLEX by Th21;
0 <= Sum sqr abs z & sqrt Sum sqr abs z = 0 by A1,Def14,RVSUM_1:116;
then Sum sqr abs z = 0 by SQUARE_1:92;
then (abs z).j = (n|->0).j by RVSUM_1:121;
then |.c.| = (n|-> 0).j by A3,Th59;
then |.c.| = 0 by A3,FINSEQ_2:70;
then c = 0c by COMPLEX1:131;
hence z.j = (n|->0c).j by A3,FINSEQ_2:70;
end;
then z = n|->0c by A2,Th23;
hence thesis by Def13;
end;
theorem Th65:
0 <= |.z.|
proof |.z.| = sqrt Sum sqr abs z & 0 <= Sum sqr abs z by Def14,RVSUM_1:116;
hence thesis by SQUARE_1:def 4;
end;
theorem Th66:
|.-z.| = |.z.|
proof
thus |.-z.| = sqrt Sum sqr abs -z by Def14
.= sqrt Sum sqr abs z by Th61
.= |.z.| by Def14;
end;
theorem
|.c*z.| = |.c.|*|.z.|
proof
A1: 0 <= |.c.|^2 & 0 <= Sum sqr abs z by RVSUM_1:116,SQUARE_1:72;
A2: 0 <= |.c.| by COMPLEX1:132;
thus |.c*z.| = sqrt Sum sqr abs(c*z) by Def14
.= sqrt Sum sqr (|.c.|*abs z) by Th62
.= sqrt Sum (|.c.|^2 * sqr abs z) by RVSUM_1:84
.= sqrt (|.c.|^2 * Sum sqr abs z) by RVSUM_1:117
.= sqrt |.c.|^2 * sqrt Sum sqr abs z by A1,SQUARE_1:97
.= |.c.| * sqrt Sum sqr abs z by A2,SQUARE_1:89
.= |.c.|*|.z.| by Def14;
end;
Lm8: for t being Element of i-tuples_on REAL st j in Seg i holds t.j is Real
proof let t be Element of i-tuples_on REAL;
assume
A1: j in Seg i;
len t = i by FINSEQ_2:109;
then Seg i = dom t by FINSEQ_1:def 3;
hence thesis by A1,FINSEQ_2:13;
end;
theorem Th68:
|.z1 + z2.| <= |.z1.| + |.z2.|
proof
A1: 0 <= Sum sqr abs z1 & 0 <= Sum sqr abs z2 by RVSUM_1:116;
then A2: 0 <= sqrt Sum sqr abs z1 & 0 <= sqrt Sum sqr abs z2 by SQUARE_1:def
4;
A3: Sum sqr (abs z1 + abs z2)
= Sum (sqr abs z1 + 2*mlt(abs z1,abs z2) + sqr abs z2) by RVSUM_1:98
.= Sum(sqr abs z1 + 2*mlt(abs z1,abs z2)) + Sum
sqr abs z2 by RVSUM_1:119
.= Sum sqr abs z1 + Sum(2*mlt(abs z1,abs z2)) + Sum
sqr abs z2 by RVSUM_1:119
.= Sum sqr abs z1 + (2*Sum mlt(abs z1,abs z2))+Sum
sqr abs z2 by RVSUM_1:117;
k in Seg n implies (sqr abs (z1 + z2)).k <= (sqr (abs z1 + abs z2)).k
proof assume that
A4: k in Seg n;
set r2 = (sqr (abs z1 + abs z2)).k;
reconsider c1 = z1.k, c2 = z2.k as Element of COMPLEX by A4,Th21;
reconsider c12 = (z1 + z2).k as Element of COMPLEX by A4,Th21;
reconsider abs1 = (abs z1).k, abs2 = (abs z2).k as Real by A4,Lm8;
reconsider abs12 = (abs z1 + abs z2).k as Real by A4,Lm8;
reconsider abs'12 = (abs (z1 + z2)).k as Real by A4,Lm8;
|.c1 + c2.| <= |.c1.| + |.c2.| by COMPLEX1:142;
then |.c12.| <= |.c1.| + |.c2.| by A4,Th24;
then |.c12.| <= |.c1.| + abs2 by A4,Th59;
then A5: |.c12.| <= abs1 + abs2 by A4,Th59;
len(abs z1 + abs z2) = n by FINSEQ_2:109;
then dom (abs z1 + abs z2) = Seg n by FINSEQ_1:def 3;
then 0 <= |.c12.| & |.c12.| <= abs12 by A4,A5,COMPLEX1:132,RVSUM_1:26;
then abs'12 <= abs12 & 0 <= abs'12 by A4,Th59;
then (abs'12)^2 <= (abs12)^2 by SQUARE_1:77;
then (abs'12)^2 <= r2 by RVSUM_1:79;
hence thesis by RVSUM_1:79;
end;
then A6: Sum sqr abs (z1 + z2) <=
Sum sqr abs z1 + (2*Sum mlt(abs z1,abs z2))+Sum sqr abs z2
by A3,RVSUM_1:112;
A7: k in Seg n implies 0 <= (mlt(abs z1,abs z2)).k
proof assume that
A8: k in Seg n;
set r = (mlt(abs z1,abs z2)).k;
reconsider c1 = z1.k, c2 = z2.k as Element of COMPLEX by A8,Th21;
len mlt(abs z1,abs z2) = n & (abs z1).k = |.c1.| & (abs z2).k = |.c2.|
by A8,Th59,FINSEQ_2:109;
then r = |.c1.|*|.c2.| & 0 <= |.c1.| & 0 <= |.c2.|
by COMPLEX1:132,RVSUM_1:87;
then 0*|.c2.| <= r by AXIOMS:25;
hence thesis;
end;
len mlt(abs z1,abs z2) = n by FINSEQ_2:109;
then dom mlt(abs z1,abs z2) = Seg n &
0 <= (Sum mlt(abs z1,abs z2))^2 &
(Sum mlt(abs z1,abs z2))^2 <= (Sum sqr abs z1)*(Sum sqr abs z2)
by FINSEQ_1:def 3,RVSUM_1:122,SQUARE_1:72;
then 0 <= Sum mlt(abs z1,abs z2) &
sqrt(Sum mlt(abs z1,abs z2))^2 <= sqrt((Sum sqr abs z1)*(Sum sqr abs z2))
by A7,RVSUM_1:114,SQUARE_1:94;
then 0 <= 2 & Sum mlt(abs z1,abs z2) <= sqrt((Sum sqr abs z1)*(Sum
sqr abs z2))
by SQUARE_1:89;
then Sum sqr abs z1 <= Sum sqr abs z1 &
2*Sum mlt(abs z1,abs z2) <= 2*sqrt((Sum sqr abs z1)*(Sum sqr abs z2))
by AXIOMS:25;
then Sum sqr abs z2 <= Sum sqr abs z2 &
Sum sqr abs z1+(2*Sum mlt(abs z1,abs z2)) <=
Sum sqr abs z1+2*sqrt((Sum sqr abs z1)*(Sum sqr abs z2)) by REAL_1:55;
then Sum sqr abs z1+(2*Sum mlt(abs z1,abs z2)) + Sum sqr abs z2 <=
Sum sqr abs z1+2*sqrt((Sum sqr abs z1)*(Sum sqr abs z2)) + Sum sqr abs z2
by REAL_1:55;
then Sum sqr abs (z1 + z2) <=
Sum sqr abs z1+2*sqrt((Sum sqr abs z1)*(Sum sqr abs z2)) + Sum
sqr abs z2
by A6,AXIOMS:22;
then Sum sqr abs (z1 + z2) <=
Sum sqr abs z1+2*((sqrt Sum sqr abs z1)*(sqrt Sum sqr abs z2)) + Sum
sqr abs z2
by A1,SQUARE_1:97;
then Sum sqr abs z1 = (sqrt Sum sqr abs z1)^2 &
(sqrt Sum sqr abs z2)^2 = Sum sqr abs z2 &
Sum sqr abs (z1 + z2) <=
Sum sqr abs z1+2*(sqrt Sum sqr abs z1)*(sqrt Sum sqr abs z2) + Sum
sqr abs z2
by A1,SQUARE_1:def 4,XCMPLX_1:4;
then 0 <= Sum sqr abs (z1 + z2) &
Sum sqr abs (z1 + z2) <= ((sqrt Sum sqr abs z1) + (sqrt Sum
sqr abs z2))^2
by RVSUM_1:116,SQUARE_1:63;
then 0 + 0 <= (sqrt Sum sqr abs z1) + (sqrt Sum sqr abs z2) &
sqrt Sum sqr abs (z1 + z2) <= sqrt(((sqrt Sum sqr abs z1) +
(sqrt Sum sqr abs z2))^2)
by A2,REAL_1:55,SQUARE_1:94;
then sqrt Sum sqr abs (z1 + z2) <= (sqrt Sum sqr abs z1) + (sqrt Sum
sqr abs z2)
by SQUARE_1:89;
then sqrt Sum sqr abs (z1 + z2) <= (sqrt Sum sqr abs z1) + |.z2.| by Def14;
then sqrt Sum sqr abs (z1 + z2) <= |.z1.| + |.z2.| by Def14;
hence thesis by Def14;
end;
theorem Th69:
|.z1 - z2.| <= |.z1.| + |.z2.|
proof |.z1 - z2.| = |.z1 + - z2.| by Th37;
then |.z1 - z2.| <= |.z1.| + |.-z2.| by Th68;
hence thesis by Th66;
end;
theorem
|.z1.| - |.z2.| <= |.z1 + z2.|
proof z1 = z1 + z2 - z2 by Th49;
then |.z1.| <= |.z1 + z2.| + |.z2.| by Th69;
hence thesis by REAL_1:86;
end;
theorem
|.z1.| - |.z2.| <= |.z1 - z2.|
proof z1 = z1 - z2 + z2 by Th51;
then |.z1.| <= |.z1 - z2.| + |.z2.| by Th68;
hence thesis by REAL_1:86;
end;
theorem Th72:
|.z1 - z2.| = 0 iff z1 = z2
proof
thus |.z1 - z2.| = 0 implies z1 = z2
proof assume |.z1 - z2.| = 0; then z1 - z2 = 0c n by Th64;
hence thesis by Th44;
end;
assume z1 = z2;
then z1 - z2 = 0c n by Th43;
hence thesis by Th63;
end;
theorem Th73:
z1 <> z2 implies 0 < |.z1 - z2.|
proof assume z1 <> z2;
then 0 <= |.z1 - z2.| & 0 <> |.z1 - z2.| by Th65,Th72;
hence thesis;
end;
theorem Th74:
|.z1 - z2.| = |.z2 - z1.|
proof
thus |.z1 - z2.| = |.-(z2 - z1).| by Th41
.= |.z2 - z1.| by Th66;
end;
theorem Th75:
|.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
|.z1 - z2.| = |.z1 - z + z - z2.| by Th51
.= |.(z1 - z) + (z - z2).| by Th46;
hence thesis by Th68;
end;
definition let n; let A be Element of bool COMPLEX n;
attr A is open means
:Def15: for x st x in A ex r st 0 < r & for z st |.z.| < r holds x + z in A;
end;
definition let n; let A be Element of bool COMPLEX n;
attr A is closed means
for x st for r st r > 0 ex z st |.z.| < r & x + z in A
holds x in A;
end;
theorem
for A being Element of bool COMPLEX n st A = {} holds A is open
proof let A be Element of bool COMPLEX n;
assume
A1: A = {};
let x; thus thesis by A1;
end;
theorem Th77:
for A being Element of bool COMPLEX n st A = COMPLEX n holds A is open
proof let A be Element of bool COMPLEX n;
assume
A1: A = COMPLEX n;
let x such that x in A;
reconsider j = 1 as Real;
take j; thus 0 < j;
let z such that |.z.| < j;
thus x + z in A by A1;
end;
theorem Th78:
for AA being Subset-Family of COMPLEX n st
for A being Element of bool COMPLEX n st A in AA holds A is open
for A being Element of bool COMPLEX n st A = union AA
holds A is open
proof let AA be Subset-Family of COMPLEX n such that
A1: for A being Element of bool COMPLEX n st A in AA holds A is open;
let A be Element of bool COMPLEX n such that
A2: A = union AA;
let x;
assume x in A;
then consider B being set such that
A3: x in B and
A4: B in AA by A2,TARSKI:def 4;
reconsider B as Element of bool COMPLEX n by A4;
B is open by A1,A4;
then consider r such that
A5: 0 < r and
A6: for z st |.z.| < r holds x + z in B by A3,Def15;
take r;
thus 0 < r by A5;
let z; assume |.z.| < r;
then x + z in B by A6;
hence x + z in A by A2,A4,TARSKI:def 4;
end;
theorem Th79:
for A,B being Subset of COMPLEX n st A is open & B is open
for C being Element of bool COMPLEX n st C = A /\ B holds C is open
proof let A,B be Subset of COMPLEX n such that
A1: A is open & B is open;
let C be Element of bool COMPLEX n such that
A2: C = A /\ B;
let x; assume
A3: x in C;
then x in A by A2,XBOOLE_0:def 3;
then consider r1 such that
A4: 0 < r1 and
A5: for z st |.z.| < r1 holds x + z in A by A1,Def15;
x in B by A2,A3,XBOOLE_0:def 3;
then consider r2 such that
A6: 0 < r2 and
A7: for z st |.z.| < r2 holds x + z in B by A1,Def15;
take min(r1,r2);
thus 0 < min(r1,r2) by A4,A6,SQUARE_1:38;
let z;
A8: min(r1,r2) <= r1 & min(r1,r2) <= r2 by SQUARE_1:35;
assume |.z.| < min(r1,r2);
then |.z.| < r1 & |.z.| < r2 by A8,AXIOMS:22;
then x + z in A & x + z in B by A5,A7;
hence x + z in C by A2,XBOOLE_0:def 3;
end;
definition let n,x,r;
func Ball(x,r) -> Subset of COMPLEX n equals
:Def17: { z : |.z - x.| < r };
coherence
proof
defpred P[FinSequence of COMPLEX] means |.$1 - x.| < r;
{ z : P[z] } c= COMPLEX n from Fr_Set0;
hence thesis;
end;
end;
theorem Th80:
z in Ball(x,r) iff |.x - z.| < r
proof
A1: |.z - x.| = |.x - z.| by Th74;
z in { z2 : |.z2 - x.| < r } iff ex z1 st z = z1 & |.z1 - x.| < r;
hence z in Ball(x,r) iff |.x - z.| < r by A1,Def17;
end;
theorem Th81:
0 < r implies x in Ball(x,r)
proof assume
A1: 0 < r;
|.x - x.| = 0 by Th72;
then x in { z : |.z - x.| < r } by A1;
hence x in Ball(x,r) by Def17;
end;
theorem Th82:
Ball(z1,r1) is open
proof let x such that
A1: x in Ball(z1,r1);
take r = r1 - |.z1 - x.|;
|.z1 - x.| < r1 by A1,Th80;
hence 0 < r by SQUARE_1:11;
let z;
z1 - x - z = z1 - (x + z) by Th45;
then A2: |.z1 - (x + z).| <= |.z.| + |.z1 - x.| by Th69;
assume |.z.| < r;
then |.z.| + |.z1 - x.| < r + |.z1 - x.| by REAL_1:53;
then |.z1 - (x + z).| < r + |.z1 - x.| by A2,AXIOMS:22;
then |.z1 - (x + z).| < r1 by XCMPLX_1:27;
hence x + z in Ball(z1,r1) by Th80;
end;
scheme SubsetFD { A, D() -> non empty set, F(set) -> Element of D(), P[set] }:
{ F(x) where x is Element of A(): P[x]} is Subset of D()
proof
set X = { F(x) where x is Element of A(): P[x]};
X c= D()
proof let y be set; assume y in X;
then ex z being Element of A() st y = F(z) & P[z];
hence thesis;
end;
hence thesis;
end;
scheme SubsetFD2 { A, B, D() -> non empty set, F(set,set) -> Element of D(),
P[set,set] }:
{ F(x,y) where x is Element of A(), y is Element of B():
P[x,y]} is Subset of D()
proof
set X = { F(x,y) where x is Element of A(), y is Element of B(): P[x,y]};
X c= D()
proof let w be set; assume w in X;
then ex x being Element of A(), y being Element of B() st w = F(x,y) & P[
x,y];
hence thesis;
end;
hence thesis;
end;
definition let n,x,A;
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = |.x - $1.|;
func dist(x,A) -> Real means
:Def18: for X being Subset of REAL st X = {|.x - z.| : z in A}
holds it = lower_bound X;
existence
proof
reconsider X = {f(z) : P[z]} as Subset of REAL from SubsetFD;
take lower_bound X;
thus thesis;
end;
uniqueness
proof let r1,r2 be Real such that
A1: for X being Subset of REAL st X = {|.x - z.| : z in A}
holds r1 = lower_bound X and
A2: for X being Subset of REAL st X = {|.x - z.| : z in A}
holds r2 = lower_bound X;
reconsider X = {f(z) : P[z]} as Subset of REAL from SubsetFD;
r1 = lower_bound X & r2 = lower_bound X by A1,A2;
hence thesis;
end;
end;
definition let n,A,r;
func Ball(A,r) -> Subset of COMPLEX n equals
:Def19: { z : dist(z,A) < r };
coherence
proof
defpred P[Element of COMPLEX n] means dist($1,A) < r;
{ z : P[z] } c= COMPLEX n from Fr_Set0;
hence thesis;
end;
end;
theorem Th83:
(for r' st r' > 0 holds r + r' > r1) implies r >= r1
proof
assume
A1: r' > 0 implies r + r' > r1;
assume not thesis;
then r1 - r > 0 & r + (r1 - r) = r1 by SQUARE_1:11,XCMPLX_1:27;
hence contradiction by A1;
end;
theorem Th84:
for X being Subset of REAL, r st
X <> {} & for r' st r' in X holds r <= r'
holds lower_bound X >= r
proof let X be Subset of REAL, r such that
A1: X <> {} and
A2: for r' st r' in X holds r <= r';
for r' be real number st r' in X holds r <= r' by A2;
then A3: X is bounded_below by SEQ_4:def 2;
now let r';
assume r' > 0; then consider r1 be real number such that
A4: r1 in X and
A5: r1 < lower_bound X + r' by A1,A3,SEQ_4:def 5;
r <= r1 by A2,A4;
hence lower_bound X + r' > r by A5,AXIOMS:22;
end;
hence lower_bound X >= r by Th83;
end;
theorem Th85:
A <> {} implies dist(x,A) >= 0
proof assume A <> {}; then consider z1 such that
A1: z1 in A by SUBSET_1:10;
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = |.x - $1.|;
reconsider X = {f(z) : P[z]} as Subset of REAL from SubsetFD;
A2: dist(x,A) = lower_bound X by Def18;
A3: |.x - z1.| in X by A1;
now let r';
assume r' in X;
then ex z st r' = |.x - z.| & z in A;
hence r'>= 0 by Th65;
end;
hence dist(x,A) >= 0 by A2,A3,Th84;
end;
theorem Th86:
A <> {} implies dist(x + z,A) <= dist(x,A) + |.z.|
proof assume A <> {}; then consider z2 such that
A1: z2 in A by SUBSET_1:10;
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = |.x - $1.|;
deffunc g(Element of COMPLEX n) = |.x + z - $1.|;
reconsider X = {f(z1) : P[z1]} as Subset of REAL from SubsetFD;
reconsider Y = {g(z1) : P[z1]} as Subset of REAL from SubsetFD;
A2: dist(x,A) = lower_bound X by Def18;
A3: dist(x+z,A) = lower_bound Y by Def18;
A4: |.x - z2.| in X by A1;
A5: Y is bounded_below
proof
reconsider zero = 0 as Real;
take zero; let r be real number;
assume r in Y; then ex z1 st r = |.x + z - z1 .| & z1 in A;
hence thesis by Th65;
end;
now let r';
assume r' in X; then consider z3 such that
A6: r' = |.x - z3.| & z3 in A;
|.x + z - z3.| in Y by A6;
then A7: |.x + z - z3.| >= dist(x + z,A) by A3,A5,SEQ_4:def 5;
|.x + z - z3.| = |.x - z3 + z.| by Th48;
then |.x + z - z3.| <= r' + |.z.| by A6,Th68;
then r'+ |.z.| >= dist(x + z,A) by A7,AXIOMS:22;
hence r' >= dist(x + z,A) - |.z.| by REAL_1:86;
end;
then dist(x + z,A) - |.z.| <= dist(x,A) by A2,A4,Th84;
hence dist(x + z,A) <= dist(x,A) + |.z.| by REAL_1:86;
end;
theorem Th87:
x in A implies dist(x,A) = 0
proof assume
A1: x in A;
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = |.x - $1.|;
reconsider X = {f(z): P[z]} as Subset of REAL from SubsetFD;
A2: |.x - x.| in X by A1;
A3: now let r be real number; assume r in X;
then ex z st r = |.x - z .| & z in A;
hence 0<=r by Th65;
end;
A4: X is bounded_below
proof
take 0;
thus thesis by A3;
end;
A5: now let r1 be real number such that
A6: 0<r1;
reconsider r = |.x - x.| as real number;
take r;
thus r in X by A1;
thus r<0+r1 by A6,Th72;
end;
thus dist(x,A) = lower_bound X by Def18
.= 0 by A2,A3,A4,A5,SEQ_4:def 5;
end;
theorem Th88:
not x in A & A <> {} & A is closed implies dist(x,A) > 0
proof assume that
A1: not x in A and
A2: A <> {} and
A3: for x st for r st r > 0 ex z st |.z.| < r & x + z in A
holds x in A and
A4: dist(x,A) <= 0;
A5: dist(x,A) = 0 by A2,A4,Th85;
now let r such that
A6: r > 0;
defpred P[set] means $1 in A;
deffunc f(Element of COMPLEX n) = |.x - $1.|;
reconsider X = {f(z) : P[z]} as Subset of REAL from SubsetFD;
A7: dist(x,A) = lower_bound X by Def18;
consider z such that
A8: z in A by A2,SUBSET_1:10;
A9: |.x - z.| in X by A8;
A10: X is bounded_below
proof
reconsider zero = 0 as Real;
take zero; let r be real number;
assume r in X; then ex z st r = |.x - z .| & z in A;
hence thesis by Th65;
end;
0+r = r;
then consider r' be real number such that
A11: r' in X & r'< r by A5,A6,A7,A9,A10,SEQ_4:def 5;
consider z1 such that
A12: r' = |.x - z1.| & z1 in A by A11;
take z = z1 - x;
thus |.z.| < r & x + z in A by A11,A12,Th50,Th74;
end;
hence contradiction by A1,A3;
end;
theorem Th89:
A <> {} implies |.z1 - x.| + dist(x,A) >= dist(z1,A)
proof
x + (z1 - x) = z1 by Th50;
hence thesis by Th86;
end;
theorem Th90:
z in Ball(A,r) iff dist(z,A) < r
proof
z in { z2 : dist(z2,A) < r } iff ex z1 st z = z1 & dist(z1,A) < r;
hence z in Ball(A,r) iff dist(z,A) < r by Def19;
end;
theorem Th91:
0 < r & x in A implies x in Ball(A,r)
proof assume that
A1: 0 < r and
A2: x in A;
dist(x,A) = 0 by A2,Th87;
then x in { z : dist(z,A) < r } by A1;
hence x in Ball(A,r) by Def19;
end;
theorem Th92:
0 < r implies A c= Ball(A,r)
proof assume
A1: r > 0;
let x be set;
assume x in A;
hence x in Ball(A,r) by A1,Th91;
end;
theorem Th93:
A <> {} implies Ball(A,r1) is open
proof assume
A1: A <> {};
let x such that
A2: x in Ball(A,r1);
take r = r1 - dist(x,A);
dist(x,A) < r1 by A2,Th90;
hence 0 < r by SQUARE_1:11;
let z;
A3: dist(x + z,A) <= |.z.| + dist(x,A) by A1,Th86;
assume |.z.| < r;
then |.z.| + dist(x,A) < r + dist(x,A) by REAL_1:53;
then dist(x + z,A) < r + dist(x,A) by A3,AXIOMS:22;
then dist(x + z,A) < r1 by XCMPLX_1:27;
hence x + z in Ball(A,r1) by Th90;
end;
definition let n,A,B;
defpred P[set,set] means $1 in A & $2 in B;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
func dist(A,B) -> Real means
:Def20: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B}
holds it = lower_bound X;
existence
proof
reconsider X = {f(x,z) : P[x,z]} as Subset of REAL from SubsetFD2;
take lower_bound X;
thus thesis;
end;
uniqueness
proof let r1,r2 be Real such that
A1: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B}
holds r1 = lower_bound X and
A2: for X being Subset of REAL st X = {|.x - z.| : x in A & z in B}
holds r2 = lower_bound X;
reconsider X = {f(x,z): P[x,z]} as Subset of REAL from SubsetFD2;
r1 = lower_bound X & r2 = lower_bound X by A1,A2;
hence thesis;
end;
end;
definition let X,Y be Subset of REAL;
defpred P[set,set] means $1 in X & $2 in Y;
deffunc f(Element of REAL,Element of REAL) = $1+$2;
func X + Y -> Subset of REAL equals
:Def21: { r + r1 : r in X & r1 in Y};
coherence
proof {f(r,r1) : P[r,r1]} is Subset of REAL from SubsetFD2;
hence thesis;
end;
end;
theorem Th94:
for X,Y being Subset of REAL holds
X <> {} & Y <> {} implies X + Y <> {}
proof let X,Y be Subset of REAL; assume X <> {};
then consider x being Real such that
A1: x in X by SUBSET_1:10;
assume Y <> {}; then consider y being Real such that
A2: y in Y by SUBSET_1:10;
X + Y = { r + r1 : r in X & r1 in Y} by Def21;
then x + y in X + Y by A1,A2;
hence X + Y <> {};
end;
theorem Th95:
for X,Y being Subset of REAL holds
X is bounded_below & Y is bounded_below
implies X+Y is bounded_below
proof let X,Y be Subset of REAL;
A1: X + Y = { r + r1 : r in X & r1 in Y} by Def21;
assume X is bounded_below; then consider r1 be real number such that
A2: for r be real number st r in X holds r1<=r by SEQ_4:def 2;
assume Y is bounded_below; then consider r2 be real number such that
A3: for r be real number st r in Y holds r2<=r by SEQ_4:def 2;
take r1 + r2; let r be real number;
assume r in X+Y; then consider r',r'' being Real such that
A4: r = r' + r'' & r' in X & r'' in Y by A1;
r1 <= r' & r2 <= r'' by A2,A3,A4;
hence r1+r2<=r by A4,REAL_1:55;
end;
theorem Th96:
for X,Y being Subset of REAL
st X <> {} & X is bounded_below & Y <> {} & Y is bounded_below
holds lower_bound (X + Y) = lower_bound X + lower_bound Y
proof let X,Y be Subset of REAL such that
A1: X <> {} and
A2: X is bounded_below and
A3: Y <> {} and
A4: Y is bounded_below;
A5: X + Y = { r + r1 : r in X & r1 in Y} by Def21;
A6: X + Y <> {} by A1,A3,Th94;
A7: X+Y is bounded_below by A2,A4,Th95;
A8:now let r be real number; assume r in X+Y; then consider r1,r2 such that
A9: r = r1 + r2 & r1 in X & r2 in Y by A5;
A10: r1 >= lower_bound X by A2,A9,SEQ_4:def 5;
r2 >= lower_bound Y by A4,A9,SEQ_4:def 5;
hence lower_bound X + lower_bound Y<=r by A9,A10,REAL_1:55;
end;
now let r' be real number; assume 0<r';
then A11: r'/2 > 0 by SEQ_2:3;
then consider r1 be real number such that
A12: r1 in X & r1<lower_bound X+r'/2 by A1,A2,SEQ_4:def 5;
consider r2 be real number such that
A13: r2 in Y & r2<lower_bound Y+r'/2 by A3,A4,A11,SEQ_4:def 5;
take r = r1 + r2;
thus r in X+Y by A5,A12,A13;
lower_bound X + r'/2 + (lower_bound Y + r'/2)
= lower_bound X + (lower_bound Y + r'/2 + r'/2) by XCMPLX_1:1
.= lower_bound X + (lower_bound Y + (r'/2 + r'/2)) by XCMPLX_1:1
.= lower_bound X + (lower_bound Y + r') by XCMPLX_1:66
.= lower_bound X + lower_bound Y + r' by XCMPLX_1:1;
hence r<lower_bound X + lower_bound Y+r' by A12,A13,REAL_1:67;
end;
hence thesis by A6,A7,A8,SEQ_4:def 5;
end;
theorem Th97:
for X,Y being Subset of REAL st
Y is bounded_below & X <> {} & for r st r in X ex r1 st r1 in Y & r1 <= r
holds lower_bound X >= lower_bound Y
proof let X,Y be Subset of REAL such that
A1: Y is bounded_below and
A2: X <> {} and
A3: for r st r in X ex r1 st r1 in Y & r1 <= r;
now let r1;
assume r1 in X; then consider r2 such that
A4: r2 in Y & r2 <= r1 by A3;
lower_bound Y <= r2 by A1,A4,SEQ_4:def 5;
hence r1 >= lower_bound Y by A4,AXIOMS:22;
end;
hence thesis by A2,Th84;
end;
theorem Th98:
A <> {} & B <> {} implies dist(A,B) >= 0
proof assume
A1: A <> {} & B <> {};
defpred P[set,set] means $1 in A & $2 in B;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
reconsider Z = {f(z1,z): P[z1,z]} as Subset of REAL from SubsetFD2;
consider z1 such that
A2: z1 in A by A1,SUBSET_1:10;
consider z2 such that
A3: z2 in B by A1,SUBSET_1:10;
A4: |.z1 - z2.| in Z by A2,A3;
A5: dist(A,B) = lower_bound Z by Def20;
now let r';
assume r' in Z; then ex z1,z st r' = |.z1 - z.| & z1 in A & z in B;
hence r'>= 0 by Th65;
end;
hence dist(A,B) >= 0 by A4,A5,Th84;
end;
theorem
dist(A,B) = dist(B,A)
proof
defpred P[set,set] means $1 in A & $2 in B;
defpred R[set,set] means $1 in B & $2 in A;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
reconsider X = {f(z1,z) : P[z1,z]} as Subset of REAL from SubsetFD2;
reconsider Y = {f(z,z1) : R[z,z1]} as Subset of REAL from SubsetFD2;
A1: now let r;
A2: now given z1,z such that
A3: r =|.z1 - z.| & z1 in A & z in B;
take z,z1;
thus r =|.z - z1.| & z in B & z1 in A by A3,Th74;
end;
now given z,z1 such that
A4: r =|.z - z1.| & z in B & z1 in A;
take z1,z;
thus r =|.z1 - z.| & z1 in A & z in B by A4,Th74;
end;
hence r in X iff r in Y by A2;
end;
dist(A,B) = lower_bound X & dist(B,A) = lower_bound Y by Def20;
hence thesis by A1,SUBSET_1:8;
end;
theorem Th100:
A <> {} & B <> {} implies dist(x,A) + dist(x,B) >= dist(A,B)
proof assume
A1: A <> {} & B <> {};
defpred P[set,set] means $1 in A & $2 in B;
defpred X[set] means $1 in A;
defpred Y[set] means $1 in B;
deffunc f(Element of COMPLEX n,Element of COMPLEX n) = |.$1 - $2.|;
deffunc g(Element of COMPLEX n) = |.x - $1.|;
reconsider X = {g(z) : X[z]} as Subset of REAL from SubsetFD;
reconsider Y = {g(z) : Y[z]} as Subset of REAL from SubsetFD;
reconsider Z = {f(z1,z) : P[z1,z]} as Subset of REAL from SubsetFD2;
A2: X + Y = { r + r1 : r in X & r1 in Y} by Def21;
consider z1 such that
A3: z1 in A by A1,SUBSET_1:10;
consider z2 such that
A4: z2 in B by A1,SUBSET_1:10;
|.x - z1.| in X & |.x - z2 .| in Y by A3,A4;
then A5: |.x - z1.| + |.x - z2 .| in X + Y by A2;
A6: Z is bounded_below
proof
take 0; let r be real number;
assume r in Z; then ex z1,z st r = |.z1 - z .| & z1 in A & z in B;
hence thesis by Th65;
end;
A7: X <> {} & X is bounded_below
proof |.x - z1.| in X by A3;
hence X <> {};
take 0; let r be real number;
assume r in X; then ex z st r = |.x - z .| & z in A;
hence thesis by Th65;
end;
A8: Y <> {} & Y is bounded_below
proof |.x - z2.| in Y by A4;
hence Y <> {};
take 0; let r be real number;
assume r in Y; then ex z1 st r = |.x - z1 .| & z1 in B;
hence thesis by Th65;
end;
now let r; assume r in X + Y;
then r in { r2 + r1 : r2 in X & r1 in Y} by Def21;
then consider r2,r1 such that
A9: r = r2 + r1 and
A10: r2 in X & r1 in Y;
consider z1 such that
A11: r2 = |.x - z1.| and
A12: z1 in A by A10;
consider z2 such that
A13: r1 = |.x - z2.| & z2 in B by A10;
take r3 = |.z1 - z2.|;
r2 = |.z1 - x.| by A11,Th74;
hence r3 in Z & r3 <= r by A9,A12,A13,Th75;
end;
then A14: lower_bound (X + Y) >= lower_bound Z by A5,A6,Th97;
lower_bound X = dist(x,A) & lower_bound Y = dist(x,B) &
lower_bound Z = dist(A,B) by Def18,Def20;
hence dist(x,A) + dist(x,B) >= dist(A,B) by A7,A8,A14,Th96;
end;
theorem
A meets B implies dist(A,B) = 0
proof assume A /\ B <> {}; then A meets B by XBOOLE_0:def 7; then consider
z
being set such that
A1: z in A & z in B by XBOOLE_0:3;
reconsider z as Element of COMPLEX n by A1;
dist(z,A) = 0 & dist(z,B) = 0 by A1,Th87;
then 0 + 0 >= dist(A,B) by A1,Th100;
hence dist(A,B) = 0 by A1,Th98;
end;
definition let n;
func ComplexOpenSets(n) -> Subset-Family of COMPLEX n equals
:Def22: {A where A is Element of bool COMPLEX n: A is open};
coherence
proof set S = {A where A is Element of bool COMPLEX n: A is open};
S c= bool COMPLEX n
proof let x be set;
assume x in S;
then ex A being Element of bool COMPLEX n st x = A & A is open;
hence thesis;
end;
hence thesis by SETFAM_1:def 7;
end;
end;
theorem Th102:
for A being Element of bool COMPLEX n holds
A in ComplexOpenSets n iff A is open
proof let B be Element of bool COMPLEX n;
B in {A where A is Element of bool COMPLEX n: A is open}
iff ex C being Element of bool COMPLEX n st B = C & C is open;
hence thesis by Def22;
end;
definition let A be non empty set, t be Subset-Family of A;
cluster TopStruct(#A,t#) -> non empty;
coherence
proof
thus the carrier of TopStruct(#A,t#) is non empty;
end;
end;
definition let n;
func the_Complex_Space n -> strict TopSpace equals
:Def23: TopStruct(#COMPLEX n,ComplexOpenSets(n)#);
coherence
proof set T = TopStruct(#COMPLEX n,ComplexOpenSets n#);
T is TopSpace-like
proof
reconsider z = COMPLEX n as Element of bool COMPLEX n by ZFMISC_1:def 1;
z is open by Th77;
hence the carrier of T in the topology of T by Th102;
thus
for A being Subset-Family of T st A c= the topology of
T
holds union A in the topology of T
proof let A be Subset-Family of T such that
A1: A c= the topology of T;
A2: for B be Element of bool COMPLEX n st
B in A holds B is open by A1,Th102;
reconsider z = union A as Element of bool COMPLEX n;
z is open by A2,Th78;
hence union A in the topology of T by Th102;
end;
let A,B be Subset of T;
assume
A3: A in the topology of T & B in the topology of T;
reconsider z1 = A, z2 = B as Subset of COMPLEX n;
A4: z1 is open & z2 is open by A3,Th102;
reconsider z = A /\ B as Element of bool COMPLEX n;
z is open by A4,Th79;
hence A /\ B in the topology of T by Th102;
end;
hence thesis;
end;
end;
definition let n;
cluster the_Complex_Space n -> non empty;
coherence
proof
the_Complex_Space n = TopStruct(#COMPLEX n,ComplexOpenSets(n)#) by Def23;
hence the carrier of the_Complex_Space n is non empty;
end;
end;
theorem Th103:
the topology of the_Complex_Space n = ComplexOpenSets n
proof
the_Complex_Space n = TopStruct(#COMPLEX n,ComplexOpenSets(n)#) by Def23;
hence thesis;
end;
theorem Th104:
the carrier of the_Complex_Space n = COMPLEX n
proof
the_Complex_Space n = TopStruct(#COMPLEX n,ComplexOpenSets(n)#) by Def23;
hence thesis;
end;
reserve p,q for Point of the_Complex_Space n,
V for Subset of the_Complex_Space n;
theorem
p is Element of COMPLEX n by Th104;
canceled 2;
theorem Th108:
for A being Subset of COMPLEX n st A = V holds
A is open iff V is open
proof let A be Subset of COMPLEX n; assume A = V;
then A in ComplexOpenSets n iff V in the topology of the_Complex_Space n
by Th103;
hence A is open iff V is open by Th102,PRE_TOPC:def 5;
end;
theorem Th109:
for A being Subset of COMPLEX n holds
A is closed iff A` is open
proof let A be Subset of COMPLEX n;
thus A is closed implies A` is open
proof assume
A1: for x st for r st r > 0 ex z st |.z.| < r & x + z in A holds x in A;
let x; assume x in A`;
then not x in A by SUBSET_1:54; then consider r such that
A2: r > 0 and
A3: for z st |.z.| < r holds not x + z in A by A1;
take r;
thus 0 < r by A2;
let z; assume |.z.| < r;
then not x + z in A by A3;
hence x + z in A` by SUBSET_1:50;
end;
assume
A4: for x st x in A` ex r st 0 < r & for z st |.z.| < r holds x + z in A`;
let x such that
A5: for r st r > 0 ex z st |.z.| < r & x + z in A;
now let r; assume r > 0;
then consider z such that
A6: |.z.| < r & x + z in A by A5;
take z;
thus |.z.| < r & not x + z in A` by A6,SUBSET_1:54;
end;
then not x in A` by A4;
hence x in A by SUBSET_1:50;
end;
theorem Th110:
for A being Subset of COMPLEX n st A = V holds
A is closed iff V is closed
proof let A be Subset of COMPLEX n such that
A1: A = V;
[#] the_Complex_Space n = the carrier of the_Complex_Space n by PRE_TOPC:
12
.= COMPLEX n by Th104;
then [#](the_Complex_Space n) \ V = A` by A1,SUBSET_1:def 5;
then [#](the_Complex_Space n) \ V is open iff A` is open by Th108;
hence thesis by Th109,PRE_TOPC:def 6;
end;
theorem
the_Complex_Space n is_T2
proof let p,q;
assume
A1: p <> q;
reconsider z1 = p, z2 = q as Element of COMPLEX n by Th104;
set d = |. z1 - z2 .|/2;
0 < |. z1 - z2 .| by A1,Th73;
then A2: 0 < d by SEQ_2:3;
Ball(z1,d) is Subset of the_Complex_Space n &
Ball(z2,d) is Subset of the_Complex_Space n by Th104;
then reconsider K1 = Ball(z1,d), K2 = Ball(z2,d)
as Subset of the_Complex_Space n;
take K1,K2;
Ball(z1,d) is open & Ball(z2,d) is open by Th82;
hence K1 is open & K2 is open by Th108;
thus p in K1 & q in K2 by A2,Th81;
assume K1 /\ K2 <> {};
then consider x such that
A3: x in Ball(z1,d) /\ Ball(z2,d) by SUBSET_1:10;
x in K1 & x in K2 by A3,XBOOLE_0:def 3;
then |.z1 - x.| < d & |.z2 - x .| < d by Th80;
then |.z1 - x.| + |.z2 - x.| < d + d by REAL_1:67;
then |.z1 - x.| + |.z2 - x.| < |.z1 - z2.| by XCMPLX_1:66;
then |.z1 - x.| + |.x - z2.| < |.z1 - z2.| by Th74;
hence contradiction by Th75;
end;
theorem
the_Complex_Space n is_T3
proof let p; let P be Subset of the_Complex_Space n such that
A1: P <> {} & P is closed & not p in P;
reconsider z1 = p as Element of COMPLEX n by Th104;
reconsider A = P as Subset of COMPLEX n by Th104;
A2: A is closed by A1,Th110;
set d = dist(z1,A)/2;
0 < dist(z1,A) by A1,A2,Th88;
then A3: 0 < d by SEQ_2:3;
Ball(z1,d) is Subset of the_Complex_Space n &
Ball(A,d) is Subset of the_Complex_Space n by Th104;
then reconsider K1 = Ball(z1,d), K2 = Ball(A,d)
as Subset of the_Complex_Space n;
take K1,K2;
Ball(z1,d) is open & Ball(A,d) is open by A1,Th82,Th93;
hence K1 is open & K2 is open by Th108;
thus p in K1 & P c= K2 by A3,Th81,Th92;
assume K1 /\ K2 <> {};
then consider x such that
A4: x in Ball(z1,d) /\ Ball(A,d) by SUBSET_1:10;
x in K1 & x in K2 by A4,XBOOLE_0:def 3;
then |.z1 - x.| < d & dist(x,A) < d by Th80,Th90;
then |.z1 - x.| + dist(x,A) < d + d by REAL_1:67;
then |.z1 - x.| + dist(x,A) < dist(z1,A) by XCMPLX_1:66;
hence contradiction by A1,Th89;
end;