:: COMSEQ_2 semantic presentation

theorem Th1: :: COMSEQ_2:1

for b₁, b₂ being Element of COMPLEX st b₁ <> 0c & b₂ <> 0c holds
|.((b₁ " ) - (b₂ " )).| = |.(b₁ - b₂).| / (|.b₁.| * |.b₂.|)

proof end;

theorem Th2: :: COMSEQ_2:2

for b₁ being Complex_Sequence
for b₂ being Nat ex b₃ being Real st
( 0 < b₃ & ( for b₄ being Nat st b₄ <= b₂ holds
|.(b₁ . b₄).| < b₃ ) )

proof end;

definition

let c₁ be non empty set ;
let c₂ be PartFunc of c₁, COMPLEX ;
deffunc H₁( set ) -> Element of COMPLEX = (c₂ /. a₁) *' ;
func c₂ *' -> PartFunc of a₁, COMPLEX means :Def1: :: COMSEQ_2:def 1
( dom a₃ = dom a₂ & ( for b₁ being Element of a₁ st b₁ in dom a₃ holds
a₃ . b₁ = (a₂ /. b₁) *' ) );
existence

proof end;

uniqueness

proof end;

end;

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

definition

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
redefine func c₂ *' -> PartFunc of a₁, COMPLEX means :Def2: :: COMSEQ_2:def 2
( dom a₃ = a₁ & ( for b₁ being Element of a₁ holds a₃ . b₁ = (a₂ . b₁) *' ) );
compatibility

proof end;

end;

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

registration

let c₁ be non empty set ;
let c₂ be Function of c₁, COMPLEX ;
cluster a₂ *' -> total ;
coherence

proof end;

end;

theorem Th3: :: COMSEQ_2:3

for b₁ being Complex_Sequence st b₁ is non-zero holds
b₁ *' is non-zero

proof end;

theorem Th4: :: COMSEQ_2:4

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence holds (b₁ (#) b₂) *' = (b₁ *' ) (#) (b₂ *' )

proof end;

theorem Th5: :: COMSEQ_2:5

for b₁, b₂ being Complex_Sequence holds (b₁ (#) b₂) *' = (b₁ *' ) (#) (b₂ *' )

proof end;

theorem Th6: :: COMSEQ_2:6

for b₁ being Complex_Sequence holds (b₁ *' ) " = (b₁ " ) *'

proof end;

theorem Th7: :: COMSEQ_2:7

for b₁, b₂ being Complex_Sequence holds (b₁ /" b₂) *' = (b₁ *' ) /" (b₂ *' )

proof end;

definition

let c₁ be Complex_Sequence;
attr a₁ is bounded means :Def3: :: COMSEQ_2:def 3
ex b₁ being Real st
for b₂ being Nat holds |.(a₁ . b₂).| < b₁;

end;

:: deftheorem Def3 defines bounded COMSEQ_2:def 3 :

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

Lemma6: for b₁ being Nat holds c₁ . b₁ = 0c
by FUNCOP_1:13;

registration

cluster bounded Relation of NAT , COMPLEX ;
existence

proof end;

end;

theorem Th8: :: COMSEQ_2:8

for b₁ being Complex_Sequence holds
( b₁ is bounded iff ex b₂ being Real st
( 0 < b₂ & ( for b₃ being Nat holds |.(b₁ . b₃).| < b₂ ) ) )

proof end;

definition

let c₂ be Complex_Sequence;
attr a₁ is convergent means :Def4: :: COMSEQ_2:def 4
ex b₁ being Element of COMPLEX st
for b₂ being Real st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
|.((a₁ . b₄) - b₁).| < b₂;

end;

:: deftheorem Def4 defines convergent COMSEQ_2:def 4 :

definition

let c₂ be Complex_Sequence;
assume E9: c₂ is convergent ;
func lim c₁ -> Element of COMPLEX means :Def5: :: COMSEQ_2:def 5
for b₁ being Real st 0 < b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
|.((a₁ . b₃) - a₂).| < b₁;
existence by E9, Def4;
uniqueness

proof end;

end;

:: deftheorem Def5 defines lim COMSEQ_2:def 5 :

theorem Th9: :: COMSEQ_2:9

for b₁ being Complex_Sequence st ex b₂ being Element of COMPLEX st
for b₃ being Nat holds b₁ . b₃ = b₂ holds
b₁ is convergent

proof end;

theorem Th10: :: COMSEQ_2:10

for b₁ being Complex_Sequence
for b₂ being Element of COMPLEX st ( for b₃ being Nat holds b₁ . b₃ = b₂ ) holds
lim b₁ = b₂

proof end;

registration

cluster convergent Relation of NAT , COMPLEX ;
existence

proof end;

end;

registration

let c₂ be convergent Complex_Sequence;
cluster |.a₁.| -> convergent ;
coherence

proof end;

end;

theorem Th11: :: COMSEQ_2:11

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

proof end;

registration

let c₂ be convergent Complex_Sequence;
cluster a₁ *' -> total convergent ;
coherence

proof end;

end;

theorem Th12: :: COMSEQ_2:12

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

proof end;

theorem Th13: :: COMSEQ_2:13

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
b₁ + b₂ is convergent

proof end;

theorem Th14: :: COMSEQ_2:14

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
lim (b₁ + b₂) = (lim b₁) + (lim b₂)

proof end;

theorem Th15: :: COMSEQ_2:15

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
lim |.(b₁ + b₂).| = |.((lim b₁) + (lim b₂)).|

proof end;

theorem Th16: :: COMSEQ_2:16

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

proof end;

theorem Th17: :: COMSEQ_2:17

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence st b₂ is convergent holds
b₁ (#) b₂ is convergent

proof end;

theorem Th18: :: COMSEQ_2:18

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence st b₂ is convergent holds
lim (b₁ (#) b₂) = b₁ * (lim b₂)

proof end;

theorem Th19: :: COMSEQ_2:19

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence st b₂ is convergent holds
lim |.(b₁ (#) b₂).| = |.b₁.| * |.(lim b₂).|

proof end;

theorem Th20: :: COMSEQ_2:20

for b₁ being Element of COMPLEX
for b₂ being Complex_Sequence st b₂ is convergent holds
lim ((b₁ (#) b₂) *' ) = (b₁ *' ) * ((lim b₂) *' )

proof end;

theorem Th21: :: COMSEQ_2:21

for b₁ being Complex_Sequence st b₁ is convergent holds
- b₁ is convergent

proof end;

theorem Th22: :: COMSEQ_2:22

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

proof end;

theorem Th23: :: COMSEQ_2:23

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

proof end;

theorem Th24: :: COMSEQ_2:24

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

proof end;

theorem Th25: :: COMSEQ_2:25

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
b₁ - b₂ is convergent

proof end;

theorem Th26: :: COMSEQ_2:26

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
lim (b₁ - b₂) = (lim b₁) - (lim b₂)

proof end;

theorem Th27: :: COMSEQ_2:27

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
lim |.(b₁ - b₂).| = |.((lim b₁) - (lim b₂)).|

proof end;

theorem Th28: :: COMSEQ_2:28

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

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 b₁, b₂ being Complex_Sequence st b₁ is convergent Complex_Sequence & b₂ is convergent Complex_Sequence holds
b₁ (#) b₂ is convergent

proof end;

theorem Th30: :: COMSEQ_2:30

for b₁, b₂ being Complex_Sequence st b₁ is convergent Complex_Sequence & b₂ is convergent Complex_Sequence holds
lim (b₁ (#) b₂) = (lim b₁) * (lim b₂)

proof end;

theorem Th31: :: COMSEQ_2:31

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent holds
lim |.(b₁ (#) b₂).| = |.(lim b₁).| * |.(lim b₂).|

proof end;

theorem Th32: :: COMSEQ_2:32

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

proof end;

theorem Th33: :: COMSEQ_2:33

for b₁ being Complex_Sequence st b₁ is convergent & lim b₁ <> 0c holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
|.(lim b₁).| / 2 < |.(b₁ . b₃).|

proof end;

theorem Th34: :: COMSEQ_2:34

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

proof end;

theorem Th35: :: COMSEQ_2:35

for b₁ being Complex_Sequence st b₁ is convergent & lim b₁ <> 0c & b₁ is non-zero holds
lim (b₁ " ) = (lim b₁) "

proof end;

theorem Th36: :: COMSEQ_2:36

for b₁ being Complex_Sequence st b₁ is convergent & lim b₁ <> 0c & b₁ is non-zero holds
lim |.(b₁ " ).| = |.(lim b₁).| "

proof end;

theorem Th37: :: COMSEQ_2:37

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

proof end;

theorem Th38: :: COMSEQ_2:38

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is convergent & lim b₂ <> 0c & b₂ is non-zero holds
b₁ /" b₂ is convergent

proof end;

theorem Th39: :: COMSEQ_2:39

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

proof end;

theorem Th40: :: COMSEQ_2:40

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

proof end;

theorem Th41: :: COMSEQ_2:41

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

proof end;

theorem Th42: :: COMSEQ_2:42

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is bounded & lim b₁ = 0c holds
b₁ (#) b₂ is convergent

proof end;

theorem Th43: :: COMSEQ_2:43

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is bounded & lim b₁ = 0c holds
lim (b₁ (#) b₂) = 0c

proof end;

theorem Th44: :: COMSEQ_2:44

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is bounded & lim b₁ = 0c holds
lim |.(b₁ (#) b₂).| = 0

proof end;

theorem Th45: :: COMSEQ_2:45

for b₁, b₂ being Complex_Sequence st b₁ is convergent & b₂ is bounded & lim b₁ = 0c holds
lim ((b₁ (#) b₂) *' ) = 0c

proof end;