Copyright (c) 1990 Association of Mizar Users
environ vocabulary ARYTM, SEQ_1, PARTFUN1, ARYTM_1, RELAT_1, BOOLE, SQUARE_1, ARYTM_3, PROB_1, RCOMP_1, SEQ_2, FUNCT_1, ORDINAL2, ABSVALUE, SEQM_3, LATTICES, RFUNCT_1, RFUNCT_2, FINSEQ_1, LIMFUNC1; notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, PROB_1, RELSET_1, SQUARE_1, PARTFUN1, RFUNCT_1, RCOMP_1, RFUNCT_2; constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PROB_1, SQUARE_1, RFUNCT_1, RCOMP_1, RFUNCT_2, PARTFUN1, MEMBERED, XBOOLE_0; clusters RELSET_1, XREAL_0, SEQ_1, SEQM_3, ARYTM_3, MEMBERED, ZFMISC_1, XBOOLE_0; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; definitions TARSKI, SEQ_2, XBOOLE_0; theorems AXIOMS, TARSKI, REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SQUARE_1, RFUNCT_1, RFUNCT_2, PROB_1, RCOMP_1, FUNCT_1, FUNCT_2, XREAL_0, XBOOLE_0, XBOOLE_1, REAL_2, FINSEQ_2, XCMPLX_0, XCMPLX_1; schemes SEQ_1, RCOMP_1; begin reserve r,r1,r2,g,g1,g2 for real number; reserve n,m,k for Nat; reserve seq,seq1,seq2 for Real_Sequence; reserve f,f1,f2 for PartFunc of REAL,REAL; Lm1: (-1)*(-1)=1; Lm2: 0<g & r<=r1 implies r-g<r1 & r<r1+g proof assume A1: 0<g & r<=r1; then r-g<r1-0 by REAL_1:92; hence r-g<r1; r+0<r1+g by A1,REAL_1:67; hence thesis; end; Lm3: rng seq c=dom(f1+f2) implies dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 proof assume A1: rng seq c=dom(f1+f2); thus dom(f1+f2)=dom f1/\dom f2 by SEQ_1:def 3; then dom(f1+f2)c=dom f1 & dom(f1+f2)c=dom f2 by XBOOLE_1:17;hence thesis by A1,XBOOLE_1:1; end; Lm4: rng seq c=dom(f1(#)f2) implies dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 proof assume A1: rng seq c=dom(f1(#)f2); thus dom(f1(#)f2)=dom f1/\dom f2 by SEQ_1:def 5; then dom(f1(#)f2)c=dom f1 & dom(f1(#)f2)c=dom f2 by XBOOLE_1:17; hence thesis by A1,XBOOLE_1:1; end; definition let n,m; redefine func max(n,m) ->Nat; coherence by FINSEQ_2:1; end; theorem Th1: 0<=r1 & r1<r2 & 0<g1 & g1<=g2 implies r1*g1<r2*g2 proof assume A1: 0<=r1 & r1<r2 & 0<g1 & g1<=g2; then A2: r1*g1<=r1*g2 by AXIOMS :25; 0<g2 by A1; then r1*g2<r2*g2 by A1,REAL_1:70; hence thesis by A2,AXIOMS:22; end; definition let r be real number; redefine func halfline(r); synonym left_open_halfline(r); end; reserve r,r1,r2,g,g1,g2 for Real; definition let r be real number; func left_closed_halfline(r) ->Subset of REAL equals :Def1: {g: g<=r}; coherence proof now let x be set; assume x in {g: g<=r}; then ex g st x=g & g<=r; hence x in REAL; end; hence thesis by TARSKI:def 3; end; func right_closed_halfline(r) ->Subset of REAL equals :Def2: {g: r<=g}; coherence proof now let x be set; assume x in {g: r<=g}; then ex g st x=g & r<=g; hence x in REAL; end; hence thesis by TARSKI:def 3; end; func right_open_halfline(r) ->Subset of REAL equals :Def3: {g: r<g}; coherence proof now let x be set; assume x in {g: r<g}; then ex g st x=g & r<g; hence x in REAL; end; hence thesis by TARSKI:def 3; end; end; canceled 6; theorem r1<=r2 implies right_open_halfline(r2) c= right_open_halfline(r1) proof assume A1: r1<=r2; let x be set; assume x in right_open_halfline(r2); then x in {r: r2<r} by Def3; then consider r such that A2: r=x & r2<r; r1<r by A1,A2,AXIOMS:22; then x in {g: r1<g} by A2; hence thesis by Def3; end; theorem r1<=r2 implies right_closed_halfline(r2) c= right_closed_halfline(r1) proof assume A1: r1<=r2; let x be set; assume x in right_closed_halfline(r2); then x in {r: r2<=r} by Def2; then consider r such that A2: r=x & r2<=r; r1<=r by A1,A2,AXIOMS:22; then x in {g: r1<=g} by A2; hence thesis by Def2; end; theorem right_open_halfline(r) c= right_closed_halfline(r) proof let x be set; assume x in right_open_halfline(r); then x in {r2: r<r2} by Def3; then consider r1 such that A1: r1=x & r<r1; x in {g: r<=g} by A1; hence thesis by Def2; end; theorem ].r,g.[ c= right_open_halfline(r) proof let x be set; assume x in ].r,g.[; then x in {r1: r<r1 & r1<g} by RCOMP_1:def 2; then ex g1 st g1=x & r<g1 & g1<g; then x in {g2: r<g2}; hence thesis by Def3; end; theorem [.r,g.] c= right_closed_halfline(r) proof let x be set; assume x in [.r,g.]; then x in {r1: r<=r1 & r1<=g} by RCOMP_1:def 1; then ex g1 st g1=x & r<=g1 & g1<=g; then x in {g2: r<=g2}; hence thesis by Def2; end; theorem r1<=r2 implies left_open_halfline(r1) c= left_open_halfline(r2) proof assume A1: r1<=r2; let x be set; assume x in left_open_halfline(r1); then x in {r: r<r1} by PROB_1:def 15; then consider r such that A2: r=x & r< r1; r<r2 by A1,A2,AXIOMS:22; then x in {g: g<r2} by A2 ; hence thesis by PROB_1:def 15; end; theorem r1<=r2 implies left_closed_halfline(r1) c= left_closed_halfline(r2) proof assume A1: r1<=r2; let x be set; assume x in left_closed_halfline(r1); then x in {r: r<=r1} by Def1 ; then consider r such that A2: r=x & r<=r1; r<=r2 by A1,A2,AXIOMS:22; then x in {g: g<=r2} by A2; hence thesis by Def1; end; theorem left_open_halfline(r) c= left_closed_halfline(r) proof let x be set; assume x in left_open_halfline(r); then x in {r2: r2<r} by PROB_1:def 15; then consider r1 such that A1: r1=x & r1<r; x in {g: g<=r} by A1; hence thesis by Def1; end; theorem ].g,r.[ c= left_open_halfline(r) proof let x be set; assume x in ].g,r.[; then x in {r1: g<r1 & r1<r} by RCOMP_1:def 2 ; then ex g1 st g1=x & g<g1 & g1<r; then x in {g2: g2<r}; hence thesis by PROB_1:def 15; end; theorem [.g,r.] c= left_closed_halfline(r) proof let x be set; assume x in [.g,r.]; then x in {r1: g<=r1 & r1<=r} by RCOMP_1:def 1; then ex g1 st g1=x & g<=g1 & g1<=r; then x in {g2: g2<=r}; hence thesis by Def1; end; theorem Th18: left_open_halfline(r) /\ right_open_halfline(g) = ].g,r.[ proof thus left_open_halfline(r)/\right_open_halfline(g)c=].g,r.[ proof let x be set; assume x in left_open_halfline(r)/\right_open_halfline(g) ; then A1: x in left_open_halfline(r) & x in right_open_halfline(g) by XBOOLE_0:def 3 ; then x in {r1: r1<r} by PROB_1:def 15; then A2: ex t1 be Real st t1=x & t1<r; x in {g1: g<g1} by A1,Def3; then ex g1 st g1=x & g<g1; then x in {g2: g<g2 & g2<r} by A2; hence x in ].g,r.[ by RCOMP_1:def 2; end; let x be set; assume x in ].g,r.[; then x in {r1: g<r1 & r1<r} by RCOMP_1:def 2 ; then A3: ex r2 st r2=x & g<r2 & r2<r; then x in {g1: g<g1}; then A4: x in right_open_halfline(g) by Def3; x in {g2: g2<r} by A3; then x in left_open_halfline(r) by PROB_1:def 15; hence thesis by A4,XBOOLE_0: def 3 ; end; theorem Th19: left_closed_halfline(r) /\ right_closed_halfline(g) = [.g,r.] proof thus left_closed_halfline(r)/\right_closed_halfline(g)c=[.g,r.] proof let x be set; assume x in left_closed_halfline(r)/\right_closed_halfline(g); then A1: x in left_closed_halfline(r) & x in right_closed_halfline(g) by XBOOLE_0:def 3 ; then x in {r1: r1<=r} by Def1; then A2: ex t1 be Real st t1=x & t1<=r; x in {g1: g<=g1} by A1,Def2; then ex g1 st g1=x & g<=g1; then x in {g2: g<=g2 & g2<=r} by A2; hence x in [.g,r.] by RCOMP_1:def 1; end; let x be set; assume x in [.g,r.]; then x in {r1: g<=r1 & r1<=r} by RCOMP_1:def 1 ; then A3: ex r2 st r2=x & g<=r2 & r2<=r; then x in {g1: g<=g1}; then A4: x in right_closed_halfline(g) by Def2; x in {g2: g2<=r} by A3; then x in left_closed_halfline(r) by Def1; hence thesis by A4,XBOOLE_0:def 3; end; theorem r<=r1 implies ].r1,r2.[ c= right_open_halfline(r) & [.r1,r2.] c= right_closed_halfline(r) proof assume A1: r<=r1; thus ].r1,r2.[c=right_open_halfline(r) proof let x be set; assume x in ].r1,r2.[; then x in {g: r1<g & g<r2} by RCOMP_1:def 2; then consider g1 such that A2: x=g1 & r1<g1 & g1<r2; r<g1 by A1,A2,AXIOMS:22 ; then x in {g2: r<g2} by A2; hence thesis by Def3; end; let x be set; assume x in [.r1,r2.]; then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1 ; then consider g1 such that A3: x=g1 & r1<=g1 & g1<=r2; r<= g1 by A1,A3,AXIOMS:22; then x in {g2: r<=g2} by A3; hence thesis by Def2; end; theorem r<r1 implies [.r1,r2.] c= right_open_halfline(r) proof assume A1: r<r1; let x be set; assume x in [.r1,r2.]; then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1; then consider g1 such that A2: x=g1 & r1<=g1 & g1<=r2; r<g1 by A1,A2,AXIOMS:22; then x in {g2: r<g2} by A2; hence thesis by Def3; end; theorem r2<=r implies ].r1,r2.[ c= left_open_halfline(r) & [.r1,r2.] c= left_closed_halfline(r) proof assume A1: r2<=r; thus ].r1,r2.[c=left_open_halfline(r) proof let x be set; assume x in ].r1,r2.[; then x in {g: r1<g & g<r2} by RCOMP_1:def 2; then consider g1 such that A2: x=g1 & r1<g1 & g1<r2; g1<r by A1,A2,AXIOMS:22 ; then x in {g2: g2<r} by A2; hence thesis by PROB_1:def 15; end; let x be set; assume x in [.r1,r2.]; then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1 ; then consider g1 such that A3: x=g1 & r1<=g1 & g1<=r2; g1<= r by A1,A3,AXIOMS:22; then x in {g2: g2<=r} by A3; hence thesis by Def1; end; theorem r2<r implies [.r1,r2.] c= left_open_halfline(r) proof assume A1: r2<r; let x be set; assume x in [.r1,r2.]; then x in {g: r1<=g & g<=r2} by RCOMP_1:def 1; then consider g1 such that A2: x=g1 & r1<=g1 & g1<=r2; g1<r by A1,A2,AXIOMS:22; then x in {g2: g2<r} by A2; hence thesis by PROB_1:def 15; end; theorem Th24: REAL \ right_open_halfline(r) = left_closed_halfline(r) & REAL \ right_closed_halfline(r) = left_open_halfline(r) & REAL \ left_open_halfline(r) = right_closed_halfline(r) & REAL \ left_closed_halfline(r) = right_open_halfline(r) proof now let x be set; thus x in REAL\right_open_halfline(r) implies x in left_closed_halfline(r) proof assume A1: x in REAL\right_open_halfline(r); then A2: x in REAL & not x in right_open_halfline(r) by XBOOLE_0:def 4; reconsider x'=x as Real by A1,XBOOLE_0:def 4; not x' in {g: r<g} by A2,Def3; then x'<=r; then x in {g1: g1<=r}; hence thesis by Def1; end; thus x in left_closed_halfline(r) implies x in REAL\right_open_halfline(r) proof assume x in left_closed_halfline(r); then x in {r2: r2<=r} by Def1; then A3: ex g2 st x=g2 & g2<=r; then not ex g2 st x=g2 & r<g2; then not x in {g1: r<g1}; then not x in right_open_halfline(r) by Def3; hence thesis by A3,XBOOLE_0:def 4; end; end; hence REAL\right_open_halfline(r)=left_closed_halfline(r) by TARSKI:2; now let x be set; thus x in REAL\right_closed_halfline(r) implies x in left_open_halfline(r) proof assume A4: x in REAL\right_closed_halfline(r); then A5: x in REAL & not x in right_closed_halfline(r) by XBOOLE_0:def 4; reconsider x'=x as Real by A4,XBOOLE_0:def 4; not x' in {g: r<=g} by A5,Def2 ; then x'<r; then x in {g1: g1<r}; hence thesis by PROB_1:def 15; end; thus x in left_open_halfline(r) implies x in REAL\right_closed_halfline(r) proof assume x in left_open_halfline(r); then x in {r2: r2<r} by PROB_1:def 15; then A6: ex g2 st x=g2 & g2<r; then not ex g1 st x=g1 & r<=g1; then not x in {g: r<=g}; then not x in right_closed_halfline(r) by Def2; hence thesis by A6,XBOOLE_0:def 4; end; end; hence REAL\right_closed_halfline(r)=left_open_halfline(r) by TARSKI:2; now let x be set; thus x in REAL\left_open_halfline(r) implies x in right_closed_halfline(r) proof assume A7: x in REAL\left_open_halfline(r); then A8: x in REAL & not x in left_open_halfline(r) by XBOOLE_0:def 4; reconsider x'=x as Real by A7,XBOOLE_0:def 4; not x' in {g: g<r} by A8,PROB_1:def 15; then r<=x'; then x in {g1: r<=g1}; hence thesis by Def2; end; thus x in right_closed_halfline(r) implies x in REAL\left_open_halfline(r) proof assume x in right_closed_halfline(r); then x in {r2: r<=r2} by Def2; then A9: ex g2 st x=g2 & r<=g2; then not ex g2 st x=g2 & g2<r; then not x in {g1: g1<r}; then not x in left_open_halfline(r) by PROB_1:def 15; hence thesis by A9,XBOOLE_0:def 4; end; end; hence REAL\left_open_halfline(r)=right_closed_halfline(r) by TARSKI:2; now let x be set; thus x in REAL\left_closed_halfline(r) implies x in right_open_halfline(r) proof assume A10: x in REAL\left_closed_halfline(r); then A11: x in REAL & not x in left_closed_halfline(r) by XBOOLE_0:def 4; reconsider x'=x as Real by A10,XBOOLE_0:def 4 ; not x' in {g: g<=r} by A11,Def1; then r<x'; then x in {g1: r<g1}; hence thesis by Def3; end; thus x in right_open_halfline(r) implies x in REAL\left_closed_halfline(r) proof assume x in right_open_halfline(r); then x in {r2: r<r2} by Def3; then A12: ex g2 st x=g2 & r<g2; then not ex g1 st x=g1 & g1<=r; then not x in {g: g<=r}; then not x in left_closed_halfline(r) by Def1; hence thesis by A12,XBOOLE_0:def 4; end; end; hence thesis by TARSKI:2; end; theorem REAL \ ].r1,r2.[ = left_closed_halfline(r1) \/ right_closed_halfline(r2) & REAL \ [.r1,r2.] = left_open_halfline(r1) \/ right_open_halfline(r2) proof thus REAL\].r1,r2.[=REAL\(left_open_halfline(r2)/\right_open_halfline(r1)) by Th18 .=(REAL\left_open_halfline(r2))\/(REAL\right_open_halfline(r1)) by XBOOLE_1:54 .=right_closed_halfline(r2)\/ (REAL\right_open_halfline(r1)) by Th24 .=left_closed_halfline(r1)\/ right_closed_halfline(r2) by Th24; thus REAL\[.r1,r2.]=REAL\(left_closed_halfline(r2)/\right_closed_halfline(r1) ) by Th19 .=(REAL\left_closed_halfline(r2))\/ (REAL\right_closed_halfline(r1)) by XBOOLE_1:54 .=right_open_halfline(r2)\/ (REAL\right_closed_halfline(r1)) by Th24 .=left_open_halfline(r1)\/ right_open_halfline(r2) by Th24; end; theorem Th26: (seq is non-decreasing implies seq is bounded_below) & (seq is non-increasing implies seq is bounded_above) proof thus seq is non-decreasing implies seq is bounded_below proof assume A1: seq is non-decreasing; take seq.0-1; let n; A2: seq.0-1<seq.0-0 by REAL_1:92; seq.0<=seq.n by A1,SEQM_3:21; hence thesis by A2,AXIOMS:22; end; assume A3: seq is non-increasing; take seq.0+1; let n; A4: seq.0+0<seq.0+1 by REAL_1:67; seq.n<=seq.0 by A3,SEQM_3:22; hence thesis by A4,AXIOMS:22; end; theorem Th27: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing implies for n holds seq.n<0 proof assume that A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing and A2: ex n st not seq.n<0; consider n such that A3: not seq.n<0 by A2; now per cases by A3; suppose A4: 0<seq.n; then consider n1 be Nat such that A5: for m st n1<=m holds abs(seq.m-0)<seq.n by A1,SEQ_2:def 7; n1<=n1+n by NAT_1:37; then A6: abs(seq.(n1+n)-0)<seq.n by A5; A7: n<=n1+n by NAT_1:37; then 0<seq.(n1+n) by A1,A4,SEQM_3:12; then seq.(n1+n)<seq.n by A6,ABSVALUE:def 1; hence contradiction by A1,A7,SEQM_3:12; suppose seq.n=0; hence contradiction by A1,SEQ_1:7; end; hence contradiction; end; theorem Th28: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing implies for n holds 0<seq.n proof assume that A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing and A2: ex n st not 0<seq.n; consider n such that A3: not 0<seq.n by A2; now per cases by A3; suppose A4: seq.n<0; then 0<-seq.n by REAL_1:26,50; then consider n1 be Nat such that A5: for m st n1<=m holds abs(seq.m-0)<-seq.n by A1,SEQ_2:def 7; n1<=n1+n by NAT_1:37; then A6: abs(seq.(n1+n)-0)<-seq.n by A5; A7: n<=n1+n by NAT_1:37; then seq.(n1+n)<0 by A1,A4,SEQM_3:14; then -seq.(n1+n)<-seq.n by A6,ABSVALUE:def 1; then seq.n<seq.(n1+n) by REAL_1 :50; hence contradiction by A1,A7,SEQM_3:14; suppose seq.n=0; hence contradiction by A1,SEQ_1:7; end; hence contradiction; end; theorem Th29: seq is convergent & 0<lim seq implies ex n st for m st n<=m holds 0<seq.m proof assume that A1: seq is convergent & 0<lim seq and A2: for n ex m st n<=m & not 0<seq.m; consider n such that A3: for m st n<=m holds abs(seq.m-lim seq)<lim seq by A1,SEQ_2:def 7; consider m such that A4: n<=m & not 0<seq.m by A2; A5: abs(seq.m-lim seq)<lim seq by A3,A4; now per cases by A4; suppose A6: seq.m<0; then seq.m-lim seq<0-0 by A1,REAL_1:92; then -(seq.m-lim seq)<lim seq by A5,ABSVALUE:def 1; then lim seq-seq.m<lim seq by XCMPLX_1:143; then lim seq<lim seq+seq.m by REAL_1:84; then lim seq - lim seq<seq.m by REAL_1:84; hence contradiction by A6,XCMPLX_1:14; suppose seq.m=0; then abs(-lim seq)<lim seq by A5,XCMPLX_1:150; then abs(lim seq)<lim seq by ABSVALUE:17; hence contradiction by A1,ABSVALUE:def 1; end; hence contradiction; end; theorem Th30: seq is convergent & 0<lim seq implies ex n st for m st n<=m holds (lim seq)/2<seq.m proof assume A1: seq is convergent & 0<lim seq; deffunc U(set) = (lim seq)/2; consider s1 be Real_Sequence such that A2: for n holds s1.n= U(n) from ExRealSeq; A3: s1 is constant by A2,SEQM_3:def 6; s1.0=(lim seq)/2 by A2; then lim(seq-s1)=lim seq-(lim seq)/2 by A1,A3,SEQ_4:59 .=(lim seq)/2+(lim seq)/2-(lim seq)/2 by XCMPLX_1:66 .=(lim seq)/2 by XCMPLX_1:26; then A4: 0<lim(seq-s1) by A1,SEQ_2:3; s1 is convergent by A3,SEQ_4:39; then seq-s1 is convergent by A1,SEQ_2:25 ; then consider n such that A5: for m st n<=m holds 0<(seq-s1).m by A4,Th29; take n; let m; assume n<=m; then 0<(seq-s1).m by A5; then 0<seq.m-s1.m by RFUNCT_2:6; then 0<seq.m-(lim seq)/2 by A2; then 0+(lim seq)/2<seq.m by REAL_1:86; hence thesis; end; definition let seq; attr seq is divergent_to+infty means :Def4: for r ex n st for m st n<=m holds r<seq.m; attr seq is divergent_to-infty means :Def5: for r ex n st for m st n<=m holds seq.m<r; end; canceled 2; theorem seq is divergent_to+infty or seq is divergent_to-infty implies ex n st for m st n<=m holds seq^\m is_not_0 proof assume A1: seq is divergent_to+infty or seq is divergent_to-infty; now per cases by A1; suppose seq is divergent_to+infty; then consider n such that A2: for m st n<=m holds 0<seq.m by Def4; take n; let m such that A3: n<=m; now let k; n<=k+m by A3,NAT_1:37; then 0<seq.(k+m) by A2; hence 0<>(seq^\m).k by SEQM_3:def 9; end; hence seq^\m is_not_0 by SEQ_1:7; suppose seq is divergent_to-infty; then consider n such that A4: for m st n<=m holds seq.m<0 by Def5; take n; let m such that A5: n<=m; now let k; n<=k+m by A5,NAT_1:37; then seq.(k+m)<0 by A4; hence (seq^\m).k<>0 by SEQM_3:def 9; end; hence seq^\m is_not_0 by SEQ_1:7; end; hence thesis; end; theorem Th34: (seq^\k is divergent_to+infty implies seq is divergent_to+infty) & (seq^\k is divergent_to-infty implies seq is divergent_to-infty) proof thus seq^\k is divergent_to+infty implies seq is divergent_to+infty proof assume A1: seq^\k is divergent_to+infty; let r; consider n1 be Nat such that A2: for m st n1<=m holds r<(seq^\k).m by A1,Def4; take n=n1+k; let m; assume n<=m; then consider n2 be Nat such that A3: m=n+n2 by NAT_1:28; A4: n1+n2+k=m by A3,XCMPLX_1:1; n1<=n1+n2 by NAT_1:37 ; then r<(seq^\k).(n1+n2) by A2; hence r<seq.m by A4,SEQM_3:def 9; end; assume A5: seq^\k is divergent_to-infty; let r; consider n1 be Nat such that A6: for m st n1<=m holds (seq^\k).m<r by A5,Def5; take n=n1+k; let m; assume n<=m; then consider n2 be Nat such that A7: m=n+n2 by NAT_1:28; A8: n1+n2+k=m by A7,XCMPLX_1:1; n1<=n1+n2 by NAT_1:37; then (seq^\k).(n1+n2 )< r by A6; hence seq.m<r by A8,SEQM_3:def 9; end; theorem Th35: seq1 is divergent_to+infty & seq2 is divergent_to+infty implies seq1+seq2 is divergent_to+infty proof assume A1: seq1 is divergent_to+infty & seq2 is divergent_to+infty; let r ; consider n1 be Nat such that A2: for m st n1<=m holds r/2<seq1.m by A1,Def4; consider n2 be Nat such that A3: for m st n2<=m holds r/2<seq2.m by A1,Def4; take n=max(n1,n2); let m such that A4: n<=m; n1<=n by SQUARE_1:46; then n1<=m by A4,AXIOMS:22; then A5: r/2<seq1.m by A2 ; n2<=n by SQUARE_1:46; then n2<=m by A4,AXIOMS:22; then r/2<seq2.m by A3; then r/2+r/2<seq1.m+seq2.m by A5,REAL_1:67; then r<seq1.m+seq2.m by XCMPLX_1: 66; hence thesis by SEQ_1:11; end; theorem Th36: seq1 is divergent_to+infty & seq2 is bounded_below implies seq1+seq2 is divergent_to+infty proof assume A1: seq1 is divergent_to+infty & seq2 is bounded_below; then consider M be real number such that A2: for n holds M<seq2.n by SEQ_2:def 4; let r; r-M is Real by XREAL_0:def 1; then consider n such that A3: for m st n<=m holds r-M<seq1.m by A1,Def4; take n; let m; assume n<=m; then A4: r-M<seq1.m by A3; M<seq2.m by A2; then r-M+M<seq1.m+seq2.m by A4,REAL_1:67; then r<seq1.m+seq2.m by XCMPLX_1:27; hence thesis by SEQ_1:11; end; theorem Th37: seq1 is divergent_to+infty & seq2 is divergent_to+infty implies seq1(#)seq2 is divergent_to+infty proof assume A1: seq1 is divergent_to+infty & seq2 is divergent_to+infty; let r ; consider n1 be Nat such that A2: for m st n1<=m holds sqrt abs(r)<seq1.m by A1,Def4; consider n2 be Nat such that A3: for m st n2<=m holds sqrt abs(r)<seq2.m by A1,Def4; take n=max(n1,n2); let m such that A4: n<=m; n1<=n by SQUARE_1:46; then n1<= m by A4,AXIOMS:22; then A5: sqrt abs(r)<seq1.m by A2; n2<=n by SQUARE_1:46; then n2<= m by A4,AXIOMS:22; then A6: sqrt abs(r)<seq2.m by A3; A7: abs(r)>=0 by ABSVALUE:5; then sqrt abs(r)>=0 by SQUARE_1:def 4; then (sqrt abs(r))*(sqrt abs(r))<seq1.m*seq2.m by A5,A6,SEQ_2:7; then (sqrt abs(r))^2<seq1.m*seq2.m by SQUARE_1:def 3; then A8: abs(r)<seq1.m*seq2.m by A7,SQUARE_1:def 4; r<=abs(r) by ABSVALUE:11; then r<seq1.m*seq2.m by A8,AXIOMS:22; hence thesis by SEQ_1:12; end; theorem Th38: seq1 is divergent_to-infty & seq2 is divergent_to-infty implies seq1+seq2 is divergent_to-infty proof assume A1: seq1 is divergent_to-infty & seq2 is divergent_to-infty; let r ; consider n1 be Nat such that A2: for m st n1<=m holds seq1.m<r/2 by A1,Def5; consider n2 be Nat such that A3: for m st n2<=m holds seq2.m<r/2 by A1,Def5; take n=max(n1,n2); let m such that A4: n<=m; n1<=n by SQUARE_1:46; then n1<=m by A4,AXIOMS:22; then A5: seq1.m<r/2 by A2 ; n2<=n by SQUARE_1:46; then n2<=m by A4,AXIOMS:22; then seq2.m<r/2 by A3; then seq1.m+seq2.m<r/2+r/2 by A5,REAL_1:67; then seq1.m+seq2.m<r by XCMPLX_1: 66; hence thesis by SEQ_1:11; end; theorem Th39: seq1 is divergent_to-infty & seq2 is bounded_above implies seq1+seq2 is divergent_to-infty proof assume A1: seq1 is divergent_to-infty & seq2 is bounded_above; then consider M be real number such that A2: for n holds seq2.n<M by SEQ_2:def 3; let r; r-M is Real by XREAL_0:def 1; then consider n such that A3: for m st n<=m holds seq1.m<r-M by A1,Def5; take n; let m; assume n<=m; then A4: seq1.m<r-M by A3; seq2.m<M by A2; then seq1.m+seq2.m<r-M+M by A4,REAL_1:67; then seq1.m+seq2.m<r by XCMPLX_1:27; hence thesis by SEQ_1:11; end; theorem Th40: (seq is divergent_to+infty & r>0 implies r(#)seq is divergent_to+infty) & (seq is divergent_to+infty & r<0 implies r(#)seq is divergent_to-infty) & (seq is divergent_to+infty & r=0 implies rng (r(#)seq)={0} & r(#) seq is constant) proof thus seq is divergent_to+infty & r>0 implies r(#)seq is divergent_to+infty proof assume A1: seq is divergent_to+infty & r>0; let g; consider n such that A2: for m st n<=m holds g/r<seq.m by A1,Def4; take n; let m; assume n<=m; then g/r<seq.m by A2; then g/r*r<r*seq.m by A1,REAL_1:70; then g<r*seq.m by A1,XCMPLX_1:88; hence thesis by SEQ_1:13; end; thus seq is divergent_to+infty & r<0 implies r(#)seq is divergent_to-infty proof assume A3: seq is divergent_to+infty & r<0; let g; consider n such that A4: for m st n<=m holds g/r<seq.m by A3,Def4; take n; let m; assume n<=m; then g/r<seq.m by A4; then r*seq.m<g/r*r by A3,REAL_1:71; then r*seq.m<g by A3,XCMPLX_1:88; hence thesis by SEQ_1:13; end; assume A5: seq is divergent_to+infty & r=0; thus rng(r(#)seq)={0} proof thus rng(r(#)seq)c={0} proof let x be set; assume x in rng(r(#)seq); then consider n such that A6: x=(r(#)seq).n by RFUNCT_2:9; x=r*seq.n by A6,SEQ_1:13 .=0 by A5; hence x in {0} by TARSKI:def 1; end; let x be set; assume x in {0}; then A7: x=0 by TARSKI:def 1; now thus (r(#)seq).0=r*seq.0 by SEQ_1:13 .=0 by A5; end; hence x in rng(r(#)seq) by A7,RFUNCT_2:9; end; hence thesis by SEQM_3:15; end; theorem Th41: (seq is divergent_to-infty & r>0 implies r(#)seq is divergent_to-infty) & (seq is divergent_to-infty & r<0 implies r(#)seq is divergent_to+infty) & (seq is divergent_to-infty & r=0 implies rng (r(#)seq)={0} & r(#) seq is constant) proof thus seq is divergent_to-infty & r>0 implies r(#)seq is divergent_to-infty proof assume A1: seq is divergent_to-infty & r>0; let g; consider n such that A2: for m st n<=m holds seq.m<g/r by A1,Def5; take n; let m; assume n<=m; then seq.m<g/r by A2; then r*seq.m<g/r*r by A1,REAL_1:70; then r*seq.m<g by A1,XCMPLX_1:88; hence thesis by SEQ_1:13; end; thus seq is divergent_to-infty & r<0 implies r(#)seq is divergent_to+infty proof assume A3: seq is divergent_to-infty & r<0; let g; consider n such that A4: for m st n<=m holds seq.m<g/r by A3,Def5; take n; let m; assume n<=m; then seq.m<g/r by A4; then g/r*r<r*seq.m by A3,REAL_1:71; then g<r*seq.m by A3,XCMPLX_1:88; hence thesis by SEQ_1:13; end; assume A5: seq is divergent_to-infty & r=0; thus rng(r(#)seq)={0} proof thus rng(r(#)seq)c={0} proof let x be set; assume x in rng(r(#)seq); then consider n such that A6: x=(r(#)seq).n by RFUNCT_2:9; x=r*seq.n by A6,SEQ_1:13 .=0 by A5; hence x in {0} by TARSKI:def 1; end; let x be set; assume x in {0}; then A7: x=0 by TARSKI:def 1; now thus (r(#)seq).0=r*seq.0 by SEQ_1:13 .=0 by A5; end; hence x in rng(r(#)seq) by A7,RFUNCT_2:9; end; hence thesis by SEQM_3:15; end; theorem (seq is divergent_to+infty implies -seq is divergent_to-infty) & (seq is divergent_to-infty implies -seq is divergent_to+infty) proof A1: (-1)(#)seq=-seq by SEQ_1:25; hence seq is divergent_to+infty implies -seq is divergent_to-infty by Th40; assume seq is divergent_to-infty; hence thesis by A1,Th41; end; theorem seq is bounded_below & seq1 is divergent_to-infty implies seq-seq1 is divergent_to+infty proof assume A1: seq is bounded_below & seq1 is divergent_to-infty; A2: (-1)(#)seq1+seq=seq+-seq1 by SEQ_1:25 .=seq-seq1 by SEQ_1:15; (-1)(#)seq1 is divergent_to+infty by A1,Th41; hence thesis by A1,A2,Th36; end; theorem seq is bounded_above & seq1 is divergent_to+infty implies seq-seq1 is divergent_to-infty proof assume A1: seq is bounded_above & seq1 is divergent_to+infty; A2: (-1)(#)seq1+seq=seq+-seq1 by SEQ_1:25 .=seq-seq1 by SEQ_1:15; (-1)(#)seq1 is divergent_to-infty by A1,Th40; hence thesis by A1,A2,Th39; end; theorem seq is divergent_to+infty & seq1 is convergent implies seq+seq1 is divergent_to+infty proof assume A1: seq is divergent_to+infty & seq1 is convergent; then seq1 is bounded by SEQ_2:27; then seq1 is bounded_below by SEQ_2:def 5; hence thesis by A1,Th36; end; theorem seq is divergent_to-infty & seq1 is convergent implies seq+seq1 is divergent_to-infty proof assume A1: seq is divergent_to-infty & seq1 is convergent; then seq1 is bounded by SEQ_2:27; then seq1 is bounded_above by SEQ_2:def 5; hence thesis by A1,Th39; end; theorem Th47: (for n holds seq.n=n) implies seq is divergent_to+infty proof assume A1: for n holds seq.n=n; let r; consider n such that A2: r<n by SEQ_4:10; take n; let m; assume n<=m; then r<m by A2,AXIOMS:22; hence r<seq.m by A1; end; theorem Th48: (for n holds seq.n=-n) implies seq is divergent_to-infty proof assume A1: for n holds seq.n=-n; deffunc U(Nat) = $1; consider s1 be Real_Sequence such that A2: for n holds s1.n=U(n) from ExRealSeq; s1 is divergent_to+infty by A2,Th47; then (-1)(#)s1 is divergent_to-infty by Th40; then A3: -s1 is divergent_to-infty by SEQ_1:25; now let n; thus (-s1).n=-s1.n by SEQ_1:14 .=-n by A2 .=seq.n by A1; end; hence thesis by A3,FUNCT_2:113; end; theorem Th49: seq1 is divergent_to+infty & (ex r st r>0 & for n holds seq2.n>=r) implies seq1(#)seq2 is divergent_to+infty proof assume A1: seq1 is divergent_to+infty & ex r st r>0 & for n holds seq2.n>=r; then consider M be Real such that A2: M>0 & for n holds seq2.n>=M; let r; consider n such that A3: for m st n<=m holds abs(r)/M<seq1.m by A1,Def4; take n; let m; assume n<=m; then A4: abs(r)/M<seq1.m by A3; A5: M<=seq2.m by A2; 0<=abs(r) by ABSVALUE:5; then abs(r)/M>=0 by A2,SQUARE_1:27; then abs(r)/M*M<seq1.m*seq2.m by A2,A4,A5,Th1; then A6: abs(r)<seq1.m*seq2.m by A2,XCMPLX_1:88; r<=abs(r) by ABSVALUE:11; then r<seq1.m*seq2.m by A6,AXIOMS:22; hence thesis by SEQ_1:12; end; theorem seq1 is divergent_to-infty & (ex r st 0<r & for n holds seq2.n>=r) implies seq1(#)seq2 is divergent_to-infty proof assume A1: seq1 is divergent_to-infty & (ex r st 0<r & for n holds seq2.n>=r); then (-1)(#)seq1 is divergent_to+infty by Th41; then A2: (-1)(#)seq1(#)seq2 is divergent_to+infty by A1,Th49; (-1)(#)((-1)(#)seq1(#)seq2)=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:26 .=1(#)(seq1(#)seq2) by Lm1,SEQ_1:31 .=seq1(#)seq2 by SEQ_1:35; hence thesis by A2,Th40; end; theorem Th51: seq1 is divergent_to-infty & seq2 is divergent_to-infty implies seq1(#)seq2 is divergent_to+infty proof assume A1: seq1 is divergent_to-infty & seq2 is divergent_to-infty; then A2: (-1)(#)seq1 is divergent_to+infty by Th41; A3: (-1)(#)seq2 is divergent_to+infty by A1,Th41; (-1)(#)seq1(#)((-1)(#)seq2)=(-1)(#)(seq1(#)((-1)(#)seq2)) by SEQ_1:26 .=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:27 .=1(#)(seq1(#)seq2) by Lm1,SEQ_1:31 .=seq1(#)seq2 by SEQ_1:35; hence thesis by A2,A3,Th37; end; theorem Th52: (seq is divergent_to+infty or seq is divergent_to-infty) implies abs(seq) is divergent_to+infty proof assume A1: seq is divergent_to+infty or seq is divergent_to-infty; let r; now per cases by A1; suppose seq is divergent_to+infty; then consider n such that A2: for m st n<=m holds abs(r)<seq.m by Def4; take n; let m; seq.m<=abs(seq.m) by ABSVALUE:11; then A3: seq.m<=abs(seq).m by SEQ_1:16; A4: r<=abs(r) by ABSVALUE:11; assume n<=m; then abs(r)<seq.m by A2; then r<seq.m by A4,AXIOMS:22; hence r<abs(seq).m by A3,AXIOMS:22; suppose seq is divergent_to-infty; then consider n such that A5: for m st n<=m holds seq.m<-r by Def5; take n; let m; -abs(seq.m)<=seq.m by ABSVALUE:11; then A6: -abs(seq).m<=seq.m by SEQ_1:16; assume n<=m; then seq.m<-r by A5; then -abs(seq).m<-r by A6,AXIOMS:22; hence r<abs(seq).m by REAL_1:50; end; hence thesis; end; theorem Th53: seq is divergent_to+infty & seq1 is_subsequence_of seq implies seq1 is divergent_to+infty proof assume A1: seq is divergent_to+infty & seq1 is_subsequence_of seq; then consider Ns be increasing Seq_of_Nat such that A2: seq1=seq*Ns by SEQM_3: def 10 ; let r; consider n such that A3: for m st n<=m holds r<seq.m by A1,Def4; take n; let m; A4: m<=Ns.m by SEQM_3:33; assume n<=m; then n<=Ns.m by A4,AXIOMS:22; then r<seq.(Ns.m) by A3; hence r<seq1.m by A2,SEQM_3:31; end; theorem Th54: seq is divergent_to-infty & seq1 is_subsequence_of seq implies seq1 is divergent_to-infty proof assume A1: seq is divergent_to-infty & seq1 is_subsequence_of seq; then consider Ns be increasing Seq_of_Nat such that A2: seq1=seq*Ns by SEQM_3: def 10 ; let r; consider n such that A3: for m st n<=m holds seq.m<r by A1,Def5; take n; let m; A4: m<=Ns.m by SEQM_3:33; assume n<=m; then n<=Ns.m by A4,AXIOMS:22; then seq.(Ns.m)<r by A3; hence seq1.m<r by A2,SEQM_3:31; end; theorem seq1 is divergent_to+infty & seq2 is convergent & 0<lim seq2 implies seq1(#)seq2 is divergent_to+infty proof assume A1: seq1 is divergent_to+infty & seq2 is convergent & 0<lim seq2; then consider n1 be Nat such that A2: for m st n1<=m holds (lim seq2)/2<seq2.m by Th30; seq1^\n1 is_subsequence_of seq1 by SEQM_3:47; then A3: seq1^\n1 is divergent_to+infty by A1,Th53; now thus 0<(lim seq2)/2 by A1,SEQ_2:3; let n; n1<=n+n1 by NAT_1:37; then (lim seq2)/2<seq2.(n+n1) by A2; hence (lim seq2)/2<=(seq2^\n1).n by SEQM_3:def 9; end; then (seq1^\n1)(#)(seq2^\n1) is divergent_to+infty by A3,Th49; then (seq1(#)seq2)^\n1 is divergent_to+infty by SEQM_3:42; hence thesis by Th34; end; theorem Th56: seq is non-decreasing & not seq is bounded_above implies seq is divergent_to+infty proof assume A1: seq is non-decreasing & not seq is bounded_above; let r; consider n such that A2: r+1<=seq.n by A1,SEQ_2:def 3; take n; let m; assume n<=m; then seq.n<=seq.m by A1,SEQM_3:12; then r+1<=seq.m by A2,AXIOMS:22; hence thesis by Lm2; end; theorem Th57: seq is non-increasing & not seq is bounded_below implies seq is divergent_to-infty proof assume A1: seq is non-increasing & not seq is bounded_below; let r; consider n such that A2: seq.n<=r-1 by A1,SEQ_2:def 4; take n; let m; assume n<=m; then seq.m<=seq.n by A1,SEQM_3:14; then seq.m<=r-1 by A2,AXIOMS:22; hence thesis by Lm2; end; theorem seq is increasing & not seq is bounded_above implies seq is divergent_to+infty proof assume A1: seq is increasing & not seq is bounded_above; then seq is non-decreasing by SEQM_3:23; hence thesis by A1,Th56; end; theorem seq is decreasing & not seq is bounded_below implies seq is divergent_to-infty proof assume A1: seq is decreasing & not seq is bounded_below; then seq is non-increasing by SEQM_3:24; hence thesis by A1,Th57; end; theorem seq is monotone implies seq is convergent or seq is divergent_to+infty or seq is divergent_to-infty proof assume A1: seq is monotone; now per cases by A1,SEQM_3:def 7; suppose A2: seq is non-decreasing; then A3: seq is bounded_below by Th26; now per cases; suppose seq is bounded_above; then A4: seq is bounded by A3,SEQ_2:def 5; seq is monotone by A2,SEQM_3:def 7; hence thesis by A4,SEQ_4:53; suppose not seq is bounded_above; hence thesis by A2,Th56; end; hence thesis; suppose A5: seq is non-increasing; then A6: seq is bounded_above by Th26; now per cases; suppose seq is bounded_below; then A7: seq is bounded by A6,SEQ_2:def 5; seq is monotone by A5,SEQM_3:def 7; hence thesis by A7,SEQ_4:53; suppose not seq is bounded_below; hence thesis by A5,Th57; end; hence thesis; end; hence thesis; end; theorem Th61: (seq is divergent_to+infty or seq is divergent_to-infty) implies seq" is convergent & lim(seq")=0 proof assume that A1: seq is divergent_to+infty or seq is divergent_to-infty; now per cases by A1; suppose A2: seq is divergent_to+infty; A3: now let r be real number such that A4: 0<r; r" is Real by XREAL_0:def 1; then consider n such that A5: for m st n<=m holds r"<seq.m by A2,Def4; take n; let m; A6: 0<r" by A4,REAL_1:72; assume n<=m; then A7: r"<seq.m by A5; then A8: 0<seq.m by A6,AXIOMS:22; 1/seq.m<1/r" by A6,A7,SEQ_2:10; then A9: 1/seq.m<r by XCMPLX_1:218; A10: 1/seq.m=(seq.m)" by XCMPLX_1:217; A11: 0<(seq.m)" by A8,REAL_1:72; (seq.m)"=(seq").m by SEQ_1:def 8; hence abs((seq").m-0)<r by A9,A10,A11,ABSVALUE:def 1; end; hence seq" is convergent by SEQ_2:def 6; hence thesis by A3,SEQ_2:def 7; suppose A12: seq is divergent_to-infty; A13: now let r be real number such that A14: 0<r; -(r") is Real by XREAL_0:def 1; then consider n such that A15: for m st n<=m holds seq.m<-(r") by A12,Def5; take n; let m; A16: 0<r" by A14,REAL_1:72; then A17: -(r")<0 by REAL_1:26,50; assume n<=m; then A18: seq.m<-(r") by A15; then A19: seq.m<0 by A16,REAL_1:26,50; A20: (-1)"=-1; 1/(-(r"))<1/seq.m by A17,A18,REAL_2:200; then (-(1*(r")))"<1/seq.m by XCMPLX_1:217; then ((-1)*(r"))"<1/seq.m by XCMPLX_1:175; then A21: (-1)*(r"")<1/seq.m by A20,XCMPLX_1:205; 1/seq.m<0/seq.m by A19,REAL_1:74; then abs(1/seq.m)=-(1/seq.m) by ABSVALUE:def 1; then -(1*r)<-abs(1/seq.m) by A21,XCMPLX_1:175; then abs(1/seq.m)<r by REAL_1 :50; then abs((seq.m)")<r by XCMPLX_1:217; hence abs((seq").m-0)<r by SEQ_1:def 8 ; end; hence seq" is convergent by SEQ_2:def 6; hence thesis by A13,SEQ_2:def 7 ; end; hence thesis; end; theorem Th62: seq is_not_0 & seq is convergent & lim seq=0 & (ex k st for n st k<=n holds 0<seq.n) implies seq" is divergent_to+infty proof assume A1: seq is_not_0 & seq is convergent & lim seq=0; given k such that A2: for n st k<=n holds 0<seq.n; let r; set l=abs(r)+1; 0<=abs(r) by ABSVALUE:5; then 0<l by Lm2; then 0<l" by REAL_1:72; then consider o be Nat such that A3: for n st o<=n holds abs(seq.n-0)<l" by A1,SEQ_2:def 7; r<=abs(r) by ABSVALUE:11; then A4: r<l by Lm2; take m=max(k,o); let n; assume A5: m<=n; o<=m by SQUARE_1:46; then o<=n by A5,AXIOMS:22; then A6: abs(seq.n-0)<l" by A3; k<=m by SQUARE_1:46; then k<=n by A5,AXIOMS:22; then A7: 0<seq.n by A2; then seq.n<l" by A6,ABSVALUE:def 1; then 1/(l")<1/seq.n by A7,SEQ_2:10; then l<1/seq.n by XCMPLX_1:218; then r<1/seq.n by A4,AXIOMS:22; then r<(seq.n)" by XCMPLX_1:217; hence r<(seq").n by SEQ_1:def 8; end; theorem Th63: seq is_not_0 & seq is convergent & lim seq=0 & (ex k st for n st k<=n holds seq.n<0) implies seq" is divergent_to-infty proof assume A1: seq is_not_0 & seq is convergent & lim seq=0; given k such that A2: for n st k<=n holds seq.n<0; let r; set l=abs(r)+1; 0<=abs(r) by ABSVALUE:5; then 0<l by Lm2; then 0<l" by REAL_1:72; then consider o be Nat such that A3: for n st o<=n holds abs(seq.n-0)<l" by A1,SEQ_2:def 7; -abs(r)<=r by ABSVALUE:11; then A4: -abs(r)-1<r by Lm2; A5: -l=-(1*l) .=(-1)*l by XCMPLX_1:175 .=(-1)*abs(r)+(-1)*1 by XCMPLX_1:8 .=-(1*abs(r))+(-1)*1 by XCMPLX_1:175 .=-abs(r)-1 by XCMPLX_0:def 8; take m=max(k,o); let n; assume A6: m<=n; o<=m by SQUARE_1:46; then o<=n by A6,AXIOMS:22; then A7: abs(seq.n-0)<l" by A3; k<=m by SQUARE_1:46 ; then k<= n by A6,AXIOMS:22; then A8: seq.n<0 by A2; then A9: 0<-(seq.n) by REAL_1:66; -(seq.n)<l" by A7,A8,ABSVALUE:def 1; then 1/(l")<1/(-(seq.n)) by A9,SEQ_2:10; then l<1/(-(seq.n)) by XCMPLX_1:218; then l<(-(seq.n))" by XCMPLX_1:217; then l<-((seq.n)") by XCMPLX_1:224; then --((seq.n)")<-l by REAL_1:50; then (seq.n)"<r by A4,A5,AXIOMS:22; hence (seq").n<r by SEQ_1:def 8; end; theorem Th64: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing implies seq" is divergent_to-infty proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-decreasing; then for n holds 0<=n implies seq.n<0 by Th27; hence thesis by A1,Th63; end; theorem Th65: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing implies seq" is divergent_to+infty proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is non-increasing; then for n holds 0<=n implies 0<seq.n by Th28; hence thesis by A1,Th62; end; theorem seq is_not_0 & seq is convergent & lim seq=0 & seq is increasing implies seq" is divergent_to-infty proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is increasing; then seq is non-decreasing by SEQM_3:23; hence thesis by A1,Th64; end; theorem seq is_not_0 & seq is convergent & lim seq=0 & seq is decreasing implies seq" is divergent_to+infty proof assume A1: seq is_not_0 & seq is convergent & lim seq=0 & seq is decreasing; then seq is non-increasing by SEQM_3:24; hence thesis by A1,Th65; end; theorem seq1 is bounded & (seq2 is divergent_to+infty or seq2 is divergent_to-infty) & seq2 is_not_0 implies seq1/"seq2 is convergent & lim(seq1/"seq2)=0 proof assume A1: seq1 is bounded & (seq2 is divergent_to+infty or seq2 is divergent_to-infty) & seq2 is_not_0; then A2: seq2" is convergent & lim(seq2")=0 by Th61; (seq2")(#) seq1=seq1/"seq2 by SEQ_1:def 9; hence thesis by A1,A2,SEQ_2:39,40; end; theorem Th69: seq is divergent_to+infty & (for n holds seq.n<=seq1.n) implies seq1 is divergent_to+infty proof assume A1: seq is divergent_to+infty & (for n holds seq.n<= seq1.n); let r; consider n such that A2: for m st n<=m holds r<seq.m by A1,Def4; take n; let m; A3: seq.m<=seq1.m by A1; assume n<=m; then r<seq.m by A2; hence r<seq1.m by A3,AXIOMS:22; end; theorem Th70: seq is divergent_to-infty & (for n holds seq1.n<=seq.n) implies seq1 is divergent_to-infty proof assume A1: seq is divergent_to-infty & (for n holds seq1.n<= seq.n); let r; consider n such that A2: for m st n<=m holds seq.m<r by A1,Def5; take n; let m; A3: seq1.m<=seq.m by A1; assume n<=m; then seq.m<r by A2; hence seq1.m<r by A3,AXIOMS:22; end; definition let f; attr f is convergent_in+infty means :Def6: (for r ex g st r<g & g in dom f) & ex g st for seq st seq is divergent_to+infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=g; attr f is divergent_in+infty_to+infty means :Def7: (for r ex g st r<g & g in dom f) & for seq st seq is divergent_to+infty & rng seq c= dom f holds f*seq is divergent_to+infty; attr f is divergent_in+infty_to-infty means :Def8: (for r ex g st r<g & g in dom f) & for seq st seq is divergent_to+infty & rng seq c= dom f holds f*seq is divergent_to-infty; attr f is convergent_in-infty means :Def9: (for r ex g st g<r & g in dom f) & ex g st for seq st seq is divergent_to-infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=g; attr f is divergent_in-infty_to+infty means :Def10: (for r ex g st g<r & g in dom f) & for seq st seq is divergent_to-infty & rng seq c= dom f holds f*seq is divergent_to+infty; attr f is divergent_in-infty_to-infty means :Def11: (for r ex g st g<r & g in dom f) & for seq st seq is divergent_to-infty & rng seq c= dom f holds f*seq is divergent_to-infty; end; canceled 6; theorem f is convergent_in+infty iff (for r ex g st r<g & g in dom f) & (ex g st for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1) proof thus f is convergent_in+infty implies (for r ex g st r<g & g in dom f) & (ex g st for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1) proof assume A1: f is convergent_in+infty; then consider g2 such that A2: for seq st seq is divergent_to+infty & rng seq c=dom f holds f*seq is convergent & lim(f*seq)=g2 by Def6; assume not (for r ex g st r<g & g in dom f) or for g ex g1 st 0<g1 & for r ex r1 st r<r1 & r1 in dom f & abs(f.r1-g)>=g1; then consider g such that A3: 0<g & for r ex r1 st r<r1 & r1 in dom f & abs(f.r1-g2)>=g by A1,Def6; defpred X[Nat,real number] means $1<$2 & $2 in dom f & abs(f.$2-g2)>=g; A4: now let n; consider r such that A5: n<r & r in dom f & abs(f.r-g2)>=g by A3; reconsider r as real number; take r; thus X[n,r] by A5; end; consider s be Real_Sequence such that A6: for n holds X[n,s.n] from RealSeqChoice(A4); deffunc U(Nat) = $1; consider s1 be Real_Sequence such that A7: for n holds s1.n=U(n) from ExRealSeq; A8: s1 is divergent_to+infty by A7,Th47; now let n; n<s.n by A6; hence s1.n<=s.n by A7;end; then A9: s is divergent_to+infty by A8,Th69; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A6; end; then A10: rng s c=dom f by TARSKI:def 3; then f*s is convergent & lim(f*s)=g2 by A2,A9; then consider n such that A11: for m st n<=m holds abs((f*s).m-g2)<g by A3,SEQ_2:def 7; abs((f*s).n-g2)<g by A11; then abs(f.(s.n)-g2)<g by A10,RFUNCT_2:21; hence contradiction by A6; end; assume A12: for r ex g st r<g & g in dom f; given g such that A13: for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1; now let s be Real_Sequence such that A14: s is divergent_to+infty & rng s c=dom f; A15: now let g1 be real number; A16: g1 is Real by XREAL_0:def 1; assume 0<g1; then consider r such that A17: for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1 by A13,A16; consider n such that A18: for m st n<=m holds r<s.m by A14,Def4; take n; let m; assume n<=m; then A19: r<s.m by A18; s.m in rng s by RFUNCT_2:10; then abs(f.(s.m)-g)<g1 by A14,A17,A19; hence abs((f*s).m-g)<g1 by A14,RFUNCT_2:21; end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A15,SEQ_2:def 7; end; hence thesis by A12,Def6; end; theorem f is convergent_in-infty iff (for r ex g st g<r & g in dom f) & ex g st for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1 proof thus f is convergent_in-infty implies (for r ex g st g<r & g in dom f) & (ex g st for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1) proof assume A1: f is convergent_in-infty; then consider g2 such that A2: for seq st seq is divergent_to-infty & rng seq c=dom f holds f*seq is convergent & lim(f*seq)=g2 by Def9; assume not (for r ex g st g<r & g in dom f) or for g ex g1 st 0<g1 & for r ex r1 st r1<r & r1 in dom f & abs(f.r1-g)>=g1; then consider g such that A3: 0<g & for r ex r1 st r1<r & r1 in dom f & abs(f.r1-g2)>=g by A1,Def9; defpred X[Nat,real number] means $2<-$1 & $2 in dom f & abs(f.$2-g2)>=g; A4: now let n; consider r such that A5: r<-n & r in dom f & abs(f.r-g2)>=g by A3; reconsider r as real number; take r; thus X[n,r] by A5; end; consider s be Real_Sequence such that A6: for n holds X[n,s.n] from RealSeqChoice(A4); deffunc U(Nat) = -$1; consider s1 be Real_Sequence such that A7: for n holds s1.n=U(n) from ExRealSeq; A8: s1 is divergent_to-infty by A7,Th48; now let n; s.n<-n by A6; hence s.n<=s1.n by A7;end; then A9: s is divergent_to-infty by A8,Th70; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A6; end; then A10: rng s c=dom f by TARSKI:def 3; then f*s is convergent & lim(f*s)=g2 by A2,A9; then consider n such that A11: for m st n<=m holds abs((f*s).m-g2)<g by A3, SEQ_2:def 7; abs((f*s).n-g2)<g by A11; then abs(f.(s.n)-g2)<g by A10,RFUNCT_2:21; hence contradiction by A6; end; assume A12: for r ex g st g<r & g in dom f; given g such that A13: for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1; now let s be Real_Sequence such that A14: s is divergent_to-infty & rng s c=dom f; A15: now let g1 be real number; A16: g1 is Real by XREAL_0:def 1; assume 0<g1; then consider r such that A17: for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1 by A13,A16; consider n such that A18: for m st n<=m holds s.m<r by A14,Def5; take n; let m; assume n<=m; then A19: s.m<r by A18; s.m in rng s by RFUNCT_2:10; then abs(f.(s.m)-g)<g1 by A14,A17,A19; hence abs((f*s).m-g)<g1 by A14,RFUNCT_2:21; end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A15,SEQ_2: def 7; end; hence thesis by A12,Def9; end; theorem f is divergent_in+infty_to+infty iff (for r ex g st r<g & g in dom f) & for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1 proof thus f is divergent_in+infty_to+infty implies (for r ex g st r<g & g in dom f) & (for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1) proof assume A1: f is divergent_in+infty_to+infty; assume not (for r ex g st r<g & g in dom f) or ex g st for r ex r1 st r<r1 & r1 in dom f & g>=f.r1; then consider g such that A2: for r ex r1 st r<r1 & r1 in dom f & g>=f.r1 by A1,Def7; defpred X[Nat,real number] means $1<$2 & $2 in dom f & g >= f.$2; A3: now let n; consider r such that A4: n<r & r in dom f & g>=f.r by A2; reconsider r as real number; take r; thus X[n,r] by A4; end; consider s be Real_Sequence such that A5: for n holds X[n,s.n] from RealSeqChoice(A3); deffunc U(Nat) = $1; consider s1 be Real_Sequence such that A6: for n holds s1.n=U(n) from ExRealSeq; A7: s1 is divergent_to+infty by A6,Th47; now let n; n<s.n by A5; hence s1.n<=s.n by A6;end; then A8: s is divergent_to+infty by A7,Th69; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A5; end; then A9: rng s c=dom f by TARSKI:def 3; then f*s is divergent_to+infty by A1,A8,Def7; then consider n such that A10: for m st n<=m holds g<(f*s).m by Def4; g<(f*s).n by A10; then g<f.(s.n) by A9,RFUNCT_2:21; hence contradiction by A5 ; end; assume that A11: for r ex g st r<g & g in dom f and A12: for g ex r st for r1 st r<r1 & r1 in dom f holds g<f.r1; now let s be Real_Sequence such that A13: s is divergent_to+infty & rng s c=dom f; now let g; consider r such that A14: for r1 st r<r1 & r1 in dom f holds g<f.r1 by A12; consider n such that A15: for m st n<=m holds r<s.m by A13,Def4; take n; let m; assume n<=m; then A16: r<s.m by A15; s.m in rng s by RFUNCT_2:10; then g<f.(s.m) by A13,A14,A16; hence g<(f*s).m by A13,RFUNCT_2:21; end; hence f*s is divergent_to+infty by Def4; end; hence thesis by A11,Def7; end; theorem f is divergent_in+infty_to-infty iff (for r ex g st r<g & g in dom f) & for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g proof thus f is divergent_in+infty_to-infty implies (for r ex g st r<g & g in dom f) & (for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g) proof assume A1: f is divergent_in+infty_to-infty; assume not (for r ex g st r<g & g in dom f) or ex g st for r ex r1 st r<r1 & r1 in dom f & f.r1>=g; then consider g such that A2: for r ex r1 st r<r1 & r1 in dom f & f.r1>=g by A1,Def8; defpred X[Nat,real number] means $1<$2 & $2 in dom f & g <= f.$2; A3: now let n; consider r such that A4: n<r & r in dom f & f.r>=g by A2; reconsider r as real number; take r; thus X[n,r] by A4; end; consider s be Real_Sequence such that A5: for n holds X[n,s.n] from RealSeqChoice(A3); deffunc U(Nat) = $1; consider s1 be Real_Sequence such that A6: for n holds s1.n=U(n) from ExRealSeq; A7: s1 is divergent_to+infty by A6,Th47; now let n; n<s.n by A5; hence s1.n<=s.n by A6;end; then A8: s is divergent_to+infty by A7,Th69; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A5; end; then A9: rng s c=dom f by TARSKI:def 3; then f*s is divergent_to-infty by A1,A8,Def8; then consider n such that A10: for m st n<=m holds (f*s).m<g by Def5; (f*s).n<g by A10; then f.(s.n)<g by A9,RFUNCT_2:21; hence contradiction by A5 ; end; assume that A11: for r ex g st r<g & g in dom f and A12: for g ex r st for r1 st r<r1 & r1 in dom f holds f.r1<g; now let s be Real_Sequence such that A13: s is divergent_to+infty & rng s c=dom f; now let g; consider r such that A14: for r1 st r<r1 & r1 in dom f holds f.r1<g by A12; consider n such that A15: for m st n<=m holds r<s.m by A13,Def4; take n; let m; assume n<=m; then A16: r<s.m by A15; s.m in rng s by RFUNCT_2:10; then f.(s.m)<g by A13,A14,A16; hence (f*s).m<g by A13,RFUNCT_2:21; end; hence f*s is divergent_to-infty by Def5; end; hence thesis by A11,Def8; end; theorem f is divergent_in-infty_to+infty iff (for r ex g st g<r & g in dom f) & for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1 proof thus f is divergent_in-infty_to+infty implies (for r ex g st g<r & g in dom f) & (for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1) proof assume A1: f is divergent_in-infty_to+infty; assume not (for r ex g st g<r & g in dom f) or ex g st for r ex r1 st r1<r & r1 in dom f & g>=f.r1; then consider g such that A2: for r ex r1 st r1<r & r1 in dom f & g>=f.r1 by A1,Def10; defpred X[Nat,real number] means $2<-$1 & $2 in dom f & g >= f.$2; A3: now let n; consider r such that A4: r<-n & r in dom f & g>=f.r by A2; reconsider r as real number; take r; thus X[n,r] by A4; end; consider s be Real_Sequence such that A5: for n holds X[n,s.n] from RealSeqChoice(A3); deffunc U(Nat) = -$1; consider s1 be Real_Sequence such that A6: for n holds s1.n=U(n) from ExRealSeq; A7: s1 is divergent_to-infty by A6,Th48; now let n; s.n<-n by A5; hence s.n<=s1.n by A6;end; then A8: s is divergent_to-infty by A7,Th70; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A5; end; then A9: rng s c=dom f by TARSKI:def 3; then f*s is divergent_to+infty by A1,A8,Def10; then consider n such that A10: for m st n<=m holds g<(f*s).m by Def4; g<(f*s).n by A10; then g<f.(s.n) by A9,RFUNCT_2:21; hence contradiction by A5; end; assume that A11: for r ex g st g<r & g in dom f and A12: for g ex r st for r1 st r1<r & r1 in dom f holds g<f.r1; now let s be Real_Sequence such that A13: s is divergent_to-infty & rng s c=dom f; now let g; consider r such that A14: for r1 st r1<r & r1 in dom f holds g<f.r1 by A12; consider n such that A15: for m st n<=m holds s.m<r by A13,Def5; take n; let m; assume n<=m; then A16: s.m<r by A15; s.m in rng s by RFUNCT_2:10; then g<f.(s.m) by A13,A14,A16; hence g<(f*s).m by A13,RFUNCT_2:21; end; hence f*s is divergent_to+infty by Def4; end; hence thesis by A11,Def10; end; theorem f is divergent_in-infty_to-infty iff (for r ex g st g<r & g in dom f) & for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g proof thus f is divergent_in-infty_to-infty implies (for r ex g st g<r & g in dom f) & (for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g) proof assume A1: f is divergent_in-infty_to-infty; assume not (for r ex g st g<r & g in dom f) or ex g st for r ex r1 st r1<r & r1 in dom f & f.r1>=g; then consider g such that A2: for r ex r1 st r1<r & r1 in dom f & f.r1>=g by A1,Def11; defpred X[Nat,real number] means $2<-$1 & $2 in dom f & g <= f.$2; A3: now let n; consider r such that A4: r<-n & r in dom f & f.r>=g by A2; reconsider r as real number; take r; thus X[n,r] by A4; end; consider s be Real_Sequence such that A5: for n holds X[n,s.n] from RealSeqChoice(A3); deffunc U(Nat) = -$1; consider s1 be Real_Sequence such that A6: for n holds s1.n=U(n) from ExRealSeq; A7: s1 is divergent_to-infty by A6,Th48; now let n; s.n<-n by A5; hence s.n<=s1.n by A6;end; then A8: s is divergent_to-infty by A7,Th70; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A5; end; then A9: rng s c=dom f by TARSKI:def 3; then f*s is divergent_to-infty by A1,A8,Def11; then consider n such that A10: for m st n<=m holds (f*s).m<g by Def5; (f*s).n<g by A10; then f.(s.n)<g by A9,RFUNCT_2:21; hence contradiction by A5; end; assume that A11: for r ex g st g<r & g in dom f and A12: for g ex r st for r1 st r1<r & r1 in dom f holds f.r1<g; now let s be Real_Sequence such that A13: s is divergent_to-infty & rng s c=dom f; now let g; consider r such that A14: for r1 st r1<r & r1 in dom f holds f.r1<g by A12; consider n such that A15: for m st n<=m holds s.m<r by A13,Def5; take n; let m; assume n<=m; then A16: s.m<r by A15; s.m in rng s by RFUNCT_2:10; then f.(s.m)<g by A13,A14,A16; hence (f*s).m<g by A13,RFUNCT_2:21; end; hence f*s is divergent_to-infty by Def5; end; hence thesis by A11,Def11; end; theorem f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom f1 /\ dom f2) implies f1+f2 is divergent_in+infty_to+infty & f1(#)f2 is divergent_in+infty_to+infty proof assume A1: f1 is divergent_in+infty_to+infty & f2 is divergent_in+infty_to+infty & for r ex g st r<g & g in dom f1/\dom f2; A2: now let r; consider g such that A3: r<g & g in dom f1/\dom f2 by A1; take g; thus r<g & g in dom(f1+f2) by A3,SEQ_1:def 3; end; now let seq; assume A4: seq is divergent_to+infty & rng seq c=dom(f1+f2); then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; then A6: f1*seq is divergent_to+infty by A1,A4,Def7; f2*seq is divergent_to+infty by A1,A4,A5,Def7; then f1*seq+f2*seq is divergent_to+infty by A6,Th35; hence (f1+f2)*seq is divergent_to+infty by A4,A5,RFUNCT_2:23; end; hence f1+f2 is divergent_in+infty_to+infty by A2,Def7; A7: now let r; consider g such that A8: r<g & g in dom f1/\dom f2 by A1; take g; thus r<g & g in dom(f1(#)f2) by A8,SEQ_1:def 5; end; now let seq; assume A9: seq is divergent_to+infty & rng seq c=dom(f1(#) f2); then A10: dom(f1(#)f2)=dom f1/\ dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; then A11: f1*seq is divergent_to+infty by A1,A9,Def7; f2*seq is divergent_to+infty by A1,A9,A10,Def7; then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th37; hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23; end; hence thesis by A7,Def7; end; theorem f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty & (for r ex g st r<g & g in dom f1 /\ dom f2) implies f1+f2 is divergent_in+infty_to-infty & f1(#)f2 is divergent_in+infty_to+infty proof assume A1: f1 is divergent_in+infty_to-infty & f2 is divergent_in+infty_to-infty & for r ex g st r<g & g in dom f1/\dom f2; A2: now let r; consider g such that A3: r<g & g in dom f1/\dom f2 by A1; take g; thus r<g & g in dom(f1+f2) by A3,SEQ_1:def 3; end; now let seq; assume A4: seq is divergent_to+infty & rng seq c=dom(f1+f2); then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; then A6: f1*seq is divergent_to-infty by A1,A4,Def8; f2*seq is divergent_to-infty by A1,A4,A5,Def8; then f1*seq+f2*seq is divergent_to-infty by A6,Th38; hence (f1+f2)*seq is divergent_to-infty by A4,A5,RFUNCT_2:23; end; hence f1+f2 is divergent_in+infty_to-infty by A2,Def8; A7: now let r; consider g such that A8: r<g & g in dom f1/\dom f2 by A1; take g; thus r<g & g in dom(f1(#)f2) by A8,SEQ_1:def 5; end; now let seq; assume A9: seq is divergent_to+infty & rng seq c=dom(f1(#) f2); then A10: dom(f1(#)f2)=dom f1/\ dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; then A11: f1*seq is divergent_to-infty by A1,A9,Def8; f2*seq is divergent_to-infty by A1,A9,A10,Def8; then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th51; hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23; end; hence thesis by A7,Def7; end; theorem f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom f1 /\ dom f2) implies f1+f2 is divergent_in-infty_to+infty & f1(#)f2 is divergent_in-infty_to+infty proof assume A1: f1 is divergent_in-infty_to+infty & f2 is divergent_in-infty_to+infty & for r ex g st g<r & g in dom f1/\dom f2; A2: now let r; consider g such that A3: g<r & g in dom f1/\dom f2 by A1; take g; thus g<r & g in dom(f1+f2) by A3,SEQ_1:def 3; end; now let seq; assume A4: seq is divergent_to-infty & rng seq c=dom(f1+f2); then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; then A6: f1*seq is divergent_to+infty by A1,A4,Def10; f2*seq is divergent_to+infty by A1,A4,A5,Def10; then f1*seq+f2*seq is divergent_to+infty by A6,Th35; hence (f1+f2)*seq is divergent_to+infty by A4,A5,RFUNCT_2:23; end; hence f1+f2 is divergent_in-infty_to+infty by A2,Def10; A7: now let r; consider g such that A8: g<r & g in dom f1/\dom f2 by A1; take g; thus g<r & g in dom(f1(#)f2) by A8,SEQ_1:def 5; end; now let seq; assume A9: seq is divergent_to-infty & rng seq c=dom(f1(#) f2); then A10: dom(f1(#)f2)=dom f1/\ dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; then A11: f1*seq is divergent_to+infty by A1,A9,Def10; f2*seq is divergent_to+infty by A1,A9,A10,Def10; then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th37; hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23; end; hence thesis by A7,Def10; end; theorem f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & (for r ex g st g<r & g in dom f1 /\ dom f2) implies f1+f2 is divergent_in-infty_to-infty & f1(#)f2 is divergent_in-infty_to+infty proof assume A1: f1 is divergent_in-infty_to-infty & f2 is divergent_in-infty_to-infty & for r ex g st g<r & g in dom f1/\dom f2; A2: now let r; consider g such that A3: g<r & g in dom f1/\dom f2 by A1; take g; thus g<r & g in dom(f1+f2) by A3,SEQ_1:def 3; end; now let seq; assume A4: seq is divergent_to-infty & rng seq c=dom(f1+f2); then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; then A6: f1*seq is divergent_to-infty by A1,A4,Def11; f2*seq is divergent_to-infty by A1,A4,A5,Def11; then f1*seq+f2*seq is divergent_to-infty by A6,Th38; hence (f1+f2)*seq is divergent_to-infty by A4,A5,RFUNCT_2:23; end; hence f1+f2 is divergent_in-infty_to-infty by A2,Def11; A7: now let r; consider g such that A8: g<r & g in dom f1/\dom f2 by A1; take g; thus g<r & g in dom(f1(#)f2) by A8,SEQ_1:def 5; end; now let seq; assume A9: seq is divergent_to-infty & rng seq c=dom(f1(#) f2); then A10: dom(f1(#)f2)=dom f1/\ dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; then A11: f1*seq is divergent_to-infty by A1,A9,Def11; f2*seq is divergent_to-infty by A1,A9,A10,Def11; then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,Th51; hence (f1(#)f2)*seq is divergent_to+infty by A9,A10,RFUNCT_2:23; end; hence thesis by A7,Def10; end; theorem f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom(f1+f2)) & (ex r st f2 is_bounded_below_on right_open_halfline(r)) implies f1+f2 is divergent_in+infty_to+infty proof assume A1: f1 is divergent_in+infty_to+infty & for r ex g st r<g & g in dom(f1+f2); given r1 such that A2: f2 is_bounded_below_on right_open_halfline(r1); now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom(f1+f2); then A4: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; consider k such that A5: for n st k<=n holds r1<seq.n by A3,Def4; seq^\k is_subsequence_of seq by SEQM_3:47; then A6: seq^\k is divergent_to+infty by A3,Th53; A7: rng(seq^\k)c=rng seq by RFUNCT_2:7; then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1; then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def7; consider r2 be real number such that A10:for g st g in right_open_halfline(r1)/\dom f2 holds r2<=f2.g by A2,RFUNCT_1:def 10; now let n; A11: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37; then r1<seq.(n+k) by A5; then r1<(seq^\k).n by SEQM_3:def 9; then (seq^\k).n in {g2: r1<g2}; then (seq^\k).n in right_open_halfline(r1) by Def3; then (seq^\k).n in right_open_halfline(r1)/\dom f2 by A8,A11,XBOOLE_0:def 3 ; then r2<=f2.((seq^\k).n) by A10; then A12: r2<=(f2*(seq^\k)).n by A8, RFUNCT_2:21; -abs(r2)<=r2 by ABSVALUE:11; then -abs(r2)-1<r2-0 by REAL_1:92; hence -abs(r2)-1<(f2*(seq^\k)).n by A12,AXIOMS:22; end; then f2*(seq^\k) is bounded_below by SEQ_2:def 4; then A13: f1*(seq^\k)+f2*(seq^\k) is divergent_to+infty by A9,Th36; rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1; then f1*(seq^\k)+f2*(seq^\k)=(f1+f2)*(seq^\k) by RFUNCT_2:23 .=((f1+f2)*seq)^\k by A3,RFUNCT_2:22; hence (f1+f2)*seq is divergent_to+infty by A13,Th34; end; hence thesis by A1,Def7; end; theorem f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom(f1(#)f2)) & (ex r,r1 st 0<r & for g st g in dom f2 /\ right_open_halfline(r1) holds r<=f2.g) implies f1(#)f2 is divergent_in+infty_to+infty proof assume A1: f1 is divergent_in+infty_to+infty & for r ex g st r<g & g in dom(f1(#)f2); given r2,r1 such that A2: 0<r2 & for g st g in dom f2/\right_open_halfline(r1) holds r2<=f2.g; now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom(f1(#) f2); then A4: dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; consider k such that A5: for n st k<=n holds r1<seq.n by A3,Def4; seq^\k is_subsequence_of seq by SEQM_3:47; then A6: seq^\k is divergent_to+infty by A3,Th53; A7: rng(seq^\k)c=rng seq by RFUNCT_2:7; then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1; then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def7; now thus 0<r2 by A2; let n; A10: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37; then r1<seq.(n+k) by A5; then r1<(seq^\k).n by SEQM_3:def 9; then (seq^\k).n in {g2: r1<g2}; then (seq^\k).n in right_open_halfline(r1) by Def3; then (seq^\k).n in dom f2/\right_open_halfline(r1) by A8,A10,XBOOLE_0:def 3 ; then r2<=f2.((seq^\k).n) by A2; hence r2<=(f2*(seq^\k)).n by A8,RFUNCT_2:21; end; then A11: (f1*(seq^\k))(#)(f2*(seq^\k)) is divergent_to+infty by A9,Th49; rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1; then (f1*(seq^\k))(#)(f2*(seq^\k))=(f1(#)f2)*(seq^\k) by RFUNCT_2:23 .=((f1(#)f2)*seq)^\k by A3,RFUNCT_2:22; hence (f1(#)f2)*seq is divergent_to+infty by A11,Th34; end; hence thesis by A1,Def7; end; theorem f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom(f1+f2)) & (ex r st f2 is_bounded_below_on left_open_halfline(r)) implies f1+f2 is divergent_in-infty_to+infty proof assume A1: f1 is divergent_in-infty_to+infty & for r ex g st g<r & g in dom(f1+f2); given r1 such that A2: f2 is_bounded_below_on left_open_halfline(r1); now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom(f1+f2); then A4: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; consider k such that A5: for n st k<=n holds seq.n<r1 by A3,Def5; seq^\k is_subsequence_of seq by SEQM_3:47; then A6: seq^\k is divergent_to-infty by A3,Th54; A7: rng(seq^\k)c=rng seq by RFUNCT_2:7; then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1; then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def10; consider r2 be real number such that A10:for g st g in left_open_halfline(r1)/\dom f2 holds r2<=f2.g by A2,RFUNCT_1:def 10; now let n; A11: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; k<=n+k by NAT_1: 37; then seq.(n+k)<r1 by A5; then (seq^\k).n<r1 by SEQM_3:def 9; then (seq^\k).n in {g2: g2<r1}; then (seq^\k).n in left_open_halfline(r1) by PROB_1:def 15; then (seq^\k).n in left_open_halfline(r1)/\dom f2 by A8,A11,XBOOLE_0:def 3; then r2<=f2.((seq^\k).n) by A10; then A12: r2<=(f2*(seq^\k)).n by A8, RFUNCT_2:21; -abs(r2)<=r2 by ABSVALUE:11; then -abs(r2)-1<r2-0 by REAL_1:92; hence -abs(r2)-1<(f2*(seq^\k)).n by A12,AXIOMS:22; end; then f2*(seq^\k) is bounded_below by SEQ_2:def 4; then A13: f1*(seq^\k)+f2*(seq^\k) is divergent_to+infty by A9,Th36; rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1; then f1*(seq^\k)+f2*(seq^\k)=(f1+f2)*(seq^\k) by RFUNCT_2:23 .=((f1+f2)*seq)^\k by A3,RFUNCT_2:22; hence (f1+f2)*seq is divergent_to+infty by A13,Th34; end; hence thesis by A1,Def10; end; theorem f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom(f1(#)f2)) & (ex r,r1 st 0<r & for g st g in dom f2 /\ left_open_halfline(r1) holds r<=f2.g) implies f1(#)f2 is divergent_in-infty_to+infty proof assume A1: f1 is divergent_in-infty_to+infty & for r ex g st g<r & g in dom(f1(#)f2); given r2,r1 such that A2: 0<r2 & for g st g in dom f2/\left_open_halfline(r1) holds r2<=f2.g; now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom(f1(#) f2); then A4: dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; consider k such that A5: for n st k<=n holds seq.n<r1 by A3,Def5; seq^\k is_subsequence_of seq by SEQM_3:47; then A6: seq^\k is divergent_to-infty by A3,Th54; A7: rng(seq^\k)c=rng seq by RFUNCT_2:7; then A8: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A4,XBOOLE_1:1; then A9: f1*(seq^\k) is divergent_to+infty by A1,A6,Def10; now thus 0<r2 by A2; let n; A10: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then seq.(n+k)<r1 by A5; then (seq^\k).n<r1 by SEQM_3:def 9; then (seq^\k).n in {g2: g2<r1}; then (seq^\k).n in left_open_halfline(r1) by PROB_1:def 15; then (seq^\k).n in dom f2/\left_open_halfline(r1) by A8,A10,XBOOLE_0:def 3; then r2<=f2.((seq^\k).n) by A2; hence r2<=(f2*(seq^\k)).n by A8,RFUNCT_2:21 ; end; then A11: (f1*(seq^\k))(#)(f2*(seq^\k)) is divergent_to+infty by A9,Th49; rng(seq^\k)c=dom f1/\dom f2 by A3,A4,A7,XBOOLE_1:1; then (f1*(seq^\k))(#)(f2*(seq^\k))=(f1(#)f2)*(seq^\k) by RFUNCT_2:23 .=((f1(#)f2)*seq)^\k by A3,RFUNCT_2:22; hence (f1(#)f2)*seq is divergent_to+infty by A11,Th34; end; hence thesis by A1,Def10; end; theorem (f is divergent_in+infty_to+infty & r>0 implies r(#)f is divergent_in+infty_to+infty) & (f is divergent_in+infty_to+infty & r<0 implies r(#)f is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r>0 implies r(#)f is divergent_in+infty_to-infty) & (f is divergent_in+infty_to-infty & r<0 implies r(#)f is divergent_in+infty_to+infty) proof thus f is divergent_in+infty_to+infty & r>0 implies r(#)f is divergent_in+infty_to+infty proof assume A1: f is divergent_in+infty_to+infty & r>0; A2: now let r1; consider g such that A3: r1<g & g in dom f by A1,Def7; take g; thus r1<g & g in dom(r(#)f) by A3,SEQ_1:def 6; end; now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f); then A4: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to+infty by A1,Def7; then r(#)(f*seq) is divergent_to+infty by A1,Th40; hence (r(#)f)*seq is divergent_to+infty by A4,RFUNCT_2:24; end; hence thesis by A2,Def7; end; thus f is divergent_in+infty_to+infty & r<0 implies r(#)f is divergent_in+infty_to-infty proof assume A5: f is divergent_in+infty_to+infty & r<0; A6: now let r1; consider g such that A7: r1<g & g in dom f by A5,Def7; take g; thus r1<g & g in dom(r(#)f) by A7,SEQ_1:def 6; end; now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f); then A8: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to+infty by A5,Def7; then r(#)(f*seq) is divergent_to-infty by A5,Th40; hence (r(#)f)*seq is divergent_to-infty by A8,RFUNCT_2:24; end; hence thesis by A6,Def8; end; thus f is divergent_in+infty_to-infty & r>0 implies r(#)f is divergent_in+infty_to-infty proof assume A9: f is divergent_in+infty_to-infty & r>0; A10: now let r1; consider g such that A11: r1<g & g in dom f by A9,Def8; take g; thus r1<g & g in dom(r(#)f) by A11,SEQ_1:def 6; end; now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f); then A12: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to-infty by A9,Def8; then r(#)(f*seq) is divergent_to-infty by A9,Th41; hence (r(#)f)*seq is divergent_to-infty by A12,RFUNCT_2:24; end; hence thesis by A10,Def8; end; assume A13: f is divergent_in+infty_to-infty & r<0; A14: now let r1; consider g such that A15: r1<g & g in dom f by A13,Def8; take g; thus r1<g & g in dom(r(#)f) by A15,SEQ_1:def 6; end; now let seq; assume seq is divergent_to+infty & rng seq c=dom(r(#)f); then A16: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to-infty by A13,Def8; then r(#)(f*seq) is divergent_to+infty by A13,Th41; hence (r(#)f)*seq is divergent_to+infty by A16,RFUNCT_2:24; end; hence thesis by A14,Def7; end; theorem (f is divergent_in-infty_to+infty & r>0 implies r(#)f is divergent_in-infty_to+infty) & (f is divergent_in-infty_to+infty & r<0 implies r(#)f is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r>0 implies r(#)f is divergent_in-infty_to-infty) & (f is divergent_in-infty_to-infty & r<0 implies r(#)f is divergent_in-infty_to+infty) proof thus f is divergent_in-infty_to+infty & r>0 implies r(#)f is divergent_in-infty_to+infty proof assume A1: f is divergent_in-infty_to+infty & r>0; A2: now let r1; consider g such that A3: g<r1 & g in dom f by A1,Def10; take g; thus g<r1 & g in dom(r(#)f) by A3,SEQ_1:def 6; end; now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f); then A4: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to+infty by A1,Def10; then r(#)(f*seq) is divergent_to+infty by A1,Th40; hence (r(#)f)*seq is divergent_to+infty by A4,RFUNCT_2:24; end; hence thesis by A2,Def10; end; thus f is divergent_in-infty_to+infty & r<0 implies r(#)f is divergent_in-infty_to-infty proof assume A5: f is divergent_in-infty_to+infty & r<0; A6: now let r1; consider g such that A7: g<r1 & g in dom f by A5,Def10; take g; thus g<r1 & g in dom(r(#)f) by A7,SEQ_1:def 6; end; now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f); then A8: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to+infty by A5,Def10; then r(#)(f*seq) is divergent_to-infty by A5,Th40; hence (r(#)f)*seq is divergent_to-infty by A8,RFUNCT_2:24; end; hence thesis by A6,Def11; end; thus f is divergent_in-infty_to-infty & r>0 implies r(#)f is divergent_in-infty_to-infty proof assume A9: f is divergent_in-infty_to-infty & r>0; A10: now let r1; consider g such that A11: g<r1 & g in dom f by A9,Def11; take g; thus g<r1 & g in dom(r(#)f) by A11,SEQ_1:def 6; end; now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f); then A12: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to-infty by A9,Def11; then r(#)(f*seq) is divergent_to-infty by A9,Th41; hence (r(#)f)*seq is divergent_to-infty by A12,RFUNCT_2:24; end; hence thesis by A10,Def11; end; assume A13: f is divergent_in-infty_to-infty & r<0; A14: now let r1; consider g such that A15: g<r1 & g in dom f by A13,Def11; take g; thus g<r1 & g in dom(r(#)f) by A15,SEQ_1:def 6; end; now let seq; assume seq is divergent_to-infty & rng seq c=dom(r(#)f); then A16: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6; then f*seq is divergent_to-infty by A13,Def11; then r(#)(f*seq) is divergent_to+infty by A13,Th41; hence (r(#)f)*seq is divergent_to+infty by A16,RFUNCT_2:24; end; hence thesis by A14,Def10; end; theorem (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) implies abs(f) is divergent_in+infty_to+infty proof assume A1: f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty; now per cases by A1; suppose A2: f is divergent_in+infty_to+infty; A3: now let r; consider g such that A4: r<g & g in dom f by A2,Def7; take g; thus r<g & g in dom abs(f) by A4,SEQ_1:def 10; end; now let seq; assume A5: seq is divergent_to+infty & rng seq c=dom abs(f); then A6: rng seq c=dom f by SEQ_1:def 10 ; then f*seq is divergent_to+infty by A2,A5,Def7; then abs(f*seq) is divergent_to+infty by Th52; hence abs(f)*seq is divergent_to+infty by A6,RFUNCT_2:25; end; hence thesis by A3,Def7; suppose A7: f is divergent_in+infty_to-infty; A8: now let r; consider g such that A9: r<g & g in dom f by A7,Def8; take g; thus r<g & g in dom abs(f) by A9,SEQ_1:def 10; end; now let seq; assume A10: seq is divergent_to+infty & rng seq c=dom abs(f); then A11: rng seq c=dom f by SEQ_1:def 10 ; then f*seq is divergent_to-infty by A7,A10,Def8; then abs(f*seq) is divergent_to+infty by Th52; hence abs(f)*seq is divergent_to+infty by A11,RFUNCT_2:25; end; hence thesis by A8,Def7; end; hence thesis; end; theorem (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) implies abs(f) is divergent_in-infty_to+infty proof assume A1: f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty; now per cases by A1; suppose A2: f is divergent_in-infty_to+infty; A3: now let r; consider g such that A4: g<r & g in dom f by A2,Def10; take g; thus g<r & g in dom abs(f) by A4,SEQ_1:def 10; end; now let seq; assume A5: seq is divergent_to-infty & rng seq c=dom abs(f); then A6: rng seq c=dom f by SEQ_1:def 10 ; then f*seq is divergent_to+infty by A2,A5,Def10; then abs(f*seq) is divergent_to+infty by Th52; hence abs(f)*seq is divergent_to+infty by A6,RFUNCT_2:25; end; hence thesis by A3,Def10; suppose A7: f is divergent_in-infty_to-infty; A8: now let r; consider g such that A9: g<r & g in dom f by A7,Def11; take g; thus g<r & g in dom abs(f) by A9,SEQ_1:def 10; end; now let seq; assume A10: seq is divergent_to-infty & rng seq c=dom abs(f); then A11: rng seq c=dom f by SEQ_1:def 10 ; then f*seq is divergent_to-infty by A7,A10,Def11; then abs(f*seq) is divergent_to+infty by Th52; hence abs(f)*seq is divergent_to+infty by A11,RFUNCT_2:25; end; hence thesis by A8,Def10; end; hence thesis; end; theorem Th95: (ex r st f is_non_decreasing_on right_open_halfline(r) & not f is_bounded_above_on right_open_halfline(r)) & (for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to+infty proof given r1 such that A1: f is_non_decreasing_on right_open_halfline(r1) & not f is_bounded_above_on right_open_halfline(r1); assume A2: for r ex g st r<g & g in dom f; now let seq such that A3: seq is divergent_to+infty & rng seq c=dom f; now let r; consider g1 such that A4: g1 in right_open_halfline(r1)/\dom f & r<f.g1 by A1,RFUNCT_1:def 9; consider n such that A5: for m st n<=m holds abs(g1)+abs(r1)<seq.m by A3,Def4; take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m; then A7: abs(g1)+abs(r1)<seq.m by A5; A8: r1<=abs(r1) by ABSVALUE:11; 0<=abs(g1) by ABSVALUE:5; then 0+r1<=abs(g1)+abs(r1) by A8,REAL_1:55; then r1<seq.m by A7,AXIOMS:22; then seq.m in {g2: r1<g2}; then seq.m in right_open_halfline(r1) by Def3; then A9: seq.m in right_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3; A10: g1<=abs(g1) by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5; then g1+0<=abs(g1)+abs(r1) by A10,REAL_1:55; then g1<seq.m by A7,AXIOMS:22; then f.g1<=f.(seq.m) by A1,A4,A9,RFUNCT_2:def 4 ; then r<f.(seq.m) by A4,AXIOMS:22; hence r<(f*seq).m by A3,RFUNCT_2:21; end; hence f*seq is divergent_to+infty by Def4; end; hence thesis by A2,Def7; end; theorem (ex r st f is_increasing_on right_open_halfline(r) & not f is_bounded_above_on right_open_halfline(r)) & (for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to+infty proof given r such that A1: f is_increasing_on right_open_halfline(r) & not f is_bounded_above_on right_open_halfline(r); assume A2: for r ex g st r<g & g in dom f; f is_non_decreasing_on right_open_halfline(r) by A1,RFUNCT_2:55; hence thesis by A1,A2,Th95; end; theorem Th97: (ex r st f is_non_increasing_on right_open_halfline(r) & not f is_bounded_below_on right_open_halfline(r)) & (for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to-infty proof given r1 such that A1: f is_non_increasing_on right_open_halfline(r1) & not f is_bounded_below_on right_open_halfline(r1); assume A2: for r ex g st r<g & g in dom f; now let seq such that A3: seq is divergent_to+infty & rng seq c=dom f; now let r; consider g1 such that A4: g1 in right_open_halfline(r1)/\dom f & f.g1<r by A1,RFUNCT_1:def 10; consider n such that A5: for m st n<=m holds abs(g1)+abs(r1)<seq.m by A3,Def4; take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m; then A7: abs(g1)+abs(r1)<seq.m by A5; A8: r1<=abs(r1) by ABSVALUE:11; 0<=abs(g1) by ABSVALUE:5; then 0+r1<=abs(g1)+abs(r1) by A8,REAL_1:55; then r1<seq.m by A7,AXIOMS:22; then seq.m in {g2: r1<g2}; then seq.m in right_open_halfline(r1) by Def3; then A9: seq.m in right_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3; A10: g1<=abs(g1) by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5; then g1+0<=abs(g1)+abs(r1) by A10,REAL_1:55; then g1<seq.m by A7,AXIOMS:22; then f.(seq.m)<=f.g1 by A1,A4,A9,RFUNCT_2:def 5 ; then f.(seq.m)<r by A4,AXIOMS:22; hence (f*seq).m<r by A3,RFUNCT_2:21; end; hence f*seq is divergent_to-infty by Def5; end; hence thesis by A2,Def8; end; theorem (ex r st f is_decreasing_on right_open_halfline(r) & not f is_bounded_below_on right_open_halfline(r)) & (for r ex g st r<g & g in dom f) implies f is divergent_in+infty_to-infty proof given r such that A1: f is_decreasing_on right_open_halfline(r) & not f is_bounded_below_on right_open_halfline(r); assume A2: for r ex g st r<g & g in dom f; f is_non_increasing_on right_open_halfline(r) by A1,RFUNCT_2:56; hence thesis by A1,A2,Th97; end; theorem Th99: (ex r st f is_non_increasing_on left_open_halfline(r) & not f is_bounded_above_on left_open_halfline(r)) & (for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to+infty proof given r1 such that A1: f is_non_increasing_on left_open_halfline(r1) & not f is_bounded_above_on left_open_halfline(r1); assume A2: for r ex g st g<r & g in dom f; now let seq such that A3: seq is divergent_to-infty & rng seq c=dom f; now let r; consider g1 such that A4: g1 in left_open_halfline(r1)/\dom f & r<f.g1 by A1,RFUNCT_1:def 9; consider n such that A5: for m st n<=m holds seq.m<-abs(r1)-abs(g1) by A3,Def5; take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m; then A7: seq.m<-abs(r1)-abs(g1) by A5; A8: -abs(r1)<=r1 by ABSVALUE:11; 0<=abs(g1) by ABSVALUE:5; then -abs(r1)-abs(g1)<=r1-0 by A8,REAL_1:92; then seq.m<r1 by A7,AXIOMS:22; then seq.m in {g2: g2<r1}; then seq.m in left_open_halfline(r1) by PROB_1:def 15; then A9: seq.m in left_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3; A10: -abs(g1)<=g1 by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5; then -abs(g1)-abs(r1)<=g1-0 by A10,REAL_1:92; then -abs(r1)+-abs(g1)<=g1 by XCMPLX_0:def 8; then -abs(r1)-abs(g1)<=g1 by XCMPLX_0:def 8; then seq.m<g1 by A7,AXIOMS:22 ; then f.g1<= f.(seq.m) by A1,A4,A9,RFUNCT_2:def 5; then r<f.(seq.m) by A4,AXIOMS:22; hence r<(f*seq).m by A3,RFUNCT_2:21; end; hence f*seq is divergent_to+infty by Def4; end; hence thesis by A2,Def10; end; theorem (ex r st f is_decreasing_on left_open_halfline(r) & not f is_bounded_above_on left_open_halfline(r)) & (for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to+infty proof given r such that A1: f is_decreasing_on left_open_halfline(r) & not f is_bounded_above_on left_open_halfline(r); assume A2: for r ex g st g<r & g in dom f; f is_non_increasing_on left_open_halfline(r) by A1,RFUNCT_2:56; hence thesis by A1,A2,Th99; end; theorem Th101: (ex r st f is_non_decreasing_on left_open_halfline(r) & not f is_bounded_below_on left_open_halfline(r)) & (for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to-infty proof given r1 such that A1: f is_non_decreasing_on left_open_halfline(r1) & not f is_bounded_below_on left_open_halfline(r1); assume A2: for r ex g st g<r & g in dom f; now let seq such that A3: seq is divergent_to-infty & rng seq c=dom f; now let r; consider g1 such that A4: g1 in left_open_halfline(r1)/\dom f & f.g1<r by A1,RFUNCT_1:def 10; consider n such that A5: for m st n<=m holds seq.m<-abs(r1)-abs(g1) by A3,Def5; take n; let m; A6: seq.m in rng seq by RFUNCT_2:10; assume n<=m; then A7: seq.m<-abs(r1)-abs(g1) by A5; A8: -abs(r1)<=r1 by ABSVALUE:11; 0<=abs(g1) by ABSVALUE:5; then -abs(r1)-abs(g1)<=r1-0 by A8,REAL_1:92; then seq.m<r1 by A7,AXIOMS:22; then seq.m in {g2: g2<r1}; then seq.m in left_open_halfline(r1) by PROB_1:def 15; then A9: seq.m in left_open_halfline(r1)/\dom f by A3,A6,XBOOLE_0:def 3; A10: -abs(g1)<=g1 by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5; then -abs(g1)-abs(r1)<=g1-0 by A10,REAL_1:92; then -abs(r1)+-abs(g1)<=g1 by XCMPLX_0:def 8; then -abs(r1)-abs(g1)<=g1 by XCMPLX_0:def 8; then seq.m<g1 by A7,AXIOMS:22; then f.(seq.m)<= f.g1 by A1,A4,A9,RFUNCT_2:def 4; then f.(seq.m)<r by A4,AXIOMS:22; hence (f*seq).m<r by A3,RFUNCT_2:21; end; hence f*seq is divergent_to-infty by Def5; end; hence thesis by A2,Def11; end; theorem (ex r st f is_increasing_on left_open_halfline(r) & not f is_bounded_below_on left_open_halfline(r)) & (for r ex g st g<r & g in dom f) implies f is divergent_in-infty_to-infty proof given r such that A1: f is_increasing_on left_open_halfline(r) & not f is_bounded_below_on left_open_halfline(r); assume A2: for r ex g st g<r & g in dom f; f is_non_decreasing_on left_open_halfline(r) by A1,RFUNCT_2:55; hence thesis by A1,A2,Th101; end; theorem Th103: f1 is divergent_in+infty_to+infty & (for r ex g st r<g & g in dom f) & (ex r st dom f /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) & for g st g in dom f /\ right_open_halfline(r) holds f1.g<=f.g) implies f is divergent_in+infty_to+infty proof assume A1: f1 is divergent_in+infty_to+infty & for r ex g st r<g & g in dom f; given r1 such that A2: dom f/\right_open_halfline(r1)c= dom f1/\right_open_halfline(r1) & for g st g in dom f/\right_open_halfline(r1) holds f1.g<=f.g; now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom f; then consider k such that A4: for n st k<=n holds r1<seq.n by Def4; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3, XBOOLE_1:1; now let x be set; assume x in rng(seq^\k); then consider n such that A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37; then r1<seq.(n+k) by A4; then r1<(seq^\k).n by SEQM_3:def 9; then x in {g2: r1<g2} by A6; hence x in right_open_halfline(r1) by Def3; end; then rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3; then A7: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A5,XBOOLE_1:19; then A8: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A2,XBOOLE_1:1; dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1; seq^\k is_subsequence_of seq by SEQM_3:47; then seq^\k is divergent_to+infty by A3,Th53; then A10: f1*(seq^\k) is divergent_to+infty by A1,A9,Def7; now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f1.((seq^\k).n)<=f.((seq^\k).n) by A2,A7; then (f1*(seq^\k)).n<=f.((seq^\k).n) by A9,RFUNCT_2:21; hence (f1*(seq^\k)).n<=(f*(seq^\k)).n by A5,RFUNCT_2:21; end; then A11: f*(seq^\k) is divergent_to+infty by A10,Th69; f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22; hence f*seq is divergent_to+infty by A11,Th34; end; hence f is divergent_in+infty_to+infty by A1,Def7; end; theorem Th104: f1 is divergent_in+infty_to-infty & (for r ex g st r<g & g in dom f) & (ex r st dom f/\right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) & for g st g in dom f /\ right_open_halfline(r) holds f.g<=f1.g) implies f is divergent_in+infty_to-infty proof assume A1: f1 is divergent_in+infty_to-infty & for r ex g st r<g & g in dom f; given r1 such that A2: dom f/\right_open_halfline(r1)c= dom f1/\right_open_halfline(r1) & for g st g in dom f/\right_open_halfline(r1) holds f.g<=f1.g; now let seq; assume A3: seq is divergent_to+infty & rng seq c=dom f; then consider k such that A4: for n st k<=n holds r1<seq.n by Def4; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3, XBOOLE_1:1; now let x be set; assume x in rng(seq^\k); then consider n such that A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37; then r1<seq.(n+k) by A4; then r1<(seq^\k).n by SEQM_3:def 9; then x in {g2: r1<g2} by A6; hence x in right_open_halfline(r1) by Def3; end; then rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3; then A7: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A5,XBOOLE_1:19; then A8: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A2,XBOOLE_1:1; dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1; seq^\k is_subsequence_of seq by SEQM_3:47; then seq^\k is divergent_to+infty by A3,Th53; then A10: f1*(seq^\k) is divergent_to-infty by A1,A9,Def8; now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f.((seq^\k).n)<=f1.((seq^\k).n) by A2,A7; then (f*(seq^\k)).n<=f1.((seq^\k).n) by A5,RFUNCT_2:21; hence (f*(seq^\k)).n<=(f1*(seq^\k)).n by A9,RFUNCT_2:21; end; then A11: f*(seq^\k) is divergent_to-infty by A10,Th70; f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22; hence f*seq is divergent_to-infty by A11,Th34; end; hence f is divergent_in+infty_to-infty by A1,Def8; end; theorem Th105: f1 is divergent_in-infty_to+infty & (for r ex g st g<r & g in dom f) & (ex r st dom f/\left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) & for g st g in dom f /\ left_open_halfline(r) holds f1.g<=f.g) implies f is divergent_in-infty_to+infty proof assume A1: f1 is divergent_in-infty_to+infty & for r ex g st g<r & g in dom f; given r1 such that A2: dom f/\left_open_halfline(r1)c= dom f1/\left_open_halfline(r1) & for g st g in dom f/\left_open_halfline(r1) holds f1.g<=f.g; now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom f; then consider k such that A4: for n st k<=n holds seq.n<r1 by Def5; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3, XBOOLE_1:1; now let x be set; assume x in rng(seq^\k); then consider n such that A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37; then seq.(n+k)<r1 by A4; then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g2: g2<r1} by A6; hence x in left_open_halfline(r1) by PROB_1:def 15; end; then rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3; then A7: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A5,XBOOLE_1:19; then A8: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A2,XBOOLE_1:1; dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1; seq^\k is_subsequence_of seq by SEQM_3:47; then seq^\k is divergent_to-infty by A3,Th54; then A10: f1*(seq^\k) is divergent_to+infty by A1,A9,Def10; now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f1.((seq^\k).n)<=f.((seq^\k).n) by A2,A7; then (f1*(seq^\k)).n<=f.((seq^\k).n) by A9,RFUNCT_2:21; hence (f1*(seq^\k)).n<=(f*(seq^\k)).n by A5,RFUNCT_2:21; end; then A11: f*(seq^\k) is divergent_to+infty by A10,Th69; f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22; hence f*seq is divergent_to+infty by A11,Th34; end; hence f is divergent_in-infty_to+infty by A1,Def10; end; theorem Th106: f1 is divergent_in-infty_to-infty & (for r ex g st g<r & g in dom f) & (ex r st dom f/\left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) & for g st g in dom f /\ left_open_halfline(r) holds f.g<=f1.g) implies f is divergent_in-infty_to-infty proof assume A1: f1 is divergent_in-infty_to-infty & for r ex g st g<r & g in dom f; given r1 such that A2: dom f/\left_open_halfline(r1)c= dom f1/\left_open_halfline(r1) & for g st g in dom f/\left_open_halfline(r1) holds f.g<=f1.g; now let seq; assume A3: seq is divergent_to-infty & rng seq c=dom f; then consider k such that A4: for n st k<=n holds seq.n<r1 by Def5; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A5: rng(seq^\k)c=dom f by A3, XBOOLE_1:1; now let x be set; assume x in rng(seq^\k); then consider n such that A6: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37; then seq.(n+k)<r1 by A4; then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g2: g2<r1} by A6; hence x in left_open_halfline(r1) by PROB_1:def 15; end; then rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3; then A7: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A5,XBOOLE_1:19; then A8: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A2,XBOOLE_1:1; dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A9: rng(seq^\k)c=dom f1 by A8,XBOOLE_1:1; seq^\k is_subsequence_of seq by SEQM_3:47; then seq^\k is divergent_to-infty by A3,Th54; then A10: f1*(seq^\k) is divergent_to-infty by A1,A9,Def11; now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f.((seq^\k).n)<=f1.((seq^\k).n) by A2,A7; then (f*(seq^\k)).n<=f1.((seq^\k).n) by A5,RFUNCT_2:21; hence (f*(seq^\k)).n<=(f1*(seq^\k)).n by A9,RFUNCT_2:21; end; then A11: f*(seq^\k) is divergent_to-infty by A10,Th70; f*(seq^\k)=(f*seq)^\k by A3,RFUNCT_2:22; hence f*seq is divergent_to-infty by A11,Th34; end; hence f is divergent_in-infty_to-infty by A1,Def11; end; theorem f1 is divergent_in+infty_to+infty & (ex r st right_open_halfline(r) c= dom f /\ dom f1 & for g st g in right_open_halfline(r) holds f1.g<=f.g) implies f is divergent_in+infty_to+infty proof assume A1: f1 is divergent_in+infty_to+infty; given r1 such that A2: right_open_halfline(r1)c=dom f/\dom f1 & for g st g in right_open_halfline(r1) holds f1.g<=f.g; A3: now let r; consider g being real number such that A4: abs(r)+abs(r1)<g by REAL_1:76; reconsider g as Real by XREAL_0:def 1; take g; A5: 0<=abs(r1) by ABSVALUE:5; r<=abs(r) by ABSVALUE:11; then 0+r<=abs(r)+abs(r1) by A5,REAL_1:55; hence r<g by A4,AXIOMS:22; A6: 0<=abs(r) by ABSVALUE:5; r1<=abs(r1) by ABSVALUE:11; then 0+r1<=abs(r)+abs(r1) by A6,REAL_1:55; then r1<g by A4,AXIOMS:22; then g in {g2: r1<g2}; then g in right_open_halfline(r1) by Def3; hence g in dom f by A2,XBOOLE_0: def 3; end; now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17; then A7: right_open_halfline(r1)c=dom f & right_open_halfline(r1) c=dom f1 by A2,XBOOLE_1:1; then A8: dom f/\right_open_halfline(r1)=right_open_halfline(r1) by XBOOLE_1: 28; hence dom f/\right_open_halfline(r1) c=dom f1/\right_open_halfline(r1) by A7, XBOOLE_1:28; let g; assume g in dom f/\right_open_halfline(r1); hence f1.g<=f.g by A2,A8 ; end; hence thesis by A1,A3,Th103; end; theorem f1 is divergent_in+infty_to-infty & (ex r st right_open_halfline(r) c= dom f /\ dom f1 & for g st g in right_open_halfline(r) holds f.g<=f1.g) implies f is divergent_in+infty_to-infty proof assume A1: f1 is divergent_in+infty_to-infty; given r1 such that A2: right_open_halfline(r1)c=dom f/\dom f1 & for g st g in right_open_halfline(r1) holds f.g<=f1.g; A3: now let r; consider g being real number such that A4: abs(r)+abs(r1)<g by REAL_1:76; reconsider g as Real by XREAL_0:def 1; take g; A5: 0<=abs(r1) by ABSVALUE:5; r<=abs(r) by ABSVALUE:11; then 0+r<=abs(r)+abs(r1) by A5,REAL_1:55; hence r<g by A4,AXIOMS:22; A6: 0<=abs(r) by ABSVALUE:5; r1<=abs(r1) by ABSVALUE:11; then 0+r1<=abs(r)+abs(r1) by A6,REAL_1:55; then r1<g by A4,AXIOMS:22; then g in {g2: r1<g2}; then g in right_open_halfline(r1) by Def3; hence g in dom f by A2,XBOOLE_0: def 3; end; now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17; then A7: right_open_halfline(r1)c=dom f & right_open_halfline(r1) c=dom f1 by A2,XBOOLE_1:1; then A8: dom f/\right_open_halfline(r1)=right_open_halfline(r1) by XBOOLE_1: 28; hence dom f/\right_open_halfline(r1) c=dom f1/\right_open_halfline(r1) by A7, XBOOLE_1:28; let g; assume g in dom f/\right_open_halfline(r1); hence f.g<=f1.g by A2,A8 ; end; hence thesis by A1,A3,Th104; end; theorem f1 is divergent_in-infty_to+infty & (ex r st left_open_halfline(r) c= dom f /\ dom f1 & for g st g in left_open_halfline(r) holds f1.g<=f.g) implies f is divergent_in-infty_to+infty proof assume A1: f1 is divergent_in-infty_to+infty; given r1 such that A2: left_open_halfline(r1)c=dom f/\dom f1 & for g st g in left_open_halfline(r1) holds f1.g<=f.g; A3: now let r; consider g being real number such that A4: g<-abs(r)-abs(r1) by REAL_1:77; reconsider g as Real by XREAL_0:def 1; take g; A5: 0<=abs(r1) by ABSVALUE:5; -abs(r)<=r by ABSVALUE:11; then -abs(r)-abs(r1)<=r-0 by A5,REAL_1:92; hence g<r by A4,AXIOMS:22; A6: 0<=abs(r) by ABSVALUE:5; -abs(r1)<=r1 by ABSVALUE:11; then -abs(r1)-abs(r)<=r1-0 by A6,REAL_1:92; then -abs(r)+-abs(r1)<=r1 by XCMPLX_0:def 8; then -abs(r)-abs(r1)<=r1 by XCMPLX_0:def 8; then g<r1 by A4,AXIOMS:22; then g in {g2: g2<r1}; then g in left_open_halfline(r1) by PROB_1:def 15; hence g in dom f by A2,XBOOLE_0:def 3; end; now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17; then A7: left_open_halfline(r1)c=dom f & left_open_halfline(r1) c=dom f1 by A2,XBOOLE_1:1; then A8: dom f/\left_open_halfline(r1)=left_open_halfline(r1) by XBOOLE_1:28; hence dom f/\left_open_halfline(r1) c=dom f1/\left_open_halfline(r1) by A7, XBOOLE_1:28; let g; assume g in dom f/\left_open_halfline(r1); hence f1.g<=f.g by A2,A8; end; hence thesis by A1,A3,Th105; end; theorem f1 is divergent_in-infty_to-infty & (ex r st left_open_halfline(r) c= dom f /\ dom f1 & for g st g in left_open_halfline(r) holds f.g<=f1.g) implies f is divergent_in-infty_to-infty proof assume A1: f1 is divergent_in-infty_to-infty; given r1 such that A2: left_open_halfline(r1)c=dom f/\dom f1 & for g st g in left_open_halfline(r1) holds f.g<=f1.g; A3: now let r; consider g being real number such that A4: g<-abs(r)-abs(r1) by REAL_1:77; reconsider g as Real by XREAL_0:def 1; take g; A5: 0<=abs(r1) by ABSVALUE:5; -abs(r)<=r by ABSVALUE:11; then -abs(r)-abs(r1)<=r-0 by A5,REAL_1:92; hence g<r by A4,AXIOMS:22; A6: 0<=abs(r) by ABSVALUE:5; -abs(r1)<=r1 by ABSVALUE:11; then -abs(r1)-abs(r)<=r1-0 by A6,REAL_1:92; then -abs(r)+-abs(r1)<=r1 by XCMPLX_0:def 8; then -abs(r)-abs(r1)<=r1 by XCMPLX_0:def 8; then g<r1 by A4,AXIOMS:22; then g in {g2: g2<r1}; then g in left_open_halfline(r1) by PROB_1:def 15; hence g in dom f by A2,XBOOLE_0:def 3; end; now dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17; then A7: left_open_halfline(r1)c=dom f & left_open_halfline(r1) c=dom f1 by A2,XBOOLE_1:1; then A8: dom f/\left_open_halfline(r1)=left_open_halfline(r1) by XBOOLE_1:28; hence dom f/\left_open_halfline(r1) c=dom f1/\left_open_halfline(r1) by A7, XBOOLE_1:28; let g; assume g in dom f/\left_open_halfline(r1); hence f.g<=f1.g by A2,A8; end; hence thesis by A1,A3,Th106; end; definition let f; assume A1: f is convergent_in+infty; func lim_in+infty f ->Real means :Def12: for seq st seq is divergent_to+infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=it; existence by A1,Def6; uniqueness proof let g1,g2 such that A2: for seq st seq is divergent_to+infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=g1 and A3: for seq st seq is divergent_to+infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=g2; defpred X[Nat,real number] means $1<$2 & $2 in dom f; A4: now let n; consider g such that A5: n<g & g in dom f by A1,Def6; reconsider g as real number; take g; thus X[n,g] by A5; end; consider s1 be Real_Sequence such that A6: for n holds X[n,s1.n] from RealSeqChoice(A4); deffunc U(Nat) = $1; consider s2 be Real_Sequence such that A7: for n holds s2.n=U(n) from ExRealSeq; A8: s2 is divergent_to+infty by A7,Th47; now let n; n<s1.n by A6; hence s2.n<=s1.n by A7; end; then A9: s1 is divergent_to+infty by A8,Th69; A10: rng s1 c= dom f proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; hence x in dom f by A6; end; then lim(f*s1)=g1 by A2,A9; hence g1=g2 by A3,A9,A10; end; end; definition let f; assume A1: f is convergent_in-infty; func lim_in-infty f ->Real means :Def13: for seq st seq is divergent_to-infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=it; existence by A1,Def9; uniqueness proof let g1,g2 such that A2: for seq st seq is divergent_to-infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=g1 and A3: for seq st seq is divergent_to-infty & rng seq c= dom f holds f*seq is convergent & lim(f*seq)=g2; defpred X[Nat,real number] means $2<-$1 & $2 in dom f; A4: now let n; consider g such that A5: g<-n & g in dom f by A1,Def9; reconsider g as real number; take g; thus X[n,g] by A5; end; consider s1 be Real_Sequence such that A6: for n holds X[n,s1.n] from RealSeqChoice(A4); deffunc U(Nat) = -$1; consider s2 be Real_Sequence such that A7: for n holds s2.n=U(n) from ExRealSeq; A8: s2 is divergent_to-infty by A7,Th48; now let n; s1.n<-n by A6; hence s1.n<=s2.n by A7; end; then A9: s1 is divergent_to-infty by A8,Th70; A10: rng s1 c= dom f proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; hence x in dom f by A6; end; then lim(f*s1)=g1 by A2,A9; hence g1=g2 by A3,A9,A10; end; end; canceled 2; theorem f is convergent_in-infty implies (lim_in-infty f=g iff for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1) proof assume A1: f is convergent_in-infty; thus lim_in-infty f=g implies for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1 proof assume A2: lim_in-infty f=g; given g1 such that A3: 0<g1 & for r ex r1 st r1<r & r1 in dom f & abs(f.r1-g)>=g1; defpred X[Nat,real number] means $2<-$1 & $2 in dom f & abs(f.$2-g)>=g1; A4: now let n; consider r such that A5: r<-n & r in dom f & abs(f.r-g)>=g1 by A3; reconsider r as real number; take r; thus X[n,r] by A5; end; consider s be Real_Sequence such that A6: for n holds X[n,s.n] from RealSeqChoice(A4); deffunc U(Nat) = -$1; consider s1 be Real_Sequence such that A7: for n holds s1.n=U(n) from ExRealSeq; A8: s1 is divergent_to-infty by A7,Th48; now let n; s.n<-n by A6; hence s.n<=s1.n by A7;end; then A9: s is divergent_to-infty by A8,Th70; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A6; end; then A10: rng s c=dom f by TARSKI:def 3; then f*s is convergent & lim(f*s)=g by A1,A2,A9,Def13; then consider n such that A11: for m st n<=m holds abs((f*s).m-g)<g1 by A3, SEQ_2:def 7; abs((f*s).n-g)<g1 by A11; then abs(f.(s.n)-g)<g1 by A10,RFUNCT_2:21; hence contradiction by A6; end; assume A12: for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1; now let s be Real_Sequence such that A13: s is divergent_to-infty & rng s c=dom f; A14: now let g1 be real number; A15: g1 is Real by XREAL_0:def 1; assume 0<g1; then consider r such that A16: for r1 st r1<r & r1 in dom f holds abs(f.r1-g)<g1 by A12,A15; consider n such that A17: for m st n<=m holds s.m<r by A13,Def5; take n; let m; assume n<=m; then A18: s.m<r by A17; s.m in rng s by RFUNCT_2:10; then abs(f.(s.m)-g)<g1 by A13,A16,A18; hence abs((f*s).m-g)<g1 by A13,RFUNCT_2:21; end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A14,SEQ_2: def 7; end; hence thesis by A1,Def13; end; theorem f is convergent_in+infty implies (lim_in+infty f=g iff for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1) proof assume A1: f is convergent_in+infty; thus lim_in+infty f=g implies for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1 proof assume A2: lim_in+infty f=g; given g1 such that A3: 0<g1 & for r ex r1 st r<r1 & r1 in dom f & abs(f.r1-g)>=g1; defpred X[Nat,real number] means $1<$2 & $2 in dom f & abs(f.$2-g)>=g1; A4: now let n; consider r such that A5: n<r & r in dom f & abs(f.r-g)>=g1 by A3; reconsider r as real number; take r; thus X[n,r] by A5; end; consider s be Real_Sequence such that A6: for n holds X[n,s.n] from RealSeqChoice(A4); deffunc U(Nat) = $1; consider s1 be Real_Sequence such that A7: for n holds s1.n=U(n) from ExRealSeq; A8: s1 is divergent_to+infty by A7,Th47; now let n; n<s.n by A6; hence s1.n<=s.n by A7;end; then A9: s is divergent_to+infty by A8,Th69; now let x be set; assume x in rng s; then ex n st s.n=x by RFUNCT_2:9; hence x in dom f by A6; end; then A10: rng s c=dom f by TARSKI:def 3; then f*s is convergent & lim(f*s)=g by A1,A2,A9,Def12; then consider n such that A11: for m st n<=m holds abs((f*s).m-g)<g1 by A3, SEQ_2:def 7; abs((f*s).n-g)<g1 by A11; then abs(f.(s.n)-g)<g1 by A10,RFUNCT_2:21; hence contradiction by A6; end; assume A12: for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1; now let s be Real_Sequence such that A13: s is divergent_to+infty & rng s c=dom f; A14: now let g1 be real number; A15: g1 is Real by XREAL_0:def 1; assume 0<g1; then consider r such that A16: for r1 st r<r1 & r1 in dom f holds abs(f.r1-g)<g1 by A12,A15; consider n such that A17: for m st n<=m holds r<s.m by A13,Def4; take n; let m; assume n<=m; then A18: r<s.m by A17; s.m in rng s by RFUNCT_2:10; then abs(f.(s.m)-g)<g1 by A13,A16,A18; hence abs((f*s).m-g)<g1 by A13,RFUNCT_2:21; end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A14,SEQ_2: def 7; end; hence thesis by A1,Def12; end; theorem Th115: f is convergent_in+infty implies r(#)f is convergent_in+infty & lim_in+infty(r(#)f)=r*(lim_in+infty f) proof assume A1: f is convergent_in+infty; A2: for r1 ex g st r1<g & g in dom(r(#)f) proof let r1; consider g such that A3: r1<g & g in dom f by A1,Def6; take g; thus r1<g & g in dom(r(#)f) by A3,SEQ_1:def 6; end; A4: now let seq; A5: lim_in+infty f=lim_in+infty f; assume seq is divergent_to+infty & rng seq c=dom(r(#)f); then A6: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 6; then A7: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A5,Def12; then r(#)(f*seq) is convergent by SEQ_2:21; hence (r(#)f)*seq is convergent by A6,RFUNCT_2:24; thus lim((r(#)f)*seq)=lim(r(#)(f*seq)) by A6,RFUNCT_2:24 .=r*(lim_in+infty f) by A7,SEQ_2:22; end; hence r(#)f is convergent_in+infty by A2,Def6; hence thesis by A4,Def12 ; end; theorem Th116: f is convergent_in+infty implies -f is convergent_in+infty & lim_in+infty(-f)=-(lim_in+infty f) proof assume A1: f is convergent_in+infty; A2: (-1)(#)f=-f by RFUNCT_1:38; hence -f is convergent_in+infty by A1,Th115; thus lim_in+infty (-f)=(-1)*(lim_in+infty f) by A1,A2,Th115 .=-(1*(lim_in+infty f)) by XCMPLX_1:175 .=-(lim_in+infty f); end; theorem Th117: f1 is convergent_in+infty & f2 is convergent_in+infty & (for r ex g st r<g & g in dom(f1+f2)) implies f1+f2 is convergent_in+infty & lim_in+infty(f1+f2) = lim_in+infty f1 + lim_in+infty f2 proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty & for r ex g st r<g & g in dom(f1+f2); A2: now let seq; A3: lim_in+infty f1=lim_in+infty f1 & lim_in+infty f2=lim_in+infty f2; assume A4: seq is divergent_to+infty & rng seq c=dom(f1+f2); then A5: dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm3; then A6: f1*seq is convergent & lim(f1*seq)=lim_in+infty f1 by A1,A3,A4,Def12 ; A7: f2*seq is convergent & lim(f2*seq)=lim_in+infty f2 by A1,A3,A4,A5,Def12; then f1*seq+f2*seq is convergent by A6,SEQ_2:19; hence (f1+f2)*seq is convergent by A4,A5,RFUNCT_2:23; thus lim((f1+f2)*seq)=lim(f1*seq+f2*seq) by A4,A5,RFUNCT_2:23 .=lim_in+infty f1+lim_in+infty f2 by A6,A7,SEQ_2:20; end; hence f1+f2 is convergent_in+infty by A1,Def6; hence thesis by A2,Def12 ; end; theorem f1 is convergent_in+infty & f2 is convergent_in+infty & (for r ex g st r<g & g in dom(f1-f2)) implies f1-f2 is convergent_in+infty & lim_in+infty(f1-f2)=(lim_in+infty f1)-(lim_in+infty f2) proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty & for r ex g st r<g & g in dom(f1-f2); A2: now let r; consider g such that A3: r<g & g in dom(f1-f2) by A1; take g; thus r<g & g in dom(f1+-f2) by A3,RFUNCT_1:40; end; A4: -f2 is convergent_in+infty & lim_in+infty(-f2)=-(lim_in+infty f2) by A1,Th116; then f1+-f2 is convergent_in+infty by A1,A2,Th117; hence f1-f2 is convergent_in+infty by RFUNCT_1:40; thus lim_in+infty(f1-f2)=lim_in+infty(f1+-f2) by RFUNCT_1:40 .=lim_in+infty f1+-lim_in+infty f2 by A1,A2,A4,Th117 .=lim_in+infty f1-lim_in+infty f2 by XCMPLX_0:def 8; end; theorem f is convergent_in+infty & f"{0}={} & (lim_in+infty f)<>0 implies f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)" proof assume A1: f is convergent_in+infty & f"{0}={} & (lim_in+infty f)<>0; then A2: dom f= dom f\f"{0} .=dom(f^) by RFUNCT_1:def 8; then A3: for r ex g st r<g & g in dom(f^) by A1,Def6; A4: now let seq; assume A5: seq is divergent_to+infty & rng seq c=dom(f^); then A6: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A2,Def12; A7: f*seq is_not_0 by A5,RFUNCT_2:26; then (f*seq)" is convergent by A1,A6,SEQ_2:35; hence (f^)*seq is convergent by A5,RFUNCT_2:27; thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27 .=(lim_in+infty f)" by A1,A6,A7,SEQ_2:36; end; hence f^ is convergent_in+infty by A3,Def6; hence thesis by A4,Def12; end; theorem f is convergent_in+infty implies abs(f) is convergent_in+infty & lim_in+infty abs(f)=abs(lim_in+infty f) proof assume A1: f is convergent_in+infty; A2: now let r; consider g such that A3: r<g & g in dom f by A1,Def6; take g; thus r<g & g in dom abs(f) by A3,SEQ_1:def 10; end; A4: now let seq; A5: lim_in+infty f=lim_in+infty f; assume seq is divergent_to+infty & rng seq c=dom abs(f); then A6: seq is divergent_to+infty & rng seq c=dom f by SEQ_1:def 10; then A7: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A5,Def12; then abs(f*seq) is convergent by SEQ_4:26; hence abs(f)*seq is convergent by A6,RFUNCT_2:25; thus lim(abs(f)*seq)=lim abs(f*seq) by A6,RFUNCT_2:25 .=abs(lim_in+infty f) by A7,SEQ_4:27; end; hence abs(f) is convergent_in+infty by A2,Def6; hence thesis by A4,Def12; end; theorem Th121: f is convergent_in+infty & lim_in+infty f<>0 & (for r ex g st r<g & g in dom f & f.g<>0) implies f^ is convergent_in+infty & lim_in+infty(f^)=(lim_in+infty f)" proof assume A1: f is convergent_in+infty & lim_in+infty f<>0 & for r ex g st r<g & g in dom f & f.g<>0; A2: now let r; consider g such that A3: r<g & g in dom f & f.g<>0 by A1; take g; not f.g in {0} by A3,TARSKI:def 1; then not g in f"{0} by FUNCT_1:def 13; then g in dom f\f"{0} by A3,XBOOLE_0:def 4; hence r<g & g in dom(f^) by A3,RFUNCT_1:def 8; end; A4: now let seq such that A5: seq is divergent_to+infty & rng seq c=dom(f^); A6: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8 ; dom f\f"{0}c=dom f by XBOOLE_1:36; then rng seq c=dom f by A5,A6,XBOOLE_1:1; then A7: f*seq is convergent & lim(f*seq)=lim_in+infty f by A1,A5,Def12; A8: f*seq is_not_0 by A5,RFUNCT_2:26; then (f*seq)" is convergent by A1,A7,SEQ_2:35; hence (f^)*seq is convergent by A5,RFUNCT_2:27; thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27 .=(lim_in+infty f)" by A1,A7,A8,SEQ_2:36; end; hence f^ is convergent_in+infty by A2,Def6; hence thesis by A4,Def12; end; theorem Th122: f1 is convergent_in+infty & f2 is convergent_in+infty & (for r ex g st r<g & g in dom(f1(#)f2)) implies f1(#) f2 is convergent_in+infty & lim_in+infty(f1(#)f2)=(lim_in+infty f1)*(lim_in+infty f2) proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty & for r ex g st r<g & g in dom(f1(#)f2); A2: now let seq; A3: lim_in+infty f1=lim_in+infty f1 & lim_in+infty f2=lim_in+infty f2; assume A4: seq is divergent_to+infty & rng seq c=dom(f1(#)f2); then A5: dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1 & rng seq c=dom f2 by Lm4; then A6: f1*seq is convergent & lim(f1*seq)=lim_in+infty f1 by A1,A3,A4,Def12 ; A7: f2*seq is convergent & lim(f2*seq)=lim_in+infty f2 by A1,A3,A4,A5,Def12; then (f1*seq)(#)(f2*seq) is convergent by A6,SEQ_2:28; hence (f1(#)f2)*seq is convergent by A4,A5,RFUNCT_2:23; thus lim((f1(#)f2)*seq)=lim((f1*seq)(#)(f2*seq)) by A4,A5,RFUNCT_2:23 .=(lim_in+infty f1)*(lim_in+infty f2) by A6,A7,SEQ_2:29; end; hence f1(#) f2 is convergent_in+infty by A1,Def6; hence thesis by A2,Def12; end; theorem f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2<>0 & (for r ex g st r<g & g in dom(f1/f2)) implies f1/f2 is convergent_in+infty & lim_in+infty(f1/f2)=(lim_in+infty f1)/(lim_in+infty f2) proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f2<>0 & for r ex g st r<g & g in dom(f1/f2); dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 4; then A2: dom(f1/f2)=dom f1/\dom(f2^) by RFUNCT_1:def 8; A3: dom f1/\dom(f2^)c=dom f1 & dom f1/\dom(f2^)c=dom(f2^) by XBOOLE_1:17; A4: now let r; consider g such that A5: r<g & g in dom(f1/f2) by A1; take g; thus r<g & g in dom(f1(#)(f2^)) by A2,A5,SEQ_1:def 5; end; now let r; consider g such that A6: r<g & g in dom(f1/f2) by A1; take g; g in dom(f2^) by A2,A3,A6; then A7: g in dom f2\f2"{0} by RFUNCT_1:def 8; then g in dom f2 & not g in f2"{0} by XBOOLE_0:def 4; then not f2.g in {0} by FUNCT_1:def 13; hence r<g & g in dom f2 & f2.g<>0 by A6,A7,TARSKI:def 1,XBOOLE_0:def 4; end; then A8: f2^ is convergent_in+infty & lim_in+infty(f2^)=(lim_in+infty f2)" by A1,Th121; then f1(#)(f2^) is convergent_in+infty by A1,A4,Th122; hence f1/f2 is convergent_in+infty by RFUNCT_1:47; thus lim_in+infty(f1/f2)=lim_in+infty(f1(#)(f2^)) by RFUNCT_1:47 .=(lim_in+infty f1)*((lim_in+infty f2)") by A1,A4,A8,Th122 .=(lim_in+infty f1)/(lim_in+infty f2) by XCMPLX_0:def 9; end; theorem Th124: f is convergent_in-infty implies r(#)f is convergent_in-infty & lim_in-infty(r(#)f)=r*(lim_in-infty f) proof assume A1: f is convergent_in-infty; A2: for r1 ex g st g<r1 & g in dom(r(#)f) proof let r1; consider g such that A3: g<r1 & g in dom f by A1,Def9; take g; thus g<r1 & g in dom(r(#)f) by A3,SEQ_1:def 6; end; A4: now let seq; A5: lim_in-infty f=lim_in-infty f; assume seq is divergent_to-infty & rng seq c=dom(r(#)f); then A6: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 6; then A7: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A5,Def13; then r(#)(f*seq) is convergent by SEQ_2:21; hence (r(#)f)*seq is convergent by A6,RFUNCT_2:24; thus lim((r(#)f)*seq)=lim(r(#)(f*seq)) by A6,RFUNCT_2:24 .=r*(lim_in-infty f) by A7,SEQ_2:22; end; hence r(#)f is convergent_in-infty by A2,Def9; hence thesis by A4,Def13 ; end; theorem Th125: f is convergent_in-infty implies -f is convergent_in-infty & lim_in-infty(-f)=-(lim_in-infty f) proof assume A1: f is convergent_in-infty; A2: (-1)(#)f=-f by RFUNCT_1:38; hence -f is convergent_in-infty by A1,Th124; thus lim_in-infty (-f)=(-1)*(lim_in-infty f) by A1,A2,Th124 .=-(1*(lim_in-infty f)) by XCMPLX_1:175 .=-(lim_in-infty f); end; theorem Th126: f1 is convergent_in-infty & f2 is convergent_in-infty & (for r ex g st g<r & g in dom(f1+f2)) implies f1+f2 is convergent_in-infty & lim_in-infty(f1+f2) = lim_in-infty f1 + lim_in-infty f2 proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty & for r ex g st g<r & g in dom(f1+f2); A2: now let seq; A3: lim_in-infty f1=lim_in-infty f1 & lim_in-infty f2=lim_in-infty f2; assume A4: seq is divergent_to-infty & rng seq c=dom(f1+f2); then A5: rng seq c=dom f1/\dom f2 by SEQ_1:def 3; dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17; then A6: rng seq c=dom f1 & rng seq c=dom f2 by A5,XBOOLE_1:1; then A7: f1*seq is convergent & lim(f1*seq)=lim_in-infty f1 by A1,A3,A4,Def13 ; A8: f2*seq is convergent & lim(f2*seq)=lim_in-infty f2 by A1,A3,A4,A6,Def13; then f1*seq+f2*seq is convergent by A7,SEQ_2:19; hence (f1+f2)*seq is convergent by A5,RFUNCT_2:23; thus lim((f1+f2)*seq)=lim(f1*seq+f2*seq) by A5,RFUNCT_2:23 .=lim_in-infty f1+lim_in-infty f2 by A7,A8,SEQ_2:20; end; hence f1+f2 is convergent_in-infty by A1,Def9; hence thesis by A2,Def13 ; end; theorem f1 is convergent_in-infty & f2 is convergent_in-infty & (for r ex g st g<r & g in dom(f1-f2)) implies f1-f2 is convergent_in-infty & lim_in-infty(f1-f2)=(lim_in-infty f1)-(lim_in-infty f2) proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty & for r ex g st g<r & g in dom(f1-f2); A2: now let r; consider g such that A3: g<r & g in dom(f1-f2) by A1; take g; thus g<r & g in dom(f1+-f2) by A3,RFUNCT_1:40; end; A4: -f2 is convergent_in-infty & lim_in-infty(-f2)=-(lim_in-infty f2) by A1,Th125; then f1+-f2 is convergent_in-infty by A1,A2,Th126; hence f1-f2 is convergent_in-infty by RFUNCT_1:40; thus lim_in-infty(f1-f2)=lim_in-infty(f1+-f2) by RFUNCT_1:40 .=lim_in-infty f1+-lim_in-infty f2 by A1,A2,A4,Th126 .=lim_in-infty f1-lim_in-infty f2 by XCMPLX_0:def 8; end; theorem f is convergent_in-infty & f"{0}={} & (lim_in-infty f)<>0 implies f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)" proof assume A1: f is convergent_in-infty & f"{0}={} & (lim_in-infty f)<>0; then A2: dom f= dom f\f"{0} .=dom(f^) by RFUNCT_1:def 8; then A3: for r ex g st g<r & g in dom(f^) by A1,Def9; A4: now let seq; assume A5: seq is divergent_to-infty & rng seq c=dom(f^); then A6: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A2,Def13; A7: f*seq is_not_0 by A5,RFUNCT_2:26; then (f*seq)" is convergent by A1,A6,SEQ_2:35; hence (f^)*seq is convergent by A5,RFUNCT_2:27; thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27 .=(lim_in-infty f)" by A1,A6,A7,SEQ_2:36; end; hence f^ is convergent_in-infty by A3,Def9; hence thesis by A4,Def13; end; theorem f is convergent_in-infty implies abs(f) is convergent_in-infty & lim_in-infty abs(f)=abs(lim_in-infty f) proof assume A1: f is convergent_in-infty; A2: now let r; consider g such that A3: g<r & g in dom f by A1,Def9; take g; thus g<r & g in dom abs(f) by A3,SEQ_1:def 10; end; A4: now let seq; A5: lim_in-infty f=lim_in-infty f; assume seq is divergent_to-infty & rng seq c=dom abs(f); then A6: seq is divergent_to-infty & rng seq c=dom f by SEQ_1:def 10; then A7: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A5,Def13; then abs(f*seq) is convergent by SEQ_4:26; hence abs(f)*seq is convergent by A6,RFUNCT_2:25; thus lim(abs(f)*seq)=lim abs(f*seq) by A6,RFUNCT_2:25 .=abs(lim_in-infty f) by A7,SEQ_4:27; end; hence abs(f) is convergent_in-infty by A2,Def9; hence thesis by A4,Def13; end; theorem Th130: f is convergent_in-infty & lim_in-infty f<>0 & (for r ex g st g<r & g in dom f & f.g<>0) implies f^ is convergent_in-infty & lim_in-infty(f^)=(lim_in-infty f)" proof assume A1: f is convergent_in-infty & lim_in-infty f<>0 & for r ex g st g<r & g in dom f & f.g<>0; A2: now let r; consider g such that A3: g<r & g in dom f & f.g<>0 by A1; take g; not f.g in {0} by A3,TARSKI:def 1; then not g in f"{0} by FUNCT_1:def 13; then g in dom f\f"{0} by A3,XBOOLE_0:def 4; hence g<r & g in dom(f^) by A3,RFUNCT_1:def 8; end; A4: now let seq such that A5: seq is divergent_to-infty & rng seq c=dom(f^); A6: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8 ; dom f\f"{0}c=dom f by XBOOLE_1:36; then rng seq c=dom f by A5,A6,XBOOLE_1:1; then A7: f*seq is convergent & lim(f*seq)=lim_in-infty f by A1,A5,Def13; A8: f*seq is_not_0 by A5,RFUNCT_2:26; then (f*seq)" is convergent by A1,A7,SEQ_2:35; hence (f^)*seq is convergent by A5,RFUNCT_2:27; thus lim((f^)*seq)=lim((f*seq)") by A5,RFUNCT_2:27 .=(lim_in-infty f)" by A1,A7,A8,SEQ_2:36; end; hence f^ is convergent_in-infty by A2,Def9; hence thesis by A4,Def13; end; theorem Th131: f1 is convergent_in-infty & f2 is convergent_in-infty & (for r ex g st g<r & g in dom(f1(#)f2)) implies f1(#) f2 is convergent_in-infty & lim_in-infty(f1(#)f2)=(lim_in-infty f1)*(lim_in-infty f2) proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty & for r ex g st g<r & g in dom(f1(#)f2); A2: now let seq; A3: lim_in-infty f1=lim_in-infty f1 & lim_in-infty f2=lim_in-infty f2; assume A4: seq is divergent_to-infty & rng seq c=dom(f1(#)f2); A5: dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17; A6: dom(f1(#)f2)=dom f1/\dom f2 by SEQ_1:def 5; then rng seq c=dom f1 by A4,A5,XBOOLE_1:1; then A7: f1*seq is convergent & lim(f1*seq)=lim_in-infty f1 by A1,A3,A4,Def13 ; rng seq c=dom f2 by A4,A5,A6,XBOOLE_1:1; then A8: f2*seq is convergent & lim(f2*seq)=lim_in-infty f2 by A1,A3,A4,Def13 ; then (f1*seq)(#)(f2*seq) is convergent by A7,SEQ_2:28; hence (f1(#)f2)*seq is convergent by A4,A6,RFUNCT_2:23; thus lim((f1(#)f2)*seq)=lim((f1*seq)(#)(f2*seq)) by A4,A6,RFUNCT_2:23 .=(lim_in-infty f1)*(lim_in-infty f2) by A7,A8,SEQ_2:29; end; hence f1(#) f2 is convergent_in-infty by A1,Def9; hence thesis by A2,Def13; end; theorem f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2<>0 & (for r ex g st g<r & g in dom(f1/f2)) implies f1/f2 is convergent_in-infty & lim_in-infty(f1/f2)=(lim_in-infty f1)/(lim_in-infty f2) proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f2<>0 & for r ex g st g<r & g in dom(f1/f2); dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 4; then A2: dom(f1/f2)=dom f1/\dom(f2^) by RFUNCT_1:def 8; A3: dom f1/\dom(f2^) c=dom f1 & dom f1/\dom(f2^) c=dom(f2^) by XBOOLE_1:17; A4: now let r; consider g such that A5: g<r & g in dom(f1/f2) by A1; take g; thus g<r & g in dom(f1(#)(f2^)) by A2,A5,SEQ_1:def 5; end; now let r; consider g such that A6: g<r & g in dom(f1/f2) by A1; take g; g in dom(f2^) by A2,A3,A6; then A7: g in dom f2\f2"{0} by RFUNCT_1:def 8; then g in dom f2 & not g in f2"{0} by XBOOLE_0:def 4; then not f2.g in {0} by FUNCT_1:def 13; hence g<r & g in dom f2 & f2.g<>0 by A6,A7,TARSKI:def 1,XBOOLE_0:def 4; end; then A8: f2^ is convergent_in-infty & lim_in-infty(f2^)=(lim_in-infty f2)" by A1,Th130; then f1(#)(f2^) is convergent_in-infty by A1,A4,Th131; hence f1/f2 is convergent_in-infty by RFUNCT_1:47; thus lim_in-infty(f1/f2)=lim_in-infty(f1(#)(f2^)) by RFUNCT_1:47 .=(lim_in-infty f1)*((lim_in-infty f2)") by A1,A4,A8,Th131 .=(lim_in-infty f1)/(lim_in-infty f2) by XCMPLX_0:def 9; end; theorem f1 is convergent_in+infty & lim_in+infty f1=0 & (for r ex g st r<g & g in dom(f1(#)f2)) & (ex r st f2 is_bounded_on right_open_halfline(r)) implies f1(#)f2 is convergent_in+infty & lim_in+infty(f1(#)f2)=0 proof assume A1: f1 is convergent_in+infty & lim_in+infty f1=0 & for r ex g st r<g & g in dom(f1(#)f2); given r such that A2: f2 is_bounded_on right_open_halfline(r); consider g be real number such that A3: for r1 st r1 in right_open_halfline(r)/\dom f2 holds abs(f2.r1)<=g by A2,RFUNCT_1:90; A4: now let s be Real_Sequence; assume A5: s is divergent_to+infty & rng s c=dom(f1(#)f2); then A6: dom(f1(#)f2)=dom f1/\dom f2 & rng s c=dom f1 & rng s c=dom f2 by Lm4 ; consider k such that A7: for n st k<=n holds r<s.n by A5,Def4; s^\k is_subsequence_of s by SEQM_3:47; then A8: s^\k is divergent_to+infty by A5,Th53; rng(s^\k)c=rng s by RFUNCT_2:7; then A9: rng(s^\k)c=dom f1/\dom f2 & rng(s^\k)c=dom f1 & rng(s^\k)c=dom f2 by A5,A6,XBOOLE_1:1; then A10: f1*(s^\k) is convergent & lim(f1*(s^\k))=0 by A1,A8,Def12; now set t=abs(g)+1; 0<=abs(g) by ABSVALUE:5; hence 0<t by Lm2; let n; A11: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37; then r<s.(n+k) by A7; then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g1: r<g1}; then (s^\k).n in right_open_halfline(r) by Def3; then (s^\k).n in right_open_halfline(r)/\dom f2 by A9,A11,XBOOLE_0:def 3; then abs(f2.((s^\k).n))<=g by A3; then A12: abs((f2*(s^\k)).n)<= g by A9,RFUNCT_2:21; g<=abs(g) by ABSVALUE:11; then g<t by Lm2; hence abs((f2*(s^\k)).n)<t by A12,AXIOMS:22; end; then A13: f2*(s^\k) is bounded by SEQ_2:15; then A14: (f1*(s^\k))(#)(f2*(s^\k)) is convergent by A10,SEQ_2:39; A15: lim((f1*(s^\k))(#)(f2*(s^\k)))=0 by A10,A13,SEQ_2:40; A16: (f1*(s^\k))(#)(f2*(s^\k))=(f1(#)f2)*(s^\k) by A9,RFUNCT_2:23 .=((f1(#)f2)*s)^\k by A5,RFUNCT_2:22; hence (f1(#)f2)*s is convergent by A14,SEQ_4:35; thus lim((f1(#)f2)*s)=0 by A14,A15,A16,SEQ_4:36; end; hence f1(#) f2 is convergent_in+infty by A1,Def6; hence thesis by A4,Def12; end; theorem f1 is convergent_in-infty & lim_in-infty f1=0 & (for r ex g st g<r & g in dom(f1(#)f2)) & (ex r st f2 is_bounded_on left_open_halfline(r)) implies f1(#)f2 is convergent_in-infty & lim_in-infty(f1(#)f2)=0 proof assume A1: f1 is convergent_in-infty & lim_in-infty f1=0 & for r ex g st g<r & g in dom(f1(#)f2); given r such that A2: f2 is_bounded_on left_open_halfline(r); consider g be real number such that A3: for r1 st r1 in left_open_halfline(r)/\dom f2 holds abs(f2.r1)<=g by A2,RFUNCT_1:90; A4: now let s be Real_Sequence; assume A5: s is divergent_to-infty & rng s c=dom(f1(#)f2); then A6: dom(f1(#)f2)=dom f1/\dom f2 & rng s c=dom f1 & rng s c=dom f2 by Lm4 ; consider k such that A7: for n st k<=n holds s.n<r by A5,Def5; s^\k is_subsequence_of s by SEQM_3:47; then A8: s^\k is divergent_to-infty by A5,Th54; rng(s^\k)c=rng s by RFUNCT_2:7; then A9: rng(s^\k)c=dom f1/\dom f2 & rng(s^\k)c=dom f1 & rng(s^\k)c=dom f2 by A5,A6,XBOOLE_1:1; then A10: f1*(s^\k) is convergent & lim(f1*(s^\k))=0 by A1,A8,Def13; now set t=abs(g)+1; 0<=abs(g) by ABSVALUE:5; hence 0<t by Lm2; let n; A11: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37; then s.(n+k)<r by A7; then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g1: g1<r}; then (s^\k).n in left_open_halfline(r) by PROB_1:def 15; then (s^\k).n in left_open_halfline(r)/\dom f2 by A9,A11,XBOOLE_0:def 3; then abs(f2.((s^\k).n))<=g by A3; then A12: abs((f2*(s^\k)).n)<= g by A9,RFUNCT_2:21; g<=abs(g) by ABSVALUE:11; then g<t by Lm2; hence abs((f2*(s^\k)).n)<t by A12,AXIOMS:22; end; then A13: f2*(s^\k) is bounded by SEQ_2:15; then A14: (f1*(s^\k))(#)(f2*(s^\k)) is convergent by A10,SEQ_2:39; A15: lim((f1*(s^\k))(#)(f2*(s^\k)))=0 by A10,A13,SEQ_2:40; A16: (f1*(s^\k))(#)(f2*(s^\k))=(f1(#)f2)*(s^\k) by A9,RFUNCT_2:23 .=((f1(#)f2)*s)^\k by A5,RFUNCT_2:22; hence (f1(#)f2)*s is convergent by A14,SEQ_4:35; thus lim((f1(#)f2)*s)=0 by A14,A15,A16,SEQ_4:36; end; hence f1(#) f2 is convergent_in-infty by A1,Def9; hence thesis by A4,Def13; end; theorem Th135: f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1=lim_in+infty f2 & (for r ex g st r<g & g in dom f) & (ex r st ((dom f1 /\ right_open_halfline(r) c= dom f2 /\ right_open_halfline(r) & dom f /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r)) or (dom f2 /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) & dom f /\ right_open_halfline(r) c= dom f2 /\ right_open_halfline(r))) & for g st g in dom f /\ right_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies f is convergent_in+infty & lim_in+infty f=lim_in+infty f1 proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1=lim_in+infty f2 & (for r ex g st r<g & g in dom f); given r1 such that A2: (dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) & dom f/\right_open_halfline(r1)c=dom f1/\right_open_halfline(r1)) or (dom f2/\right_open_halfline(r1)c=dom f1/\right_open_halfline(r1) & dom f/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1)) and A3: for g st g in dom f/\right_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g; now per cases by A2; suppose A4: dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) & dom f/\right_open_halfline(r1)c=dom f1/\right_open_halfline(r1); A5: now let seq; assume A6: seq is divergent_to+infty & rng seq c=dom f; then consider k such that A7: for n st k<=n holds r1<seq.n by Def4; seq^\k is_subsequence_of seq by SEQM_3:47; then A8: seq^\k is divergent_to+infty by A6,Th53; now let x be set; assume x in rng(seq^\k); then consider n such that A9: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37 ; then r1<seq.(n+k) by A7; then r1<(seq^\k).n by SEQM_3:def 9; then x in {g: r1<g} by A9; hence x in right_open_halfline(r1) by Def3; end; then A10: rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A11: rng(seq^\k)c=dom f by A6,XBOOLE_1:1; then A12: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A10,XBOOLE_1:19; then A13: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A4,XBOOLE_1:1; dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A14: rng(seq^\k)c=dom f1 by A13,XBOOLE_1:1; then A15: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in+infty f1 by A1,A8,Def12; A16: rng(seq^\k)c=dom f2/\right_open_halfline(r1) by A4,A13,XBOOLE_1:1; dom f2/\right_open_halfline(r1) c=dom f2 by XBOOLE_1:17; then A17: rng(seq^\k)c=dom f2 by A16,XBOOLE_1:1; then A18: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in+infty f1 by A1,A8,Def12; A19: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by A3,A12 ; then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n) by A11,RFUNCT_2:21; hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n by A14,A17,RFUNCT_2:21; end; A20: f*(seq^\k)=(f*seq)^\k by A6,RFUNCT_2:22; then (f*seq)^\k is convergent by A15,A18,A19,SEQ_2:33; hence A21: f*seq is convergent by SEQ_4:35; lim((f*seq)^\k)=lim_in+infty f1 by A15,A18,A19,A20,SEQ_2:34; hence lim(f*seq)=lim_in+infty f1 by A21,SEQ_4:33; end; hence f is convergent_in+infty by A1,Def6; hence thesis by A5,Def12; suppose A22: dom f2/\right_open_halfline(r1)c=dom f1/\ right_open_halfline(r1) & dom f/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1); A23: now let seq; assume A24: seq is divergent_to+infty & rng seq c=dom f; then consider k such that A25: for n st k<=n holds r1<seq.n by Def4; seq^\k is_subsequence_of seq by SEQM_3:47; then A26: seq^\k is divergent_to+infty by A24,Th53; now let x be set; assume x in rng(seq^\k); then consider n such that A27: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37 ; then r1<seq.(n+k) by A25; then r1<(seq^\k).n by SEQM_3:def 9; then x in {g: r1<g} by A27; hence x in right_open_halfline(r1) by Def3; end; then A28: rng(seq^\k)c=right_open_halfline(r1) by TARSKI:def 3; rng(seq^\k) c=rng seq by RFUNCT_2:7; then A29: rng(seq^\k)c=dom f by A24,XBOOLE_1:1; then A30: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A28,XBOOLE_1:19; then A31: rng(seq^\k)c=dom f2/\right_open_halfline(r1) by A22,XBOOLE_1:1; dom f2/\right_open_halfline(r1)c=dom f2 by XBOOLE_1:17; then A32: rng(seq^\k)c=dom f2 by A31,XBOOLE_1:1; then A33: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in+infty f1 by A1,A26,Def12; A34: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A22,A31,XBOOLE_1:1; dom f1/\right_open_halfline(r1) c=dom f1 by XBOOLE_1:17; then A35: rng(seq^\k)c=dom f1 by A34,XBOOLE_1:1; then A36: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in+infty f1 by A1,A26,Def12; A37: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by A3,A30 ; then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n) by A29,RFUNCT_2:21; hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n by A32,A35,RFUNCT_2:21; end; A38: f*(seq^\k)=(f*seq)^\k by A24,RFUNCT_2:22; then (f*seq)^\k is convergent by A33,A36,A37,SEQ_2:33; hence A39: f*seq is convergent by SEQ_4:35; lim((f*seq)^\k)=lim_in+infty f1 by A33,A36,A37,A38,SEQ_2:34; hence lim(f*seq)=lim_in+infty f1 by A39,SEQ_4:33; end; hence f is convergent_in+infty by A1,Def6; hence thesis by A23,Def12; end; hence thesis; end; theorem f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1=lim_in+infty f2 & (ex r st right_open_halfline(r) c= dom f1 /\ dom f2 /\ dom f & for g st g in right_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies f is convergent_in+infty & lim_in+infty f=lim_in+infty f1 proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty & lim_in+infty f1=lim_in+infty f2; given r1 such that A2: right_open_halfline(r1)c=dom f1/\dom f2/\dom f & for g st g in right_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g; A3: dom f1/\dom f2/\dom f c=dom f & dom f1/\dom f2/\dom f c=dom f1/\dom f2 by XBOOLE_1:17; then A4: right_open_halfline(r1)c=dom f by A2,XBOOLE_1:1; A5: now let r; consider g being real number such that A6: abs(r)+abs(r1)<g by REAL_1:76; reconsider g as Real by XREAL_0:def 1; take g; A7: r<=abs(r) by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5; then r+0<=abs(r)+abs(r1) by A7,REAL_1:55; hence r<g by A6,AXIOMS:22; A8: r1<=abs(r1) by ABSVALUE:11; 0<=abs(r) by ABSVALUE:5; then 0+r1<=abs(r)+abs(r1) by A8,REAL_1:55; then r1<g by A6,AXIOMS:22; then g in {g1: r1<g1}; then g in right_open_halfline(r1) by Def3; hence g in dom f by A4; end; now dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17; then dom f1/\dom f2/\dom f c=dom f1 & dom f1/\dom f2/\ dom f c=dom f2 by A3,XBOOLE_1:1; then A9: right_open_halfline(r1)c=dom f1 & right_open_halfline(r1)c=dom f2 by A2,XBOOLE_1:1; then A10: dom f1/\right_open_halfline(r1)=right_open_halfline(r1) by XBOOLE_1 :28; hence dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) by A9, XBOOLE_1:28; thus dom f/\right_open_halfline(r1)c=dom f1/\ right_open_halfline(r1) by A4,A10,XBOOLE_1:28; let g; assume g in dom f/\right_open_halfline(r1); then g in right_open_halfline(r1) by XBOOLE_0:def 3; hence f1.g<=f.g & f.g<=f2.g by A2; end; hence thesis by A1,A5,Th135; end; theorem Th137: f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1=lim_in-infty f2 & (for r ex g st g<r & g in dom f) & (ex r st ((dom f1 /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r) & dom f /\ left_open_halfline(r) c= dom f1 /\ left_open_halfline(r)) or (dom f2 /\ left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) & dom f /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r))) & for g st g in dom f /\ left_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies f is convergent_in-infty & lim_in-infty f=lim_in-infty f1 proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1=lim_in-infty f2 & (for r ex g st g<r & g in dom f); given r1 such that A2: (dom f1/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1) & dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1)) or (dom f2/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) & dom f/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1)) and A3: for g st g in dom f/\left_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g; now per cases by A2; suppose A4: dom f1/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1) & dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1); A5: now let seq; assume A6: seq is divergent_to-infty & rng seq c=dom f; then consider k such that A7: for n st k<=n holds seq.n<r1 by Def5; seq^\k is_subsequence_of seq by SEQM_3:47; then A8: seq^\k is divergent_to-infty by A6,Th54; now let x be set; assume x in rng(seq^\k); then consider n such that A9: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37 ; then seq.(n+k)<r1 by A7; then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g: g<r1} by A9; hence x in left_open_halfline(r1) by PROB_1:def 15; end; then A10: rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A11: rng(seq^\k)c=dom f by A6,XBOOLE_1:1; then A12: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A10,XBOOLE_1:19; then A13: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A4,XBOOLE_1:1; dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A14: rng(seq^\k)c=dom f1 by A13,XBOOLE_1:1; then A15: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in-infty f1 by A1,A8,Def13; A16: rng(seq^\k)c=dom f2/\left_open_halfline(r1) by A4,A13,XBOOLE_1:1; dom f2/\left_open_halfline(r1)c=dom f2 by XBOOLE_1:17; then A17: rng(seq^\k)c=dom f2 by A16,XBOOLE_1:1; then A18: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in-infty f1 by A1,A8,Def13; A19: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by A3,A12 ; then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n) by A11,RFUNCT_2:21; hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n by A14,A17,RFUNCT_2:21; end; A20: f*(seq^\k)=(f*seq)^\k by A6,RFUNCT_2:22; then (f*seq)^\k is convergent by A15,A18,A19,SEQ_2:33; hence A21: f*seq is convergent by SEQ_4:35; lim((f*seq)^\k)=lim_in-infty f1 by A15,A18,A19,A20,SEQ_2:34; hence lim(f*seq)=lim_in-infty f1 by A21,SEQ_4:33; end; hence f is convergent_in-infty by A1,Def9; hence thesis by A5,Def13; suppose A22: dom f2/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) & dom f/\left_open_halfline(r1)c=dom f2/\left_open_halfline(r1); A23: now let seq; assume A24: seq is divergent_to-infty & rng seq c=dom f; then consider k such that A25: for n st k<=n holds seq.n<r1 by Def5; seq^\k is_subsequence_of seq by SEQM_3:47; then A26: seq^\k is divergent_to-infty by A24,Th54; now let x be set; assume x in rng(seq^\k); then consider n such that A27: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37 ; then seq.(n+k)<r1 by A25; then (seq^\k).n<r1 by SEQM_3:def 9; then x in {g: g<r1} by A27; hence x in left_open_halfline(r1) by PROB_1:def 15; end; then A28: rng(seq^\k)c=left_open_halfline(r1) by TARSKI:def 3; rng(seq^\k)c=rng seq by RFUNCT_2:7; then A29: rng(seq^\k)c=dom f by A24,XBOOLE_1:1; then A30: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A28,XBOOLE_1:19; then A31: rng(seq^\k)c=dom f2/\left_open_halfline(r1) by A22,XBOOLE_1:1; dom f2/\left_open_halfline(r1)c=dom f2 by XBOOLE_1:17; then A32: rng(seq^\k)c=dom f2 by A31,XBOOLE_1:1; then A33: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_in-infty f1 by A1,A26,Def13; A34: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A22,A31,XBOOLE_1:1; dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17; then A35: rng(seq^\k)c=dom f1 by A34,XBOOLE_1:1; then A36: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_in-infty f1 by A1,A26,Def13; A37: now let n; (seq^\k).n in rng(seq^\k) by RFUNCT_2:10; then f1.((seq^\k).n)<=f.((seq^\k).n) & f.((seq^\k).n)<=f2.((seq^\k).n) by A3,A30 ; then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n) by A29,RFUNCT_2:21; hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n by A32,A35,RFUNCT_2:21; end; A38: f*(seq^\k)=(f*seq)^\k by A24,RFUNCT_2:22; then (f*seq)^\k is convergent by A33,A36,A37,SEQ_2:33; hence A39: f*seq is convergent by SEQ_4:35; lim((f*seq)^\k)=lim_in-infty f1 by A33,A36,A37,A38,SEQ_2:34; hence lim(f*seq)=lim_in-infty f1 by A39,SEQ_4:33; end; hence f is convergent_in-infty by A1,Def9; hence thesis by A23,Def13; end; hence thesis; end; theorem f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1=lim_in-infty f2 & (ex r st left_open_halfline(r) c= dom f1 /\ dom f2 /\ dom f & for g st g in left_open_halfline(r) holds f1.g<=f.g & f.g<=f2.g) implies f is convergent_in-infty & lim_in-infty f=lim_in-infty f1 proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty & lim_in-infty f1=lim_in-infty f2; given r1 such that A2: left_open_halfline(r1)c=dom f1/\dom f2/\dom f & for g st g in left_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g; A3: dom f1/\dom f2/\dom f c=dom f & dom f1/\dom f2/\dom f c=dom f1/\dom f2 by XBOOLE_1:17; then A4: left_open_halfline(r1) c=dom f by A2,XBOOLE_1:1; A5: now let r; consider g being real number such that A6: g<-abs(r)-abs(r1) by REAL_1:77; reconsider g as Real by XREAL_0:def 1; take g; A7: -abs(r)<=r by ABSVALUE:11; 0<=abs(r1) by ABSVALUE:5; then -abs(r)-abs(r1)<=r-0 by A7,REAL_1:92; hence g<r by A6,AXIOMS:22; A8: -abs(r1)<=r1 by ABSVALUE:11; 0<=abs(r) by ABSVALUE:5; then -abs(r1)-abs(r)<=r1-0 by A8,REAL_1:92; then -abs(r)+-abs(r1)<=r1 by XCMPLX_0:def 8; then -abs(r)-abs(r1)<=r1 by XCMPLX_0:def 8; then g<r1 by A6,AXIOMS:22; then g in {g1: g1<r1}; then g in left_open_halfline(r1) by PROB_1:def 15; hence g in dom f by A4; end; now dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17; then dom f1/\dom f2/\dom f c=dom f1 & dom f1/\dom f2/\ dom f c=dom f2 by A3,XBOOLE_1:1; then A9: left_open_halfline(r1)c=dom f1 & left_open_halfline(r1)c=dom f2 by A2,XBOOLE_1:1; then A10: dom f1/\left_open_halfline(r1)=left_open_halfline(r1) by XBOOLE_1: 28; hence dom f1/\left_open_halfline(r1) c=dom f2/\left_open_halfline(r1) by A9, XBOOLE_1:28; thus dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) by A4,A10, XBOOLE_1:28; let g; assume g in dom f/\left_open_halfline(r1); then g in left_open_halfline(r1) by XBOOLE_0:def 3; hence f1.g<=f.g & f.g<=f2.g by A2; end; hence thesis by A1,A5,Th137; end; theorem f1 is convergent_in+infty & f2 is convergent_in+infty & (ex r st ((dom f1 /\ right_open_halfline(r) c= dom f2 /\ right_open_halfline(r) & for g st g in dom f1 /\ right_open_halfline(r) holds f1.g<=f2.g) or (dom f2 /\ right_open_halfline(r) c= dom f1 /\ right_open_halfline(r) & for g st g in dom f2 /\ right_open_halfline(r) holds f1.g<=f2.g))) implies lim_in+infty f1<=lim_in+infty f2 proof assume A1: f1 is convergent_in+infty & f2 is convergent_in+infty; given r such that A2: (dom f1/\right_open_halfline(r)c=dom f2/\right_open_halfline(r) & for g st g in dom f1/\right_open_halfline(r) holds f1.g<=f2.g) or (dom f2/\right_open_halfline(r)c=dom f1/\right_open_halfline(r) & for g st g in dom f2/\right_open_halfline(r) holds f1.g<=f2.g); now per cases by A2; suppose A3: dom f1/\right_open_halfline(r)c=dom f2/\right_open_halfline(r) & for g st g in dom f1/\right_open_halfline(r) holds f1.g<=f2.g; defpred X[Nat,real number] means $1<$2 & $2 in dom f1/\right_open_halfline r; A4: now let n; consider g such that A5: n+abs(r)<g & g in dom f1 by A1,Def6; reconsider g as real number; take g; 0<=abs(r) by ABSVALUE:5; then A6: n+0<=n+abs(r) by REAL_1:55; A7: 0<=n by NAT_1:18; r<=abs(r) by ABSVALUE:11; then 0+r<=n+abs(r) by A7,REAL_1:55; then r<g by A5,AXIOMS:22; then g in {g2: r<g2}; then g in right_open_halfline(r) by Def3; hence X[n,g] by A5,A6,AXIOMS:22,XBOOLE_0:def 3; end; consider s1 be Real_Sequence such that A8: for n holds X[n,s1.n] from RealSeqChoice(A4); deffunc U(Nat) = $1; consider s2 be Real_Sequence such that A9: for n holds s2.n=U(n) from ExRealSeq; A10: s2 is divergent_to+infty by A9,Th47; now let n; n<s1.n by A8; hence s2.n<=s1.n by A9; end; then A11: s1 is divergent_to+infty by A10,Th69; A12: lim_in+infty f1=lim_in+infty f1 & lim_in+infty f2=lim_in+infty f2; A13: rng s1 c=dom f1 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f1/\right_open_halfline(r) by A8; hence x in dom f1 by XBOOLE_0:def 3; end; then A14: f1*s1 is convergent & lim(f1*s1)=lim_in+infty f1 by A1,A11,A12,Def12; A15: rng s1 c=dom f2 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f1/\right_open_halfline(r) by A8; hence x in dom f2 by A3,XBOOLE_0:def 3; end; then A16: f2*s1 is convergent & lim(f2*s1)=lim_in+infty f2 by A1,A11,A12,Def12; now let n; s1.n in dom f1/\right_open_halfline(r) by A8; then f1.(s1.n)<=f2.(s1.n) by A3; then (f1*s1).n<=f2.(s1.n) by A13,RFUNCT_2: 21; hence (f1*s1).n<=(f2*s1).n by A15,RFUNCT_2:21; end; hence thesis by A14,A16,SEQ_2:32; suppose A17: dom f2/\right_open_halfline(r)c=dom f1/\right_open_halfline(r) & for g st g in dom f2/\right_open_halfline(r) holds f1.g<=f2.g; defpred X[Nat,real number] means $1<$2 & $2 in dom f2/\right_open_halfline r; A18: now let n; consider g such that A19: n+abs(r)<g & g in dom f2 by A1,Def6; reconsider g as real number; take g; 0<=abs(r) by ABSVALUE:5; then A20: n+0<=n+abs(r) by REAL_1:55; A21: 0<=n by NAT_1:18; r<=abs(r) by ABSVALUE:11; then 0+r<=n+abs(r) by A21,REAL_1:55; then r<g by A19,AXIOMS:22; then g in {g2: r<g2}; then g in right_open_halfline(r) by Def3; hence X[n,g] by A19,A20,AXIOMS:22,XBOOLE_0:def 3; end; consider s1 be Real_Sequence such that A22: for n holds X[n,s1.n] from RealSeqChoice(A18); deffunc U(Nat) = $1; consider s2 be Real_Sequence such that A23: for n holds s2.n=U(n) from ExRealSeq; A24: s2 is divergent_to+infty by A23,Th47; now let n; n<s1.n by A22; hence s2.n<=s1.n by A23; end; then A25: s1 is divergent_to+infty by A24,Th69; A26: lim_in+infty f1=lim_in+infty f1 & lim_in+infty f2=lim_in+infty f2; A27: rng s1 c=dom f2 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f2/\right_open_halfline(r) by A22; hence x in dom f2 by XBOOLE_0:def 3; end; then A28: f2*s1 is convergent & lim(f2*s1)=lim_in+infty f2 by A1,A25,A26,Def12; A29: rng s1 c=dom f1 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f2/\right_open_halfline(r) by A22; hence x in dom f1 by A17,XBOOLE_0:def 3; end; then A30: f1*s1 is convergent & lim(f1*s1)=lim_in+infty f1 by A1,A25,A26,Def12; now let n; s1.n in dom f2/\right_open_halfline(r) by A22; then f1.(s1.n)<=f2.(s1.n) by A17; then (f1*s1).n<=f2.(s1.n) by A29,RFUNCT_2: 21; hence (f1*s1).n<=(f2*s1).n by A27,RFUNCT_2:21; end; hence thesis by A28,A30,SEQ_2:32; end; hence thesis; end; theorem f1 is convergent_in-infty & f2 is convergent_in-infty & (ex r st ((dom f1 /\ left_open_halfline(r) c= dom f2 /\ left_open_halfline(r) & for g st g in dom f1 /\ left_open_halfline(r) holds f1.g<=f2.g) or (dom f2 /\ left_open_halfline(r) c= dom f1 /\ left_open_halfline(r) & for g st g in dom f2 /\ left_open_halfline(r) holds f1.g<=f2.g))) implies lim_in-infty f1<=lim_in-infty f2 proof assume A1: f1 is convergent_in-infty & f2 is convergent_in-infty; given r such that A2: (dom f1/\left_open_halfline(r)c=dom f2/\left_open_halfline(r) & for g st g in dom f1/\left_open_halfline(r) holds f1.g<=f2.g) or (dom f2/\left_open_halfline(r)c=dom f1/\left_open_halfline(r) & for g st g in dom f2/\left_open_halfline(r) holds f1.g<=f2.g); now per cases by A2; suppose A3: dom f1/\left_open_halfline(r)c=dom f2/\left_open_halfline(r) & for g st g in dom f1/\left_open_halfline(r) holds f1.g<=f2.g; defpred X[Nat,real number] means $2<-$1 & $2 in dom f1/\left_open_halfline r; A4: now let n; consider g such that A5: g<-n-abs(r) & g in dom f1 by A1,Def9; reconsider g as real number; take g; 0<=abs(r) by ABSVALUE:5; then -n-abs(r)<=-n-0 by REAL_1:92; then A6: g < -n by A5,AXIOMS:22; A7: 0<=n by NAT_1:18; -abs(r)<=r by ABSVALUE:11; then -abs(r)-n<=r-0 by A7,REAL_1:92; then -n+-abs(r) <=r by XCMPLX_0:def 8; then -n-abs(r)<=r by XCMPLX_0:def 8 ; then g<r by A5,AXIOMS:22; then g in {g2: g2<r}; then g in left_open_halfline(r) by PROB_1:def 15; hence X[n,g] by A5,A6,XBOOLE_0:def 3; end; consider s1 be Real_Sequence such that A8: for n holds X[n,s1.n] from RealSeqChoice(A4); deffunc U(Nat) = -$1; consider s2 be Real_Sequence such that A9: for n holds s2.n=U(n) from ExRealSeq; A10: s2 is divergent_to-infty by A9,Th48; now let n; s1.n<-n by A8; hence s1.n<=s2.n by A9; end; then A11: s1 is divergent_to-infty by A10,Th70; A12: lim_in-infty f1=lim_in-infty f1 & lim_in-infty f2=lim_in-infty f2; A13: rng s1 c=dom f1 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f1/\left_open_halfline(r) by A8; hence x in dom f1 by XBOOLE_0:def 3; end; then A14: f1*s1 is convergent & lim(f1*s1)=lim_in-infty f1 by A1,A11,A12,Def13; A15: rng s1 c=dom f2 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f1/\left_open_halfline(r) by A8; hence x in dom f2 by A3,XBOOLE_0:def 3; end; then A16: f2*s1 is convergent & lim(f2*s1)=lim_in-infty f2 by A1,A11,A12,Def13; now let n; s1.n in dom f1/\left_open_halfline(r) by A8; then f1.(s1.n)<=f2.(s1.n) by A3; then (f1*s1).n<=f2.(s1.n) by A13,RFUNCT_2: 21; hence (f1*s1).n<=(f2*s1).n by A15,RFUNCT_2:21; end; hence thesis by A14,A16,SEQ_2:32; suppose A17: dom f2/\left_open_halfline(r)c=dom f1/\left_open_halfline(r) & for g st g in dom f2/\left_open_halfline(r) holds f1.g<=f2.g; defpred X[Nat,real number] means $2<-$1 & $2 in dom f2/\left_open_halfline r; A18: now let n; consider g such that A19: g<-n-abs(r) & g in dom f2 by A1,Def9; reconsider g as real number; take g; 0<=abs(r) by ABSVALUE:5; then A20: -n-abs(r)<=-n-0 by REAL_1:92; A21: 0<=n by NAT_1:18; -abs(r)<=r by ABSVALUE:11; then -abs(r)-n<=r-0 by A21,REAL_1:92; then -n+-abs(r)<=r by XCMPLX_0:def 8; then -n-abs(r)<=r by XCMPLX_0:def 8 ; then g<r by A19,AXIOMS:22; then g in {g2: g2<r}; then g in left_open_halfline(r) by PROB_1:def 15; hence X[n,g] by A19,A20,AXIOMS:22,XBOOLE_0:def 3; end; consider s1 be Real_Sequence such that A22: for n holds X[n,s1.n] from RealSeqChoice(A18); deffunc U(Nat) = -$1; consider s2 be Real_Sequence such that A23: for n holds s2.n=U(n) from ExRealSeq; A24: s2 is divergent_to-infty by A23,Th48; now let n; s1.n<-n by A22; hence s1.n<=s2.n by A23; end; then A25: s1 is divergent_to-infty by A24,Th70; A26: lim_in-infty f1=lim_in-infty f1 & lim_in-infty f2=lim_in-infty f2; A27: rng s1 c=dom f2 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f2/\left_open_halfline(r) by A22; hence x in dom f2 by XBOOLE_0:def 3; end; then A28: f2*s1 is convergent & lim(f2*s1)=lim_in-infty f2 by A1,A25,A26,Def13; A29: rng s1 c=dom f1 proof let x be set; assume x in rng s1; then ex n st x=s1.n by RFUNCT_2:9; then x in dom f2/\left_open_halfline(r) by A22; hence x in dom f1 by A17,XBOOLE_0:def 3; end; then A30: f1*s1 is convergent & lim(f1*s1)=lim_in-infty f1 by A1,A25,A26,Def13; now let n; s1.n in dom f2/\left_open_halfline(r) by A22; then f1.(s1.n)<=f2.(s1.n) by A17; then (f1*s1).n<=f2.(s1.n) by A29,RFUNCT_2: 21; hence (f1*s1).n<=(f2*s1).n by A27,RFUNCT_2:21; end; hence thesis by A28,A30,SEQ_2:32; end; hence thesis; end; theorem (f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty) & (for r ex g st r<g & g in dom f & f.g<>0) implies f^ is convergent_in+infty & lim_in+infty(f^)=0 proof assume that A1: f is divergent_in+infty_to+infty or f is divergent_in+infty_to-infty and A2: for r ex g st r<g & g in dom f & f.g<>0; A3: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; A4: now let r; consider g such that A5: r<g & g in dom f & f.g<>0 by A2; take g; not f.g in {0} by A5,TARSKI:def 1; then not g in f"{0} by FUNCT_1:def 13; hence r<g & g in dom(f^) by A3,A5,XBOOLE_0:def 4; end; now per cases by A1; suppose A6: f is divergent_in+infty_to+infty; A7: now let seq such that A8: seq is divergent_to+infty & rng seq c=dom(f^); dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A8,XBOOLE_1:1 ; then f*seq is divergent_to+infty by A6,A8,Def7; then (f*seq)" is convergent & lim((f*seq)")=0 by Th61; hence (f^)*seq is convergent & lim((f^)*seq)=0 by A8,RFUNCT_2:27; end; hence f^ is convergent_in+infty by A4,Def6; hence thesis by A7,Def12; suppose A9: f is divergent_in+infty_to-infty; A10: now let seq such that A11: seq is divergent_to+infty & rng seq c=dom(f^) ; dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A11,XBOOLE_1:1 ; then f*seq is divergent_to-infty by A9,A11,Def8; then (f*seq)" is convergent & lim((f*seq)")=0 by Th61; hence (f^)*seq is convergent & lim((f^)*seq)=0 by A11,RFUNCT_2:27; end; hence f^ is convergent_in+infty by A4,Def6; hence thesis by A10,Def12; end; hence thesis; end; theorem (f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty) & (for r ex g st g<r & g in dom f & f.g<>0) implies f^ is convergent_in-infty & lim_in-infty(f^)=0 proof assume that A1: f is divergent_in-infty_to+infty or f is divergent_in-infty_to-infty and A2: for r ex g st g<r & g in dom f & f.g<>0; A3: dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; A4: now let r; consider g such that A5: g<r & g in dom f & f.g<>0 by A2; take g; not f.g in {0} by A5,TARSKI:def 1; then not g in f"{0} by FUNCT_1:def 13; hence g<r & g in dom(f^) by A3,A5,XBOOLE_0:def 4; end; now per cases by A1; suppose A6: f is divergent_in-infty_to+infty; A7: now let seq such that A8: seq is divergent_to-infty & rng seq c=dom(f^); dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A8,XBOOLE_1:1 ; then f*seq is divergent_to+infty by A6,A8,Def10; then (f*seq)" is convergent & lim((f*seq)")=0 by Th61; hence (f^)*seq is convergent & lim((f^)*seq)=0 by A8,RFUNCT_2:27; end; hence f^ is convergent_in-infty by A4,Def9; hence thesis by A7,Def13; suppose A9: f is divergent_in-infty_to-infty; A10: now let seq such that A11: seq is divergent_to-infty & rng seq c=dom(f^) ; dom(f^) c=dom f by A3,XBOOLE_1:36; then rng seq c=dom f by A11,XBOOLE_1:1 ; then f*seq is divergent_to-infty by A9,A11,Def11; then (f*seq)" is convergent & lim((f*seq)")=0 by Th61; hence (f^)*seq is convergent & lim((f^)*seq)=0 by A11,RFUNCT_2:27; end; hence f^ is convergent_in-infty by A4,Def9; hence thesis by A10,Def13; end; hence thesis; end; theorem f is convergent_in+infty & lim_in+infty f=0 & (for r ex g st r<g & g in dom f & f.g<>0) & (ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<=f.g) implies f^ is divergent_in+infty_to+infty proof assume A1: f is convergent_in+infty & lim_in+infty f=0 & for r ex g st r<g & g in dom f & f.g<>0; given r such that A2: for g st g in dom f/\ right_open_halfline(r) holds 0<=f.g; thus for r1 ex g1 st r1<g1 & g1 in dom(f^) proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f & f.g1<>0 by A1; take g1; thus r1<g1 by A3; not f.g1 in {0} by A3,TARSKI:def 1; then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0 :def 4; hence thesis by RFUNCT_1:def 8; end; let s be Real_Sequence; assume A4: s is divergent_to+infty & rng s c=dom(f^); then consider k such that A5: for n st k<=n holds r<s.n by Def4; s^\k is_subsequence_of s by SEQM_3:47; then A6: s^\k is divergent_to+infty by A4,Th53; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A8: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1; then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def12; A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26; A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then r<s.(n+k) by A5; then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2}; then (s^\k).n in right_open_halfline(r) by Def3; then (s^\k).n in dom f/\right_open_halfline(r) by A8,A12,XBOOLE_0:def 3; then A13: 0<= f.((s^\k).n) by A2; (f*(s^\k)).n<>0 by A10,SEQ_1:7; hence 0<(f*(s^\k)).n by A8,A13,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A14: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies 0<(f*(s^\k)).n by A11; then A15: (f*(s^\k))" is divergent_to+infty by A9,A14,Th62; (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34; end; theorem f is convergent_in+infty & lim_in+infty f=0 & (for r ex g st r<g & g in dom f & f.g<>0) & (ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<=0) implies f^ is divergent_in+infty_to-infty proof assume A1: f is convergent_in+infty & lim_in+infty f=0 & for r ex g st r<g & g in dom f & f.g<>0; given r such that A2: for g st g in dom f/\right_open_halfline(r) holds f.g<=0; thus for r1 ex g1 st r1<g1 & g1 in dom(f^) proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f & f.g1<>0 by A1; take g1; thus r1<g1 by A3; not f.g1 in {0} by A3,TARSKI:def 1; then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0 :def 4; hence thesis by RFUNCT_1:def 8; end; let s be Real_Sequence; assume A4: s is divergent_to+infty & rng s c=dom(f^); then consider k such that A5: for n st k<=n holds r<s.n by Def4; s^\k is_subsequence_of s by SEQM_3:47; then A6: s^\k is divergent_to+infty by A4,Th53; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A8: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1; then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def12; A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26; A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then r<s.(n+k) by A5; then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2}; then (s^\k).n in right_open_halfline(r) by Def3; then (s^\k).n in dom f/\right_open_halfline(r) by A8,A12,XBOOLE_0:def 3; then A13: f.((s^\k).n)<=0 by A2; (f*(s^\k)).n<>0 by A10,SEQ_1:7; hence (f*(s^\k)).n<0 by A8,A13,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A14: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies (f*(s^\k)).n<0 by A11; then A15: (f*(s^\k))" is divergent_to-infty by A9,A14,Th63; (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34; end; theorem f is convergent_in-infty & lim_in-infty f=0 & (for r ex g st g<r & g in dom f & f.g<>0) & (ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<=f.g) implies f^ is divergent_in-infty_to+infty proof assume A1: f is convergent_in-infty & lim_in-infty f=0 & for r ex g st g<r & g in dom f & f.g<>0; given r such that A2: for g st g in dom f/\left_open_halfline(r) holds 0<=f.g; thus for r1 ex g1 st g1<r1 & g1 in dom(f^) proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f & f.g1<>0 by A1; take g1; thus g1<r1 by A3; not f.g1 in {0} by A3,TARSKI:def 1; then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0 :def 4; hence thesis by RFUNCT_1:def 8; end; let s be Real_Sequence; assume A4: s is divergent_to-infty & rng s c=dom (f^); then consider k such that A5: for n st k<=n holds s.n<r by Def5; s^\k is_subsequence_of s by SEQM_3:47; then A6: s^\k is divergent_to-infty by A4,Th54; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A8: rng(s^\k)c=dom (f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1; then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def13; A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26; A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then s.(n+k)<r by A5; then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r}; then (s^\k).n in left_open_halfline(r) by PROB_1:def 15; then (s^\k).n in dom f/\left_open_halfline(r) by A8,A12,XBOOLE_0:def 3 ; then A13: 0<=f.((s^\k).n) by A2; 0<>(f*(s^\k)).n by A10,SEQ_1:7; hence 0<(f*(s^\k)).n by A8,A13,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A14: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies 0<(f*(s^\k)).n by A11; then A15: (f*(s^\k))" is divergent_to+infty by A9,A14,Th62; (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34; end; theorem f is convergent_in-infty & lim_in-infty f=0 & (for r ex g st g<r & g in dom f & f.g<>0) & (ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<=0) implies f^ is divergent_in-infty_to-infty proof assume A1: f is convergent_in-infty & lim_in-infty f=0 & for r ex g st g<r & g in dom f & f.g<>0; given r such that A2: for g st g in dom f/\left_open_halfline(r) holds f.g<=0; thus for r1 ex g1 st g1<r1 & g1 in dom(f^) proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f & f.g1<>0 by A1; take g1; thus g1<r1 by A3; not f.g1 in {0} by A3,TARSKI:def 1; then not g1 in f"{0} by FUNCT_1:def 13; then g1 in dom f\f"{0} by A3,XBOOLE_0 :def 4; hence thesis by RFUNCT_1:def 8; end; let s be Real_Sequence; assume A4: s is divergent_to-infty & rng s c=dom (f^); then consider k such that A5: for n st k<=n holds s.n<r by Def5; s^\k is_subsequence_of s by SEQM_3:47; then A6: s^\k is divergent_to-infty by A4,Th54; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A7: rng s c=dom f by A4,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A8: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A4,A7,XBOOLE_1:1; then A9: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def13; A10: f*(s^\k) is_not_0 by A8,RFUNCT_2:26; A11: now let n; A12: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then s.(n+k)<r by A5; then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r}; then (s^\k).n in left_open_halfline(r) by PROB_1:def 15; then (s^\k).n in dom f/\left_open_halfline(r) by A8,A12,XBOOLE_0:def 3 ; then A13: f.((s^\k).n)<=0 by A2; (f*(s^\k)).n<>0 by A10,SEQ_1:7; hence (f*(s^\k)).n<0 by A8,A13,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A14: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies (f*(s^\k)).n<0 by A11; then A15: (f*(s^\k))" is divergent_to-infty by A9,A14,Th63; (f*(s^\k))"=((f*s)^\k)" by A7,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A4,RFUNCT_2:27; hence thesis by A15,Th34; end; theorem f is convergent_in+infty & lim_in+infty f=0 & (ex r st for g st g in dom f /\ right_open_halfline(r) holds 0<f.g) implies f^ is divergent_in+infty_to+infty proof assume A1: f is convergent_in+infty & lim_in+infty f=0; given r such that A2: for g st g in dom f/\right_open_halfline(r) holds 0<f.g; thus for r1 ex g1 st r1<g1 & g1 in dom(f^) proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f by A1,Def6; now per cases; suppose A4: g1<=r; consider g2 such that A5: r<g2 & g2 in dom f by A1,Def6 ; take g2; g1<g2 by A4,A5,AXIOMS:22; hence r1<g2 by A3,AXIOMS:22; g2 in {r2: r<r2} by A5; then g2 in right_open_halfline(r) by Def3; then g2 in dom f/\right_open_halfline(r) by A5,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; suppose A6: r<=g1; consider g2 such that A7: g1<g2 & g2 in dom f by A1,Def6 ; take g2; thus r1<g2 by A3,A7,AXIOMS:22; r<g2 by A6,A7,AXIOMS:22; then g2 in {r2: r<r2}; then g2 in right_open_halfline(r) by Def3; then g2 in dom f/\right_open_halfline(r) by A7,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; end; hence thesis; end; let s be Real_Sequence; assume A8: s is divergent_to+infty & rng s c=dom (f^); then consider k such that A9: for n st k<=n holds r<s.n by Def4; s^\k is_subsequence_of s by SEQM_3:47; then A10: s^\k is divergent_to+infty by A8,Th53; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1; then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def12; A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then r<s.(n+k) by A9; then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2}; then (s^\k).n in right_open_halfline(r) by Def3; then (s^\k).n in dom f/\right_open_halfline(r) by A12,A15,XBOOLE_0:def 3; then 0<f.((s^\k).n) by A2; hence 0<(f*(s^\k)).n by A12,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A16: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies 0<(f*(s^\k)).n by A14; then A17: (f*(s^\k))" is divergent_to+infty by A13,A16,Th62; (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence thesis by A17,Th34; end; theorem f is convergent_in+infty & lim_in+infty f=0 & (ex r st for g st g in dom f /\ right_open_halfline(r) holds f.g<0) implies f^ is divergent_in+infty_to-infty proof assume A1: f is convergent_in+infty & lim_in+infty f=0; given r such that A2: for g st g in dom f/\right_open_halfline(r) holds f.g<0; thus for r1 ex g1 st r1<g1 & g1 in dom(f^) proof let r1; consider g1 such that A3: r1<g1 & g1 in dom f by A1,Def6; now per cases; suppose A4: g1<=r; consider g2 such that A5: r<g2 & g2 in dom f by A1,Def6 ; take g2; g1<g2 by A4,A5,AXIOMS:22; hence r1<g2 by A3,AXIOMS:22; g2 in {r2: r<r2} by A5; then g2 in right_open_halfline(r) by Def3; then g2 in dom f/\right_open_halfline(r) by A5,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; suppose A6: r<=g1; consider g2 such that A7: g1<g2 & g2 in dom f by A1,Def6 ; take g2; thus r1<g2 by A3,A7,AXIOMS:22; r<g2 by A6,A7,AXIOMS:22; then g2 in {r2: r<r2}; then g2 in right_open_halfline(r) by Def3; then g2 in dom f/\right_open_halfline(r) by A7,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; end; hence thesis; end; let s be Real_Sequence; assume A8: s is divergent_to+infty & rng s c=dom (f^); then consider k such that A9: for n st k<=n holds r<s.n by Def4; s^\k is_subsequence_of s by SEQM_3:47; then A10: s^\k is divergent_to+infty by A8,Th53; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1; then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def12; A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then r<s.(n+k) by A9; then r<(s^\k).n by SEQM_3:def 9; then (s^\k).n in {g2: r<g2}; then (s^\k).n in right_open_halfline(r) by Def3; then (s^\k).n in dom f/\right_open_halfline(r) by A12,A15,XBOOLE_0:def 3; then f.((s^\k).n)<0 by A2; hence (f*(s^\k)).n<0 by A12,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A16: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies (f*(s^\k)).n<0 by A14; then A17: (f*(s^\k))" is divergent_to-infty by A13,A16,Th63; (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence (f^)*s is divergent_to-infty by A17,Th34; end; theorem f is convergent_in-infty & lim_in-infty f=0 & (ex r st for g st g in dom f /\ left_open_halfline(r) holds 0<f.g) implies f^ is divergent_in-infty_to+infty proof assume A1: f is convergent_in-infty & lim_in-infty f=0; given r such that A2: for g st g in dom f/\left_open_halfline(r) holds 0<f.g; thus for r1 ex g1 st g1<r1 & g1 in dom(f^) proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f by A1,Def9; now per cases; suppose A4: g1<=r; consider g2 such that A5: g2<g1 & g2 in dom f by A1,Def9 ; take g2; thus g2<r1 by A3,A5,AXIOMS:22; g2<r by A4,A5,AXIOMS:22; then g2 in {r2: r2<r}; then g2 in left_open_halfline(r) by PROB_1:def 15; then g2 in dom f/\left_open_halfline(r) by A5,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; suppose A6: r<=g1; consider g2 such that A7: g2<r & g2 in dom f by A1,Def9 ; take g2; g2<g1 by A6,A7,AXIOMS:22; hence g2<r1 by A3,AXIOMS:22; g2 in {r2: r2<r} by A7; then g2 in left_open_halfline(r) by PROB_1:def 15; then g2 in dom f/\left_open_halfline(r) by A7,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; end; hence thesis; end; let s be Real_Sequence; assume A8: s is divergent_to-infty & rng s c=dom (f^); then consider k such that A9: for n st k<=n holds s.n<r by Def5; s^\k is_subsequence_of s by SEQM_3:47; then A10: s^\k is divergent_to-infty by A8,Th54; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1; then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def13; A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then s.(n+k)<r by A9; then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r}; then (s^\k).n in left_open_halfline(r) by PROB_1:def 15; then (s^\k).n in dom f/\left_open_halfline(r) by A12,A15,XBOOLE_0:def 3 ; then 0<f.((s^\k).n) by A2; hence 0<(f*(s^\k)).n by A12,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A16: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies 0<(f*(s^\k)).n by A14; then A17: (f*(s^\k))" is divergent_to+infty by A13,A16,Th62; (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence thesis by A17,Th34; end; theorem f is convergent_in-infty & lim_in-infty f=0 & (ex r st for g st g in dom f /\ left_open_halfline(r) holds f.g<0) implies f^ is divergent_in-infty_to-infty proof assume A1: f is convergent_in-infty & lim_in-infty f=0; given r such that A2: for g st g in dom f/\left_open_halfline(r) holds f.g<0; thus for r1 ex g1 st g1<r1 & g1 in dom(f^) proof let r1; consider g1 such that A3: g1<r1 & g1 in dom f by A1,Def9; now per cases; suppose A4: g1<=r; consider g2 such that A5: g2<g1 & g2 in dom f by A1,Def9 ; take g2; thus g2<r1 by A3,A5,AXIOMS:22; g2<r by A4,A5,AXIOMS:22; then g2 in {r2: r2<r}; then g2 in left_open_halfline(r) by PROB_1:def 15; then g2 in dom f/\left_open_halfline(r) by A5,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A5,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; suppose A6: r<=g1; consider g2 such that A7: g2<r & g2 in dom f by A1,Def9 ; take g2; g2<g1 by A6,A7,AXIOMS:22; hence g2<r1 by A3,AXIOMS:22; g2 in {r2: r2<r} by A7; then g2 in left_open_halfline(r) by PROB_1:def 15; then g2 in dom f/\left_open_halfline(r) by A7,XBOOLE_0:def 3; then 0<>f.g2 by A2 ; then not f.g2 in {0} by TARSKI:def 1; then not g2 in f"{0} by FUNCT_1:def 13; then g2 in dom f\f"{0} by A7,XBOOLE_0:def 4; hence g2 in dom(f^) by RFUNCT_1:def 8; end; hence thesis; end; let s be Real_Sequence; assume A8: s is divergent_to-infty & rng s c=dom (f^); then consider k such that A9: for n st k<=n holds s.n<r by Def5; s^\k is_subsequence_of s by SEQM_3:47; then A10: s^\k is divergent_to-infty by A8,Th54; dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36 ; then A11: rng s c=dom f by A8,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7; then A12: rng(s^\k)c=dom(f^) & rng(s^\k)c=dom f by A8,A11,XBOOLE_1:1; then A13: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def13; A14: now let n; A15: (s^\k).n in rng(s^\k) by RFUNCT_2:10; k<=n+k by NAT_1:37 ; then s.(n+k)<r by A9; then (s^\k).n<r by SEQM_3:def 9; then (s^\k).n in {g2: g2<r}; then (s^\k).n in left_open_halfline(r) by PROB_1:def 15; then (s^\k).n in dom f/\left_open_halfline(r) by A12,A15,XBOOLE_0:def 3 ; then f.((s^\k).n)<0 by A2; hence (f*(s^\k)).n<0 by A12,RFUNCT_2:21; end; then for n holds 0<>(f*(s^\k)).n; then A16: f*(s^\k) is_not_0 by SEQ_1:7; for n holds 0<=n implies (f*(s^\k)).n<0 by A14; then A17: (f*(s^\k))" is divergent_to-infty by A13,A16,Th63; (f*(s^\k))"=((f*s)^\k)" by A11,RFUNCT_2:22 .=((f*s)")^\k by SEQM_3:41 .=((f^)*s)^\k by A8,RFUNCT_2:27; hence thesis by A17,Th34; end;