:: COMSEQ_2 semantic presentation

theorem Th1: :: COMSEQ_2:1

for g, r being Element of COMPLEX st g <> 0c & r <> 0c holds
|.((g " ) - (r " )).| = |.(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 C be non empty set ;
let f be PartFunc of C, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = (f /. $1) *' ;
func f *' -> PartFunc of C, COMPLEX means :Def1: :: COMSEQ_2:def 1
( dom it = dom f & ( for c being Element of C st c in dom it holds
it . c = (f /. c) *' ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def1 defines *' COMSEQ_2:def 1 :

definition

let C be non empty set ;
let f be Function of C, COMPLEX ;
redefine func f *' means :Def2: :: COMSEQ_2:def 2
( dom it = C & ( for n being Element of C holds it . n = (f . n) *' ) );
compatibility

proof end;

end;

:: deftheorem Def2 defines *' COMSEQ_2:def 2 :

registration

let C be non empty set ;
let seq be Function of C, COMPLEX ;
cluster seq *' -> total ;
coherence

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 Element of COMPLEX
for s being Complex_Sequence holds (r (#) s) *' = (r *' ) (#) (s *' )

proof end;

theorem :: COMSEQ_2:5

for s, s' being Complex_Sequence holds (s (#) s') *' = (s *' ) (#) (s' *' )

proof end;

theorem :: COMSEQ_2:6

for s being Complex_Sequence holds (s *' ) " = (s " ) *'

proof end;

theorem :: COMSEQ_2:7

for s', s being Complex_Sequence holds (s' /" s) *' = (s' *' ) /" (s *' )

proof end;

definition

let s be Complex_Sequence;
attr s is bounded means :Def3: :: COMSEQ_2:def 3
ex r being Real st
for n being Nat holds |.(s . n).| < r;

end;

:: deftheorem Def3 defines bounded COMSEQ_2:def 3 :

reconsider sc = NAT --> 0c as Complex_Sequence by FUNCOP_1:57;

Lm1: for n being Nat holds sc . n = 0c
by FUNCOP_1:13;

registration

cluster bounded Relation of NAT , COMPLEX ;
existence

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;

definition

let s be Complex_Sequence;
attr s is convergent means :Def4: :: COMSEQ_2:def 4
ex g being Element of 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 Def4 defines convergent COMSEQ_2:def 4 :

definition

let s be Complex_Sequence;
assume A1: s is convergent ;
func lim s -> Element of COMPLEX means :Def5: :: COMSEQ_2:def 5
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 by A1, Def4;
uniqueness

proof end;

end;

:: deftheorem Def5 defines lim COMSEQ_2:def 5 :

theorem Th9: :: COMSEQ_2:9

for s being Complex_Sequence st ex g being Element of 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 Element of COMPLEX st ( for n being Nat holds s . n = g ) holds
lim s = g

proof end;

registration

cluster convergent Relation of NAT , COMPLEX ;
existence

proof end;

end;

registration

let s be convergent Complex_Sequence;
cluster |.s.| -> convergent ;
coherence

proof end;

end;

theorem Th11: :: COMSEQ_2:11

for s being Complex_Sequence st s is convergent holds
lim |.s.| = |.(lim s).|

proof end;

registration

let s be convergent Complex_Sequence;
cluster s *' -> total convergent ;
coherence

proof end;

end;

theorem Th12: :: COMSEQ_2:12

for s being Complex_Sequence st s is convergent holds
lim (s *' ) = (lim s) *'

proof end;

theorem Th13: :: COMSEQ_2:13

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
s + s' is convergent

proof end;

theorem Th14: :: COMSEQ_2:14

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim (s + s') = (lim s) + (lim s')

proof end;

theorem :: COMSEQ_2:15

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim |.(s + s').| = |.((lim s) + (lim s')).|

proof end;

theorem :: COMSEQ_2:16

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim ((s + s') *' ) = ((lim s) *' ) + ((lim s') *' )

proof end;

theorem Th17: :: COMSEQ_2:17

for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
r (#) s is convergent

proof end;

theorem Th18: :: COMSEQ_2:18

for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
lim (r (#) s) = r * (lim s)

proof end;

theorem :: COMSEQ_2:19

for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
lim |.(r (#) s).| = |.r.| * |.(lim s).|

proof end;

theorem :: COMSEQ_2:20

for r being Element of COMPLEX
for s being Complex_Sequence st s is convergent holds
lim ((r (#) s) *' ) = (r *' ) * ((lim s) *' )

proof end;

theorem Th21: :: COMSEQ_2:21

for s being Complex_Sequence st s is convergent holds
- s is convergent

proof end;

theorem Th22: :: COMSEQ_2:22

for s being Complex_Sequence st s is convergent holds
lim (- s) = - (lim s)

proof end;

theorem :: COMSEQ_2:23

for s being Complex_Sequence st s is convergent holds
lim |.(- s).| = |.(lim s).|

proof end;

theorem :: COMSEQ_2:24

for s being Complex_Sequence st s is convergent holds
lim ((- s) *' ) = - ((lim s) *' )

proof end;

theorem Th25: :: COMSEQ_2:25

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
s - s' is convergent

proof end;

theorem Th26: :: COMSEQ_2:26

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim (s - s') = (lim s) - (lim s')

proof end;

theorem :: COMSEQ_2:27

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim |.(s - s').| = |.((lim s) - (lim s')).|

proof end;

theorem :: COMSEQ_2:28

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim ((s - s') *' ) = ((lim s) *' ) - ((lim s') *' )

proof end;

registration

cluster convergent -> bounded Relation of NAT , COMPLEX ;
coherence

proof end;

end;

registration

cluster non bounded -> non convergent Relation of NAT , COMPLEX ;
coherence

proof end;

end;

theorem Th29: :: COMSEQ_2:29

for s, s' being Complex_Sequence st s is convergent Complex_Sequence & s' is convergent Complex_Sequence holds
s (#) s' is convergent

proof end;

theorem Th30: :: COMSEQ_2:30

for s, s' being Complex_Sequence st s is convergent Complex_Sequence & s' is convergent Complex_Sequence holds
lim (s (#) s') = (lim s) * (lim s')

proof end;

theorem :: COMSEQ_2:31

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim |.(s (#) s').| = |.(lim s).| * |.(lim s').|

proof end;

theorem :: COMSEQ_2:32

for s, s' being Complex_Sequence st s is convergent & s' is convergent holds
lim ((s (#) s') *' ) = ((lim s) *' ) * ((lim s') *' )

proof end;

theorem Th33: :: COMSEQ_2:33

for s being Complex_Sequence st s is convergent & 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 Th34: :: COMSEQ_2:34

for s being Complex_Sequence st s is convergent & lim s <> 0c & s is non-zero holds
s " is convergent

proof end;

theorem Th35: :: 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

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: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 Th38: :: COMSEQ_2:38

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
s' /" s is convergent

proof end;

theorem Th39: :: COMSEQ_2:39

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim (s' /" s) = (lim s') / (lim s)

proof end;

theorem :: COMSEQ_2:40

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim |.(s' /" s).| = |.(lim s').| / |.(lim s).|

proof end;

theorem :: COMSEQ_2:41

for s', s being Complex_Sequence st s' is convergent & s is convergent & lim s <> 0c & s is non-zero holds
lim ((s' /" s) *' ) = ((lim s') *' ) / ((lim s) *' )

proof end;

theorem Th42: :: 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 Th43: :: 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

for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim |.(s (#) s1).| = 0

proof end;

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;