:: SEQ_2 semantic presentation

theorem :: SEQ_2:1

canceled;

theorem :: SEQ_2:2

canceled;

theorem Th3: :: SEQ_2:3

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

Lm1: for g being real number st 0 < g holds
g / 2 < g
by XREAL_1:218;

Lm2: for g, p being real number st 0 < g & 0 < p holds
0 < g / p
by XREAL_1:141;

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

theorem :: SEQ_2:4

canceled;

theorem :: SEQ_2:5

canceled;

theorem :: SEQ_2:6

canceled;

theorem :: SEQ_2:7

canceled;

theorem :: SEQ_2:8

canceled;

theorem Th9: :: SEQ_2:9

for g, r being real number holds
( ( - g < r & r < g ) iff abs r < g )

proof end;

Lm4: for r1, r, g being real number st 0 < r1 & r1 < r & 0 < g holds
g / r < g / r1
by XREAL_1:78;

theorem :: SEQ_2:10

canceled;

theorem Th11: :: SEQ_2:11

for g, r being real number st g <> 0 & r <> 0 holds
abs ((g " ) - (r " )) = (abs (g - r)) / ((abs g) * (abs r))

proof end;

definition

let f be real-yielding Function;
attr f is bounded_above means :: SEQ_2:def 1
ex r being real number st
for y being set st y in dom f holds
f . y < r;
attr f is bounded_below means :: SEQ_2:def 2
ex r being real number st
for y being set st y in dom f holds
r < f . y;

end;

:: deftheorem defines bounded_above SEQ_2:def 1 :

:: deftheorem defines bounded_below SEQ_2:def 2 :

definition

let seq be Real_Sequence;
A1: dom seq = NAT by SEQ_1:3;
redefine attr seq is bounded_above means :Def3: :: SEQ_2:def 3
ex r being real number st
for n being Nat holds seq . n < r;
compatibility

proof end;

redefine attr seq is bounded_below means :Def4: :: SEQ_2:def 4
ex r being real number st
for n being Nat holds r < seq . n;
compatibility

proof end;

end;

:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :

:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :

definition

let f be real-yielding Function;
attr f is bounded means :Def5: :: SEQ_2:def 5
( f is bounded_above & f 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 :: SEQ_2:12

canceled;

theorem :: SEQ_2:13

canceled;

theorem :: SEQ_2:14

canceled;

theorem Th15: :: SEQ_2:15

for seq being Real_Sequence holds
( seq is bounded iff ex r being real number st
( 0 < r & ( for n being Nat holds abs (seq . n) < r ) ) )

proof end;

theorem Th16: :: SEQ_2:16

for seq being Real_Sequence
for n being Nat ex r being real number st
( 0 < r & ( for m being Nat st m <= n holds
abs (seq . m) < r ) )

proof end;

definition

let seq be Real_Sequence;
attr seq is convergent means :Def6: :: SEQ_2:def 6
ex g being real number st
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
abs ((seq . m) - g) < p;

end;

:: deftheorem Def6 defines convergent SEQ_2:def 6 :

definition

let seq be Real_Sequence;
assume A1: seq is convergent ;
func lim seq -> real number means :Def7: :: SEQ_2:def 7
for p being real number st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
abs ((seq . m) - it) < p;
existence by A1, Def6;
uniqueness

proof end;

end;

:: deftheorem Def7 defines lim SEQ_2:def 7 :

definition

let seq be Real_Sequence;
:: original: lim
redefine func lim seq -> Real;
coherence by XREAL_0:def 1;

end;

theorem :: SEQ_2:17

canceled;

theorem :: SEQ_2:18

canceled;

theorem Th19: :: SEQ_2:19

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent holds
seq + seq' is convergent

proof end;

theorem Th20: :: SEQ_2:20

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent holds
lim (seq + seq') = (lim seq) + (lim seq')

proof end;

theorem Th21: :: SEQ_2:21

for r being real number
for seq being Real_Sequence st seq is convergent holds
r (#) seq is convergent

proof end;

theorem Th22: :: SEQ_2:22

for r being real number
for seq being Real_Sequence st seq is convergent holds
lim (r (#) seq) = r * (lim seq)

proof end;

theorem Th23: :: SEQ_2:23

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

proof end;

theorem Th24: :: SEQ_2:24

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

proof end;

theorem Th25: :: SEQ_2:25

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent holds
seq - seq' is convergent

proof end;

theorem Th26: :: SEQ_2:26

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent holds
lim (seq - seq') = (lim seq) - (lim seq')

proof end;

theorem Th27: :: SEQ_2:27

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

proof end;

theorem Th28: :: SEQ_2:28

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent holds
seq (#) seq' is convergent

proof end;

theorem Th29: :: SEQ_2:29

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent holds
lim (seq (#) seq') = (lim seq) * (lim seq')

proof end;

theorem Th30: :: SEQ_2:30

for seq being Real_Sequence st seq is convergent & lim seq <> 0 holds
ex n being Nat st
for m being Nat st n <= m holds
(abs (lim seq)) / 2 < abs (seq . m)

proof end;

theorem Th31: :: SEQ_2:31

for seq being Real_Sequence st seq is convergent & ( for n being Nat holds 0 <= seq . n ) holds
0 <= lim seq

proof end;

theorem :: SEQ_2:32

for seq, seq' being Real_Sequence st seq is convergent & seq' is convergent & ( for n being Nat holds seq . n <= seq' . n ) holds
lim seq <= lim seq'

proof end;

theorem Th33: :: SEQ_2:33

for seq, seq', seq1 being Real_Sequence st seq is convergent & seq' is convergent & ( for n being Nat holds
( seq . n <= seq1 . n & seq1 . n <= seq' . n ) ) & lim seq = lim seq' holds
seq1 is convergent

proof end;

theorem :: SEQ_2:34

for seq, seq', seq1 being Real_Sequence st seq is convergent & seq' is convergent & ( for n being Nat holds
( seq . n <= seq1 . n & seq1 . n <= seq' . n ) ) & lim seq = lim seq' holds
lim seq1 = lim seq

proof end;

theorem Th35: :: SEQ_2:35

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

proof end;

theorem Th36: :: SEQ_2:36

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

proof end;

theorem :: SEQ_2:37

for seq', seq being Real_Sequence st seq' is convergent & seq is convergent & lim seq <> 0 & seq is_not_0 holds
seq' /" seq is convergent

proof end;

theorem :: SEQ_2:38

for seq', seq being Real_Sequence st seq' is convergent & seq is convergent & lim seq <> 0 & seq is_not_0 holds
lim (seq' /" seq) = (lim seq') / (lim seq)

proof end;

theorem Th39: :: SEQ_2:39

for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
seq (#) seq1 is convergent

proof end;

theorem :: SEQ_2:40

for seq, seq1 being Real_Sequence st seq is convergent & seq1 is bounded & lim seq = 0 holds
lim (seq (#) seq1) = 0

proof end;