convergent for Real_Sequence; end; theorem :: SEQ_2:5 seq is convergent & seq9 is convergent implies seq + seq9 is convergent; registration let seq1,seq2 be convergent Real_Sequence; cluster seq1 + seq2 -> convergent for Real_Sequence; end; theorem :: SEQ_2:6 seq is convergent & seq9 is convergent implies lim (seq + seq9)=(lim seq)+(lim seq9); theorem :: SEQ_2:7 seq is convergent implies r(#)seq is convergent; registration let r be Real; let seq be convergent Real_Sequence; cluster r(#)seq -> convergent for Real_Sequence; end; theorem :: SEQ_2:8 seq is convergent implies lim(r(#)seq)=r*(lim seq); theorem :: SEQ_2:9 seq is convergent implies -seq is convergent; registration let seq be convergent Real_Sequence; cluster -seq -> convergent for Real_Sequence; end; theorem :: SEQ_2:10 seq is convergent implies lim(-seq) = -(lim seq); theorem :: SEQ_2:11 seq is convergent & seq9 is convergent implies seq - seq9 is convergent; registration let seq1,seq2 be convergent Real_Sequence; cluster seq1 - seq2 -> convergent for Real_Sequence; end; theorem :: SEQ_2:12 seq is convergent & seq9 is convergent implies lim(seq - seq9)=(lim seq)-(lim seq9); theorem :: SEQ_2:13 seq is convergent implies seq is bounded; registration cluster convergent -> bounded for Real_Sequence; end; theorem :: SEQ_2:14 seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent; registration let seq1,seq2 be convergent Real_Sequence; cluster seq1 (#) seq2 -> convergent for Real_Sequence; end; theorem :: SEQ_2:15 seq is convergent & seq9 is convergent implies lim(seq(#)seq9)=(lim seq)*(lim seq9); theorem :: SEQ_2:16 seq is convergent implies (lim seq<>0 implies ex n st for m st n<=m holds |.lim seq.|/2<|.seq.m.|); theorem :: SEQ_2:17 seq is convergent & (for n holds 0<=seq.n) implies 0<=lim seq; theorem :: SEQ_2:18 seq is convergent & seq9 is convergent & (for n holds seq.n<=(seq9.n)) implies (lim seq)<=(lim seq9); theorem :: SEQ_2:19 seq is convergent & seq9 is convergent & (for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n) & (lim seq)=(lim seq9) implies seq1 is convergent; theorem :: SEQ_2:20 seq is convergent & seq9 is convergent & (for n holds seq.n<=(seq1.n) & seq1.n<=seq9.n) & lim seq = lim seq9 implies lim seq1 = lim seq; theorem :: SEQ_2:21 seq is convergent & lim seq <> 0 & seq is non-zero implies seq" is convergent ; theorem :: SEQ_2:22 seq is convergent & lim seq <> 0 & seq is non-zero implies lim seq"=(lim seq)"; theorem :: SEQ_2:23 seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero implies seq9/"seq is convergent; theorem :: SEQ_2:24 seq9 is convergent & seq is convergent & lim seq <> 0 & seq is non-zero implies lim(seq9/"seq)=(lim seq9)/(lim seq); theorem :: SEQ_2:25 seq is convergent & seq1 is bounded & lim seq=0 implies seq(#)seq1 is convergent; theorem :: SEQ_2:26 seq is convergent & seq1 is bounded & lim seq=0 implies lim(seq(#)seq1)=0; :: from COMSEQ_2, 2011.07.10, A.T. reserve g for Complex; registration let s be convergent Complex_Sequence; cluster |.s.| -> convergent for Real_Sequence; end; reserve s,s1,s9 for Complex_Sequence; theorem :: SEQ_2:27 s is convergent implies lim |.s.| = |.lim s.|; theorem :: SEQ_2:28 for s,s9 being convergent Complex_Sequence holds lim |.(s + s9).| = |.(lim s)+(lim s9).|; theorem :: SEQ_2:29 for s being convergent Complex_Sequence holds lim |.(r(#)s).| = |.r.|*|.(lim s).|; theorem :: SEQ_2:30 for s being convergent Complex_Sequence holds lim |.-s.| = |.lim s.|; theorem :: SEQ_2:31 for s,s9 being convergent Complex_Sequence holds lim |.s - s9.| = |.(lim s) - (lim s9).|; theorem :: SEQ_2:32 for s,s9 being convergent Complex_Sequence holds lim |.s(#)s9.| = |.lim s.|*|.lim s9.|; theorem :: SEQ_2:33 s is convergent & (lim s)<>0c & s is non-zero implies lim |.s".| = (|. lim s.|)"; theorem :: SEQ_2:34 s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim |.(s9/"s).|=|.(lim s9).|/|.(lim s).|; theorem :: SEQ_2:35 s is convergent & s1 is bounded & (lim s)=0c implies lim |.s(#)s1.| = 0;