:: SEQ_4 semantic presentation

Lm1: for r1, r, g being real number st 0 < r1 & r1 <= r & 0 <= g holds
g / r <= g / r1
by XREAL_1:120;

Lm2: for s being real number st 0 < s holds
0 < s / 3
by XREAL_1:224;

Lm3: for g, r, g1, r1 being real number st 0 < g & 0 <= r & g <= g1 & r < r1 holds
g * r < g1 * r1
by XREAL_1:99;

Lm4: for g, r, g1, r1 being real number st 0 <= g & 0 <= r & g <= g1 & r <= r1 holds
g * r <= g1 * r1
by XREAL_1:68;

theorem :: SEQ_4:1

canceled;

theorem :: SEQ_4:2

canceled;

theorem :: SEQ_4:3

canceled;

theorem :: SEQ_4:4

canceled;

theorem :: SEQ_4:5

canceled;

theorem :: SEQ_4:6

canceled;

theorem :: SEQ_4:7

canceled;

theorem Th8: :: SEQ_4:8

for X, Y being Subset of REAL st ( for r, p being real number st r in X & p in Y holds
r < p ) holds
ex g being real number st
for r, p being real number st r in X & p in Y holds
( r <= g & g <= p )

proof end;

theorem Th9: :: SEQ_4:9

for p being real number
for X being Subset of REAL st 0 < p & ex r being real number st r in X & ( for r being real number st r in X holds
r + p in X ) holds
for g being real number ex r being real number st
( r in X & g < r )

proof end;

theorem Th10: :: SEQ_4:10

for r being real number ex n being Nat st r < n

proof end;

definition

let X be real-membered set ;
attr X is bounded_above means :Def1: :: SEQ_4:def 1
ex p being real number st
for r being real number st r in X holds
r <= p;
attr X is bounded_below means :Def2: :: SEQ_4:def 2
ex p being real number st
for r being real number st r in X holds
p <= r;

end;

:: deftheorem Def1 defines bounded_above SEQ_4:def 1 :

:: deftheorem Def2 defines bounded_below SEQ_4:def 2 :

definition

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

end;

:: deftheorem Def3 defines bounded SEQ_4:def 3 :

theorem :: SEQ_4:11

canceled;

theorem :: SEQ_4:12

canceled;

theorem :: SEQ_4:13

canceled;

theorem Th14: :: SEQ_4:14

for X being Subset of REAL holds
( X is bounded iff ex s being real number st
( 0 < s & ( for r being real number st r in X holds
abs r < s ) ) )

proof end;

definition

let r be real number ;
:: original: {
redefine func {r} -> Subset of REAL ;
coherence

proof end;

end;

theorem Th15: :: SEQ_4:15

for r being real number holds {r} is bounded

proof end;

theorem Th16: :: SEQ_4:16

for X being real-membered set st not X is empty & X is bounded_above holds
ex g being real number st
( ( for r being real number st r in X holds
r <= g ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g - s < r ) ) )

proof end;

theorem Th17: :: SEQ_4:17

for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
r <= g1 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g1 - s < r ) ) & ( for r being real number st r in X holds
r <= g2 ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & g2 - s < r ) ) holds
g1 = g2

proof end;

theorem Th18: :: SEQ_4:18

for X being real-membered set st not X is empty & X is bounded_below holds
ex g being real number st
( ( for r being real number st r in X holds
g <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g + s ) ) )

proof end;

theorem Th19: :: SEQ_4:19

for g1, g2 being real number
for X being real-membered set st ( for r being real number st r in X holds
g1 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g1 + s ) ) & ( for r being real number st r in X holds
g2 <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < g2 + s ) ) holds
g1 = g2

proof end;

definition

let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_above ) ;
func upper_bound X -> real number means :Def4: :: SEQ_4:def 4
( ( for r being real number st r in X holds
r <= it ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & it - s < r ) ) );
existence by A1, Th16;
uniqueness by Th17;

end;

:: deftheorem Def4 defines upper_bound SEQ_4:def 4 :

definition

let X be real-membered set ;
assume A1: ( not X is empty & X is bounded_below ) ;
func lower_bound X -> real number means :Def5: :: SEQ_4:def 5
( ( for r being real number st r in X holds
it <= r ) & ( for s being real number st 0 < s holds
ex r being real number st
( r in X & r < it + s ) ) );
existence by A1, Th18;
uniqueness by Th19;

end;

:: deftheorem Def5 defines lower_bound SEQ_4:def 5 :

definition

let X be Subset of REAL ;
:: original: upper_bound
redefine func upper_bound X -> Real;
coherence by XREAL_0:def 1;
:: original: lower_bound
redefine func lower_bound X -> Real;
coherence by XREAL_0:def 1;

end;

theorem :: SEQ_4:20

canceled;

theorem :: SEQ_4:21

canceled;

theorem Th22: :: SEQ_4:22

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

proof end;

theorem Th23: :: SEQ_4:23

for r being real number holds lower_bound {r} = upper_bound {r}

proof end;

theorem :: SEQ_4:24

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

proof end;

theorem :: SEQ_4:25

for X being Subset of REAL st X is bounded & not X is empty holds
( ex r, p being real number st
( r in X & p in X & p <> r ) iff lower_bound X < upper_bound X )

proof end;

theorem Th26: :: SEQ_4:26

for seq being Real_Sequence st seq is convergent holds
abs seq is convergent

proof end;

theorem :: SEQ_4:27

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

proof end;

theorem :: SEQ_4:28

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

proof end;

theorem Th29: :: SEQ_4:29

for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
seq1 is convergent

proof end;

theorem Th30: :: SEQ_4:30

for seq1, seq being Real_Sequence st seq1 is subsequence of seq & seq is convergent holds
lim seq1 = lim seq

proof end;

theorem Th31: :: SEQ_4:31

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
seq1 is convergent

proof end;

theorem :: SEQ_4:32

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st
for n being Nat st k <= n holds
seq1 . n = seq . n holds
lim seq = lim seq1

proof end;

theorem Th33: :: SEQ_4:33

for k being Nat
for seq being Real_Sequence st seq is convergent holds
( seq ^\ k is convergent & lim (seq ^\ k) = lim seq )

proof end;

theorem :: SEQ_4:34

canceled;

theorem Th35: :: SEQ_4:35

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
seq1 is convergent

proof end;

theorem :: SEQ_4:36

for seq, seq1 being Real_Sequence st seq is convergent & ex k being Nat st seq = seq1 ^\ k holds
lim seq1 = lim seq

proof end;

theorem Th37: :: SEQ_4:37

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex k being Nat st seq ^\ k is_not_0

proof end;

theorem :: SEQ_4:38

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is_not_0 )

proof end;

theorem Th39: :: SEQ_4:39

for seq being Real_Sequence st seq is constant holds
seq is convergent

proof end;

registration

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

end;

theorem Th40: :: SEQ_4:40

for r being real number
for seq being Real_Sequence st ( ( seq is constant & r in rng seq ) or ( seq is constant & ex n being Nat st seq . n = r ) ) holds
lim seq = r

proof end;

theorem :: SEQ_4:41

for seq being Real_Sequence st seq is constant holds
for n being Nat holds lim seq = seq . n by Th40;

theorem :: SEQ_4:42

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
for seq1 being Real_Sequence st seq1 is subsequence of seq & seq1 is_not_0 holds
lim (seq1 " ) = (lim seq) "

proof end;

theorem Th43: :: SEQ_4:43

for r being real number
for seq being Real_Sequence st 0 < r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds
seq is convergent

proof end;

theorem Th44: :: SEQ_4:44

for r being real number
for seq being Real_Sequence st 0 < r & ( for n being Nat holds seq . n = 1 / (n + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:45

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

theorem :: SEQ_4:46

for r, g being real number
for seq being Real_Sequence st 0 < r & ( for n being Nat holds seq . n = g / (n + r) ) holds
( seq is convergent & lim seq = 0 )

proof end;

theorem Th47: :: SEQ_4:47

for r being real number
for seq being Real_Sequence st 0 < r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
seq is convergent

proof end;

theorem Th48: :: SEQ_4:48

for r being real number
for seq being Real_Sequence st 0 < r & ( for n being Nat holds seq . n = 1 / ((n * n) + r) ) holds
lim seq = 0

proof end;

theorem :: SEQ_4:49

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

theorem :: SEQ_4:50

for r, g being real number
for seq being Real_Sequence st 0 < r & ( for n being Nat holds seq . n = g / ((n * n) + r) ) holds
( seq is convergent & lim seq = 0 )

proof end;

theorem Th51: :: SEQ_4:51

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

proof end;

theorem Th52: :: SEQ_4:52

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

proof end;

theorem Th53: :: SEQ_4:53

for seq being Real_Sequence st seq is monotone & seq is bounded holds
seq is convergent

proof end;

theorem :: SEQ_4:54

for seq being Real_Sequence st seq is bounded_above & seq is non-decreasing holds
for n being Nat holds seq . n <= lim seq

proof end;

theorem :: SEQ_4:55

for seq being Real_Sequence st seq is bounded_below & seq is non-increasing holds
for n being Nat holds lim seq <= seq . n

proof end;

theorem Th56: :: SEQ_4:56

for seq being Real_Sequence ex Nseq being increasing Seq_of_Nat st seq * Nseq is monotone

proof end;

theorem Th57: :: SEQ_4:57

for seq being Real_Sequence st seq is bounded holds
ex seq1 being Real_Sequence st
( seq1 is subsequence of seq & seq1 is convergent )

proof end;

theorem :: SEQ_4:58

for seq being Real_Sequence holds
( seq is convergent iff for s being real number st 0 < s holds
ex n being Nat st
for m being Nat st n <= m holds
abs ((seq . m) - (seq . n)) < s )

proof end;

theorem :: SEQ_4:59

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

proof end;

theorem Th60: :: SEQ_4:60

for X being non empty real-membered set
for t being real number st ( for s being real number st s in X holds
s >= t ) holds
lower_bound X >= t

proof end;

theorem :: SEQ_4:61

for r being real number
for X being non empty real-membered set st ( for s being real number st s in X holds
s >= r ) & ( for t being real number st ( for s being real number st s in X holds
s >= t ) holds
r >= t ) holds
r = lower_bound X

proof end;

theorem Th62: :: SEQ_4:62

for X being non empty real-membered set
for r, t being real number st ( for s being real number st s in X holds
s <= t ) holds
upper_bound X <= t

proof end;

theorem :: SEQ_4:63

for X being non empty real-membered set
for r being real number st ( for s being real number st s in X holds
s <= r ) & ( for t being real number st ( for s being real number st s in X holds
s <= t ) holds
r <= t ) holds
r = upper_bound X

proof end;

theorem :: SEQ_4:64

for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_below holds
lower_bound Y <= lower_bound X

proof end;

theorem :: SEQ_4:65

for X being non empty real-membered set
for Y being real-membered set st X c= Y & Y is bounded_above holds
upper_bound X <= upper_bound Y

proof end;