:: Convergent Sequences and the Limit of Sequences :: by Jaros{\l}aw Kotowicz :: :: Received July 4, 1989 :: Copyright (c) 1990-2012 Association of Mizar Users begin theorem Th1: :: SEQ_2:1 for g, r being real number holds ( ( - g < r & r < g ) iff abs r < g ) proofend; 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)) proofend; definition let f be real-valued Function; attrf 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; attrf 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; end; :: 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 ); :: 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 ); 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 number st for n being Element of NAT holds seq . n < r; compatibility ( seq is bounded_above iff ex r being real number st for n being Element of NAT holds seq . n < r ) proofend; 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 ( seq is bounded_below iff ex r being real number st for n being Element of NAT holds r < seq . n ) proofend; 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 ); :: 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 ); registration cluster Relation-like Function-like real-valued bounded -> real-valued bounded_above bounded_below for set ; coherence for b1 being real-valued Function st b1 is bounded holds ( b1 is bounded_above & b1 is bounded_below ) proofend; cluster Relation-like Function-like real-valued bounded_above bounded_below -> real-valued bounded for set ; coherence for b1 being real-valued Function st b1 is bounded_above & b1 is bounded_below holds b1 is bounded proofend; 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 ) ) ) proofend; 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 ) ) proofend; :: :: CONVERGENT REAL SEQUENCES :: THE LIMIT OF SEQUENCES :: definition canceled; 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 ( 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 ) proofend; end; :: deftheorem SEQ_2:def_5_:_ canceled; :: 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 ); 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 Element of NAT st for m being Element of NAT st n <= m holds abs ((seq . m) - it) < p; existence ex b1 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) - b1) < p by A1, Def6; uniqueness for b1, b2 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) - b1) < 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) - b2) < p ) holds b1 = b2 proofend; end; :: deftheorem Def7 defines lim SEQ_2:def_7_:_ for seq being Real_Sequence st seq is convergent holds for b2 being real number holds ( b2 = 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) - b2) < 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 ) ); definition let seq be Real_Sequence; :: original:lim redefine func lim seq -> Real; coherence lim seq is Real by XREAL_0:def_1; end; registration cluster Function-like constant V30( NAT , REAL ) -> convergent for Element of K11(K12(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is constant holds b1 is convergent proofend; end; registration 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 b1 being Real_Sequence st b1 is constant proofend; end; theorem Th5: :: SEQ_2:5 for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds seq + seq9 is convergent proofend; registration let seq1, seq2 be convergent Real_Sequence; clusterseq1 + seq2 -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = seq1 + seq2 holds b1 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) proofend; theorem Th7: :: SEQ_2:7 for r being real number for seq being Real_Sequence st seq is convergent holds r (#) seq is convergent proofend; registration let r be real number ; let seq be convergent Real_Sequence; clusterr (#) seq -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = r (#) seq holds b1 is convergent by Th7; end; 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) proofend; 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 b1 being Real_Sequence st b1 = - seq holds b1 is convergent ; end; theorem Th10: :: SEQ_2:10 for seq being Real_Sequence st seq is convergent holds lim (- seq) = - (lim seq) proofend; theorem Th11: :: SEQ_2:11 for seq, seq9 being Real_Sequence st seq is convergent & seq9 is convergent holds seq - seq9 is convergent proofend; registration let seq1, seq2 be convergent Real_Sequence; clusterseq1 - seq2 -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = seq1 - seq2 holds b1 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) proofend; theorem Th13: :: SEQ_2:13 for seq being Real_Sequence st seq is convergent holds seq is bounded proofend; registration cluster Function-like V30( NAT , REAL ) convergent -> bounded for Element of K11(K12(NAT,REAL)); coherence for b1 being Real_Sequence st b1 is convergent holds b1 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 proofend; registration let seq1, seq2 be convergent Real_Sequence; clusterseq1 (#) seq2 -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = seq1 (#) seq2 holds b1 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) proofend; 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) proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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 proofend; 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) " proofend; 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 proofend; 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) proofend; 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 proofend; 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 proofend; registration let s be convergent Complex_Sequence; cluster|.s.| -> convergent for Real_Sequence; coherence for b1 being Real_Sequence st b1 = |.s.| holds b1 is convergent proofend; end; theorem Th27: :: SEQ_2:27 for s being Complex_Sequence st s is convergent holds lim |.s.| = |.(lim s).| proofend; theorem :: SEQ_2:28 for s, s9 being convergent Complex_Sequence holds lim |.(s + s9).| = |.((lim s) + (lim s9)).| proofend; theorem :: SEQ_2:29 for r being real number for s being convergent Complex_Sequence holds lim |.(r (#) s).| = |.r.| * |.(lim s).| proofend; theorem :: SEQ_2:30 for s being convergent Complex_Sequence holds lim |.(- s).| = |.(lim s).| proofend; theorem :: SEQ_2:31 for s, s9 being convergent Complex_Sequence holds lim |.(s - s9).| = |.((lim s) - (lim s9)).| proofend; theorem :: SEQ_2:32 for s, s9 being convergent Complex_Sequence holds lim |.(s (#) s9).| = |.(lim s).| * |.(lim s9).| proofend; 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).| " proofend; 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).| proofend; 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 proofend;