:: Convergent Sequences and the Limit of Sequences
:: by Jaros{\l}aw Kotowicz
::
:: Received July 4, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

theorem Th1: :: SEQ_2:1

for r, g being Real holds
( ( - g < r & r < g ) iff |.r.| < g )

proof end;

theorem Th2: :: SEQ_2:2

for r, g being Real st g <> 0 & r <> 0 holds
|.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|)

proof end;

definition

let f be real-valued Function;

attr f is bounded_above means :: SEQ_2:def 1
ex r being Real st
for y being object st y in dom f holds
f . y < r;

attr f is bounded_below means :: SEQ_2:def 2
ex r being Real st
for y being object st y in dom f holds
r < f . y;

end;

:: deftheorem defines bounded_above SEQ_2:def 1 :
for f being real-valued Function holds
( f is bounded_above iff ex r being Real st
for y being object st y in dom f holds
f . y < r );

:: deftheorem defines bounded_below SEQ_2:def 2 :
for f being real-valued Function holds
( f is bounded_below iff ex r being Real st
for y being object st y in dom f holds
r < f . y );

definition

let seq be Real_Sequence;
A1: dom seq = NAT by SEQ_1:1;

redefine attr seq is bounded_above means :Def3: :: SEQ_2:def 3
ex r being Real st
for n being Nat holds seq . n < r;

compatibility
( seq is bounded_above iff ex r being Real st
for n being Nat holds seq . n < r )

proof end;

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

compatibility
( seq is bounded_below iff ex r being Real st
for n being Nat holds r < seq . n )

proof end;

end;

:: deftheorem Def3 defines bounded_above SEQ_2:def 3 :
for seq being Real_Sequence holds
( seq is bounded_above iff ex r being Real st
for n being Nat holds seq . n < r );

:: deftheorem Def4 defines bounded_below SEQ_2:def 4 :
for seq being Real_Sequence holds
( seq is bounded_below iff ex r being Real st
for n being Nat holds r < seq . n );

registration

cluster Relation-like Function-like real-valued bounded -> real-valued bounded_above bounded_below for set ;

coherence
for b₁ being real-valued Function st b₁ is bounded holds
( b₁ is bounded_above & b₁ is bounded_below )

proof end;

cluster Relation-like Function-like real-valued bounded_above bounded_below -> real-valued bounded for set ;

coherence
for b₁ being real-valued Function st b₁ is bounded_above & b₁ is bounded_below holds
b₁ is bounded

proof end;

end;

theorem Th3: :: SEQ_2:3

for seq being Real_Sequence holds
( seq is bounded iff ex r being Real st
( 0 < r & ( for n being Nat holds |.(seq . n).| < r ) ) )

proof end;

theorem Th4: :: SEQ_2:4

for seq being Real_Sequence
for n being Nat ex r being Real st
( 0 < r & ( for m being Nat st m <= n holds
|.(seq . m).| < r ) )

proof end;

::
:: CONVERGENT REAL SEQUENCES
:: THE LIMIT OF SEQUENCES
::

definition

let seq be Real_Sequence;

redefine attr seq is convergent means :: SEQ_2:def 6
ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p;

compatibility
( seq is convergent iff ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p )

proof end;

end;

:: deftheorem SEQ_2:def 5 :
canceled;

:: deftheorem defines convergent SEQ_2:def 6 :
for seq being Real_Sequence holds
( seq is convergent iff ex g being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - g).| < p );

definition

let seq be Real_Sequence;
assume A1: seq is convergent ;

func lim seq -> Real means :Def6: :: SEQ_2:def 7
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - it).| < p;

existence
ex b₁ being Real st
for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - b₁).| < p by A1;
uniqueness
for b₁, b₂ being Real st ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - b₁).| < p ) & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - b₂).| < p ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines lim SEQ_2:def 7 :
for seq being Real_Sequence st seq is convergent holds
for b₂ being Real holds
( b₂ = lim seq iff for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.((seq . m) - b₂).| < p );

definition

let f be real-valued Function;

redefine attr f is bounded means :: SEQ_2:def 8
( f is bounded_above & f is bounded_below );

compatibility
( f is bounded iff ( f is bounded_above & f is bounded_below ) ) ;

end;

:: deftheorem defines bounded SEQ_2:def 8 :
for f being real-valued Function holds
( f is bounded iff ( f is bounded_above & f is bounded_below ) );

registration

cluster Function-like constant V32( NAT , REAL ) -> convergent for Element of K21(K22(NAT,REAL));

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

proof end;

end;

theorem Th5: :: SEQ_2:5

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

proof end;

registration

let seq1, seq2 be convergent Real_Sequence;

cluster seq1 + seq2 -> convergent for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = seq1 + seq2 holds
b₁ is convergent by Th5;

end;

theorem Th6: :: SEQ_2:6

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

proof end;

theorem Th7: :: SEQ_2:7

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

proof end;

registration

let r be Real;
let seq be convergent Real_Sequence;

cluster r (#) seq -> convergent for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = r (#) seq holds
b₁ is convergent by Th7;

end;

theorem Th8: :: SEQ_2:8

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

proof end;

theorem :: SEQ_2:9

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

registration

let seq be convergent Real_Sequence;

cluster - seq -> convergent for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = - seq holds
b₁ is convergent ;

end;

theorem Th10: :: SEQ_2:10

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

proof end;

theorem Th11: :: SEQ_2:11

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

proof end;

registration

let seq1, seq2 be convergent Real_Sequence;

cluster seq1 - seq2 -> convergent for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = seq1 - seq2 holds
b₁ is convergent by Th11;

end;

theorem Th12: :: SEQ_2:12

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

proof end;

theorem Th13: :: SEQ_2:13

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

proof end;

registration

cluster Function-like V32( NAT , REAL ) convergent -> bounded for Element of K21(K22(NAT,REAL));

coherence
for b₁ being Real_Sequence st b₁ is convergent holds
b₁ is bounded by Th13;

end;

theorem Th14: :: SEQ_2:14

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

proof end;

registration

let seq1, seq2 be convergent Real_Sequence;

cluster seq1 (#) seq2 -> convergent for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = seq1 (#) seq2 holds
b₁ is convergent by Th14;

end;

theorem Th15: :: SEQ_2:15

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

proof end;

theorem Th16: :: SEQ_2:16

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
|.(lim seq).| / 2 < |.(seq . m).|

proof end;

theorem Th17: :: SEQ_2:17

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:18

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

proof end;

theorem Th19: :: SEQ_2:19

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

proof end;

theorem :: SEQ_2:20

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

proof end;

theorem Th21: :: SEQ_2:21

for seq being Real_Sequence st seq is convergent & lim seq <> 0 & seq is non-zero holds
seq " is convergent

proof end;

theorem Th22: :: SEQ_2:22

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

proof end;

theorem :: SEQ_2:23

for seq, seq9 being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero holds
seq9 /" seq is convergent

proof end;

theorem :: SEQ_2:24

for seq, seq9 being Real_Sequence st seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero holds
lim (seq9 /" seq) = (lim seq9) / (lim seq)

proof end;

theorem Th25: :: SEQ_2:25

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:26

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

proof end;

registration

let s be convergent Complex_Sequence;

cluster |.s.| -> convergent for Real_Sequence;

coherence
for b₁ being Real_Sequence st b₁ = |.s.| holds
b₁ is convergent

proof end;

end;

theorem Th27: :: SEQ_2:27

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

proof end;

theorem :: SEQ_2:28

for s, s9 being convergent Complex_Sequence holds lim |.(s + s9).| = |.((lim s) + (lim s9)).|

proof end;

theorem :: SEQ_2:29

for r being Real
for s being convergent Complex_Sequence holds lim |.(r (#) s).| = |.r.| * |.(lim s).|

proof end;

theorem :: SEQ_2:30

for s being convergent Complex_Sequence holds lim |.(- s).| = |.(lim s).|

proof end;

theorem :: SEQ_2:31

for s, s9 being convergent Complex_Sequence holds lim |.(s - s9).| = |.((lim s) - (lim s9)).|

proof end;

theorem :: SEQ_2:32

for s, s9 being convergent Complex_Sequence holds lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).|

proof end;

theorem :: SEQ_2:33

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

proof end;

theorem :: SEQ_2:34

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

proof end;

theorem :: SEQ_2:35

for s, s1 being Complex_Sequence st s is convergent & s1 is bounded & lim s = 0c holds
lim |.(s (#) s1).| = 0

proof end;