Real means :Def6: for p st 0

g2; A5: now assume |.g1-g2.|=0; then 0+g2=g1-g2+g2 by ABSVALUE:2; hence contradiction by A4; end; A6: 0<=|.g1-g2.| by COMPLEX1:46; then consider n1 such that A7: for m st n1<=m holds |.seq.m-g1.|<|.g1-g2.|/4 by A2,A5; consider n2 such that A8: for m st n2<=m holds |.seq.m-g2.|<|.g1-g2.|/4 by A3,A5,A6; A9: |.seq.(n1+n2)-g1.|<|.g1-g2.|/4 by A7,NAT_1:12; |.seq.(n1+n2)-g2.|<|.g1-g2.|/4 by A8,NAT_1:12; then A10: |.seq.(n1+n2)-g2.|+|.seq.(n1+n2)-g1.|<|.g1-g2.|/4+|.g1-g2.|/4 by A9,XREAL_1:8; |.g1-g2.|=|.-(seq.(n1+n2)-g1)+(seq.(n1+n2)-g2).|; then |.g1-g2.|<=|.-(seq.(n1+n2)-g1).|+|.seq.(n1+n2)-g2.| by COMPLEX1:56; then A11: |.g1-g2.|<=|.seq.(n1+n2)-g1.|+|.seq.(n1+n2)-g2.| by COMPLEX1:52; |.g1-g2.|/2 <|.g1-g2.| by A5,A6,XREAL_1:216; hence contradiction by A10,A11,XXREAL_0:2; end; end; definition let f be real-valued Function; redefine attr f is bounded means f is bounded_above bounded_below; compatibility; end; registration cluster constant -> convergent for Real_Sequence; coherence proof let seq be Real_Sequence; assume seq is constant; then consider r being Element of REAL such that A1: for n being Nat holds seq.n=r by VALUED_0:def 18; take g=r; let p such that A2: 0

convergent for Real_Sequence; coherence by Th5; end; theorem Th6: seq is convergent & seq9 is convergent implies lim (seq + seq9)=(lim seq)+(lim seq9) proof assume that A1: seq is convergent and A2: seq9 is convergent; now let p; assume 0

0; then A6: 0<|.r.| by COMPLEX1:47; let p such that A7: 0

|.r.| by A5,COMPLEX1:47; consider n1 such that A9: for m st n1<=m holds |.seq.m-g1.|

convergent for Real_Sequence; coherence by Th7; end; theorem Th8: seq is convergent implies lim(r(#)seq)=r*(lim seq) proof assume A1: seq is convergent; A2: now assume A3: r=0; let p such that A4: 0

0; then A6: 0<|.r.| by COMPLEX1:47; let p such that A7: 0

|.r.| by A5,COMPLEX1:47; 0

convergent for Real_Sequence; coherence; end; theorem Th10: seq is convergent implies lim(-seq) = -(lim seq) proof assume seq is convergent; then lim ((-1)(#)seq)=(-1)*(lim seq) by Th8; hence thesis; end; theorem Th11: seq is convergent & seq9 is convergent implies seq - seq9 is convergent proof assume that A1: seq is convergent and A2: seq9 is convergent; -seq9 is convergent by A2; hence thesis by A1; end; registration let seq1,seq2 be convergent Real_Sequence; cluster seq1 - seq2 -> convergent for Real_Sequence; coherence by Th11; end; theorem Th12: seq is convergent & seq9 is convergent implies lim(seq - seq9)=(lim seq)-(lim seq9) proof assume that A1: seq is convergent and A2: seq9 is convergent; thus lim(seq - seq9)=(lim seq)+(lim(- seq9)) by A1,A2,Th6 .=(lim seq)+-(lim seq9) by A2,Th10 .=(lim seq)-(lim seq9); end; theorem Th13: seq is convergent implies seq is bounded proof assume seq is convergent; then consider g such that A1: for p st 0

bounded for Real_Sequence; coherence by Th13; end; theorem Th14: seq is convergent & seq9 is convergent implies seq (#) seq9 is convergent proof assume that A1: seq is convergent and A2: seq9 is convergent; consider g1 such that A3: for p st 0

convergent for Real_Sequence;
coherence by Th14;
end;
theorem Th15:
seq is convergent & seq9 is convergent implies
lim(seq(#)seq9)=(lim seq)*(lim seq9)
proof
assume that
A1: seq is convergent and
A2: seq9 is convergent;
consider r such that
A3: 0 0 & seq is non-zero implies seq" is convergent
proof
assume that
A1: seq is convergent and
A2: lim seq<>0 and
A3: seq is non-zero;
A4: 0<|.lim seq.| by A2,COMPLEX1:47;
A5: 0<>|.lim seq.| by A2,COMPLEX1:47;
consider n1 such that
A6: for m st n1<=m holds |.lim seq.|/2<|.seq.m.| by A1,A2,Th16;
0*0<|.lim seq.|*|.lim seq.| by A4;
then
A7: 0<(|.lim seq.|*|.lim seq.|)/2;
take (lim seq)";
let p;
assume
A8: 0 0 by A3,SEQ_1:5;
then seq.m*(lim seq)<>0 by A2;
then 0<|.seq.m*(lim seq).| by COMPLEX1:47;
then 0<|.seq.m.|*|.lim seq.| by COMPLEX1:65;
then
A14: |.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|)<
(p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
by A11,XREAL_1:74;
A15: (p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
=(p*(2"*(|.lim seq.|*|.lim seq.|)))*
(|.seq.m.|*|.lim seq.|)" by XCMPLX_0:def 9
.=p*2"*((|.lim seq.|*|.lim seq.|)*(|.lim seq.|*|.seq.m.|)")
.=p*2"*((|.lim seq.|*|.lim seq.|)*
(|.lim seq.|"*(|.seq.m.|)")) by XCMPLX_1:204
.=p*2"*(|.lim seq.|*(|.lim seq.|*|.lim seq.|")*|.seq.m.|")
.=p*2"*(|.lim seq.|*1*(|.seq.m.|)") by A5,XCMPLX_0:def 7
.=p*(|.lim seq.|/2)*|.seq.m.|"
.=(p*(|.lim seq.|/2))/|.seq.m.| by XCMPLX_0:def 9;
A16: |.(seq").m-(lim seq)".|=|.(seq.m)"-(lim seq)".| by VALUED_1:10
.=|.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|) by A2,A13,Th2;
A17: 0<|.lim seq.|/2 by A4;
A18: 0<>|.lim seq.|/2 by A2,COMPLEX1:47;
0*0 0 & seq is non-zero
implies lim seq"=(lim seq)"
proof
assume that
A1: seq is convergent and
A2: (lim seq)<>0 and
A3: seq is non-zero;
A4: seq" is convergent by A1,A2,A3,Th21;
A5: 0<|.lim seq.| by A2,COMPLEX1:47;
A6: 0<>|.lim seq.| by A2,COMPLEX1:47;
consider n1 such that
A7: for m st n1<=m holds |.lim seq.|/2<|.seq.m.| by A1,A2,Th16;
0*0<|.lim seq.|*|.lim seq.| by A5;
then
A8: 0<(|.lim seq.|*|.lim seq.|)/2;
now
let p;
assume
A9: 0 0 by A3,SEQ_1:5;
then seq.m*(lim seq)<>0 by A2;
then 0<|.seq.m*(lim seq).| by COMPLEX1:47;
then 0<|.seq.m.|*|.lim seq.| by COMPLEX1:65;
then
A15: |.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|)<
(p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
by A12,XREAL_1:74;
A16: (p*((|.lim seq.|*|.lim seq.|)/2))/(|.seq.m.|*|.lim seq.|)
=(p*(2"*(|.lim seq.|*|.lim seq.|)))*
(|.seq.m.|*|.lim seq.|)" by XCMPLX_0:def 9
.=p*2"*((|.lim seq.|*|.lim seq.|)*(|.lim seq.|*|.seq.m.|)")
.=p*2"*((|.lim seq.|*|.lim seq.|)*
((|.lim seq.|)"*(|.seq.m.|)")) by XCMPLX_1:204
.=p*2"*(|.lim seq.|*(|.lim seq.|*|.lim seq.|")*|.seq.m.|")
.=p*2"*(|.lim seq.|*1*|.seq.m.|") by A6,XCMPLX_0:def 7
.=p*(|.lim seq.|/2)*|.seq.m.|"
.=(p*(|.lim seq.|/2))/|.seq.m.| by XCMPLX_0:def 9;
A17: |.(seq").m-(lim seq)".|=|.(seq.m)"-(lim seq)".| by VALUED_1:10
.=|.seq.m-lim seq.|/(|.seq.m.|*|.lim seq.|) by A2,A14,Th2;
A18: 0<|.lim seq.|/2 by A5;
A19: 0<>|.lim seq.|/2 by A2,COMPLEX1:47;
0*0 0
& seq is non-zero implies seq9/"seq is convergent
proof
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: (lim seq)<>0 and
A4: seq is non-zero;
seq" is convergent by A2,A3,A4,Th21;
hence thesis by A1;
end;
theorem
seq9 is convergent & seq is convergent & lim seq <> 0
& seq is non-zero implies lim(seq9/"seq)=(lim seq9)/(lim seq)
proof
assume that
A1: seq9 is convergent and
A2: seq is convergent and
A3: (lim seq)<>0 and
A4: seq is non-zero;
seq" is convergent by A2,A3,A4,Th21;
then lim (seq9(#)(seq"))=(lim seq9)*(lim seq") by A1,Th15
.=(lim seq9)*(lim seq)" by A2,A3,A4,Th22
.=(lim seq9)/(lim seq) by XCMPLX_0:def 9;
hence thesis;
end;
theorem Th25:
seq is convergent & seq1 is bounded & lim seq=0 implies
seq(#)seq1 is convergent
proof
assume that
A1: seq is convergent and
A2: seq1 is bounded and
A3: lim seq=0;
reconsider g1=0 as Real;
take g=g1;
let p such that
A4: 0 0;
(p/r)*r=p*r"*r by XCMPLX_0:def 9
.=p*(r"*r)
.=p*1 by A5,XCMPLX_0:def 7
.=p;
then
A13: (p/r)*|.seq1.m.|

0; (p/r)*r=p*r"*r by XCMPLX_0:def 9 .=p*(r"*r) .=p*1 by A6,XCMPLX_0:def 7; then A13: (p/r)*|.seq1.m.|

convergent for Real_Sequence; coherence proof |.s.| is convergent proof consider g such that A1: for p be Real st 0

0c & s is non-zero implies lim |.s".| = (|. lim s.|)" proof assume A1: s is convergent & (lim s)<>0c & s is non-zero; then s" is convergent by COMSEQ_2:34; hence lim |.s".| = |.lim s".| by Th27 .= |.(lim s)".| by A1,COMSEQ_2:35 .= (|.lim s.|)" by COMPLEX1:66; end; theorem s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero implies lim |.(s9/"s).|=|.(lim s9).|/|.(lim s).| proof assume A1: s9 is convergent & s is convergent & (lim s)<>0c & s is non-zero; then s9/"s is convergent by COMSEQ_2:38; hence lim |.s9/"s.| = |.lim (s9/"s).| by Th27 .= |.(lim s9)/(lim s).| by A1,COMSEQ_2:39 .= |.(lim s9).|/|.(lim s).| by COMPLEX1:67; end; theorem s is convergent & s1 is bounded & (lim s)=0c implies lim |.s(#)s1.| = 0 proof assume A1: s is convergent & s1 is bounded & (lim s)=0c; then s(#)s1 is convergent by COMSEQ_2:42; hence lim |.s(#)s1.| = |.(lim (s(#)s1)).| by Th27 .= 0 by A1,COMPLEX1:44,COMSEQ_2:43; end;