:: SEQ_4 semantic presentation

Lemma1: for b₁, b₂, b₃ being real number st 0 < b₁ & b₁ <= b₂ & 0 <= b₃ holds
b₃ / b₂ <= b₃ / b₁
by XREAL_1:120;

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

Lemma3: 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:99;

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:68;

theorem Th1: :: SEQ_4:1

canceled;

theorem Th2: :: SEQ_4:2

canceled;

theorem Th3: :: SEQ_4:3

canceled;

theorem Th4: :: SEQ_4:4

canceled;

theorem Th5: :: SEQ_4:5

canceled;

theorem Th6: :: SEQ_4:6

canceled;

theorem Th7: :: SEQ_4:7

canceled;

theorem Th8: :: SEQ_4:8

for b₁, b₂ being Subset of REAL st ( for b₃, b₄ being real number st b₃ in b₁ & b₄ in b₂ holds
b₃ < b₄ ) holds
ex b₃ being real number st
for b₄, b₅ being real number st b₄ in b₁ & b₅ in b₂ holds
( b₄ <= b₃ & b₃ <= b₅ )

proof end;

theorem Th9: :: SEQ_4:9

for b₁ being real number
for b₂ being Subset of REAL st 0 < b₁ & ex b₃ being real number st b₃ in b₂ & ( for b₃ being real number st b₃ in b₂ holds
b₃ + b₁ in b₂ ) holds
for b₃ being real number ex b₄ being real number st
( b₄ in b₂ & b₃ < b₄ )

proof end;

theorem Th10: :: SEQ_4:10

for b₁ being real number ex b₂ being Nat st b₁ < b₂

proof end;

definition

let c₁ be real-membered set ;
attr a₁ is bounded_above means :Def1: :: SEQ_4:def 1
ex b₁ being real number st
for b₂ being real number st b₂ in a₁ holds
b₂ <= b₁;
attr a₁ is bounded_below means :Def2: :: SEQ_4:def 2
ex b₁ being real number st
for b₂ being real number st b₂ in a₁ holds
b₁ <= b₂;

end;

:: deftheorem Def1 defines bounded_above SEQ_4:def 1 :

:: deftheorem Def2 defines bounded_below SEQ_4:def 2 :

definition

let c₁ be Subset of REAL ;
attr a₁ is bounded means :Def3: :: SEQ_4:def 3
( a₁ is bounded_below & a₁ is bounded_above );

end;

:: deftheorem Def3 defines bounded SEQ_4:def 3 :

theorem Th11: :: SEQ_4:11

canceled;

theorem Th12: :: SEQ_4:12

canceled;

theorem Th13: :: SEQ_4:13

canceled;

theorem Th14: :: SEQ_4:14

for b₁ being Subset of REAL holds
( b₁ is bounded iff ex b₂ being real number st
( 0 < b₂ & ( for b₃ being real number st b₃ in b₁ holds
abs b₃ < b₂ ) ) )

proof end;

definition

let c₁ be real number ;
redefine func { as {c₁} -> Subset of REAL ;
coherence

proof end;

end;

theorem Th15: :: SEQ_4:15

for b₁ being real number holds {b₁} is bounded

proof end;

theorem Th16: :: SEQ_4:16

for b₁ being real-membered set st not b₁ is empty & b₁ is bounded_above holds
ex b₂ being real number st
( ( for b₃ being real number st b₃ in b₁ holds
b₃ <= b₂ ) & ( for b₃ being real number st 0 < b₃ holds
ex b₄ being real number st
( b₄ in b₁ & b₂ - b₃ < b₄ ) ) )

proof end;

theorem Th17: :: SEQ_4:17

for b₁, b₂ being real number
for b₃ being real-membered set st ( for b₄ being real number st b₄ in b₃ holds
b₄ <= b₁ ) & ( for b₄ being real number st 0 < b₄ holds
ex b₅ being real number st
( b₅ in b₃ & b₁ - b₄ < b₅ ) ) & ( for b₄ being real number st b₄ in b₃ holds
b₄ <= b₂ ) & ( for b₄ being real number st 0 < b₄ holds
ex b₅ being real number st
( b₅ in b₃ & b₂ - b₄ < b₅ ) ) holds
b₁ = b₂

proof end;

theorem Th18: :: SEQ_4:18

for b₁ being real-membered set st not b₁ is empty & b₁ is bounded_below holds
ex b₂ being real number st
( ( for b₃ being real number st b₃ in b₁ holds
b₂ <= b₃ ) & ( for b₃ being real number st 0 < b₃ holds
ex b₄ being real number st
( b₄ in b₁ & b₄ < b₂ + b₃ ) ) )

proof end;

theorem Th19: :: SEQ_4:19

for b₁, b₂ being real number
for b₃ being real-membered set st ( for b₄ being real number st b₄ in b₃ holds
b₁ <= b₄ ) & ( for b₄ being real number st 0 < b₄ holds
ex b₅ being real number st
( b₅ in b₃ & b₅ < b₁ + b₄ ) ) & ( for b₄ being real number st b₄ in b₃ holds
b₂ <= b₄ ) & ( for b₄ being real number st 0 < b₄ holds
ex b₅ being real number st
( b₅ in b₃ & b₅ < b₂ + b₄ ) ) holds
b₁ = b₂

proof end;

definition

let c₁ be real-membered set ;
assume E17: ( not c₁ is empty & c₁ is bounded_above ) ;
func upper_bound c₁ -> real number means :Def4: :: SEQ_4:def 4
( ( for b₁ being real number st b₁ in a₁ holds
b₁ <= a₂ ) & ( for b₁ being real number st 0 < b₁ holds
ex b₂ being real number st
( b₂ in a₁ & a₂ - b₁ < b₂ ) ) );
existence by E17, Th16;
uniqueness by Th17;

end;

:: deftheorem Def4 defines upper_bound SEQ_4:def 4 :

definition

let c₁ be real-membered set ;
assume E18: ( not c₁ is empty & c₁ is bounded_below ) ;
func lower_bound c₁ -> real number means :Def5: :: SEQ_4:def 5
( ( for b₁ being real number st b₁ in a₁ holds
a₂ <= b₁ ) & ( for b₁ being real number st 0 < b₁ holds
ex b₂ being real number st
( b₂ in a₁ & b₂ < a₂ + b₁ ) ) );
existence by E18, Th18;
uniqueness by Th19;

end;

:: deftheorem Def5 defines lower_bound SEQ_4:def 5 :

definition

let c₁ be Subset of REAL ;
redefine func upper_bound as upper_bound c₁ -> Real;
coherence by XREAL_0:def 1;
redefine func lower_bound as lower_bound c₁ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th20: :: SEQ_4:20

canceled;

theorem Th21: :: SEQ_4:21

canceled;

theorem Th22: :: SEQ_4:22

for b₁ being real number holds
( lower_bound {b₁} = b₁ & upper_bound {b₁} = b₁ )

proof end;

theorem Th23: :: SEQ_4:23

for b₁ being real number holds lower_bound {b₁} = upper_bound {b₁}

proof end;

theorem Th24: :: SEQ_4:24

for b₁ being Subset of REAL st b₁ is bounded & not b₁ is empty holds
lower_bound b₁ <= upper_bound b₁

proof end;

theorem Th25: :: SEQ_4:25

for b₁ being Subset of REAL st b₁ is bounded & not b₁ is empty holds
( ex b₂, b₃ being real number st
( b₂ in b₁ & b₃ in b₁ & b₃ <> b₂ ) iff lower_bound b₁ < upper_bound b₁ )

proof end;

theorem Th26: :: SEQ_4:26

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

proof end;

theorem Th27: :: SEQ_4:27

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

proof end;

theorem Th28: :: SEQ_4:28

for b₁ being Real_Sequence st abs b₁ is convergent & lim (abs b₁) = 0 holds
( b₁ is convergent & lim b₁ = 0 )

proof end;

theorem Th29: :: SEQ_4:29

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

proof end;

theorem Th30: :: SEQ_4:30

for b₁, b₂ being Real_Sequence st b₁ is subsequence of b₂ & b₂ is convergent holds
lim b₁ = lim b₂

proof end;

theorem Th31: :: SEQ_4:31

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

proof end;

theorem Th32: :: SEQ_4:32

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

proof end;

theorem Th33: :: SEQ_4:33

for b₁ being Nat
for b₂ being Real_Sequence st b₂ is convergent holds
( b₂ ^\ b₁ is convergent & lim (b₂ ^\ b₁) = lim b₂ )

proof end;

theorem Th34: :: SEQ_4:34

canceled;

theorem Th35: :: SEQ_4:35

for b₁, b₂ being Real_Sequence st b₁ is convergent & ex b₃ being Nat st b₁ = b₂ ^\ b₃ holds
b₂ is convergent

proof end;

theorem Th36: :: SEQ_4:36

for b₁, b₂ being Real_Sequence st b₁ is convergent & ex b₃ being Nat st b₁ = b₂ ^\ b₃ holds
lim b₂ = lim b₁

proof end;

theorem Th37: :: SEQ_4:37

for b₁ being Real_Sequence st b₁ is convergent & lim b₁ <> 0 holds
ex b₂ being Nat st b₁ ^\ b₂ is_not_0

proof end;

theorem Th38: :: SEQ_4:38

for b₁ being Real_Sequence st b₁ is convergent & lim b₁ <> 0 holds
ex b₂ being Real_Sequence st
( b₂ is subsequence of b₁ & b₂ is_not_0 )

proof end;

theorem Th39: :: SEQ_4:39

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

proof end;

registration

cluster constant -> convergent M5( NAT , REAL );
coherence by Th39;

end;

theorem Th40: :: SEQ_4:40

for b₁ being real number
for b₂ being Real_Sequence st ( ( b₂ is constant & b₁ in rng b₂ ) or ( b₂ is constant & ex b₃ being Nat st b₂ . b₃ = b₁ ) ) holds
lim b₂ = b₁

proof end;

theorem Th41: :: SEQ_4:41

for b₁ being Real_Sequence st b₁ is constant holds
for b₂ being Nat holds lim b₁ = b₁ . b₂ by Th40;

theorem Th42: :: SEQ_4:42

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

proof end;

theorem Th43: :: SEQ_4:43

for b₁ being real number
for b₂ being Real_Sequence st 0 < b₁ & ( for b₃ being Nat holds b₂ . b₃ = 1 / (b₃ + b₁) ) holds
b₂ is convergent

proof end;

theorem Th44: :: SEQ_4:44

for b₁ being real number
for b₂ being Real_Sequence st 0 < b₁ & ( for b₃ being Nat holds b₂ . b₃ = 1 / (b₃ + b₁) ) holds
lim b₂ = 0

proof end;

theorem Th45: :: SEQ_4:45

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 1 / (b₂ + 1) ) holds
( b₁ is convergent & lim b₁ = 0 ) by Th43, Th44;

theorem Th46: :: SEQ_4:46

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

proof end;

theorem Th47: :: SEQ_4:47

for b₁ being real number
for b₂ being Real_Sequence st 0 < b₁ & ( for b₃ being Nat holds b₂ . b₃ = 1 / ((b₃ * b₃) + b₁) ) holds
b₂ is convergent

proof end;

theorem Th48: :: SEQ_4:48

for b₁ being real number
for b₂ being Real_Sequence st 0 < b₁ & ( for b₃ being Nat holds b₂ . b₃ = 1 / ((b₃ * b₃) + b₁) ) holds
lim b₂ = 0

proof end;

theorem Th49: :: SEQ_4:49

for b₁ being Real_Sequence st ( for b₂ being Nat holds b₁ . b₂ = 1 / ((b₂ * b₂) + 1) ) holds
( b₁ is convergent & lim b₁ = 0 ) by Th47, Th48;

theorem Th50: :: SEQ_4:50

for b₁, b₂ being real number
for b₃ being Real_Sequence st 0 < b₁ & ( for b₄ being Nat holds b₃ . b₄ = b₂ / ((b₄ * b₄) + b₁) ) holds
( b₃ is convergent & lim b₃ = 0 )

proof end;

theorem Th51: :: SEQ_4:51

for b₁ being Real_Sequence st b₁ is non-decreasing & b₁ is bounded_above holds
b₁ is convergent

proof end;

theorem Th52: :: SEQ_4:52

for b₁ being Real_Sequence st b₁ is non-increasing & b₁ is bounded_below holds
b₁ is convergent

proof end;

theorem Th53: :: SEQ_4:53

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

proof end;

theorem Th54: :: SEQ_4:54

for b₁ being Real_Sequence st b₁ is bounded_above & b₁ is non-decreasing holds
for b₂ being Nat holds b₁ . b₂ <= lim b₁

proof end;

theorem Th55: :: SEQ_4:55

for b₁ being Real_Sequence st b₁ is bounded_below & b₁ is non-increasing holds
for b₂ being Nat holds lim b₁ <= b₁ . b₂

proof end;

theorem Th56: :: SEQ_4:56

for b₁ being Real_Sequence ex b₂ being increasing Seq_of_Nat st b₁ * b₂ is monotone

proof end;

theorem Th57: :: SEQ_4:57

for b₁ being Real_Sequence st b₁ is bounded holds
ex b₂ being Real_Sequence st
( b₂ is subsequence of b₁ & b₂ is convergent )

proof end;

theorem Th58: :: SEQ_4:58

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

proof end;

theorem Th59: :: SEQ_4:59

for b₁, b₂ being Real_Sequence st b₁ is constant & b₂ is convergent holds
( lim (b₁ + b₂) = (b₁ . 0) + (lim b₂) & lim (b₁ - b₂) = (b₁ . 0) - (lim b₂) & lim (b₂ - b₁) = (lim b₂) - (b₁ . 0) & lim (b₁ (#) b₂) = (b₁ . 0) * (lim b₂) )

proof end;

theorem Th60: :: SEQ_4:60

for b₁ being non empty real-membered set
for b₂ being real number st ( for b₃ being real number st b₃ in b₁ holds
b₃ >= b₂ ) holds
lower_bound b₁ >= b₂

proof end;

theorem Th61: :: SEQ_4:61

for b₁ being real number
for b₂ being non empty real-membered set st ( for b₃ being real number st b₃ in b₂ holds
b₃ >= b₁ ) & ( for b₃ being real number st ( for b₄ being real number st b₄ in b₂ holds
b₄ >= b₃ ) holds
b₁ >= b₃ ) holds
b₁ = lower_bound b₂

proof end;

theorem Th62: :: SEQ_4:62

for b₁ being non empty real-membered set
for b₂, b₃ being real number st ( for b₄ being real number st b₄ in b₁ holds
b₄ <= b₃ ) holds
upper_bound b₁ <= b₃

proof end;

theorem Th63: :: SEQ_4:63

for b₁ being non empty real-membered set
for b₂ being real number st ( for b₃ being real number st b₃ in b₁ holds
b₃ <= b₂ ) & ( for b₃ being real number st ( for b₄ being real number st b₄ in b₁ holds
b₄ <= b₃ ) holds
b₂ <= b₃ ) holds
b₂ = upper_bound b₁

proof end;

theorem Th64: :: SEQ_4:64

for b₁ being non empty real-membered set
for b₂ being real-membered set st b₁ c= b₂ & b₂ is bounded_below holds
lower_bound b₂ <= lower_bound b₁

proof end;

theorem Th65: :: SEQ_4:65

for b₁ being non empty real-membered set
for b₂ being real-membered set st b₁ c= b₂ & b₂ is bounded_above holds
upper_bound b₁ <= upper_bound b₂

proof end;