:: SEQ_2 semantic presentation

theorem Th1: :: SEQ_2:1

canceled;

theorem Th2: :: SEQ_2:2

canceled;

theorem Th3: :: SEQ_2:3

for b₁ being real number st 0 < b₁ holds
( 0 < b₁ / 2 & 0 < b₁ / 4 ) by XREAL_1:217, XREAL_1:226;

Lemma2: for b₁ being real number st 0 < b₁ holds
b₁ / 2 < b₁
by XREAL_1:218;

Lemma3: for b₁, b₂ being real number st 0 < b₁ & 0 < b₂ holds
0 < b₁ / b₂
by XREAL_1:141;

Lemma4: for b₁, b₂, b₃, b₄ being real number st 0 <= b₁ & 0 <= b₂ & b₁ < b₃ & b₂ < b₄ holds
b₁ * b₂ < b₃ * b₄
by XREAL_1:98;

theorem Th4: :: SEQ_2:4

canceled;

theorem Th5: :: SEQ_2:5

canceled;

theorem Th6: :: SEQ_2:6

canceled;

theorem Th7: :: SEQ_2:7

canceled;

theorem Th8: :: SEQ_2:8

canceled;

theorem Th9: :: SEQ_2:9

for b₁, b₂ being real number holds
( ( - b₁ < b₂ & b₂ < b₁ ) iff abs b₂ < b₁ )

proof end;

Lemma6: for b₁, b₂, b₃ being real number st 0 < b₁ & b₁ < b₂ & 0 < b₃ holds
b₃ / b₂ < b₃ / b₁
by XREAL_1:78;

theorem Th10: :: SEQ_2:10

canceled;

theorem Th11: :: SEQ_2:11

for b₁, b₂ being real number st b₁ <> 0 & b₂ <> 0 holds
abs ((b₁ " ) - (b₂ " )) = (abs (b₁ - b₂)) / ((abs b₁) * (abs b₂))

proof end;

definition

let c₁ be real-yielding Function;
attr a₁ is bounded_above means :: SEQ_2:def 1
ex b₁ being real number st
for b₂ being set st b₂ in dom a₁ holds
a₁ . b₂ < b₁;
attr a₁ is bounded_below means :: SEQ_2:def 2
ex b₁ being real number st
for b₂ being set st b₂ in dom a₁ holds
b₁ < a₁ . b₂;

end;

:: deftheorem Def1 defines bounded_above SEQ_2:def 1 :

:: deftheorem Def2 defines bounded_below SEQ_2:def 2 :

definition

let c₁ be Real_Sequence;
E8: dom c₁ = NAT by SEQ_1:3;
redefine attr a₁ is bounded_above means :Def3: :: SEQ_2:def 3
ex b₁ being real number st
for b₂ being Nat holds a₁ . b₂ < b₁;
compatibility

proof end;

redefine attr a₁ is bounded_below means :Def4: :: SEQ_2:def 4
ex b₁ being real number st
for b₂ being Nat holds b₁ < a₁ . b₂;
compatibility

proof end;

end;

:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :

:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :

definition

let c₁ be real-yielding Function;
attr a₁ is bounded means :Def5: :: SEQ_2:def 5
( a₁ is bounded_above & a₁ is bounded_below );

end;

:: deftheorem Def5 defines bounded SEQ_2:def 5 :

registration

cluster real-yielding bounded -> real-yielding bounded_above bounded_below set ;
coherence by Def5;
cluster real-yielding bounded_above bounded_below -> real-yielding bounded set ;
coherence by Def5;

end;

theorem Th12: :: SEQ_2:12

canceled;

theorem Th13: :: SEQ_2:13

canceled;

theorem Th14: :: SEQ_2:14

canceled;

theorem Th15: :: SEQ_2:15

for b₁ being Real_Sequence holds
( b₁ is bounded iff ex b₂ being real number st
( 0 < b₂ & ( for b₃ being Nat holds abs (b₁ . b₃) < b₂ ) ) )

proof end;

theorem Th16: :: SEQ_2:16

for b₁ being Real_Sequence
for b₂ being Nat ex b₃ being real number st
( 0 < b₃ & ( for b₄ being Nat st b₄ <= b₂ holds
abs (b₁ . b₄) < b₃ ) )

proof end;

definition

let c₁ be Real_Sequence;
attr a₁ is convergent means :Def6: :: SEQ_2:def 6
ex b₁ being real number st
for b₂ being real number st 0 < b₂ holds
ex b₃ being Nat st
for b₄ being Nat st b₃ <= b₄ holds
abs ((a₁ . b₄) - b₁) < b₂;

end;

:: deftheorem Def6 defines convergent SEQ_2:def 6 :

definition

let c₁ be Real_Sequence;
assume E14: c₁ is convergent ;
func lim c₁ -> real number means :Def7: :: SEQ_2:def 7
for b₁ being real number st 0 < b₁ holds
ex b₂ being Nat st
for b₃ being Nat st b₂ <= b₃ holds
abs ((a₁ . b₃) - a₂) < b₁;
existence by E14, Def6;
uniqueness

proof end;

end;

:: deftheorem Def7 defines lim SEQ_2:def 7 :

definition

let c₁ be Real_Sequence;
redefine func lim as lim c₁ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th17: :: SEQ_2:17

canceled;

theorem Th18: :: SEQ_2:18

canceled;

theorem Th19: :: SEQ_2:19

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

proof end;

theorem Th20: :: SEQ_2:20

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

proof end;

theorem Th21: :: SEQ_2:21

for b₁ being real number
for b₂ being Real_Sequence st b₂ is convergent holds
b₁ (#) b₂ is convergent

proof end;

theorem Th22: :: SEQ_2:22

for b₁ being real number
for b₂ being Real_Sequence st b₂ is convergent holds
lim (b₁ (#) b₂) = b₁ * (lim b₂)

proof end;

theorem Th23: :: SEQ_2:23

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

proof end;

theorem Th24: :: SEQ_2:24

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

proof end;

theorem Th25: :: SEQ_2:25

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

proof end;

theorem Th26: :: SEQ_2:26

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

proof end;

theorem Th27: :: SEQ_2:27

for b₁ being Real_Sequence st b₁ is convergent holds
b₁ is bounded

proof end;

theorem Th28: :: SEQ_2:28

for b₁, b₂ being Real_Sequence st b₁ is convergent & b₂ is convergent holds
b₁ (#) b₂ is convergent

proof end;

theorem Th29: :: SEQ_2:29

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

proof end;

theorem Th30: :: SEQ_2:30

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

proof end;

theorem Th31: :: SEQ_2:31

for b₁ being Real_Sequence st b₁ is convergent & ( for b₂ being Nat holds 0 <= b₁ . b₂ ) holds
0 <= lim b₁

proof end;

theorem Th32: :: SEQ_2:32

for b₁, b₂ being Real_Sequence st b₁ is convergent & b₂ is convergent & ( for b₃ being Nat holds b₁ . b₃ <= b₂ . b₃ ) holds
lim b₁ <= lim b₂

proof end;

theorem Th33: :: SEQ_2:33

for b₁, b₂, b₃ being Real_Sequence st b₁ is convergent & b₂ is convergent & ( for b₄ being Nat holds
( b₁ . b₄ <= b₃ . b₄ & b₃ . b₄ <= b₂ . b₄ ) ) & lim b₁ = lim b₂ holds
b₃ is convergent

proof end;

theorem Th34: :: SEQ_2:34

for b₁, b₂, b₃ being Real_Sequence st b₁ is convergent & b₂ is convergent & ( for b₄ being Nat holds
( b₁ . b₄ <= b₃ . b₄ & b₃ . b₄ <= b₂ . b₄ ) ) & lim b₁ = lim b₂ holds
lim b₃ = lim b₁

proof end;

theorem Th35: :: SEQ_2:35

for b₁ being Real_Sequence st b₁ is convergent & lim b₁ <> 0 & b₁ is_not_0 holds
b₁ " is convergent

proof end;

theorem Th36: :: SEQ_2:36

for b₁ being Real_Sequence st b₁ is convergent & lim b₁ <> 0 & b₁ is_not_0 holds
lim (b₁ " ) = (lim b₁) "

proof end;

theorem Th37: :: SEQ_2:37

for b₁, b₂ being Real_Sequence st b₁ is convergent & b₂ is convergent & lim b₂ <> 0 & b₂ is_not_0 holds
b₁ /" b₂ is convergent

proof end;

theorem Th38: :: SEQ_2:38

for b₁, b₂ being Real_Sequence st b₁ is convergent & b₂ is convergent & lim b₂ <> 0 & b₂ is_not_0 holds
lim (b₁ /" b₂) = (lim b₁) / (lim b₂)

proof end;

theorem Th39: :: SEQ_2:39

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

proof end;

theorem Th40: :: SEQ_2:40

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

proof end;