:: Conjugate Sequences, Bounded Complex Sequences and Convergent Complex Sequences
::
:: Copyright (c) 1996-2021 Association of Mizar Users

theorem Th1: :: COMSEQ_2:1
for r, g being Complex st g <> 0c & r <> 0c holds
|.((g ") - (r ")).| = |.(g - r).| / ()
proof end;

theorem Th2: :: COMSEQ_2:2
for s being Complex_Sequence
for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(s . m).| < r ) )
proof end;

definition
let f be complex-valued Function;
deffunc H1( object ) -> object = (f . $1) *' ; func f *' -> complex-valued Function means :Def1: :: COMSEQ_2:def 1 ( dom it = dom f & ( for c being set st c in dom it holds it . c = (f . c) *' ) ); existence ex b1 being complex-valued Function st ( dom b1 = dom f & ( for c being set st c in dom b1 holds b1 . c = (f . c) *' ) ) proof end; uniqueness for b1, b2 being complex-valued Function st dom b1 = dom f & ( for c being set st c in dom b1 holds b1 . c = (f . c) *' ) & dom b2 = dom f & ( for c being set st c in dom b2 holds b2 . c = (f . c) *' ) holds b1 = b2 proof end; involutiveness for b1, b2 being complex-valued Function st dom b1 = dom b2 & ( for c being set st c in dom b1 holds b1 . c = (b2 . c) *' ) holds ( dom b2 = dom b1 & ( for c being set st c in dom b2 holds b2 . c = (b1 . c) *' ) ) proof end; end; :: deftheorem Def1 defines *' COMSEQ_2:def 1 : for f, b2 being complex-valued Function holds ( b2 = f *' iff ( dom b2 = dom f & ( for c being set st c in dom b2 holds b2 . c = (f . c) *' ) ) ); definition let C be non empty set ; let f be Function of C,COMPLEX; :: original: *' redefine func f *' -> Function of C,COMPLEX means :Def2: :: COMSEQ_2:def 2 for n being Element of C holds it . n = (f . n) *' ; coherence f *' is Function of C,COMPLEX proof end; compatibility for b1 being Function of C,COMPLEX holds ( b1 = f *' iff for n being Element of C holds b1 . n = (f . n) *' ) proof end; end; :: deftheorem Def2 defines *' COMSEQ_2:def 2 : for C being non empty set for f, b3 being Function of C,COMPLEX holds ( b3 = f *' iff for n being Element of C holds b3 . n = (f . n) *' ); registration let C be non empty set ; let s be complex-valued ManySortedSet of C; coherence s *' is C -defined proof end; end; registration let C be non empty set ; let seq be complex-valued ManySortedSet of C; cluster seq *' -> C -defined total for C -defined Function; coherence for b1 being C -defined Function st b1 = seq *' holds b1 is total proof end; end; theorem :: COMSEQ_2:3 for s being Complex_Sequence st s is non-zero holds s *' is non-zero proof end; theorem :: COMSEQ_2:4 for r being Complex for s being Complex_Sequence holds (r (#) s) *' = (r *') (#) (s *') proof end; theorem :: COMSEQ_2:5 for s, s9 being Complex_Sequence holds (s (#) s9) *' = (s *') (#) (s9 *') proof end; theorem :: COMSEQ_2:6 for s being Complex_Sequence holds (s *') " = (s ") *' proof end; theorem :: COMSEQ_2:7 for s, s9 being Complex_Sequence holds (s9 /" s) *' = (s9 *') /" (s *') proof end; definition let f be complex-valued Function; :: SEQ_2:def 5 attr f is bounded means :: COMSEQ_2:def 3 ex r being Real st for y being set st y in dom f holds |.(f . y).| < r; end; :: deftheorem defines bounded COMSEQ_2:def 3 : for f being complex-valued Function holds ( f is bounded iff ex r being Real st for y being set st y in dom f holds |.(f . y).| < r ); definition let s be Complex_Sequence; redefine attr s is bounded means :: COMSEQ_2:def 4 ex r being Real st for n being Nat holds |.(s . n).| < r; compatibility ( s is bounded iff ex r being Real st for n being Nat holds |.(s . n).| < r ) proof end; end; :: deftheorem defines bounded COMSEQ_2:def 4 : for s being Complex_Sequence holds ( s is bounded iff ex r being Real st for n being Nat holds |.(s . n).| < r ); set sc = NAT --> 0c; registration existence ex b1 being Complex_Sequence st b1 is bounded proof end; end; theorem Th8: :: COMSEQ_2:8 for s being Complex_Sequence holds ( s is bounded iff ex r being Real st ( 0 < r & ( for n being Nat holds |.(s . n).| < r ) ) ) proof end; :: Convergent Complex Sequences :: The Limit of Complex Sequences definition let s be complex-valued ManySortedSet of NAT ; attr s is convergent means :Def5: :: COMSEQ_2:def 5 ex g being Complex st for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - g).| < p; end; :: deftheorem Def5 defines convergent COMSEQ_2:def 5 : for s being complex-valued ManySortedSet of NAT holds ( s is convergent iff ex g being Complex st for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - g).| < p ); definition let s be Complex_Sequence; assume A1: s is convergent ; func lim s -> Complex means :Def6: :: COMSEQ_2:def 6 for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - it).| < p; existence ex b1 being Complex st for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - b1).| < p by A1; uniqueness for b1, b2 being Complex st ( for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - b1).| < p ) & ( for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - b2).| < p ) holds b1 = b2 proof end; end; :: deftheorem Def6 defines lim COMSEQ_2:def 6 : for s being Complex_Sequence st s is convergent holds for b2 being Complex holds ( b2 = lim s iff for p being Real st 0 < p holds ex n being Nat st for m being Nat st n <= m holds |.((s . m) - b2).| < p ); theorem Th9: :: COMSEQ_2:9 for s being Complex_Sequence st ex g being Complex st for n being Nat holds s . n = g holds s is convergent proof end; theorem Th10: :: COMSEQ_2:10 for s being Complex_Sequence for g being Complex st ( for n being Nat holds s . n = g ) holds lim s = g proof end; registration existence ex b1 being Complex_Sequence st b1 is convergent proof end; end; registration let s be convergent Complex_Sequence; coherence for b1 being Complex_Sequence st b1 = s *' holds b1 is convergent proof end; end; theorem :: COMSEQ_2:11 canceled; ::$CT
theorem Th11: :: COMSEQ_2:12
for s being Complex_Sequence st s is convergent holds
lim (s *') = (lim s) *'
proof end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 + s2 -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 + s2 holds
b1 is convergent
proof end;
end;

theorem :: COMSEQ_2:13
canceled;

::$CT theorem Th12: :: COMSEQ_2:14 for s, s9 being convergent Complex_Sequence holds lim (s + s9) = (lim s) + (lim s9) proof end; theorem :: COMSEQ_2:15 canceled; ::$CT
theorem :: COMSEQ_2:16
for s, s9 being convergent Complex_Sequence holds lim ((s + s9) *') = ((lim s) *') + ((lim s9) *')
proof end;

registration
let s be convergent Complex_Sequence;
let c be Complex;
coherence
for b1 being Complex_Sequence st b1 = c (#) s holds
b1 is convergent
proof end;
end;

theorem :: COMSEQ_2:17
canceled;

::$CT theorem Th14: :: COMSEQ_2:18 for s being convergent Complex_Sequence for r being Complex holds lim (r (#) s) = r * (lim s) proof end; theorem :: COMSEQ_2:19 canceled; ::$CT
theorem :: COMSEQ_2:20
for r being Complex
for s being convergent Complex_Sequence holds lim ((r (#) s) *') = (r *') * ((lim s) *')
proof end;

registration
let s be convergent Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = - s holds
b1 is convergent
;
end;

theorem :: COMSEQ_2:21
canceled;

::$CT theorem Th16: :: COMSEQ_2:22 for s being convergent Complex_Sequence holds lim (- s) = - (lim s) proof end; theorem :: COMSEQ_2:23 canceled; ::$CT
theorem :: COMSEQ_2:24
for s being convergent Complex_Sequence holds lim ((- s) *') = - ((lim s) *')
proof end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 - s2 -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 - s2 holds
b1 is convergent
proof end;
end;

theorem :: COMSEQ_2:25
canceled;

::$CT theorem Th18: :: COMSEQ_2:26 for s, s9 being convergent Complex_Sequence holds lim (s - s9) = (lim s) - (lim s9) proof end; theorem :: COMSEQ_2:27 canceled; ::$CT
theorem :: COMSEQ_2:28
for s, s9 being convergent Complex_Sequence holds lim ((s - s9) *') = ((lim s) *') - ((lim s9) *')
proof end;

registration
coherence
for b1 being Complex_Sequence st b1 is convergent holds
b1 is bounded
proof end;
end;

registration
cluster Function-like V18( NAT , COMPLEX ) non bounded -> non convergent for Element of K19(K20(NAT,COMPLEX));
coherence
for b1 being Complex_Sequence st not b1 is bounded holds
not b1 is convergent
;
end;

registration
let s1, s2 be convergent Complex_Sequence;
cluster s1 (#) s2 -> convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = s1 (#) s2 holds
b1 is convergent
proof end;
end;

theorem :: COMSEQ_2:29
canceled;

::$CT theorem Th20: :: COMSEQ_2:30 for s, s9 being convergent Complex_Sequence holds lim (s (#) s9) = (lim s) * (lim s9) proof end; theorem :: COMSEQ_2:31 canceled; ::$CT
theorem :: COMSEQ_2:32
for s, s9 being convergent Complex_Sequence holds lim ((s (#) s9) *') = ((lim s) *') * ((lim s9) *')
proof end;

theorem Th22: :: COMSEQ_2:33
for s being convergent Complex_Sequence st lim s <> 0c holds
ex n being Nat st
for m being Nat st n <= m holds
|.(lim s).| / 2 < |.(s . m).|
proof end;

theorem Th23: :: COMSEQ_2:34
for s being convergent Complex_Sequence st lim s <> 0c & s is non-zero holds
s " is convergent
proof end;

theorem Th24: :: COMSEQ_2:35
for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds
lim (s ") = (lim s) "
proof end;

theorem :: COMSEQ_2:36
canceled;

::$CT theorem :: COMSEQ_2:37 for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds lim ((s ") *') = ((lim s) *') " proof end; theorem Th26: :: COMSEQ_2:38 for s, s9 being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds s9 /" s is convergent proof end; theorem Th27: :: COMSEQ_2:39 for s, s9 being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds lim (s9 /" s) = (lim s9) / (lim s) proof end; theorem :: COMSEQ_2:40 canceled; ::$CT
theorem :: COMSEQ_2:41
for s, s9 being Complex_Sequence st s9 is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim ((s9 /" s) *') = ((lim s9) *') / ((lim s) *')
proof end;

theorem Th29: :: COMSEQ_2:42
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
s (#) s1 is convergent
proof end;

theorem Th30: :: COMSEQ_2:43
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim (s (#) s1) = 0c
proof end;

theorem :: COMSEQ_2:44
canceled;

::\$CT
theorem :: COMSEQ_2:45
for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim ((s (#) s1) *') = 0c
proof end;