:: CLVECT_2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

deffunc H1( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attr seq is convergent means :Def1: :: CLVECT_2:def 1
ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),g < r;
end;

:: deftheorem Def1 defines convergent CLVECT_2:def 1 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),g < r );

theorem Th1: :: CLVECT_2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is convergent
proof end;

theorem Th2: :: CLVECT_2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq2 . n = seq1 . n holds
seq2 is convergent
proof end;

theorem Th3: :: CLVECT_2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 + seq2 is convergent
proof end;

theorem Th4: :: CLVECT_2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
seq1 - seq2 is convergent
proof end;

theorem Th5: :: CLVECT_2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is convergent holds
z * seq is convergent
proof end;

theorem Th6: :: CLVECT_2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
- seq is convergent
proof end;

theorem Th7: :: CLVECT_2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq + x is convergent
proof end;

theorem Th8: :: CLVECT_2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
seq - x is convergent
proof end;

theorem Th9: :: CLVECT_2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is convergent iff ex g being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r )
proof end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
assume A1: seq is convergent ;
func lim seq -> Point of X means :Def2: :: CLVECT_2:def 2
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),it < r;
existence
ex b1 being Point of X st
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),b1 < r
by A1, Def1;
uniqueness
for b1, b2 being Point of X st ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),b1 < r ) & ( for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),b2 < r ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines lim CLVECT_2:def 2 :
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
for b3 being Point of X holds
( b3 = lim seq iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq . n),b3 < r );

theorem Th10: :: CLVECT_2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & x in rng seq holds
lim seq = x
proof end;

theorem :: CLVECT_2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is constant & ex n being Nat st seq . n = x holds
lim seq = x
proof end;

theorem :: CLVECT_2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & ex k being Nat st
for n being Nat st n >= k holds
seq2 . n = seq1 . n holds
lim seq1 = lim seq2
proof end;

theorem Th13: :: CLVECT_2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 + seq2) = (lim seq1) + (lim seq2)
proof end;

theorem Th14: :: CLVECT_2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq2 is convergent holds
lim (seq1 - seq2) = (lim seq1) - (lim seq2)
proof end;

theorem Th15: :: CLVECT_2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is convergent holds
lim (z * seq) = z * (lim seq)
proof end;

theorem Th16: :: CLVECT_2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
lim (- seq) = - (lim seq)
proof end;

theorem Th17: :: CLVECT_2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq + x) = (lim seq) + x
proof end;

theorem :: CLVECT_2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is convergent holds
lim (seq - x) = (lim seq) - x
proof end;

theorem Th19: :: CLVECT_2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent holds
( lim seq = g iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq . n) - g).|| < r )
proof end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
func ||.seq.|| -> Real_Sequence means :Def3: :: CLVECT_2:def 3
for n being Nat holds it . n = ||.(seq . n).||;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = ||.(seq . n).||
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = ||.(seq . n).|| ) & ( for n being Nat holds b2 . n = ||.(seq . n).|| ) holds
b1 = b2
proof end;
end;

:: deftheorem Def3 defines ||. CLVECT_2:def 3 :
for X being ComplexUnitarySpace
for seq being sequence of X
for b3 being Real_Sequence holds
( b3 = ||.seq.|| iff for n being Nat holds b3 . n = ||.(seq . n).|| );

theorem Th20: :: CLVECT_2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
||.seq.|| is convergent
proof end;

theorem Th21: :: CLVECT_2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.seq.|| is convergent & lim ||.seq.|| = ||.g.|| )
proof end;

theorem Th22: :: CLVECT_2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - g).|| is convergent & lim ||.(seq - g).|| = 0 )
proof end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let x be Point of X;
func dist seq,x -> Real_Sequence means :Def4: :: CLVECT_2:def 4
for n being Nat holds it . n = dist (seq . n),x;
existence
ex b1 being Real_Sequence st
for n being Nat holds b1 . n = dist (seq . n),x
proof end;
uniqueness
for b1, b2 being Real_Sequence st ( for n being Nat holds b1 . n = dist (seq . n),x ) & ( for n being Nat holds b2 . n = dist (seq . n),x ) holds
b1 = b2
proof end;
end;

:: deftheorem Def4 defines dist CLVECT_2:def 4 :
for X being ComplexUnitarySpace
for seq being sequence of X
for x being Point of X
for b4 being Real_Sequence holds
( b4 = dist seq,x iff for n being Nat holds b4 . n = dist (seq . n),x );

theorem Th23: :: CLVECT_2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
dist seq,g is convergent
proof end;

theorem Th24: :: CLVECT_2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist seq,g is convergent & lim (dist seq,g) = 0 )
proof end;

theorem :: CLVECT_2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 + seq2).|| is convergent & lim ||.(seq1 + seq2).|| = ||.(g1 + g2).|| )
proof end;

theorem :: CLVECT_2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 + seq2) - (g1 + g2)).|| is convergent & lim ||.((seq1 + seq2) - (g1 + g2)).|| = 0 )
proof end;

theorem :: CLVECT_2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.(seq1 - seq2).|| is convergent & lim ||.(seq1 - seq2).|| = ||.(g1 - g2).|| )
proof end;

theorem :: CLVECT_2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( ||.((seq1 - seq2) - (g1 - g2)).|| is convergent & lim ||.((seq1 - seq2) - (g1 - g2)).|| = 0 )
proof end;

theorem :: CLVECT_2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(z * seq).|| is convergent & lim ||.(z * seq).|| = ||.(z * g).|| )
proof end;

theorem :: CLVECT_2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((z * seq) - (z * g)).|| is convergent & lim ||.((z * seq) - (z * g)).|| = 0 )
proof end;

theorem :: CLVECT_2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(- seq).|| is convergent & lim ||.(- seq).|| = ||.(- g).|| )
proof end;

theorem :: CLVECT_2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((- seq) - (- g)).|| is convergent & lim ||.((- seq) - (- g)).|| = 0 )
proof end;

Lm1: for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq + x).|| is convergent & lim ||.(seq + x).|| = ||.(g + x).|| )
proof end;

theorem Th33: :: CLVECT_2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq + x) - (g + x)).|| is convergent & lim ||.((seq + x) - (g + x)).|| = 0 )
proof end;

theorem :: CLVECT_2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.(seq - x).|| is convergent & lim ||.(seq - x).|| = ||.(g - x).|| )
proof end;

theorem :: CLVECT_2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( ||.((seq - x) - (g - x)).|| is convergent & lim ||.((seq - x) - (g - x)).|| = 0 )
proof end;

theorem :: CLVECT_2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist (seq1 + seq2),(g1 + g2) is convergent & lim (dist (seq1 + seq2),(g1 + g2)) = 0 )
proof end;

theorem :: CLVECT_2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g1, g2 being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g1 & seq2 is convergent & lim seq2 = g2 holds
( dist (seq1 - seq2),(g1 - g2) is convergent & lim (dist (seq1 - seq2),(g1 - g2)) = 0 )
proof end;

theorem :: CLVECT_2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for z being Complex
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (z * seq),(z * g) is convergent & lim (dist (z * seq),(z * g)) = 0 )
proof end;

theorem :: CLVECT_2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g, x being Point of X
for seq being sequence of X st seq is convergent & lim seq = g holds
( dist (seq + x),(g + x) is convergent & lim (dist (seq + x),(g + x)) = 0 )
proof end;

definition
let X be ComplexUnitarySpace;
let x be Point of X;
let r be Real;
func Ball x,r -> Subset of X equals :: CLVECT_2:def 5
{ y where y is Point of X : ||.(x - y).|| < r } ;
coherence
{ y where y is Point of X : ||.(x - y).|| < r } is Subset of X
proof end;
func cl_Ball x,r -> Subset of X equals :: CLVECT_2:def 6
{ y where y is Point of X : ||.(x - y).|| <= r } ;
coherence
{ y where y is Point of X : ||.(x - y).|| <= r } is Subset of X
proof end;
func Sphere x,r -> Subset of X equals :: CLVECT_2:def 7
{ y where y is Point of X : ||.(x - y).|| = r } ;
coherence
{ y where y is Point of X : ||.(x - y).|| = r } is Subset of X
proof end;
end;

:: deftheorem defines Ball CLVECT_2:def 5 :
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Ball x,r = { y where y is Point of X : ||.(x - y).|| < r } ;

:: deftheorem defines cl_Ball CLVECT_2:def 6 :
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds cl_Ball x,r = { y where y is Point of X : ||.(x - y).|| <= r } ;

:: deftheorem defines Sphere CLVECT_2:def 7 :
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Sphere x,r = { y where y is Point of X : ||.(x - y).|| = r } ;

theorem Th40: :: CLVECT_2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Ball x,r iff ||.(x - w).|| < r )
proof end;

theorem Th41: :: CLVECT_2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Ball x,r iff dist x,w < r )
proof end;

theorem :: CLVECT_2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for r being Real st r > 0 holds
x in Ball x,r
proof end;

theorem :: CLVECT_2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for y, x, w being Point of X
for r being Real st y in Ball x,r & w in Ball x,r holds
dist y,w < 2 * r
proof end;

theorem :: CLVECT_2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for y, x, w being Point of X
for r being Real st y in Ball x,r holds
y - w in Ball (x - w),r
proof end;

theorem :: CLVECT_2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for y, x being Point of X
for r being Real st y in Ball x,r holds
y - x in Ball (0. X),r
proof end;

theorem :: CLVECT_2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for y, x being Point of X
for r, q being Real st y in Ball x,r & r <= q holds
y in Ball x,q
proof end;

theorem Th47: :: CLVECT_2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in cl_Ball x,r iff ||.(x - w).|| <= r )
proof end;

theorem Th48: :: CLVECT_2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in cl_Ball x,r iff dist x,w <= r )
proof end;

theorem :: CLVECT_2:49  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for r being Real st r >= 0 holds
x in cl_Ball x,r
proof end;

theorem Th50: :: CLVECT_2:50  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for y, x being Point of X
for r being Real st y in Ball x,r holds
y in cl_Ball x,r
proof end;

theorem Th51: :: CLVECT_2:51  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Sphere x,r iff ||.(x - w).|| = r )
proof end;

theorem :: CLVECT_2:52  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for w, x being Point of X
for r being Real holds
( w in Sphere x,r iff dist x,w = r )
proof end;

theorem :: CLVECT_2:53  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for y, x being Point of X
for r being Real st y in Sphere x,r holds
y in cl_Ball x,r
proof end;

theorem Th54: :: CLVECT_2:54  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Ball x,r c= cl_Ball x,r
proof end;

theorem Th55: :: CLVECT_2:55  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds Sphere x,r c= cl_Ball x,r
proof end;

theorem :: CLVECT_2:56  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for r being Real holds (Ball x,r) \/ (Sphere x,r) = cl_Ball x,r
proof end;

deffunc H2( ComplexUnitarySpace) -> Element of the carrier of $1 = 0. $1;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attr seq is Cauchy means :Def8: :: CLVECT_2:def 8
for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (seq . n),(seq . m) < r;
end;

:: deftheorem Def8 defines Cauchy CLVECT_2:def 8 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
dist (seq . n),(seq . m) < r );

theorem :: CLVECT_2:57  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is Cauchy
proof end;

theorem :: CLVECT_2:58  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is Cauchy iff for r being Real st r > 0 holds
ex k being Nat st
for n, m being Nat st n >= k & m >= k holds
||.((seq . n) - (seq . m)).|| < r )
proof end;

theorem :: CLVECT_2:59  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 + seq2 is Cauchy
proof end;

theorem :: CLVECT_2:60  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq2 is Cauchy holds
seq1 - seq2 is Cauchy
proof end;

theorem Th61: :: CLVECT_2:61  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is Cauchy holds
z * seq is Cauchy
proof end;

theorem :: CLVECT_2:62  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is Cauchy holds
- seq is Cauchy
proof end;

theorem Th63: :: CLVECT_2:63  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq + x is Cauchy
proof end;

theorem :: CLVECT_2:64  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for x being Point of X
for seq being sequence of X st seq is Cauchy holds
seq - x is Cauchy
proof end;

theorem :: CLVECT_2:65  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is Cauchy
proof end;

definition
let X be ComplexUnitarySpace;
let seq1, seq2 be sequence of X;
pred seq1 is_compared_to seq2 means :Def9: :: CLVECT_2:def 9
for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq1 . n),(seq2 . n) < r;
end;

:: deftheorem Def9 defines is_compared_to CLVECT_2:def 9 :
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
dist (seq1 . n),(seq2 . n) < r );

theorem Th66: :: CLVECT_2:66  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X holds seq is_compared_to seq
proof end;

theorem Th67: :: CLVECT_2:67  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1
proof end;

definition
let X be ComplexUnitarySpace;
let seq1, seq2 be sequence of X;
:: original: is_compared_to
redefine pred seq1 is_compared_to seq2;
reflexivity
for seq1 being sequence of X holds seq1 is_compared_to seq1
by Th66;
symmetry
for seq1, seq2 being sequence of X st seq1 is_compared_to seq2 holds
seq2 is_compared_to seq1
by Th67;
end;

theorem :: CLVECT_2:68  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X st seq1 is_compared_to seq2 & seq2 is_compared_to seq3 holds
seq1 is_compared_to seq3
proof end;

theorem :: CLVECT_2:69  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X holds
( seq1 is_compared_to seq2 iff for r being Real st r > 0 holds
ex m being Nat st
for n being Nat st n >= m holds
||.((seq1 . n) - (seq2 . n)).|| < r )
proof end;

theorem :: CLVECT_2:70  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st ex k being Nat st
for n being Nat st n >= k holds
seq1 . n = seq2 . n holds
seq1 is_compared_to seq2
proof end;

theorem :: CLVECT_2:71  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is Cauchy & seq1 is_compared_to seq2 holds
seq2 is Cauchy
proof end;

theorem :: CLVECT_2:72  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is convergent & seq1 is_compared_to seq2 holds
seq2 is convergent
proof end;

theorem :: CLVECT_2:73  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for g being Point of X
for seq1, seq2 being sequence of X st seq1 is convergent & lim seq1 = g & seq1 is_compared_to seq2 holds
( seq2 is convergent & lim seq2 = g )
proof end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
attr seq is bounded means :Def10: :: CLVECT_2:def 10
ex M being Real st
( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) );
end;

:: deftheorem Def10 defines bounded CLVECT_2:def 10 :
for X being ComplexUnitarySpace
for seq being sequence of X holds
( seq is bounded iff ex M being Real st
( M > 0 & ( for n being Nat holds ||.(seq . n).|| <= M ) ) );

theorem Th74: :: CLVECT_2:74  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 + seq2 is bounded
proof end;

theorem Th75: :: CLVECT_2:75  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is bounded holds
- seq is bounded
proof end;

theorem :: CLVECT_2:76  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq2 is bounded holds
seq1 - seq2 is bounded
proof end;

theorem :: CLVECT_2:77  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X st seq is bounded holds
z * seq is bounded
proof end;

theorem :: CLVECT_2:78  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is constant holds
seq is bounded
proof end;

theorem Th79: :: CLVECT_2:79  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for m being Nat ex M being Real st
( M > 0 & ( for n being Nat st n <= m holds
||.(seq . n).|| < M ) )
proof end;

theorem Th80: :: CLVECT_2:80  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st seq is convergent holds
seq is bounded
proof end;

theorem :: CLVECT_2:81  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X st seq1 is bounded & seq1 is_compared_to seq2 holds
seq2 is bounded
proof end;

definition
let X be ComplexUnitarySpace;
let Nseq be increasing Seq_of_Nat;
let seq be sequence of X;
:: original: *
redefine func seq * Nseq -> sequence of X;
coherence
Nseq * seq is sequence of X
proof end;
end;

theorem Th82: :: CLVECT_2:82  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for s being sequence of X
for N being increasing Seq_of_Nat
for n being Nat holds (s * N) . n = s . (N . n)
proof end;

theorem :: CLVECT_2:83  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X holds seq is subsequence of seq
proof end;

theorem :: CLVECT_2:84  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2, seq3 being sequence of X st seq1 is subsequence of seq2 & seq2 is subsequence of seq3 holds
seq1 is subsequence of seq3
proof end;

theorem Th85: :: CLVECT_2:85  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is constant & seq1 is subsequence of seq holds
seq1 is constant
proof end;

theorem :: CLVECT_2:86  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is constant & seq1 is subsequence of seq holds
seq = seq1
proof end;

theorem Th87: :: CLVECT_2:87  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is bounded & seq1 is subsequence of seq holds
seq1 is bounded
proof end;

theorem Th88: :: CLVECT_2:88  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & seq1 is subsequence of seq holds
seq1 is convergent
proof end;

theorem Th89: :: CLVECT_2:89  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq being sequence of X st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq
proof end;

theorem Th90: :: CLVECT_2:90  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & seq1 is subsequence of seq holds
seq1 is Cauchy
proof end;

definition
let X be ComplexUnitarySpace;
let seq be sequence of X;
let k be Nat;
func seq ^\ k -> sequence of X means :Def11: :: CLVECT_2:def 11
for n being Nat holds it . n = seq . (n + k);
existence
ex b1 being sequence of X st
for n being Nat holds b1 . n = seq . (n + k)
proof end;
uniqueness
for b1, b2 being sequence of X st ( for n being Nat holds b1 . n = seq . (n + k) ) & ( for n being Nat holds b2 . n = seq . (n + k) ) holds
b1 = b2
proof end;
end;

:: deftheorem Def11 defines ^\ CLVECT_2:def 11 :
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat
for b4 being sequence of X holds
( b4 = seq ^\ k iff for n being Nat holds b4 . n = seq . (n + k) );

theorem :: CLVECT_2:91  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X holds seq ^\ 0 = seq
proof end;

theorem :: CLVECT_2:92  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = (seq ^\ m) ^\ k
proof end;

theorem :: CLVECT_2:93  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k, m being Nat holds (seq ^\ k) ^\ m = seq ^\ (k + m)
proof end;

theorem Th94: :: CLVECT_2:94  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat holds (seq1 + seq2) ^\ k = (seq1 ^\ k) + (seq2 ^\ k)
proof end;

theorem Th95: :: CLVECT_2:95  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat holds (- seq) ^\ k = - (seq ^\ k)
proof end;

theorem :: CLVECT_2:96  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat holds (seq1 - seq2) ^\ k = (seq1 ^\ k) - (seq2 ^\ k)
proof end;

theorem :: CLVECT_2:97  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for z being Complex
for seq being sequence of X
for k being Nat holds (z * seq) ^\ k = z * (seq ^\ k)
proof end;

theorem :: CLVECT_2:98  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat
for Nseq being increasing Seq_of_Nat holds (seq * Nseq) ^\ k = seq * (Nseq ^\ k)
proof end;

theorem Th99: :: CLVECT_2:99  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat holds seq ^\ k is subsequence of seq
proof end;

theorem :: CLVECT_2:100  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq )
proof end;

theorem :: CLVECT_2:101  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent
proof end;

theorem :: CLVECT_2:102  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq, seq1 being sequence of X st seq is Cauchy & ex k being Nat st seq = seq1 ^\ k holds
seq1 is Cauchy
proof end;

theorem :: CLVECT_2:103  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is Cauchy holds
seq ^\ k is Cauchy
proof end;

theorem :: CLVECT_2:104  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq1, seq2 being sequence of X
for k being Nat st seq1 is_compared_to seq2 holds
seq1 ^\ k is_compared_to seq2 ^\ k
proof end;

theorem :: CLVECT_2:105  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is bounded holds
seq ^\ k is bounded
proof end;

theorem :: CLVECT_2:106  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X
for k being Nat st seq is constant holds
seq ^\ k is constant
proof end;

definition
let X be ComplexUnitarySpace;
attr X is complete means :Def12: :: CLVECT_2:def 12
for seq being sequence of X st seq is Cauchy holds
seq is convergent;
end;

:: deftheorem Def12 defines complete CLVECT_2:def 12 :
for X being ComplexUnitarySpace holds
( X is complete iff for seq being sequence of X st seq is Cauchy holds
seq is convergent );

theorem :: CLVECT_2:107  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for X being ComplexUnitarySpace
for seq being sequence of X st X is complete & seq is Cauchy holds
seq is bounded
proof end;

definition
let X be ComplexUnitarySpace;
attr X is Hilbert means :: CLVECT_2:def 13
( X is ComplexUnitarySpace & X is complete );
end;

:: deftheorem defines Hilbert CLVECT_2:def 13 :
for X being ComplexUnitarySpace holds
( X is Hilbert iff ( X is ComplexUnitarySpace & X is complete ) );