:: by Jaros{\l}aw Kotowicz

::

:: Received July 4, 1989

:: Copyright (c) 1990-2012 Association of Mizar Users

begin

theorem Th2: :: SEQ_2:2

for g, r being real number st g <> 0 & r <> 0 holds

abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r))

abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r))

proof end;

definition

let f be real-valued Function;

end;
attr f is bounded_above means :Def1: :: SEQ_2:def 1

ex r being real number st

for y being set st y in dom f holds

f . y < r;

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 :Def2: :: SEQ_2:def 2

ex r being real number st

for y being set st y in dom f holds

r < f . y;

ex r being real number st

for y being set st y in dom f holds

r < f . y;

:: deftheorem Def1 defines bounded_above SEQ_2:def 1 :

for f being real-valued Function holds

( f is bounded_above iff ex r being real number st

for y being set st y in dom f holds

f . y < r );

for f being real-valued Function holds

( f is bounded_above iff ex r being real number st

for y being set st y in dom f holds

f . y < r );

:: deftheorem Def2 defines bounded_below SEQ_2:def 2 :

for f being real-valued Function holds

( f is bounded_below iff ex r being real number st

for y being set st y in dom f holds

r < f . y );

for f being real-valued Function holds

( f is bounded_below iff ex r being real number st

for y being set st y in dom f holds

r < f . y );

definition

let seq be Real_Sequence;

A1: dom seq = NAT by SEQ_1:1;

( seq is bounded_above iff ex r being real number st

for n being Element of NAT holds seq . n < r )

( seq is bounded_below iff ex r being real number st

for n being Element of NAT holds r < seq . n )

end;
A1: dom seq = NAT by SEQ_1:1;

redefine attr seq is bounded_above means :Def3: :: SEQ_2:def 3

ex r being real number st

for n being Element of NAT holds seq . n < r;

compatibility ex r being real number st

for n being Element of NAT holds seq . n < r;

( seq is bounded_above iff ex r being real number st

for n being Element of NAT holds seq . n < r )

proof end;

redefine attr seq is bounded_below means :Def4: :: SEQ_2:def 4

ex r being real number st

for n being Element of NAT holds r < seq . n;

compatibility ex r being real number st

for n being Element of NAT holds r < seq . n;

( seq is bounded_below iff ex r being real number st

for n being Element of NAT holds r < seq . n )

proof 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 number st

for n being Element of NAT holds seq . n < r );

for seq being Real_Sequence holds

( seq is bounded_above iff ex r being real number st

for n being Element of 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 number st

for n being Element of NAT holds r < seq . n );

for seq being Real_Sequence holds

( seq is bounded_below iff ex r being real number st

for n being Element of NAT holds r < seq . n );

registration

for b_{1} being real-valued Function st b_{1} is bounded holds

( b_{1} is bounded_above & b_{1} is bounded_below )

for b_{1} being real-valued Function st b_{1} is bounded_above & b_{1} is bounded_below holds

b_{1} is bounded
end;

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

coherence for b

( b

proof end;

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

coherence for b

b

proof end;

theorem Th3: :: SEQ_2:3

for seq being Real_Sequence holds

( seq is bounded iff ex r being real number st

( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) )

( seq is bounded iff ex r being real number st

( 0 < r & ( for n being Element of NAT holds abs (seq . n) < r ) ) )

proof end;

theorem Th4: :: SEQ_2:4

for seq being Real_Sequence

for n being Element of NAT ex r being real number st

( 0 < r & ( for m being Element of NAT st m <= n holds

abs (seq . m) < r ) )

for n being Element of NAT ex r being real number st

( 0 < r & ( for m being Element of NAT st m <= n holds

abs (seq . m) < r ) )

proof end;

definition

canceled;

let seq be Real_Sequence;

( seq is convergent iff ex g being real number st

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - g) < p )

end;
let seq be Real_Sequence;

redefine 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 Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - g) < p;

compatibility ex g being real number st

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - g) < p;

( seq is convergent iff ex g being real number st

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - g) < p )

proof end;

:: deftheorem Def6 defines convergent SEQ_2:def 6 :

for seq being Real_Sequence holds

( seq is convergent iff ex g being real number st

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - g) < p );

for seq being Real_Sequence holds

( seq is convergent iff ex g being real number st

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - g) < p );

definition

let seq be Real_Sequence;

assume A1: seq is convergent ;

ex b_{1} being real number st

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b_{1}) < p
by A1, Def6;

uniqueness

for b_{1}, b_{2} being real number st ( for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b_{1}) < p ) & ( for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b_{2}) < p ) holds

b_{1} = b_{2}

end;
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 Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - it) < p;

existence for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - it) < p;

ex b

for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b

uniqueness

for b

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b

b

proof end;

:: deftheorem Def7 defines lim SEQ_2:def 7 :

for seq being Real_Sequence st seq is convergent holds

for b_{2} being real number holds

( b_{2} = lim seq iff for p being real number st 0 < p holds

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b_{2}) < p );

for seq being Real_Sequence st seq is convergent holds

for b

( b

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

abs ((seq . m) - b

definition

let f be real-valued Function;

compatibility

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

end;
compatibility

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

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

for f being real-valued Function holds

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

definition

let seq be Real_Sequence;

:: original: lim

redefine func lim seq -> Real;

coherence

lim seq is Real by XREAL_0:def 1;

end;
:: original: lim

redefine func lim seq -> Real;

coherence

lim seq is Real by XREAL_0:def 1;

registration
end;

registration

ex b_{1} being Real_Sequence st b_{1} is constant
end;

cluster non zero Relation-like NAT -defined REAL -valued Function-like constant V26( NAT ) V30( NAT , REAL ) complex-valued ext-real-valued real-valued for Element of K11(K12(NAT,REAL));

existence ex b

proof end;

theorem Th5: :: SEQ_2:5

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

seq + seq9 is convergent

seq + seq9 is convergent

proof end;

registration

let seq1, seq2 be convergent Real_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = seq1 + seq2 holds

b_{1} is convergent
by Th5;

end;
coherence

for b

b

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)

lim (seq + seq9) = (lim seq) + (lim seq9)

proof end;

theorem Th7: :: SEQ_2:7

for r being real number

for seq being Real_Sequence st seq is convergent holds

r (#) seq is convergent

for seq being Real_Sequence st seq is convergent holds

r (#) seq is convergent

proof end;

registration

let r be real number ;

let seq be convergent Real_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = r (#) seq holds

b_{1} is convergent
by Th7;

end;
let seq be convergent Real_Sequence;

coherence

for b

b

theorem Th8: :: SEQ_2:8

for r being real number

for seq being Real_Sequence st seq is convergent holds

lim (r (#) seq) = r * (lim seq)

for seq being Real_Sequence st seq is convergent holds

lim (r (#) seq) = r * (lim seq)

proof end;

registration

let seq be convergent Real_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = - seq holds

b_{1} is convergent
;

end;
coherence

for b

b

theorem Th11: :: SEQ_2:11

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

seq - seq9 is convergent

seq - seq9 is convergent

proof end;

registration

let seq1, seq2 be convergent Real_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = seq1 - seq2 holds

b_{1} is convergent
by Th11;

end;
coherence

for b

b

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)

lim (seq - seq9) = (lim seq) - (lim seq9)

proof end;

registration
end;

theorem Th14: :: SEQ_2:14

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

seq (#) seq9 is convergent

seq (#) seq9 is convergent

proof end;

registration

let seq1, seq2 be convergent Real_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = seq1 (#) seq2 holds

b_{1} is convergent
by Th14;

end;
coherence

for b

b

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)

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 Element of NAT st

for m being Element of NAT st n <= m holds

(abs (lim seq)) / 2 < abs (seq . m)

ex n being Element of NAT st

for m being Element of NAT st n <= m holds

(abs (lim seq)) / 2 < abs (seq . m)

proof end;

theorem Th17: :: SEQ_2:17

for seq being Real_Sequence st seq is convergent & ( for n being Element of NAT holds 0 <= seq . n ) holds

0 <= lim seq

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 Element of NAT holds seq . n <= seq9 . n ) holds

lim seq <= lim seq9

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 Element of NAT holds

( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds

seq1 is convergent

( 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 Element of NAT holds

( seq . n <= seq1 . n & seq1 . n <= seq9 . n ) ) & lim seq = lim seq9 holds

lim seq1 = lim seq

( 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

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) "

lim (seq ") = (lim seq) "

proof end;

theorem :: SEQ_2:23

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

seq9 /" seq is convergent

seq9 /" seq is convergent

proof end;

theorem :: SEQ_2:24

for seq9, seq 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)

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

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

lim (seq (#) seq1) = 0

proof end;

registration

let s be convergent Complex_Sequence;

coherence

for b_{1} being Real_Sequence st b_{1} = |.s.| holds

b_{1} is convergent

end;
coherence

for b

b

proof end;

theorem :: SEQ_2:29

for r being real number

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

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

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).| "

lim |.(s ").| = |.(lim s).| "

proof end;

theorem :: SEQ_2:34

for s9, s 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).|

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

lim |.(s (#) s1).| = 0

proof end;

:: CONVERGENT REAL SEQUENCES

:: THE LIMIT OF SEQUENCES

::