:: The Limit of a Real Function at Infinity. Halflines.
:: Real Sequence Divergent to Infinity
:: by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3, XXREAL_0,
ARYTM_1, RELAT_1, TARSKI, XBOOLE_0, VALUED_1, PROB_1, XXREAL_1, VALUED_0,
XXREAL_2, FUNCT_1, SEQ_2, ORDINAL2, COMPLEX1, REAL_1, NAT_1, SQUARE_1,
SEQM_3, FUNCT_2, ORDINAL4, LIMFUNC1, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
XXREAL_0, XXREAL_1, COMPLEX1, REAL_1, SQUARE_1, NAT_1, RELSET_1,
PARTFUN1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, SEQ_1,
COMSEQ_2, SEQ_2, SEQM_3, PROB_1, FUNCT_3, RFUNCT_1, RECDEF_1;
constructors PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1,
SEQ_2, SEQM_3, PROB_1, RCOMP_1, RFUNCT_1, RFUNCT_2, RECDEF_1, RELSET_1,
BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, MEMBERED,
XXREAL_1, VALUED_0, VALUED_1, FUNCT_2, SEQ_2, SEQ_4, SQUARE_1, NAT_1,
SEQ_1, FUNCT_1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions SEQ_2, MEMBERED;
equalities SQUARE_1, XBOOLE_0, PROB_1, VALUED_1;
expansions SEQ_2, MEMBERED;
theorems TARSKI, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, SQUARE_1,
RFUNCT_1, RFUNCT_2, FUNCT_1, FUNCT_2, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1, XXREAL_0, ORDINAL1, XXREAL_1,
VALUED_1, VALUED_0, NUMBERS;
schemes SEQ_1, FUNCT_2;
begin
reserve r,r1,g for Real,
n,m,k for Nat,
seq,seq1, seq2 for Real_Sequence,
f,f1,f2 for PartFunc of REAL,REAL,
x for set;
Lm1: 0<g & r<=r1 implies r-g<r1 & r<r1+g
proof
assume
A1: 0<g & r<=r1;
then r-g<r1-0 by XREAL_1:15;
hence r-g<r1;
r+0<r1+g by A1,XREAL_1:8;
hence thesis;
end;
Lm2: 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 VALUED_1:def 1;
then dom(f1+f2)c=dom f1 & dom(f1+f2)c=dom f2 by XBOOLE_1:17;
hence thesis by A1;
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 VALUED_1:def 4;
then dom(f1(#)f2)c=dom f1 & dom(f1(#)f2)c=dom f2 by XBOOLE_1:17;
hence thesis by A1;
end;
notation
let r be Real;
synonym left_open_halfline r for halfline r;
end;
definition
let r be Real;
func left_closed_halfline r -> Subset of REAL equals
].-infty,r.];
coherence
proof
for x being object st x in ].-infty,r.] holds x in REAL by XREAL_0:def 1;
hence thesis by TARSKI:def 3;
end;
func right_closed_halfline r -> Subset of REAL equals
[.r,+infty.[;
coherence
proof
for x being object st x in [.r,+infty.[ holds x in REAL by XREAL_0:def 1;
hence thesis by TARSKI:def 3;
end;
func right_open_halfline r -> Subset of REAL equals
].r,+infty.[;
coherence
proof
for x being object st x in ].r,+infty.[ holds x in REAL by XREAL_0:def 1;
hence thesis by TARSKI:def 3;
end;
end;
theorem
(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;
seq.0-1<seq.0-0 & seq.0<=seq.n by A1,SEQM_3:11,XREAL_1:15;
hence thesis by XXREAL_0:2;
end;
assume
A2: seq is non-increasing;
take seq.0+1;
let n;
seq.0+0<seq.0+1 & seq.n<=seq.0 by A2,SEQM_3:12,XREAL_1:8;
hence thesis by XXREAL_0:2;
end;
theorem Th2:
seq is non-zero & seq is convergent & lim seq=0 & seq is
non-decreasing implies for n holds seq.n<0
proof
assume that
A1: seq is non-zero and
A2: seq is convergent & lim seq=0 and
A3: seq is non-decreasing and
A4: ex n st not seq.n<0;
consider n such that
A5: not seq.n<0 by A4;
now
per cases by A5;
suppose
A6: 0<seq.n;
then consider n1 be Nat such that
A7: for m st n1<=m holds |.seq.m-0.|<seq.n by A2,SEQ_2:def 7;
|.seq.(n1+n)-0.|<seq.n by A7,NAT_1:12;
then n<=n1+n & seq.(n1+n)<seq.n by A6,ABSVALUE:def 1,NAT_1:12;
hence contradiction by A3,SEQM_3:6;
end;
suppose
seq.n=0;
hence contradiction by A1,SEQ_1:5;
end;
end;
hence contradiction;
end;
theorem Th3:
seq is non-zero & seq is convergent & lim seq=0 & seq is
non-increasing implies for n holds 0<seq.n
proof
assume that
A1: seq is non-zero and
A2: seq is convergent & lim seq=0 and
A3: seq is non-increasing and
A4: ex n st not 0<seq.n;
consider n such that
A5: not 0<seq.n by A4;
now
per cases by A5;
suppose
A6: seq.n<0;
then -0<-seq.n by XREAL_1:24;
then consider n1 be Nat such that
A7: for m st n1<=m holds |.seq.m-0.|<-seq.n by A2,SEQ_2:def 7;
A8: |.seq.(n1+n)-0.|<-seq.n by A7,NAT_1:12;
A9: n<=n1+n by NAT_1:12;
then seq.(n1+n)<0 by A3,A6,SEQM_3:8;
then -seq.(n1+n)<-seq.n by A8,ABSVALUE:def 1;
then seq.n<seq.(n1+n) by XREAL_1:24;
hence contradiction by A3,A9,SEQM_3:8;
end;
suppose
seq.n=0;
hence contradiction by A1,SEQ_1:5;
end;
end;
hence contradiction;
end;
theorem Th4:
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 and
A2: 0<lim seq and
A3: for n ex m st n<=m & not 0<seq.m;
consider n such that
A4: for m st n<=m holds |.seq.m-lim seq.|<lim seq by A1,A2,SEQ_2:def 7;
consider m such that
A5: n<=m and
A6: not 0<seq.m by A3;
A7: |.seq.m-lim seq.|<lim seq by A4,A5;
now
per cases by A6;
suppose
A8: seq.m<0;
then -(seq.m-lim seq)<lim seq by A2,A7,ABSVALUE:def 1;
then lim seq-seq.m<lim seq;
then lim seq<lim seq+seq.m by XREAL_1:19;
then lim seq - lim seq<seq.m by XREAL_1:19;
hence contradiction by A8;
end;
suppose
seq.m=0;
then |.-lim seq.|<lim seq by A7;
then |.lim seq.|<lim seq by COMPLEX1:52;
hence contradiction by A2,ABSVALUE:def 1;
end;
end;
hence contradiction;
end;
theorem Th5:
seq is convergent & 0<lim seq implies ex n st for m st n<=m
holds (lim seq)/2<seq.m
proof
assume that
A1: seq is convergent and
A2: 0<lim seq;
reconsider ls = (lim seq)/2 as Element of REAL by XREAL_0:def 1;
set s1 = seq_const((lim seq)/2);
A3: seq-s1 is convergent by A1;
s1.0=(lim seq)/2 by SEQ_1:57;
then lim(seq-s1)=(lim seq)/2+(lim seq)/2-(lim seq)/2 by A1,SEQ_4:42
.=(lim seq)/2;
then consider n such that
A4: for m st n<=m holds 0<(seq-s1).m by A2,A3,Th4,XREAL_1:215;
take n;
let m;
assume n<=m;
then 0<(seq-s1).m by A4;
then 0<seq.m-s1.m by RFUNCT_2:1;
then 0<seq.m-(lim seq)/2 by SEQ_1:57;
then 0+(lim seq)/2<seq.m by XREAL_1:20;
hence thesis;
end;
reserve r,r1,r2,g,g1,g2 for Real;
definition
let seq;
attr seq is divergent_to+infty means
for r ex n st for m st n<=m holds r<seq.m;
attr seq is divergent_to-infty means
for r ex n st for m st n<=m holds seq.m<r;
end;
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 non-zero
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;
take n;
let m such that
A3: n<=m;
now
let k;
0<seq.(k+m) by A2,A3,NAT_1:12;
hence 0<>(seq^\m).k by NAT_1:def 3;
end;
hence seq^\m is non-zero by SEQ_1:5;
end;
suppose
seq is divergent_to-infty;
then consider n such that
A4: for m st n<=m holds seq.m<0;
take n;
let m such that
A5: n<=m;
now
let k;
seq.(k+m)<0 by A4,A5,NAT_1:12;
hence (seq^\m).k<>0 by NAT_1:def 3;
end;
hence seq^\m is non-zero by SEQ_1:5;
end;
end;
hence thesis;
end;
theorem Th7:
(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;
take n=n1+k;
let m;
assume n<=m;
then consider n2 be Nat such that
A3: m=n+n2 by NAT_1:10;
reconsider n2 as Element of NAT by ORDINAL1:def 12;
A4: r<(seq^\k).(n1+n2) by A2,NAT_1:12;
n1+n2+k=m by A3;
hence thesis by A4,NAT_1:def 3;
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;
take n=n1+k;
let m;
assume n<=m;
then consider n2 be Nat such that
A7: m=n+n2 by NAT_1:10;
reconsider n2 as Element of NAT by ORDINAL1:def 12;
A8: (seq^\k).(n1+n2)< r by A6,NAT_1:12;
n1+n2+k=m by A7;
hence thesis by A8,NAT_1:def 3;
end;
theorem Th8:
seq1 is divergent_to+infty & seq2 is divergent_to+infty implies
seq1+seq2 is divergent_to+infty
proof
assume that
A1: seq1 is divergent_to+infty and
A2: seq2 is divergent_to+infty;
let r;
consider n1 be Nat such that
A3: for m st n1<=m holds r/2<seq1.m by A1;
consider n2 be Nat such that
A4: for m st n2<=m holds r/2<seq2.m by A2;
reconsider n=max(n1,n2) as Nat by TARSKI:1;
take n;
let m such that
A5: n<=m;
n2<=n by XXREAL_0:25;
then n2<=m by A5,XXREAL_0:2;
then
A6: r/2<seq2.m by A4;
n1<=n by XXREAL_0:25;
then n1<=m by A5,XXREAL_0:2;
then r/2<seq1.m by A3;
then r/2+r/2<seq1.m+seq2.m by A6,XREAL_1:8;
hence thesis by SEQ_1:7;
end;
theorem Th9:
seq1 is divergent_to+infty & seq2 is bounded_below implies seq1+
seq2 is divergent_to+infty
proof
assume that
A1: seq1 is divergent_to+infty and
A2: seq2 is bounded_below;
let r;
consider M be Real such that
A3: for n holds M<seq2.n by A2;
consider n such that
A4: for m st n<=m holds r-M<seq1.m by A1;
take n;
let m;
assume n<=m;
then r-M<seq1.m by A4;
then r-M+M<seq1.m+seq2.m by A3,XREAL_1:8;
hence thesis by SEQ_1:7;
end;
theorem Th10:
seq1 is divergent_to+infty & seq2 is divergent_to+infty implies
seq1(#)seq2 is divergent_to+infty
proof
assume that
A1: seq1 is divergent_to+infty and
A2: seq2 is divergent_to+infty;
let r;
consider n1 be Nat such that
A3: for m st n1<=m holds sqrt |.r.|<seq1.m by A1;
consider n2 be Nat such that
A4: for m st n2<=m holds sqrt |.r.|<seq2.m by A2;
reconsider n=max(n1,n2) as Nat by TARSKI:1;
take n;
let m such that
A5: n<=m;
n2<=n by XXREAL_0:25;
then n2<= m by A5,XXREAL_0:2;
then
A6: sqrt |.r.|<seq2.m by A4;
n1<=n by XXREAL_0:25;
then n1<= m by A5,XXREAL_0:2;
then
A7: sqrt |.r.|<seq1.m by A3;
A8: |.r.|>=0 by COMPLEX1:46;
then sqrt |.r.|>=0 by SQUARE_1:def 2;
then (sqrt |.r.|)^2<seq1.m*seq2.m by A7,A6,XREAL_1:96;
then
A9: |.r.|<seq1.m*seq2.m by A8,SQUARE_1:def 2;
r<=|.r.| by ABSVALUE:4;
then r<seq1.m*seq2.m by A9,XXREAL_0:2;
hence thesis by SEQ_1:8;
end;
theorem Th11:
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1+seq2 is divergent_to-infty
proof
assume that
A1: seq1 is divergent_to-infty and
A2: seq2 is divergent_to-infty;
let r;
consider n1 be Nat such that
A3: for m st n1<=m holds seq1.m<r/2 by A1;
consider n2 be Nat such that
A4: for m st n2<=m holds seq2.m<r/2 by A2;
reconsider n=max(n1,n2) as Nat by TARSKI:1;
take n;
let m such that
A5: n<=m;
n2<=n by XXREAL_0:25;
then n2<=m by A5,XXREAL_0:2;
then
A6: seq2.m<r/2 by A4;
n1<=n by XXREAL_0:25;
then n1<=m by A5,XXREAL_0:2;
then seq1.m<r/2 by A3;
then seq1.m+seq2.m<r/2+r/2 by A6,XREAL_1:8;
hence thesis by SEQ_1:7;
end;
theorem Th12:
seq1 is divergent_to-infty & seq2 is bounded_above implies seq1+
seq2 is divergent_to-infty
proof
assume that
A1: seq1 is divergent_to-infty and
A2: seq2 is bounded_above;
let r;
consider M be Real such that
A3: for n holds seq2.n<M by A2;
consider n such that
A4: for m st n<=m holds seq1.m<r-M by A1;
take n;
let m;
assume n<=m;
then seq1.m<r-M by A4;
then seq1.m+seq2.m<r-M+M by A3,XREAL_1:8;
hence thesis by SEQ_1:7;
end;
Lm4: 0 in REAL by XREAL_0:def 1;
theorem Th13:
(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) & ( 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 that
A1: seq is divergent_to+infty and
A2: r>0;
let g;
consider n such that
A3: for m st n<=m holds g/r<seq.m by A1;
take n;
let m;
assume n<=m;
then g/r<seq.m by A3;
then g/r*r<r*seq.m by A2,XREAL_1:68;
then g<r*seq.m by A2,XCMPLX_1:87;
hence thesis by SEQ_1:9;
end;
thus seq is divergent_to+infty & r<0 implies r(#)seq is divergent_to-infty
proof
assume that
A4: seq is divergent_to+infty and
A5: r<0;
let g;
consider n such that
A6: for m st n<=m holds g/r<seq.m by A4;
take n;
let m;
assume n<=m;
then g/r<seq.m by A6;
then r*seq.m<g/r*r by A5,XREAL_1:69;
then r*seq.m<g by A5,XCMPLX_1:87;
hence thesis by SEQ_1:9;
end;
assume
A7: r=0;
thus rng(r(#)seq)={0}
proof
let x be Real;
thus x in rng(r(#)seq) implies x in {0}
proof
assume x in rng(r(#)seq);
then consider n being Element of NAT such that
A8: x=(r(#)seq).n by FUNCT_2:113;
x=r*seq.n by A8,SEQ_1:9
.=0 by A7;
hence thesis by TARSKI:def 1;
end;
assume x in {0};
then
A9: x=0 by TARSKI:def 1;
(r(#)seq).0=r*seq.0 by SEQ_1:9
.=0 by A7;
hence thesis by A9,VALUED_0:28;
end;
hence thesis by FUNCT_2:111,Lm4;
end;
theorem Th14:
(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) & ( 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 that
A1: seq is divergent_to-infty and
A2: r>0;
let g;
consider n such that
A3: for m st n<=m holds seq.m<g/r by A1;
take n;
let m;
assume n<=m;
then seq.m<g/r by A3;
then r*seq.m<g/r*r by A2,XREAL_1:68;
then r*seq.m<g by A2,XCMPLX_1:87;
hence thesis by SEQ_1:9;
end;
thus seq is divergent_to-infty & r<0 implies r(#)seq is divergent_to+infty
proof
assume that
A4: seq is divergent_to-infty and
A5: r<0;
let g;
consider n such that
A6: for m st n<=m holds seq.m<g/r by A4;
take n;
let m;
assume n<=m;
then seq.m<g/r by A6;
then g/r*r<r*seq.m by A5,XREAL_1:69;
then g<r*seq.m by A5,XCMPLX_1:87;
hence thesis by SEQ_1:9;
end;
assume
A7: r=0;
thus rng(r(#)seq)={0}
proof
let x be Real;
thus x in rng(r(#)seq) implies x in {0}
proof
assume x in rng(r(#)seq);
then consider n being Element of NAT such that
A8: x=(r(#)seq).n by FUNCT_2:113;
x=r*seq.n by A8,SEQ_1:9
.=0 by A7;
hence thesis by TARSKI:def 1;
end;
assume x in {0};
then
A9: x=0 by TARSKI:def 1;
(r(#)seq).0=r*seq.0 by SEQ_1:9
.=0 by A7;
hence thesis by A9,VALUED_0:28;
end;
hence thesis by FUNCT_2:111,Lm4;
end;
reconsider jj=1 as Real;
theorem
(seq is divergent_to+infty implies -seq is divergent_to-infty) & (seq
is divergent_to-infty implies -seq is divergent_to+infty)
by Th13,Th14;
theorem
seq is bounded_below & seq1 is divergent_to-infty implies seq-seq1 is
divergent_to+infty
proof
assume that
A1: seq is bounded_below and
A2: seq1 is divergent_to-infty;
(-jj)(#)seq1 is divergent_to+infty by A2,Th14;
hence thesis by A1,Th9;
end;
theorem
seq is bounded_above & seq1 is divergent_to+infty implies seq-seq1 is
divergent_to-infty
proof
assume that
A1: seq is bounded_above and
A2: seq1 is divergent_to+infty;
(-jj)(#)seq1 is divergent_to-infty by A2,Th13;
hence thesis by A1,Th12;
end;
theorem
seq is divergent_to+infty & seq1 is convergent implies seq+seq1 is
divergent_to+infty by Th9;
theorem
seq is divergent_to-infty & seq1 is convergent implies seq+seq1 is
divergent_to-infty by Th12;
theorem Th20:
(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:3;
take n;
let m;
assume n<=m;
then r<m by A2,XXREAL_0:2;
hence thesis by A1;
end;
reconsider s1 = id NAT as Real_Sequence by FUNCT_2:7,NUMBERS:19;
Lm5: for n holds s1.n=n
by ORDINAL1:def 12,FUNCT_1:18;
theorem Th21:
(for n holds seq.n=-n) implies seq is divergent_to-infty
proof
assume
A1: for n holds seq.n=-n;
A2: now
let n be Element of NAT;
thus (-s1).n=-s1.n by SEQ_1:10
.=-n
.=seq.n by A1;
end;
s1 is divergent_to+infty by Lm5,Th20;
then (-jj)(#)s1 is divergent_to-infty by Th13;
hence thesis by A2,FUNCT_2:63;
end;
theorem Th22:
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 that
A1: seq1 is divergent_to+infty and
A2: ex r st r>0 & for n holds seq2.n>=r;
consider M be Real such that
A3: M>0 and
A4: for n holds seq2.n>=M by A2;
let r;
A5: 0<=|.r.| by COMPLEX1:46;
consider n such that
A6: for m st n<=m holds |.r.|/M<seq1.m by A1;
take n;
let m;
assume n<=m;
then |.r.|/M<seq1.m by A6;
then |.r.|/M*M<seq1.m*seq2.m by A3,A4,A5,XREAL_1:97;
then
A7: |.r.|<seq1.m*seq2.m by A3,XCMPLX_1:87;
r<=|.r.| by ABSVALUE:4;
then r<seq1.m*seq2.m by A7,XXREAL_0:2;
hence thesis by SEQ_1:8;
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 that
A1: seq1 is divergent_to-infty and
A2: ex r st 0<r & for n holds seq2.n>=r;
(-jj)(#)seq1 is divergent_to+infty by A1,Th14;
then
A3: (-jj)(#)seq1(#)seq2 is divergent_to+infty by A2,Th22;
(-1)(#)((-1)(#)seq1(#)seq2)=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:18
.=(-1)*(-1)(#)(seq1(#)seq2) by SEQ_1:23
.=seq1(#)seq2 by SEQ_1:27;
hence thesis by A3,Th13;
end;
theorem Th24:
seq1 is divergent_to-infty & seq2 is divergent_to-infty implies
seq1(#)seq2 is divergent_to+infty
proof
assume seq1 is divergent_to-infty & seq2 is divergent_to-infty;
then
A1: (-jj)(#)seq1 is divergent_to+infty &
(-jj)(#)seq2 is divergent_to+infty
by Th14;
(-1)(#)seq1(#)((-1)(#)seq2)=(-1)(#)(seq1(#)((-1)(#)seq2)) by SEQ_1:18
.=(-1)(#)((-1)(#)(seq1(#)seq2)) by SEQ_1:19
.=(-1)*(-1)(#)(seq1(#)seq2) by SEQ_1:23
.=seq1(#)seq2 by SEQ_1:27;
hence thesis by A1,Th10;
end;
theorem Th25:
(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 |.r.|<seq.m;
take n;
let m;
assume n<=m;
then r<=|.r.| & |.r.|<seq.m by A2,ABSVALUE:4;
then
A3: r<seq.m by XXREAL_0:2;
seq.m<=|.seq.m.| by ABSVALUE:4;
then seq.m<=abs(seq).m by SEQ_1:12;
hence r<abs(seq).m by A3,XXREAL_0:2;
end;
suppose
seq is divergent_to-infty;
then consider n such that
A4: for m st n<=m holds seq.m<-r;
take n;
let m;
-|.seq.m.|<=seq.m by ABSVALUE:4;
then
A5: -abs(seq).m<=seq.m by SEQ_1:12;
assume n<=m;
then seq.m<-r by A4;
then -abs(seq).m<-r by A5,XXREAL_0:2;
hence r<abs(seq).m by XREAL_1:24;
end;
end;
hence thesis;
end;
theorem Th26:
seq is divergent_to+infty & seq1 is subsequence of seq implies
seq1 is divergent_to+infty
proof
assume that
A1: seq is divergent_to+infty and
A2: seq1 is subsequence of seq;
consider Ns be increasing sequence of NAT such that
A3: seq1=seq*Ns by A2,VALUED_0:def 17;
let r;
consider n such that
A4: for m st n<=m holds r<seq.m by A1;
take n;
let m;
assume
A5: n<=m;
A6: m in NAT by ORDINAL1:def 12;
m<=Ns.m by SEQM_3:14;
then n<=Ns.m by A5,XXREAL_0:2;
then r<seq.(Ns.m) by A4;
hence thesis by A3,FUNCT_2:15,A6;
end;
theorem Th27:
seq is divergent_to-infty & seq1 is subsequence of seq implies
seq1 is divergent_to-infty
proof
assume that
A1: seq is divergent_to-infty and
A2: seq1 is subsequence of seq;
consider Ns be increasing sequence of NAT such that
A3: seq1=seq*Ns by A2,VALUED_0:def 17;
let r;
consider n such that
A4: for m st n<=m holds seq.m<r by A1;
take n;
let m;
assume
A5: n<=m;
A6: m in NAT by ORDINAL1:def 12;
m<=Ns.m by SEQM_3:14;
then n<=Ns.m by A5,XXREAL_0:2;
then seq.(Ns.m)<r by A4;
hence thesis by A3,FUNCT_2:15,A6;
end;
theorem
seq1 is divergent_to+infty & seq2 is convergent & 0<lim seq2 implies
seq1(#)seq2 is divergent_to+infty
proof
assume that
A1: seq1 is divergent_to+infty and
A2: seq2 is convergent and
A3: 0<lim seq2;
consider n1 be Nat such that
A4: for m st n1<=m holds (lim seq2)/2<seq2.m by A2,A3,Th5;
now
thus 0<(lim seq2)/2 by A3,XREAL_1:215;
let n;
(lim seq2)/2<seq2.(n+n1) by A4,NAT_1:12;
hence (lim seq2)/2<=(seq2^\n1).n by NAT_1:def 3;
end;
then (seq1^\n1)(#)(seq2^\n1) is divergent_to+infty by A1,Th22,Th26;
then (seq1(#)seq2)^\n1 is divergent_to+infty by SEQM_3:19;
hence thesis by Th7;
end;
theorem Th29:
seq is non-decreasing & not seq is bounded_above implies seq is
divergent_to+infty
proof
assume that
A1: seq is non-decreasing and
A2: not seq is bounded_above;
let r;
consider n such that
A3: r+1<=seq.n by A2;
take n;
let m;
assume n<=m;
then seq.n<=seq.m by A1,SEQM_3:6;
then r+1<=seq.m by A3,XXREAL_0:2;
hence thesis by Lm1;
end;
theorem Th30:
seq is non-increasing & not seq is bounded_below implies seq is
divergent_to-infty
proof
assume that
A1: seq is non-increasing and
A2: not seq is bounded_below;
let r;
consider n such that
A3: seq.n<=r-1 by A2;
take n;
let m;
assume n<=m;
then seq.m<=seq.n by A1,SEQM_3:8;
then seq.m<=r-1 by A3,XXREAL_0:2;
hence thesis by Lm1;
end;
theorem
seq is increasing & not seq is bounded_above implies seq is
divergent_to+infty by Th29;
theorem
seq is decreasing & not seq is bounded_below implies seq is
divergent_to-infty by Th30;
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 5;
suppose
A2: seq is non-decreasing;
now
per cases;
suppose
seq is bounded_above;
hence thesis by A2;
end;
suppose
not seq is bounded_above;
hence thesis by A2,Th29;
end;
end;
hence thesis;
end;
suppose
A3: seq is non-increasing;
now
per cases;
suppose
seq is bounded_below;
hence thesis by A3;
end;
suppose
not seq is bounded_below;
hence thesis by A3,Th30;
end;
end;
hence thesis;
end;
end;
hence thesis;
end;
theorem Th34:
(seq is divergent_to+infty or seq is divergent_to-infty) implies
seq" is convergent & lim(seq")=0
proof
assume
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 such that
A4: 0<r;
consider n such that
A5: for m st n<=m holds r"<seq.m by A2;
take n;
let m;
assume n<=m;
then
A6: r"<seq.m by A5;
then 1/seq.m<1/r" by A4,XREAL_1:76;
then
A7: 1/seq.m<r by XCMPLX_1:216;
A8: 1/seq.m=(seq.m)" & (seq.m)"=(seq").m by VALUED_1:10,XCMPLX_1:215;
0<r" by A4;
hence |.(seq").m-0.|<r by A6,A7,A8,ABSVALUE:def 1;
end;
hence seq" is convergent;
hence thesis by A3,SEQ_2:def 7;
end;
suppose
A9: seq is divergent_to-infty;
A10: now
let r be Real such that
A11: 0<r;
A12: -(r")<-0 by A11,XREAL_1:24;
consider n such that
A13: for m st n<=m holds seq.m<-(r") by A9;
take n;
let m;
assume
A14: n<=m;
then seq.m<-(r") by A13;
then 1/(-(r"))<1/seq.m by A12,XREAL_1:99;
then ((-1)*(r"))"<1/seq.m by XCMPLX_1:215;
then
A15: (-1)"*(r"")<1/seq.m by XCMPLX_1:204;
seq.m<-0 by A11,A13,A14;
then 1/seq.m<0/seq.m by XREAL_1:75;
then |.1/seq.m.|=-(1/seq.m) by ABSVALUE:def 1;
then -(1*r)<-|.1/seq.m.| by A15;
then |.1/seq.m.|<r by XREAL_1:24;
then |.(seq.m)".|<r by XCMPLX_1:215;
hence |.(seq").m-0.|<r by VALUED_1:10;
end;
hence seq" is convergent;
hence thesis by A10,SEQ_2:def 7;
end;
end;
hence thesis;
end;
theorem Th35:
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 convergent & lim seq=0;
given k such that
A2: for n st k<=n holds 0<seq.n;
let r;
set l=|.r.|+1;
0<=|.r.| by COMPLEX1:46;
then consider o be Nat such that
A3: for n st o<=n holds |.seq.n-0.|<l" by A1,SEQ_2:def 7;
reconsider m=max(k,o) as Nat by TARSKI:1;
take m;
let n;
assume
A4: m<=n;
k<=m by XXREAL_0:25;
then k<=n by A4,XXREAL_0:2;
then
A5: 0<seq.n by A2;
o<=m by XXREAL_0:25;
then o<=n by A4,XXREAL_0:2;
then |.seq.n-0.|<l" by A3;
then seq.n<l" by A5,ABSVALUE:def 1;
then 1/(l")<1/seq.n by A5,XREAL_1:76;
then
A6: l<1/seq.n by XCMPLX_1:216;
r<=|.r.| by ABSVALUE:4;
then r<l by Lm1;
then r<1/seq.n by A6,XXREAL_0:2;
then r<(seq.n)" by XCMPLX_1:215;
hence thesis by VALUED_1:10;
end;
theorem Th36:
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 convergent & lim seq=0;
given k such that
A2: for n st k<=n holds seq.n<0;
let r;
set l=|.r.|+1;
0<=|.r.| by COMPLEX1:46;
then consider o be Nat such that
A3: for n st o<=n holds |.seq.n-0.|<l" by A1,SEQ_2:def 7;
reconsider m=max(k,o) as Nat by TARSKI:1;
take m;
let n;
assume
A4: m<=n;
k<=m by XXREAL_0:25;
then k<= n by A4,XXREAL_0:2;
then
A5: seq.n<0 by A2;
then
A6: 0<-(seq.n) by XREAL_1:58;
o<=m by XXREAL_0:25;
then o<=n by A4,XXREAL_0:2;
then |.seq.n-0.|<l" by A3;
then -(seq.n)<l" by A5,ABSVALUE:def 1;
then 1/(l")<1/(-(seq.n)) by A6,XREAL_1:76;
then l<1/(-(seq.n)) by XCMPLX_1:216;
then l<(-(seq.n))" by XCMPLX_1:215;
then l<-((seq.n)") by XCMPLX_1:222;
then
A7: --((seq.n)")<-l by XREAL_1:24;
-|.r.|<=r by ABSVALUE:4;
then -|.r.|-1<r by Lm1;
then (seq.n)"<r by A7,XXREAL_0:2;
hence thesis by VALUED_1:10;
end;
theorem Th37:
seq is non-zero & seq is convergent & lim seq=0 & seq is
non-decreasing implies seq" is divergent_to-infty
proof
assume that
A1: seq is non-zero and
A2: seq is convergent & lim seq=0 and
A3: seq is non-decreasing;
for n holds 0<=n implies seq.n<0 by A1,A2,A3,Th2;
hence thesis by A2,Th36;
end;
theorem Th38:
seq is non-zero & seq is convergent & lim seq=0 & seq is
non-increasing implies seq" is divergent_to+infty
proof
assume that
A1: seq is non-zero and
A2: seq is convergent & lim seq=0 and
A3: seq is non-increasing;
for n holds 0<=n implies 0<seq.n by A1,A2,A3,Th3;
hence thesis by A2,Th35;
end;
theorem
seq is non-zero & seq is convergent & lim seq=0 & seq is increasing
implies seq" is divergent_to-infty by Th37;
theorem
seq is non-zero & seq is convergent & lim seq=0 & seq is decreasing
implies seq" is divergent_to+infty by Th38;
theorem
seq1 is bounded & (seq2 is divergent_to+infty or seq2 is
divergent_to-infty) implies seq1/"seq2 is convergent & lim(seq1/"seq2)=0
proof
assume that
A1: seq1 is bounded and
A2: seq2 is divergent_to+infty or seq2 is divergent_to-infty;
seq2" is convergent & lim(seq2")=0 by A2,Th34;
hence thesis by A1,SEQ_2:25,26;
end;
theorem Th42:
seq is divergent_to+infty & (for n holds seq.n<=seq1.n) implies
seq1 is divergent_to+infty
proof
assume that
A1: seq is divergent_to+infty and
A2: for n holds seq.n<= seq1.n;
let r;
consider n such that
A3: for m st n<=m holds r<seq.m by A1;
take n;
let m;
assume n<=m;
then
A4: r<seq.m by A3;
seq.m<=seq1.m by A2;
hence thesis by A4,XXREAL_0:2;
end;
theorem Th43:
seq is divergent_to-infty & (for n holds seq1.n<=seq.n) implies
seq1 is divergent_to-infty
proof
assume that
A1: seq is divergent_to-infty and
A2: for n holds seq1.n<= seq.n;
let r;
consider n such that
A3: for m st n<=m holds seq.m<r by A1;
take n;
let m;
assume n<=m;
then
A4: seq.m<r by A3;
seq1.m<=seq.m by A2;
hence thesis by A4,XXREAL_0:2;
end;
definition
let f;
attr f is convergent_in+infty means
(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
(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
(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
(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
(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
(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;
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 |.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 |.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;
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 & |.f.r1-g.|>=g1;
then consider g such that
A3: 0<g and
A4: for r ex r1 st r<r1 & r1 in dom f & |.f.r1-g2.|>=g by A1;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & |.f.$2
-g2.|>=g;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n be Element of NAT;
consider r such that
A6: X[n,r] by A4;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A5);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A7;
end;
then
A8: rng s c=dom f;
now
let n;
A9: n in NAT by ORDINAL1:def 12;
then n<s.n by A7;
hence s1.n<=s.n by FUNCT_1:18,A9;
end;
then s is divergent_to+infty by Lm5,Th20,Th42;
then f/*s is convergent & lim(f/*s)=g2 by A2,A8;
then consider n such that
A10: for m st n<=m holds |.(f/*s).m-g2.|<g by A3,SEQ_2:def 7;
A11: n in NAT by ORDINAL1:def 12;
|.(f/*s).n-g2.|<g by A10;
then |.f.(s.n)-g2.|<g by A8,FUNCT_2:108,A11;
hence contradiction by A7,A11;
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 |.f.r1- g.|<g1;
now
let s be Real_Sequence such that
A14: s is divergent_to+infty and
A15: rng s c=dom f;
A16: now
let g1 be Real;
assume
A17: 0<g1;
consider r such that
A18: for r1 st r<r1 & r1 in dom f holds |.f.r1-g.|<g1 by A13,A17;
consider n such that
A19: for m st n<=m holds r<s.m by A14;
take n;
let m;
A20: s.m in rng s by VALUED_0:28;
A21: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |.f.(s.m)-g.|<g1 by A15,A18,A19,A20;
hence |.(f/*s).m-g.|<g1 by A15,FUNCT_2:108,A21;
end;
hence f/*s is convergent;
hence lim(f/*s)=g by A16,SEQ_2:def 7;
end;
hence thesis by A12;
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 |.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 |.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;
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 & |.f.r1-g.|>=g1;
then consider g such that
A3: 0<g and
A4: for r ex r1 st r1<r & r1 in dom f & |.f.r1-g2.|>=g by A1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & |.f.
$2-g2.|>=g;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT;
consider r such that
A6: X[n,r] by A4;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A5);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A7;
end;
then
A8: rng s c=dom f;
deffunc U(Nat) = -$1;
consider s1 be Real_Sequence such that
A9: for n holds s1.n=U(n) from SEQ_1:sch 1;
now
let n;
n in NAT by ORDINAL1:def 12;
then s.n<-n by A7;
hence s.n<=s1.n by A9;
end;
then s is divergent_to-infty by A9,Th21,Th43;
then f/*s is convergent & lim(f/*s)=g2 by A2,A8;
then consider n such that
A10: for m st n<=m holds |.(f/*s).m-g2.|<g by A3,SEQ_2:def 7;
A11: n in NAT by ORDINAL1:def 12;
|.(f/*s).n-g2.|<g by A10;
then |.f.(s.n)-g2.|<g by A8,FUNCT_2:108,A11;
hence contradiction by A7,A11;
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 |.f.r1- g.|<g1;
now
let s be Real_Sequence such that
A14: s is divergent_to-infty and
A15: rng s c=dom f;
A16: now
let g1 be Real;
assume
A17: 0<g1;
consider r such that
A18: for r1 st r1<r & r1 in dom f holds |.f.r1-g.|<g1 by A13,A17;
consider n such that
A19: for m st n<=m holds s.m<r by A14;
take n;
let m;
A20: s.m in rng s by VALUED_0:28;
A21: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |.f.(s.m)-g.|<g1 by A15,A18,A19,A20;
hence |.(f/*s).m-g.|<g1 by A15,FUNCT_2:108,A21;
end;
hence f/*s is convergent;
hence lim(f/*s)=g by A16,SEQ_2:def 7;
end;
hence thesis by A12;
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;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & g >= f.
$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n be Element of NAT;
consider r such that
A4: X[n,r] by A2;
reconsider r as Real;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
now
let n;
A7: n in NAT by ORDINAL1:def 12;
n<s.n by A5,A7;
hence s1.n<=s.n by FUNCT_1:18,A7;
end;
then s is divergent_to+infty by Lm5,Th20,Th42;
then f/*s is divergent_to+infty by A1,A6;
then consider n such that
A8: for m st n<=m holds g<(f/*s).m;
A9: n in NAT by ORDINAL1:def 12;
g<(f/*s).n by A8;
then g<f.(s.n) by A6,FUNCT_2:108,A9;
hence contradiction by A5,A9;
end;
assume that
A10: for r ex g st r<g & g in dom f and
A11: 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
A12: s is divergent_to+infty and
A13: 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 A11;
consider n such that
A15: for m st n<=m holds r<s.m by A12;
take n;
let m;
A16: s.m in rng s by VALUED_0:28;
A17: m in NAT by ORDINAL1:def 12;
assume n<=m;
then g<f.(s.m) by A13,A14,A15,A16;
hence g<(f/*s).m by A13,FUNCT_2:108,A17;
end;
hence f/*s is divergent_to+infty;
end;
hence thesis by A10;
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;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & g <= f.
$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT;
consider r such that
A4: X[n,r] by A2;
reconsider r as Element of REAL by XREAL_0:def 1;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
now
let n;
A7: n in NAT by ORDINAL1:def 12;
n<s.n by A5,A7;
hence s1.n<=s.n by FUNCT_1:18,A7;
end;
then s is divergent_to+infty by Lm5,Th20,Th42;
then f/*s is divergent_to-infty by A1,A6;
then consider n such that
A8: for m st n<=m holds (f/*s).m<g;
A9: n in NAT by ORDINAL1:def 12;
(f/*s).n<g by A8;
then f.(s.n)<g by A6,FUNCT_2:108,A9;
hence contradiction by A5,A9;
end;
assume that
A10: for r ex g st r<g & g in dom f and
A11: 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
A12: s is divergent_to+infty and
A13: 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 A11;
consider n such that
A15: for m st n<=m holds r<s.m by A12;
take n;
let m;
A16: s.m in rng s by VALUED_0:28;
A17: m in NAT by ORDINAL1:def 12;
assume n<=m;
then f.(s.m)<g by A13,A14,A15,A16;
hence (f/*s).m<g by A13,FUNCT_2:108,A17;
end;
hence f/*s is divergent_to-infty;
end;
hence thesis by A10;
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
deffunc U(Nat) = -$1;
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;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & g >= f.$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A4: X[n,r] by A2;
reconsider r as Real;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
consider s1 be Real_Sequence such that
A7: for n holds s1.n=U(n) from SEQ_1:sch 1;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
s.n<-n by A5,A8;
hence s.n<=s1.n by A7;
end;
then s is divergent_to-infty by A7,Th21,Th43;
then f/*s is divergent_to+infty by A1,A6;
then consider n such that
A9: for m st n<=m holds g<(f/*s).m;
A10: n in NAT by ORDINAL1:def 12;
g<(f/*s).n by A9;
then g<f.(s.n) by A6,FUNCT_2:108,A10;
hence contradiction by A5,A10;
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 and
A14: rng s c=dom f;
now
let g;
consider r such that
A15: for r1 st r1<r & r1 in dom f holds g<f.r1 by A12;
consider n such that
A16: for m st n<=m holds s.m<r by A13;
take n;
let m;
A17: s.m in rng s by VALUED_0:28;
A18: m in NAT by ORDINAL1:def 12;
assume n<=m;
then g<f.(s.m) by A14,A15,A16,A17;
hence g<(f/*s).m by A14,FUNCT_2:108,A18;
end;
hence f/*s is divergent_to+infty;
end;
hence thesis by A11;
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
deffunc U(Nat) = -$1;
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;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & g <= f.
$2;
A3: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A4: X[n,r] by A2;
reconsider r as Real;
X[n,r] by A4;
hence thesis;
end;
consider s be Real_Sequence such that
A5: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A3);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A5;
end;
then
A6: rng s c=dom f;
consider s1 be Real_Sequence such that
A7: for n holds s1.n=U(n) from SEQ_1:sch 1;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
s.n<-n by A5,A8;
hence s.n<=s1.n by A7;
end;
then s is divergent_to-infty by A7,Th21,Th43;
then f/*s is divergent_to-infty by A1,A6;
then consider n such that
A9: for m st n<=m holds (f/*s).m<g;
A10: n in NAT by ORDINAL1:def 12;
(f/*s).n<g by A9;
then f.(s.n)<g by A6,FUNCT_2:108,A10;
hence contradiction by A5,A10;
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 and
A14: rng s c=dom f;
now
let g;
consider r such that
A15: for r1 st r1<r & r1 in dom f holds f.r1<g by A12;
consider n such that
A16: for m st n<=m holds s.m<r by A13;
take n;
let m;
A17: s.m in rng s by VALUED_0:28;
A18: m in NAT by ORDINAL1:def 12;
assume n<=m;
then f.(s.m)<g by A14,A15,A16,A17;
hence (f/*s).m<g by A14,FUNCT_2:108,A18;
end;
hence f/*s is divergent_to-infty;
end;
hence thesis by A11;
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 that
A1: f1 is divergent_in+infty_to+infty and
A2: f2 is divergent_in+infty_to+infty and
A3: for r ex g st r<g & g in dom f1/\dom f2;
A4: now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f1+f2);
A7: dom(f1+f2)=dom f1/\dom f2 by A6,Lm2;
rng seq c=dom f2 by A6,Lm2;
then
A8: f2/*seq is divergent_to+infty by A2,A5;
rng seq c=dom f1 by A6,Lm2;
then f1/*seq is divergent_to+infty by A1,A5;
then f1/*seq+f2/*seq is divergent_to+infty by A8,Th8;
hence (f1+f2)/*seq is divergent_to+infty by A6,A7,RFUNCT_2:8;
end;
A9: now
let seq;
assume that
A10: seq is divergent_to+infty and
A11: rng seq c=dom(f1(#) f2);
A12: dom(f1(#)f2)=dom f1/\ dom f2 by A11,Lm3;
rng seq c=dom f2 by A11,Lm3;
then
A13: f2/*seq is divergent_to+infty by A2,A10;
rng seq c=dom f1 by A11,Lm3;
then f1/*seq is divergent_to+infty by A1,A10;
then (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A13,Th10;
hence (f1(#)f2)/*seq is divergent_to+infty by A11,A12,RFUNCT_2:8;
end;
now
let r;
consider g such that
A14: r<g & g in dom f1/\dom f2 by A3;
take g;
thus r<g & g in dom(f1+f2) by A14,VALUED_1:def 1;
end;
hence f1+f2 is divergent_in+infty_to+infty by A4;
now
let r;
consider g such that
A15: r<g & g in dom f1/\dom f2 by A3;
take g;
thus r<g & g in dom(f1(#)f2) by A15,VALUED_1:def 4;
end;
hence thesis by A9;
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 that
A1: f1 is divergent_in+infty_to-infty and
A2: f2 is divergent_in+infty_to-infty and
A3: for r ex g st r<g & g in dom f1/\dom f2;
A4: now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f1+f2);
A7: dom(f1+f2)=dom f1/\dom f2 by A6,Lm2;
rng seq c=dom f2 by A6,Lm2;
then
A8: f2/*seq is divergent_to-infty by A2,A5;
rng seq c=dom f1 by A6,Lm2;
then f1/*seq is divergent_to-infty by A1,A5;
then f1/*seq+f2/*seq is divergent_to-infty by A8,Th11;
hence (f1+f2)/*seq is divergent_to-infty by A6,A7,RFUNCT_2:8;
end;
A9: now
let seq;
assume that
A10: seq is divergent_to+infty and
A11: rng seq c=dom(f1(#) f2);
A12: dom(f1(#)f2)=dom f1/\ dom f2 by A11,Lm3;
rng seq c=dom f2 by A11,Lm3;
then
A13: f2/*seq is divergent_to-infty by A2,A10;
rng seq c=dom f1 by A11,Lm3;
then f1/*seq is divergent_to-infty by A1,A10;
then (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A13,Th24;
hence (f1(#)f2)/*seq is divergent_to+infty by A11,A12,RFUNCT_2:8;
end;
now
let r;
consider g such that
A14: r<g & g in dom f1/\dom f2 by A3;
take g;
thus r<g & g in dom(f1+f2) by A14,VALUED_1:def 1;
end;
hence f1+f2 is divergent_in+infty_to-infty by A4;
now
let r;
consider g such that
A15: r<g & g in dom f1/\dom f2 by A3;
take g;
thus r<g & g in dom(f1(#)f2) by A15,VALUED_1:def 4;
end;
hence thesis by A9;
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 that
A1: f1 is divergent_in-infty_to+infty and
A2: f2 is divergent_in-infty_to+infty and
A3: for r ex g st g<r & g in dom f1/\dom f2;
A4: now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f1+f2);
A7: dom(f1+f2)=dom f1/\dom f2 by A6,Lm2;
rng seq c=dom f2 by A6,Lm2;
then
A8: f2/*seq is divergent_to+infty by A2,A5;
rng seq c=dom f1 by A6,Lm2;
then f1/*seq is divergent_to+infty by A1,A5;
then f1/*seq+f2/*seq is divergent_to+infty by A8,Th8;
hence (f1+f2)/*seq is divergent_to+infty by A6,A7,RFUNCT_2:8;
end;
A9: now
let seq;
assume that
A10: seq is divergent_to-infty and
A11: rng seq c=dom(f1(#) f2);
A12: dom(f1(#)f2)=dom f1/\ dom f2 by A11,Lm3;
rng seq c=dom f2 by A11,Lm3;
then
A13: f2/*seq is divergent_to+infty by A2,A10;
rng seq c=dom f1 by A11,Lm3;
then f1/*seq is divergent_to+infty by A1,A10;
then (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A13,Th10;
hence (f1(#)f2)/*seq is divergent_to+infty by A11,A12,RFUNCT_2:8;
end;
now
let r;
consider g such that
A14: g<r & g in dom f1/\dom f2 by A3;
take g;
thus g<r & g in dom(f1+f2) by A14,VALUED_1:def 1;
end;
hence f1+f2 is divergent_in-infty_to+infty by A4;
now
let r;
consider g such that
A15: g<r & g in dom f1/\dom f2 by A3;
take g;
thus g<r & g in dom(f1(#)f2) by A15,VALUED_1:def 4;
end;
hence thesis by A9;
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 that
A1: f1 is divergent_in-infty_to-infty and
A2: f2 is divergent_in-infty_to-infty and
A3: for r ex g st g<r & g in dom f1/\dom f2;
A4: now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f1+f2);
A7: dom(f1+f2)=dom f1/\dom f2 by A6,Lm2;
rng seq c=dom f2 by A6,Lm2;
then
A8: f2/*seq is divergent_to-infty by A2,A5;
rng seq c=dom f1 by A6,Lm2;
then f1/*seq is divergent_to-infty by A1,A5;
then f1/*seq+f2/*seq is divergent_to-infty by A8,Th11;
hence (f1+f2)/*seq is divergent_to-infty by A6,A7,RFUNCT_2:8;
end;
A9: now
let seq;
assume that
A10: seq is divergent_to-infty and
A11: rng seq c=dom(f1(#) f2);
A12: dom(f1(#)f2)=dom f1/\ dom f2 by A11,Lm3;
rng seq c=dom f2 by A11,Lm3;
then
A13: f2/*seq is divergent_to-infty by A2,A10;
rng seq c=dom f1 by A11,Lm3;
then f1/*seq is divergent_to-infty by A1,A10;
then (f1/*seq)(#)(f2/*seq) is divergent_to+infty by A13,Th24;
hence (f1(#)f2)/*seq is divergent_to+infty by A11,A12,RFUNCT_2:8;
end;
now
let r;
consider g such that
A14: g<r & g in dom f1/\dom f2 by A3;
take g;
thus g<r & g in dom(f1+f2) by A14,VALUED_1:def 1;
end;
hence f1+f2 is divergent_in-infty_to-infty by A4;
now
let r;
consider g such that
A15: g<r & g in dom f1/\dom f2 by A3;
take g;
thus g<r & g in dom(f1(#)f2) by A15,VALUED_1:def 4;
end;
hence thesis by A9;
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|right_open_halfline r is bounded_below) implies f1+f2 is
divergent_in+infty_to+infty
proof
assume that
A1: f1 is divergent_in+infty_to+infty and
A2: for r ex g st r<g & g in dom(f1+f2);
given r1 such that
A3: f2|right_open_halfline r1 is bounded_below;
now
let seq;
assume that
A4: seq is divergent_to+infty and
A5: rng seq c=dom(f1+f2);
consider k such that
A6: for n st k<=n holds r1<seq.n by A4;
A7: rng(seq^\k)c=rng seq by VALUED_0:21;
dom(f1+f2)=dom f1/\dom f2 by A5,Lm2;
then rng(seq^\k)c=dom f1/\dom f2 by A5,A7;
then
A8: f1/*(seq^\k)+f2/*(seq^\k)=(f1+f2)/*(seq^\k) by RFUNCT_2:8
.=((f1+f2)/*seq)^\k by A5,VALUED_0:27;
consider r2 be Real such that
A9: for g being object st g in right_open_halfline(r1)/\dom f2 holds r2
<=f2.g by A3,RFUNCT_1:71;
A10: rng seq c=dom f2 by A5,Lm2;
then
A11: rng(seq^\k)c=dom f2 by A7;
now
let n;
A12: n in NAT by ORDINAL1:def 12;
reconsider nk = n+k, nn=n as Element of NAT by ORDINAL1:def 12;
r1<seq.(nk) by A6,NAT_1:12;
then (seq^\k).nn < +infty & r1<(seq^\k).nn
by NAT_1:def 3,XXREAL_0:9;
then (seq^\k).n in rng(seq^\k) & (seq^\k).n in right_open_halfline(r1)
by VALUED_0:28,XXREAL_1:4;
then (seq^\k).n in right_open_halfline(r1)/\dom f2 by A11,XBOOLE_0:def 4;
then r2<=f2.((seq^\k).n) by A9;
then
A13: r2<=(f2/*(seq^\k)).n by A10,A7,FUNCT_2:108,XBOOLE_1:1,A12;
-|.r2.|<=r2 by ABSVALUE:4;
then -|.r2.|-1<r2-0 by XREAL_1:15;
hence -|.r2.|-1<(f2/*(seq^\k)).n by A13,XXREAL_0:2;
end;
then
A14: f2/*(seq^\k) is bounded_below;
rng seq c=dom f1 by A5,Lm2;
then
A15: rng(seq^\k)c=dom f1 by A7;
seq^\k is divergent_to+infty by A4,Th26;
then f1/*(seq^\k) is divergent_to+infty by A1,A15;
then f1/*(seq^\k)+f2/*(seq^\k) is divergent_to+infty by A14,Th9;
hence (f1+f2)/*seq is divergent_to+infty by A8,Th7;
end;
hence thesis by A2;
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 that
A1: f1 is divergent_in+infty_to+infty and
A2: for r ex g st r<g & g in dom(f1(#)f2);
given r2,r1 such that
A3: 0<r2 and
A4: for g st g in dom f2/\right_open_halfline(r1) holds r2<=f2.g;
now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f1(#) f2);
consider k such that
A7: for n st k<=n holds r1<seq.n by A5;
A8: rng(seq^\k)c=rng seq by VALUED_0:21;
A9: rng seq c=dom f2 by A6,Lm3;
then
A10: rng(seq^\k)c=dom f2 by A8;
A11: now
thus 0<r2 by A3;
let n;
A12: n in NAT by ORDINAL1:def 12;
r1<seq.(n+k) by A7,NAT_1:12;
then r1<(seq^\k).n by NAT_1:def 3;
then (seq^\k).n in {g2: r1<g2};
then (seq^\k).n in rng(seq^\k) & (seq^\k).n in right_open_halfline(r1)
by VALUED_0:28,XXREAL_1:230;
then (seq^\k).n in dom f2/\right_open_halfline(r1) by A10,XBOOLE_0:def 4;
then r2<=f2.((seq^\k).n) by A4;
hence r2<=(f2/*(seq^\k)).n by A9,A8,FUNCT_2:108,XBOOLE_1:1,A12;
end;
dom(f1(#)f2)=dom f1/\dom f2 by A6,Lm3;
then rng(seq^\k)c=dom f1/\dom f2 by A6,A8;
then
A13: (f1/*(seq^\k))(#)(f2/*(seq^\k))=(f1(#)f2)/*(seq^\k) by RFUNCT_2:8
.=((f1(#)f2)/*seq)^\k by A6,VALUED_0:27;
rng seq c=dom f1 by A6,Lm3;
then
A14: rng(seq^\k)c=dom f1 by A8;
seq^\k is divergent_to+infty by A5,Th26;
then f1/*(seq^\k) is divergent_to+infty by A1,A14;
then (f1/*(seq^\k))(#)(f2/*(seq^\k)) is divergent_to+infty by A11,Th22;
hence (f1(#)f2)/*seq is divergent_to+infty by A13,Th7;
end;
hence thesis by A2;
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|left_open_halfline r is bounded_below) implies f1+f2 is
divergent_in-infty_to+infty
proof
assume that
A1: f1 is divergent_in-infty_to+infty and
A2: for r ex g st g<r & g in dom(f1+f2);
given r1 such that
A3: f2|left_open_halfline r1 is bounded_below;
now
let seq;
assume that
A4: seq is divergent_to-infty and
A5: rng seq c=dom(f1+f2);
consider k such that
A6: for n st k<=n holds seq.n<r1 by A4;
A7: rng(seq^\k)c=rng seq by VALUED_0:21;
dom(f1+f2)=dom f1/\dom f2 by A5,Lm2;
then rng(seq^\k)c=dom f1/\dom f2 by A5,A7;
then
A8: f1/*(seq^\k)+f2/*(seq^\k)=(f1+f2)/*(seq^\k) by RFUNCT_2:8
.=((f1+f2)/*seq)^\k by A5,VALUED_0:27;
consider r2 be Real such that
A9: for g being object st g in left_open_halfline(r1)/\dom f2 holds r2<=
f2.g by A3,RFUNCT_1:71;
A10: rng seq c=dom f2 by A5,Lm2;
then
A11: rng(seq^\k)c=dom f2 by A7;
now
let n;
A12: n in NAT by ORDINAL1:def 12;
seq.(n+k)<r1 by A6,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then (seq^\k).n in {g2: g2<r1};
then
(seq^\k).n in rng(seq^\k) & (seq^\k).n in left_open_halfline(r1) by
VALUED_0:28,XXREAL_1:229;
then (seq^\k).n in left_open_halfline(r1)/\dom f2 by A11,XBOOLE_0:def 4;
then r2<=f2.((seq^\k).n) by A9;
then
A13: r2<=(f2/*(seq^\k)).n by A10,A7,FUNCT_2:108,XBOOLE_1:1,A12;
-|.r2.|<=r2 by ABSVALUE:4;
then -|.r2.|-1<r2-0 by XREAL_1:15;
hence -|.r2.|-1<(f2/*(seq^\k)).n by A13,XXREAL_0:2;
end;
then
A14: f2/*(seq^\k) is bounded_below;
rng seq c=dom f1 by A5,Lm2;
then
A15: rng(seq^\k)c=dom f1 by A7;
seq^\k is divergent_to-infty by A4,Th27;
then f1/*(seq^\k) is divergent_to+infty by A1,A15;
then f1/*(seq^\k)+f2/*(seq^\k) is divergent_to+infty by A14,Th9;
hence (f1+f2)/*seq is divergent_to+infty by A8,Th7;
end;
hence thesis by A2;
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 that
A1: f1 is divergent_in-infty_to+infty and
A2: for r ex g st g<r & g in dom(f1(#)f2);
given r2,r1 such that
A3: 0<r2 and
A4: for g st g in dom f2/\left_open_halfline(r1) holds r2<=f2.g;
now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f1(#) f2);
consider k such that
A7: for n st k<=n holds seq.n<r1 by A5;
A8: rng(seq^\k)c=rng seq by VALUED_0:21;
A9: rng seq c=dom f2 by A6,Lm3;
then
A10: rng(seq^\k)c=dom f2 by A8;
A11: now
thus 0<r2 by A3;
let n;
A12: n in NAT by ORDINAL1:def 12;
seq.(n+k)<r1 by A7,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then (seq^\k).n in {g2: g2<r1};
then
(seq^\k).n in rng(seq^\k) & (seq^\k).n in left_open_halfline(r1) by
VALUED_0:28,XXREAL_1:229;
then (seq^\k).n in dom f2/\left_open_halfline(r1) by A10,XBOOLE_0:def 4;
then r2<=f2.((seq^\k).n) by A4;
hence r2<=(f2/*(seq^\k)).n by A9,A8,FUNCT_2:108,XBOOLE_1:1,A12;
end;
dom(f1(#)f2)=dom f1/\dom f2 by A6,Lm3;
then rng(seq^\k)c=dom f1/\dom f2 by A6,A8;
then
A13: (f1/*(seq^\k))(#)(f2/*(seq^\k))=(f1(#)f2)/*(seq^\k) by RFUNCT_2:8
.=((f1(#)f2)/*seq)^\k by A6,VALUED_0:27;
rng seq c=dom f1 by A6,Lm3;
then
A14: rng(seq^\k)c=dom f1 by A8;
seq^\k is divergent_to-infty by A5,Th27;
then f1/*(seq^\k) is divergent_to+infty by A1,A14;
then (f1/*(seq^\k))(#)(f2/*(seq^\k)) is divergent_to+infty by A11,Th22;
hence (f1(#)f2)/*seq is divergent_to+infty by A13,Th7;
end;
hence thesis by A2;
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 that
A1: f is divergent_in+infty_to+infty and
A2: r>0;
A3: now
let seq;
assume that
A4: seq is divergent_to+infty and
A5: rng seq c=dom(r(#)f);
A6: rng seq c=dom f by A5,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A1,A4;
then r(#)(f/*seq) is divergent_to+infty by A2,Th13;
hence (r(#)f)/*seq is divergent_to+infty by A6,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A7: r1<g & g in dom f by A1;
take g;
thus r1<g & g in dom(r(#)f) by A7,VALUED_1:def 5;
end;
hence thesis by A3;
end;
thus f is divergent_in+infty_to+infty & r<0 implies r(#)f is
divergent_in+infty_to-infty
proof
assume that
A8: f is divergent_in+infty_to+infty and
A9: r<0;
A10: now
let seq;
assume that
A11: seq is divergent_to+infty and
A12: rng seq c=dom(r(#)f);
A13: rng seq c=dom f by A12,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A8,A11;
then r(#)(f/*seq) is divergent_to-infty by A9,Th13;
hence (r(#)f)/*seq is divergent_to-infty by A13,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A14: r1<g & g in dom f by A8;
take g;
thus r1<g & g in dom(r(#)f) by A14,VALUED_1:def 5;
end;
hence thesis by A10;
end;
thus f is divergent_in+infty_to-infty & r>0 implies r(#)f is
divergent_in+infty_to-infty
proof
assume that
A15: f is divergent_in+infty_to-infty and
A16: r>0;
A17: now
let seq;
assume that
A18: seq is divergent_to+infty and
A19: rng seq c=dom(r(#)f);
A20: rng seq c=dom f by A19,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A15,A18;
then r(#)(f/*seq) is divergent_to-infty by A16,Th14;
hence (r(#)f)/*seq is divergent_to-infty by A20,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A21: r1<g & g in dom f by A15;
take g;
thus r1<g & g in dom(r(#)f) by A21,VALUED_1:def 5;
end;
hence thesis by A17;
end;
assume that
A22: f is divergent_in+infty_to-infty and
A23: r<0;
A24: now
let seq;
assume that
A25: seq is divergent_to+infty and
A26: rng seq c=dom(r(#)f);
A27: rng seq c=dom f by A26,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A22,A25;
then r(#)(f/*seq) is divergent_to+infty by A23,Th14;
hence (r(#)f)/*seq is divergent_to+infty by A27,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A28: r1<g & g in dom f by A22;
take g;
thus r1<g & g in dom(r(#)f) by A28,VALUED_1:def 5;
end;
hence thesis by A24;
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 that
A1: f is divergent_in-infty_to+infty and
A2: r>0;
A3: now
let seq;
assume that
A4: seq is divergent_to-infty and
A5: rng seq c=dom(r(#)f);
A6: rng seq c=dom f by A5,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A1,A4;
then r(#)(f/*seq) is divergent_to+infty by A2,Th13;
hence (r(#)f)/*seq is divergent_to+infty by A6,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A7: g<r1 & g in dom f by A1;
take g;
thus g<r1 & g in dom(r(#)f) by A7,VALUED_1:def 5;
end;
hence thesis by A3;
end;
thus f is divergent_in-infty_to+infty & r<0 implies r(#)f is
divergent_in-infty_to-infty
proof
assume that
A8: f is divergent_in-infty_to+infty and
A9: r<0;
A10: now
let seq;
assume that
A11: seq is divergent_to-infty and
A12: rng seq c=dom(r(#)f);
A13: rng seq c=dom f by A12,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A8,A11;
then r(#)(f/*seq) is divergent_to-infty by A9,Th13;
hence (r(#)f)/*seq is divergent_to-infty by A13,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A14: g<r1 & g in dom f by A8;
take g;
thus g<r1 & g in dom(r(#)f) by A14,VALUED_1:def 5;
end;
hence thesis by A10;
end;
thus f is divergent_in-infty_to-infty & r>0 implies r(#)f is
divergent_in-infty_to-infty
proof
assume that
A15: f is divergent_in-infty_to-infty and
A16: r>0;
A17: now
let seq;
assume that
A18: seq is divergent_to-infty and
A19: rng seq c=dom(r(#)f);
A20: rng seq c=dom f by A19,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A15,A18;
then r(#)(f/*seq) is divergent_to-infty by A16,Th14;
hence (r(#)f)/*seq is divergent_to-infty by A20,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A21: g<r1 & g in dom f by A15;
take g;
thus g<r1 & g in dom(r(#)f) by A21,VALUED_1:def 5;
end;
hence thesis by A17;
end;
assume that
A22: f is divergent_in-infty_to-infty and
A23: r<0;
A24: now
let seq;
assume that
A25: seq is divergent_to-infty and
A26: rng seq c=dom(r(#)f);
A27: rng seq c=dom f by A26,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A22,A25;
then r(#)(f/*seq) is divergent_to+infty by A23,Th14;
hence (r(#)f)/*seq is divergent_to+infty by A27,RFUNCT_2:9;
end;
now
let r1;
consider g such that
A28: g<r1 & g in dom f by A22;
take g;
thus g<r1 & g in dom(r(#)f) by A28,VALUED_1:def 5;
end;
hence thesis by A24;
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 seq;
assume that
A4: seq is divergent_to+infty and
A5: rng seq c=dom abs(f);
A6: rng seq c=dom f by A5,VALUED_1:def 11;
then f/*seq is divergent_to+infty by A2,A4;
then |.f/*seq.| is divergent_to+infty by Th25;
hence (abs f)/*seq is divergent_to+infty by A6,RFUNCT_2:10;
end;
now
let r;
consider g such that
A7: r<g & g in dom f by A2;
take g;
thus r<g & g in dom abs(f) by A7,VALUED_1:def 11;
end;
hence thesis by A3;
end;
suppose
A8: f is divergent_in+infty_to-infty;
A9: now
let seq;
assume that
A10: seq is divergent_to+infty and
A11: rng seq c=dom abs(f);
A12: rng seq c=dom f by A11,VALUED_1:def 11;
then f/*seq is divergent_to-infty by A8,A10;
then |.f/*seq.| is divergent_to+infty by Th25;
hence (abs f)/*seq is divergent_to+infty by A12,RFUNCT_2:10;
end;
now
let r;
consider g such that
A13: r<g & g in dom f by A8;
take g;
thus r<g & g in dom abs(f) by A13,VALUED_1:def 11;
end;
hence thesis by A9;
end;
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 seq;
assume that
A4: seq is divergent_to-infty and
A5: rng seq c=dom abs(f);
A6: rng seq c=dom f by A5,VALUED_1:def 11;
then f/*seq is divergent_to+infty by A2,A4;
then abs(f/*seq) is divergent_to+infty by Th25;
hence (abs f)/*seq is divergent_to+infty by A6,RFUNCT_2:10;
end;
now
let r;
consider g such that
A7: g<r & g in dom f by A2;
take g;
thus g<r & g in dom abs(f) by A7,VALUED_1:def 11;
end;
hence thesis by A3;
end;
suppose
A8: f is divergent_in-infty_to-infty;
A9: now
let seq;
assume that
A10: seq is divergent_to-infty and
A11: rng seq c=dom abs(f);
A12: rng seq c=dom f by A11,VALUED_1:def 11;
then f/*seq is divergent_to-infty by A8,A10;
then abs(f/*seq) is divergent_to+infty by Th25;
hence (abs f)/*seq is divergent_to+infty by A12,RFUNCT_2:10;
end;
now
let r;
consider g such that
A13: g<r & g in dom f by A8;
take g;
thus g<r & g in dom abs(f) by A13,VALUED_1:def 11;
end;
hence thesis by A9;
end;
end;
hence thesis;
end;
theorem Th62:
(ex r st f|right_open_halfline r is non-decreasing & not f|
right_open_halfline r is bounded_above) & (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|right_open_halfline r1 is non-decreasing and
A2: not f|right_open_halfline r1 is bounded_above;
A3: now
let seq such that
A4: seq is divergent_to+infty and
A5: rng seq c=dom f;
now
let r;
consider g1 being object such that
A6: g1 in right_open_halfline(r1)/\dom f and
A7: r<f.g1 by A2,RFUNCT_1:70;
reconsider g1 as Real by A6;
consider n such that
A8: for m st n<=m holds |.g1.|+|.r1.|<seq.m by A4;
take n;
let m;
A9: m in NAT by ORDINAL1:def 12;
assume n<=m;
then
A10: |.g1.|+|.r1.|<seq.m by A8;
r1<=|.r1.| & 0<=|.g1.| by ABSVALUE:4,COMPLEX1:46;
then 0+r1<=|.g1.|+|.r1.| by XREAL_1:7;
then r1<seq.m by A10,XXREAL_0:2;
then seq.m in {g2: r1<g2};
then seq.m in rng seq & seq.m in right_open_halfline(r1) by VALUED_0:28
,XXREAL_1:230;
then
A11: seq.m in right_open_halfline(r1)/\dom f by A5,XBOOLE_0:def 4;
g1<=|.g1.| & 0<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then g1+0<=|.g1.|+|.r1.| by XREAL_1:7;
then g1<seq.m by A10,XXREAL_0:2;
then f.g1<=f.(seq.m) by A1,A6,A11,RFUNCT_2:22;
then r<f.(seq.m) by A7,XXREAL_0:2;
hence r<(f/*seq).m by A5,FUNCT_2:108,A9;
end;
hence f/*seq is divergent_to+infty;
end;
assume for r ex g st r<g & g in dom f;
hence thesis by A3;
end;
theorem
(ex r st f|right_open_halfline r is increasing & not f|
right_open_halfline r is bounded_above) & (for r ex g st r<g & g in dom f)
implies f is divergent_in+infty_to+infty by Th62;
theorem Th64:
(ex r st f|right_open_halfline r is non-increasing & not f|
right_open_halfline r is bounded_below) & (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|right_open_halfline r1 is non-increasing and
A2: not f|right_open_halfline r1 is bounded_below;
A3: now
let seq such that
A4: seq is divergent_to+infty and
A5: rng seq c=dom f;
now
let r;
consider g1 being object such that
A6: g1 in right_open_halfline(r1)/\dom f and
A7: f.g1<r by A2,RFUNCT_1:71;
reconsider g1 as Real by A6;
consider n such that
A8: for m st n<=m holds |.g1.|+|.r1.|<seq.m by A4;
take n;
let m;
A9: m in NAT by ORDINAL1:def 12;
assume n<=m;
then
A10: |.g1.|+|.r1.|<seq.m by A8;
r1<=|.r1.| & 0<=|.g1.| by ABSVALUE:4,COMPLEX1:46;
then 0+r1<=|.g1.|+|.r1.| by XREAL_1:7;
then r1<seq.m by A10,XXREAL_0:2;
then seq.m in {g2: r1<g2};
then seq.m in rng seq & seq.m in right_open_halfline(r1) by VALUED_0:28
,XXREAL_1:230;
then
A11: seq.m in right_open_halfline(r1)/\dom f by A5,XBOOLE_0:def 4;
g1<=|.g1.| & 0<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then g1+0<=|.g1.|+|.r1.| by XREAL_1:7;
then g1<seq.m by A10,XXREAL_0:2;
then f.(seq.m)<=f.g1 by A1,A6,A11,RFUNCT_2:23;
then f.(seq.m)<r by A7,XXREAL_0:2;
hence (f/*seq).m<r by A5,FUNCT_2:108,A9;
end;
hence f/*seq is divergent_to-infty;
end;
assume for r ex g st r<g & g in dom f;
hence thesis by A3;
end;
theorem
(ex r st f|right_open_halfline r is decreasing & not f|
right_open_halfline r is bounded_below) & (for r ex g st r<g & g in dom f)
implies f is divergent_in+infty_to-infty by Th64;
theorem Th66:
(ex r st f|left_open_halfline r is non-increasing & not f|
left_open_halfline r is bounded_above) & (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|left_open_halfline r1 is non-increasing and
A2: not f|left_open_halfline r1 is bounded_above;
A3: now
let seq such that
A4: seq is divergent_to-infty and
A5: rng seq c=dom f;
now
let r;
consider g1 being object such that
A6: g1 in left_open_halfline(r1)/\dom f and
A7: r<f.g1 by A2,RFUNCT_1:70;
reconsider g1 as Real by A6;
consider n such that
A8: for m st n<=m holds seq.m<-|.r1.|-|.g1.| by A4;
take n;
let m;
A9: m in NAT by ORDINAL1:def 12;
assume n<=m;
then
A10: seq.m<-|.r1.|-|.g1.| by A8;
-|.r1.|<=r1 & 0<=|.g1.| by ABSVALUE:4,COMPLEX1:46;
then -|.r1.|-|.g1.|<=r1-0 by XREAL_1:13;
then seq.m<r1 by A10,XXREAL_0:2;
then seq.m in {g2: g2<r1};
then seq.m in rng seq & seq.m in left_open_halfline(r1) by VALUED_0:28
,XXREAL_1:229;
then
A11: seq.m in left_open_halfline(r1)/\dom f by A5,XBOOLE_0:def 4;
-|.g1.|<=g1 & 0<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then -|.g1.|-|.r1.|<=g1-0 by XREAL_1:13;
then seq.m<g1 by A10,XXREAL_0:2;
then f.g1<= f.(seq.m) by A1,A6,A11,RFUNCT_2:23;
then r<f.(seq.m) by A7,XXREAL_0:2;
hence r<(f/*seq).m by A5,FUNCT_2:108,A9;
end;
hence f/*seq is divergent_to+infty;
end;
assume for r ex g st g<r & g in dom f;
hence thesis by A3;
end;
theorem
(ex r st f|left_open_halfline r is decreasing & not f|
left_open_halfline r is bounded_above) & (for r ex g st g<r & g in dom f)
implies f is divergent_in-infty_to+infty by Th66;
theorem Th68:
(ex r st f|left_open_halfline r is non-decreasing & not f|
left_open_halfline r is bounded_below) & (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|left_open_halfline r1 is non-decreasing and
A2: not f|left_open_halfline r1 is bounded_below;
A3: now
let seq such that
A4: seq is divergent_to-infty and
A5: rng seq c=dom f;
now
let r;
consider g1 being object such that
A6: g1 in left_open_halfline(r1)/\dom f and
A7: f.g1<r by A2,RFUNCT_1:71;
reconsider g1 as Real by A6;
consider n such that
A8: for m st n<=m holds seq.m<-|.r1.|-|.g1.| by A4;
take n;
let m;
A9: m in NAT by ORDINAL1:def 12;
assume n<=m;
then
A10: seq.m<-|.r1.|-|.g1.| by A8;
-|.r1.|<=r1 & 0<=|.g1.| by ABSVALUE:4,COMPLEX1:46;
then -|.r1.|-|.g1.|<=r1-0 by XREAL_1:13;
then seq.m<r1 by A10,XXREAL_0:2;
then seq.m in {g2: g2<r1};
then seq.m in rng seq & seq.m in left_open_halfline(r1) by VALUED_0:28
,XXREAL_1:229;
then
A11: seq.m in left_open_halfline(r1)/\dom f by A5,XBOOLE_0:def 4;
-|.g1.|<=g1 & 0<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then -|.g1.|-|.r1.|<=g1-0 by XREAL_1:13;
then seq.m<g1 by A10,XXREAL_0:2;
then f.(seq.m)<= f.g1 by A1,A6,A11,RFUNCT_2:22;
then f.(seq.m)<r by A7,XXREAL_0:2;
hence (f/*seq).m<r by A5,FUNCT_2:108,A9;
end;
hence f/*seq is divergent_to-infty;
end;
assume for r ex g st g<r & g in dom f;
hence thesis by A3;
end;
theorem
(ex r st f|left_open_halfline r is increasing & not f|
left_open_halfline r is bounded_below) & (for r ex g st g<r & g in dom f)
implies f is divergent_in-infty_to-infty by Th68;
theorem Th70:
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 that
A1: f1 is divergent_in+infty_to+infty and
A2: for r ex g st r<g & g in dom f;
given r1 such that
A3: dom f/\right_open_halfline(r1)c= dom f1/\right_open_halfline(r1) and
A4: for g st g in dom f/\right_open_halfline(r1) holds f1.g<=f.g;
now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom f;
consider k such that
A7: for n st k<=n holds r1<seq.n by A5;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A8: (seq^\k).n=x by FUNCT_2:113;
r1<seq.(n+k) by A7,NAT_1:12;
then r1<(seq^\k).n by NAT_1:def 3;
then x in {g2: r1<g2} by A8;
hence x in right_open_halfline(r1) by XXREAL_1:230;
end;
then
A9: rng(seq^\k)c=right_open_halfline(r1);
A10: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A6;
then
A11: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A9,XBOOLE_1:19;
then
A12: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A3;
A13: dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
A14: now
let n;
A15: n in NAT by ORDINAL1:def 12;
(seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f1.((seq^\k).n)<=f.((seq^\k).n) by A4,A11;
then (f1/*(seq^\k)).n<=f.((seq^\k).n)
by A12,A13,FUNCT_2:108,XBOOLE_1:1,A15;
hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n
by A6,A10,FUNCT_2:108,XBOOLE_1:1,A15;
end;
A16: seq^\k is divergent_to+infty by A5,Th26;
rng(seq^\k)c=dom f1 by A12,A13;
then f1/*(seq^\k) is divergent_to+infty by A1,A16;
then
A17: f/*(seq^\k) is divergent_to+infty by A14,Th42;
f/*(seq^\k)=(f/*seq)^\k by A6,VALUED_0:27;
hence f/*seq is divergent_to+infty by A17,Th7;
end;
hence thesis by A2;
end;
theorem Th71:
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 that
A1: f1 is divergent_in+infty_to-infty and
A2: for r ex g st r<g & g in dom f;
given r1 such that
A3: dom f/\right_open_halfline(r1)c= dom f1/\right_open_halfline(r1) and
A4: for g st g in dom f/\right_open_halfline(r1) holds f.g<=f1.g;
now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom f;
consider k such that
A7: for n st k<=n holds r1<seq.n by A5;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A8: (seq^\k).n=x by FUNCT_2:113;
r1<seq.(n+k) by A7,NAT_1:12;
then r1<(seq^\k).n by NAT_1:def 3;
then x in {g2: r1<g2} by A8;
hence x in right_open_halfline(r1) by XXREAL_1:230;
end;
then
A9: rng(seq^\k)c=right_open_halfline(r1);
A10: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A6;
then
A11: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A9,XBOOLE_1:19;
then
A12: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A3;
A13: dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
A14: now
let n;
A15: n in NAT by ORDINAL1:def 12;
(seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f.((seq^\k).n)<=f1.((seq^\k).n) by A4,A11;
then (f/*(seq^\k)).n<=f1.((seq^\k).n)
by A6,A10,FUNCT_2:108,XBOOLE_1:1,A15;
hence (f/*(seq^\k)).n<=(f1/*(seq^\k)).n
by A12,A13,FUNCT_2:108,XBOOLE_1:1,A15;
end;
A16: seq^\k is divergent_to+infty by A5,Th26;
rng(seq^\k)c=dom f1 by A12,A13;
then f1/*(seq^\k) is divergent_to-infty by A1,A16;
then
A17: f/*(seq^\k) is divergent_to-infty by A14,Th43;
f/*(seq^\k)=(f/*seq)^\k by A6,VALUED_0:27;
hence f/*seq is divergent_to-infty by A17,Th7;
end;
hence thesis by A2;
end;
theorem Th72:
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 that
A1: f1 is divergent_in-infty_to+infty and
A2: for r ex g st g<r & g in dom f;
given r1 such that
A3: dom f/\left_open_halfline(r1)c= dom f1/\left_open_halfline(r1) and
A4: for g st g in dom f/\left_open_halfline(r1) holds f1.g<=f.g;
now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom f;
consider k such that
A7: for n st k<=n holds seq.n<r1 by A5;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A8: (seq^\k).n=x by FUNCT_2:113;
seq.(n+k)<r1 by A7,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then x in {g2: g2<r1} by A8;
hence x in left_open_halfline(r1) by XXREAL_1:229;
end;
then
A9: rng(seq^\k)c=left_open_halfline(r1);
A10: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A6;
then
A11: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A9,XBOOLE_1:19;
then
A12: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A3;
A13: dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
A14: now
let n;
A15: n in NAT by ORDINAL1:def 12;
(seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f1.((seq^\k).n)<=f.((seq^\k).n) by A4,A11;
then (f1/*(seq^\k)).n<=f.((seq^\k).n)
by A12,A13,FUNCT_2:108,XBOOLE_1:1,A15;
hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n
by A6,A10,FUNCT_2:108,XBOOLE_1:1,A15;
end;
A16: seq^\k is divergent_to-infty by A5,Th27;
rng(seq^\k)c=dom f1 by A12,A13;
then f1/*(seq^\k) is divergent_to+infty by A1,A16;
then
A17: f/*(seq^\k) is divergent_to+infty by A14,Th42;
f/*(seq^\k)=(f/*seq)^\k by A6,VALUED_0:27;
hence f/*seq is divergent_to+infty by A17,Th7;
end;
hence thesis by A2;
end;
theorem Th73:
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 that
A1: f1 is divergent_in-infty_to-infty and
A2: for r ex g st g<r & g in dom f;
given r1 such that
A3: dom f/\left_open_halfline(r1)c= dom f1/\left_open_halfline(r1) and
A4: for g st g in dom f/\left_open_halfline(r1) holds f.g<=f1.g;
now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom f;
consider k such that
A7: for n st k<=n holds seq.n<r1 by A5;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A8: (seq^\k).n=x by FUNCT_2:113;
seq.(n+k)<r1 by A7,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then x in {g2: g2<r1} by A8;
hence x in left_open_halfline(r1) by XXREAL_1:229;
end;
then
A9: rng(seq^\k)c=left_open_halfline(r1);
A10: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A6;
then
A11: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A9,XBOOLE_1:19;
then
A12: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A3;
A13: dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
A14: now
let n;
A15: n in NAT by ORDINAL1:def 12;
(seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f.((seq^\k).n)<=f1.((seq^\k).n) by A4,A11;
then (f/*(seq^\k)).n<=f1.((seq^\k).n)
by A6,A10,FUNCT_2:108,XBOOLE_1:1,A15;
hence (f/*(seq^\k)).n<=(f1/*(seq^\k)).n
by A12,A13,FUNCT_2:108,XBOOLE_1:1,A15;
end;
A16: seq^\k is divergent_to-infty by A5,Th27;
rng(seq^\k)c=dom f1 by A12,A13;
then f1/*(seq^\k) is divergent_to-infty by A1,A16;
then
A17: f/*(seq^\k) is divergent_to-infty by A14,Th43;
f/*(seq^\k)=(f/*seq)^\k by A6,VALUED_0:27;
hence f/*seq is divergent_to-infty by A17,Th7;
end;
hence thesis by A2;
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 and
A3: for g st g in right_open_halfline(r1) holds f1.g<=f.g;
A4: now
let r;
consider g being Real such that
A5: |.r.|+|.r1.|<g by XREAL_1:1;
take g;
0<=|.r1.| & r<=|.r.| by ABSVALUE:4,COMPLEX1:46;
then 0+r<=|.r.|+|.r1.| by XREAL_1:7;
hence r<g by A5,XXREAL_0:2;
0<=|.r.| & r1<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then 0+r1<=|.r.|+|.r1.| by XREAL_1:7;
then r1<g by A5,XXREAL_0:2;
then g in {g2: r1<g2};
then g in right_open_halfline(r1) by XXREAL_1:230;
hence g in dom f by A2,XBOOLE_0:def 4;
end;
now
dom f/\dom f1 c=dom f by XBOOLE_1:17;
then
A6: dom f/\right_open_halfline(r1)=right_open_halfline(r1) by A2,XBOOLE_1:1,28;
dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
hence dom f/\right_open_halfline(r1) c=dom f1/\right_open_halfline(r1) by
A2,A6,XBOOLE_1:1,28;
let g;
assume g in dom f/\right_open_halfline(r1);
hence f1.g<=f.g by A3,A6;
end;
hence thesis by A1,A4,Th70;
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 and
A3: for g st g in right_open_halfline(r1) holds f.g<=f1.g;
A4: now
let r;
consider g being Real such that
A5: |.r.|+|.r1.|<g by XREAL_1:1;
take g;
0<=|.r1.| & r<=|.r.| by ABSVALUE:4,COMPLEX1:46;
then 0+r<=|.r.|+|.r1.| by XREAL_1:7;
hence r<g by A5,XXREAL_0:2;
0<=|.r.| & r1<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then 0+r1<=|.r.|+|.r1.| by XREAL_1:7;
then r1<g by A5,XXREAL_0:2;
then g in {g2: r1<g2};
then g in right_open_halfline(r1) by XXREAL_1:230;
hence g in dom f by A2,XBOOLE_0:def 4;
end;
now
dom f/\dom f1 c=dom f by XBOOLE_1:17;
then
A6: dom f/\right_open_halfline(r1)=right_open_halfline(r1) by A2,XBOOLE_1:1,28;
dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
hence dom f/\right_open_halfline(r1) c=dom f1/\right_open_halfline(r1) by
A2,A6,XBOOLE_1:1,28;
let g;
assume g in dom f/\right_open_halfline(r1);
hence f.g<=f1.g by A3,A6;
end;
hence thesis by A1,A4,Th71;
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 and
A3: for g st g in left_open_halfline(r1) holds f1.g<=f.g;
A4: now
let r;
consider g being Real such that
A5: g<-|.r.|-|.r1.| by XREAL_1:2;
take g;
0<=|.r1.| & -|.r.|<=r by ABSVALUE:4,COMPLEX1:46;
then -|.r.|-|.r1.|<=r-0 by XREAL_1:13;
hence g<r by A5,XXREAL_0:2;
0<=|.r.| & -|.r1.|<=r1 by ABSVALUE:4,COMPLEX1:46;
then -|.r1.|-|.r.|<=r1-0 by XREAL_1:13;
then g<r1 by A5,XXREAL_0:2;
then g in {g2: g2<r1};
then g in left_open_halfline(r1) by XXREAL_1:229;
hence g in dom f by A2,XBOOLE_0:def 4;
end;
now
dom f/\dom f1 c=dom f by XBOOLE_1:17;
then
A6: dom f/\left_open_halfline(r1)=left_open_halfline(r1) by A2,XBOOLE_1:1,28;
dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
hence
dom f/\left_open_halfline(r1) c=dom f1/\left_open_halfline(r1) by A2,A6,
XBOOLE_1:1,28;
let g;
assume g in dom f/\left_open_halfline(r1);
hence f1.g<=f.g by A3,A6;
end;
hence thesis by A1,A4,Th72;
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 and
A3: for g st g in left_open_halfline(r1) holds f.g<=f1.g;
A4: now
let r;
consider g being Real such that
A5: g<-|.r.|-|.r1.| by XREAL_1:2;
take g;
0<=|.r1.| & -|.r.|<=r by ABSVALUE:4,COMPLEX1:46;
then -|.r.|-|.r1.|<=r-0 by XREAL_1:13;
hence g<r by A5,XXREAL_0:2;
0<=|.r.| & -|.r1.|<=r1 by ABSVALUE:4,COMPLEX1:46;
then -|.r1.|-|.r.|<=r1-0 by XREAL_1:13;
then g<r1 by A5,XXREAL_0:2;
then g in {g2: g2<r1};
then g in left_open_halfline(r1) by XXREAL_1:229;
hence g in dom f by A2,XBOOLE_0:def 4;
end;
now
dom f/\dom f1 c=dom f by XBOOLE_1:17;
then
A6: dom f/\left_open_halfline(r1)=left_open_halfline(r1) by A2,XBOOLE_1:1,28;
dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
hence
dom f/\left_open_halfline(r1) c=dom f1/\left_open_halfline(r1) by A2,A6,
XBOOLE_1:1,28;
let g;
assume g in dom f/\left_open_halfline(r1);
hence f.g<=f1.g by A3,A6;
end;
hence thesis by A1,A4,Th73;
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;
uniqueness
proof
defpred X[Nat,Real] means $1<$2 & $2 in dom f;
let g1,g2 be Real 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;
A4: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A5: X[n,r] by A1;
reconsider r as Real;
X[n,r] by A5;
hence thesis;
end;
consider s2 be Real_Sequence such that
A6: for n being Element of NAT holds X[n,s2.n] from FUNCT_2:sch 3(A4);
A7: rng s2 c= dom f
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
hence thesis by A6;
end;
now
let n;
A8: n in NAT by ORDINAL1:def 12;
then n<s2.n by A6;
hence s1.n<=s2.n by FUNCT_1:18,A8;
end;
then
A9: s2 is divergent_to+infty by Lm5,Th20,Th42;
then lim(f/*s2)=g1 by A2,A7;
hence thesis by A3,A9,A7;
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;
uniqueness
proof
deffunc U(Nat) = -$1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f;
let g1,g2 be Real 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;
consider s2 be Real_Sequence such that
A4: for n holds s2.n=U(n) from SEQ_1:sch 1;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A6: X[n,r] by A1;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s1 be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s1.n] from FUNCT_2:sch 3(A5);
A8: rng s1 c= dom f
proof
let x be Real;
assume x in rng s1;
then ex n being Element of NAT st x=s1.n by FUNCT_2:113;
hence thesis by A7;
end;
now
let n;
n in NAT by ORDINAL1:def 12;
then s1.n<-n by A7;
hence s1.n<=s2.n by A4;
end;
then
A9: s1 is divergent_to-infty by A4,Th21,Th43;
then lim(f/*s1)=g1 by A2,A8;
hence thesis by A3,A9,A8;
end;
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 r1<r & r1 in dom f holds |.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 |.f.r1-g.|<g1
proof
deffunc U(Nat) = -$1;
assume
A2: lim_in-infty f=g;
consider s1 be Real_Sequence such that
A3: for n holds s1.n=U(n) from SEQ_1:sch 1;
given g1 such that
A4: 0<g1 and
A5: for r ex r1 st r1<r & r1 in dom f & |.f.r1-g.|>=g1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f & |.f.
$2-g.|>=g1;
A6: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A7: X[n,r] by A5;
reconsider r as Real;
X[n,r] by A7;
hence thesis;
end;
consider s be Real_Sequence such that
A8: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A8;
end;
then
A9: rng s c=dom f;
now
let n;
n in NAT by ORDINAL1:def 12;
then s.n<-n by A8;
hence s.n<=s1.n by A3;
end;
then s is divergent_to-infty by A3,Th21,Th43;
then f/*s is convergent & lim(f/*s)=g by A1,A2,A9,Def13;
then consider n such that
A10: for m st n<=m holds |.(f/*s).m-g.|<g1 by A4,SEQ_2:def 7;
A11: n in NAT by ORDINAL1:def 12;
|.(f/*s).n-g.|<g1 by A10;
then |.f.(s.n)-g.|<g1 by A9,FUNCT_2:108,A11;
hence contradiction by A8,A11;
end;
assume
A12: for g1 st 0<g1 ex r st for r1 st r1<r & r1 in dom f holds |.f.r1- g.|<g1;
reconsider g as Real;
now
let s be Real_Sequence such that
A13: s is divergent_to-infty and
A14: rng s c=dom f;
A15: now
let g1 be Real;
assume
A16: 0<g1;
consider r such that
A17: for r1 st r1<r & r1 in dom f holds |.f.r1-g.|<g1 by A12,A16;
consider n such that
A18: for m st n<=m holds s.m<r by A13;
take n;
let m;
A19: s.m in rng s by VALUED_0:28;
A20: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |.f.(s.m)-g.|<g1 by A14,A17,A18,A19;
hence |.(f/*s).m-g.|<g1 by A14,FUNCT_2:108,A20;
end;
hence f/*s is convergent;
hence lim(f/*s)=g by A15,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 |.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 |.f.r1-g.|<g1
proof
assume
A2: lim_in+infty f=g;
given g1 such that
A3: 0<g1 and
A4: for r ex r1 st r<r1 & r1 in dom f & |.f.r1-g.|>=g1;
defpred X[Nat,Real] means $1<$2 & $2 in dom f & |.f.$2
-g.|>=g1;
A5: for n being Element of NAT ex r being Element of REAL st X[n,r]
proof let n being Element of NAT ;
consider r such that
A6: X[n,r] by A4;
reconsider r as Real;
X[n,r] by A6;
hence thesis;
end;
consider s be Real_Sequence such that
A7: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A5);
now
let x be object;
assume x in rng s;
then ex n being Element of NAT st s.n=x by FUNCT_2:113;
hence x in dom f by A7;
end;
then
A8: rng s c=dom f;
now
let n;
A9: n in NAT by ORDINAL1:def 12;
then n<s.n by A7;
hence s1.n<=s.n by FUNCT_1:18,A9;
end;
then s is divergent_to+infty by Lm5,Th20,Th42;
then f/*s is convergent & lim(f/*s)=g by A1,A2,A8,Def12;
then consider n such that
A10: for m st n<=m holds |.(f/*s).m-g.|<g1 by A3,SEQ_2:def 7;
A11: n in NAT by ORDINAL1:def 12;
|.(f/*s).n-g.|<g1 by A10;
then |.f.(s.n)-g.|<g1 by A8,FUNCT_2:108,A11;
hence contradiction by A7,A11;
end;
assume
A12: for g1 st 0<g1 ex r st for r1 st r<r1 & r1 in dom f holds |.f.r1- g.|<g1;
reconsider g as Real;
now
let s be Real_Sequence such that
A13: s is divergent_to+infty and
A14: rng s c=dom f;
A15: now
let g1 be Real;
assume
A16: 0<g1;
consider r such that
A17: for r1 st r<r1 & r1 in dom f holds |.f.r1-g.|<g1 by A12,A16;
consider n such that
A18: for m st n<=m holds r<s.m by A13;
take n;
let m;
A19: s.m in rng s by VALUED_0:28;
A20: m in NAT by ORDINAL1:def 12;
assume n<=m;
then |.f.(s.m)-g.|<g1 by A14,A17,A18,A19;
hence |.(f/*s).m-g.|<g1 by A14,FUNCT_2:108,A20;
end;
hence f/*s is convergent;
hence lim(f/*s)=g by A15,SEQ_2:def 7;
end;
hence thesis by A1,Def12;
end;
theorem Th80:
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: now
let seq;
assume that
A3: seq is divergent_to+infty and
A4: rng seq c=dom(r(#)f);
A5: rng seq c=dom f by A4,VALUED_1:def 5;
then
A6: lim(f/*seq)=lim_in+infty f by A1,A3,Def12;
A7: f/*seq is convergent by A1,A3,A5;
then r(#)(f/*seq) is convergent;
hence (r(#)f)/*seq is convergent by A5,RFUNCT_2:9;
thus lim((r(#)f)/*seq)=lim(r(#)(f/*seq)) by A5,RFUNCT_2:9
.=r*(lim_in+infty f) by A7,A6,SEQ_2:8;
end;
for r1 ex g st r1<g & g in dom(r(#)f)
proof
let r1;
consider g such that
A8: r1<g & g in dom f by A1;
take g;
thus thesis by A8,VALUED_1:def 5;
end;
hence r(#)f is convergent_in+infty by A2;
hence thesis by A2,Def12;
end;
theorem Th81:
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;
thus -f is convergent_in+infty by A1,Th80;
thus lim_in+infty (-f)=(-jj)*(lim_in+infty f) by A1,Th80
.=-(lim_in+infty f);
end;
theorem Th82:
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 that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty and
A3: for r ex g st r<g & g in dom(f1+f2);
A4: now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f1+f2);
A7: dom(f1+f2)=dom f1/\dom f2 by A6,Lm2;
A8: rng seq c=dom f2 by A6,Lm2;
then
A9: lim(f2/*seq)=lim_in+infty f2 by A2,A5,Def12;
A10: f2/*seq is convergent by A2,A5,A8;
A11: rng seq c=dom f1 by A6,Lm2;
then
A12: lim(f1/*seq)=lim_in+infty f1 by A1,A5,Def12;
A13: f1/*seq is convergent by A1,A5,A11;
then f1/*seq+f2/*seq is convergent by A10;
hence (f1+f2)/*seq is convergent by A6,A7,RFUNCT_2:8;
thus lim((f1+f2)/*seq)=lim(f1/*seq+f2/*seq) by A6,A7,RFUNCT_2:8
.=lim_in+infty f1+lim_in+infty f2 by A13,A12,A10,A9,SEQ_2:6;
end;
hence f1+f2 is convergent_in+infty by A3;
hence thesis by A4,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 that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty and
A3: for r ex g st r<g & g in dom(f1-f2);
A4: -f2 is convergent_in+infty by A2,Th81;
hence f1-f2 is convergent_in+infty by A1,A3,Th82;
lim_in+infty(-f2)=-(lim_in+infty f2) by A2,Th81;
hence lim_in+infty(f1-f2)=lim_in+infty f1+-lim_in+infty f2 by A1,A3,A4,Th82
.=lim_in+infty f1-lim_in+infty f2;
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 that
A1: f is convergent_in+infty and
A2: f"{0}={} and
A3: (lim_in+infty f)<>0;
A4: dom f= dom f\f"{0} by A2
.=dom(f^) by RFUNCT_1:def 2;
A5: now
let seq;
assume that
A6: seq is divergent_to+infty and
A7: rng seq c=dom(f^);
A8: f/*seq is convergent & lim(f/*seq)=lim_in+infty f by A1,A4,A6,A7,Def12;
then (f/*seq)" is convergent by A3,A7,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A7,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A7,RFUNCT_2:12
.=(lim_in+infty f)" by A3,A7,A8,RFUNCT_2:11,SEQ_2:22;
end;
for r ex g st r<g & g in dom(f^) by A1,A4;
hence f^ is convergent_in+infty by A5;
hence thesis by A5,Def12;
end;
theorem
f is convergent_in+infty implies abs(f) is convergent_in+infty &
lim_in+infty abs(f)=|.lim_in+infty f.|
proof
assume
A1: f is convergent_in+infty;
A2: now
let seq;
assume that
A3: seq is divergent_to+infty and
A4: rng seq c=dom abs(f);
A5: rng seq c=dom f by A4,VALUED_1:def 11;
then
A6: lim(f/*seq)=lim_in+infty f by A1,A3,Def12;
A7: f/*seq is convergent by A1,A3,A5;
then abs(f/*seq) is convergent;
hence (abs f)/*seq is convergent by A5,RFUNCT_2:10;
thus lim((abs f)/*seq)=lim abs(f/*seq) by A5,RFUNCT_2:10
.=|.lim_in+infty f.| by A7,A6,SEQ_4:14;
end;
now
let r;
consider g such that
A8: r<g & g in dom f by A1;
take g;
thus r<g & g in dom abs(f) by A8,VALUED_1:def 11;
end;
hence abs(f) is convergent_in+infty by A2;
hence thesis by A2,Def12;
end;
theorem Th86:
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 that
A1: f is convergent_in+infty and
A2: lim_in+infty f<>0 and
A3: for r ex g st r<g & g in dom f & f.g<>0;
A4: now
let seq such that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f^);
dom(f^)=dom f\f"{0} & dom f\f"{0}c=dom f by RFUNCT_1:def 2,XBOOLE_1:36;
then rng seq c=dom f by A6;
then
A7: f/*seq is convergent & lim(f/*seq)=lim_in+infty f by A1,A5,Def12;
then (f/*seq)" is convergent by A2,A6,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A6,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A6,RFUNCT_2:12
.=(lim_in+infty f)" by A2,A6,A7,RFUNCT_2:11,SEQ_2:22;
end;
now
let r;
consider g such that
A8: r<g and
A9: g in dom f and
A10: f.g<>0 by A3;
take g;
not f.g in {0} by A10,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
then g in dom f\f"{0} by A9,XBOOLE_0:def 5;
hence r<g & g in dom(f^) by A8,RFUNCT_1:def 2;
end;
hence f^ is convergent_in+infty by A4;
hence thesis by A4,Def12;
end;
theorem Th87:
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 that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty and
A3: for r ex g st r<g & g in dom(f1(#)f2);
A4: now
let seq;
assume that
A5: seq is divergent_to+infty and
A6: rng seq c=dom(f1(#)f2);
A7: dom(f1(#)f2)=dom f1/\dom f2 by A6,Lm3;
A8: rng seq c=dom f2 by A6,Lm3;
then
A9: lim(f2/*seq)=lim_in+infty f2 by A2,A5,Def12;
A10: f2/*seq is convergent by A2,A5,A8;
A11: rng seq c=dom f1 by A6,Lm3;
then
A12: lim(f1/*seq)=lim_in+infty f1 by A1,A5,Def12;
A13: f1/*seq is convergent by A1,A5,A11;
then (f1/*seq)(#)(f2/*seq) is convergent by A10;
hence (f1(#)f2)/*seq is convergent by A6,A7,RFUNCT_2:8;
thus lim((f1(#)f2)/*seq)=lim((f1/*seq)(#)(f2/*seq)) by A6,A7,RFUNCT_2:8
.=(lim_in+infty f1)*(lim_in+infty f2) by A13,A12,A10,A9,SEQ_2:15;
end;
hence f1(#) f2 is convergent_in+infty by A3;
hence thesis by A4,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 that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty & lim_in+infty f2<>0 and
A3: 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 1;
then
A4: dom(f1/f2)=dom f1/\dom(f2^) by RFUNCT_1:def 2;
A5: dom f1/\dom(f2^)c=dom(f2^) by XBOOLE_1:17;
A6: now
let r;
consider g such that
A7: r<g and
A8: g in dom(f1/f2) by A3;
take g;
g in dom(f2^) by A4,A5,A8;
then
A9: g in dom f2\f2"{0} by RFUNCT_1:def 2;
then g in dom f2 & not g in f2"{0} by XBOOLE_0:def 5;
then not f2.g in {0} by FUNCT_1:def 7;
hence r<g & g in dom f2 & f2.g<>0 by A7,A9,TARSKI:def 1,XBOOLE_0:def 5;
end;
then
A10: f2^ is convergent_in+infty by A2,Th86;
A11: lim_in+infty(f2^)=(lim_in+infty f2)" by A2,A6,Th86;
A12: now
let r;
consider g such that
A13: r<g & g in dom(f1/f2) by A3;
take g;
thus r<g & g in dom(f1(#)(f2^)) by A4,A13,VALUED_1:def 4;
end;
then f1(#)(f2^) is convergent_in+infty by A1,A10,Th87;
hence f1/f2 is convergent_in+infty by RFUNCT_1:31;
thus lim_in+infty(f1/f2)=lim_in+infty(f1(#)(f2^)) by RFUNCT_1:31
.=(lim_in+infty f1)*((lim_in+infty f2)") by A1,A12,A10,A11,Th87
.=(lim_in+infty f1)/(lim_in+infty f2) by XCMPLX_0:def 9;
end;
theorem Th89:
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: now
let seq;
assume that
A3: seq is divergent_to-infty and
A4: rng seq c=dom(r(#)f);
A5: rng seq c=dom f by A4,VALUED_1:def 5;
then
A6: lim(f/*seq)=lim_in-infty f by A1,A3,Def13;
A7: f/*seq is convergent by A1,A3,A5;
then r(#)(f/*seq) is convergent;
hence (r(#)f)/*seq is convergent by A5,RFUNCT_2:9;
thus lim((r(#)f)/*seq)=lim(r(#)(f/*seq)) by A5,RFUNCT_2:9
.=r*(lim_in-infty f) by A7,A6,SEQ_2:8;
end;
for r1 ex g st g<r1 & g in dom(r(#)f)
proof
let r1;
consider g such that
A8: g<r1 & g in dom f by A1;
take g;
thus thesis by A8,VALUED_1:def 5;
end;
hence r(#)f is convergent_in-infty by A2;
hence thesis by A2,Def13;
end;
theorem Th90:
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;
thus -f is convergent_in-infty by A1,Th89;
thus lim_in-infty (-f)=(-jj)*(lim_in-infty f) by A1,Th89
.=-(lim_in-infty f);
end;
theorem Th91:
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 that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty and
A3: for r ex g st g<r & g in dom(f1+f2);
A4: now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f1+f2);
A7: rng seq c=dom f1/\dom f2 by A6,VALUED_1:def 1;
dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
then
A8: rng seq c=dom f2 by A7;
then
A9: lim(f2/*seq)=lim_in-infty f2 by A2,A5,Def13;
A10: f2/*seq is convergent by A2,A5,A8;
dom f1/\dom f2 c=dom f1 by XBOOLE_1:17;
then
A11: rng seq c=dom f1 by A7;
then
A12: lim(f1/*seq)=lim_in-infty f1 by A1,A5,Def13;
A13: f1/*seq is convergent by A1,A5,A11;
then f1/*seq+f2/*seq is convergent by A10;
hence (f1+f2)/*seq is convergent by A7,RFUNCT_2:8;
thus lim((f1+f2)/*seq)=lim(f1/*seq+f2/*seq) by A7,RFUNCT_2:8
.=lim_in-infty f1+lim_in-infty f2 by A13,A12,A10,A9,SEQ_2:6;
end;
hence f1+f2 is convergent_in-infty by A3;
hence thesis by A4,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 that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty and
A3: for r ex g st g<r & g in dom(f1-f2);
A4: -f2 is convergent_in-infty by A2,Th90;
hence f1-f2 is convergent_in-infty by A1,A3,Th91;
lim_in-infty(-f2)=-(lim_in-infty f2) by A2,Th90;
hence lim_in-infty(f1-f2)=lim_in-infty f1+-lim_in-infty f2 by A1,A3,A4,Th91
.=lim_in-infty f1-lim_in-infty f2;
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 that
A1: f is convergent_in-infty and
A2: f"{0}={} and
A3: (lim_in-infty f)<>0;
A4: dom f= dom f\f"{0} by A2
.=dom(f^) by RFUNCT_1:def 2;
A5: now
let seq;
assume that
A6: seq is divergent_to-infty and
A7: rng seq c=dom(f^);
A8: f/*seq is convergent & lim(f/*seq)=lim_in-infty f by A1,A4,A6,A7,Def13;
then (f/*seq)" is convergent by A3,A7,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A7,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A7,RFUNCT_2:12
.=(lim_in-infty f)" by A3,A7,A8,RFUNCT_2:11,SEQ_2:22;
end;
for r ex g st g<r & g in dom(f^) by A1,A4;
hence f^ is convergent_in-infty by A5;
hence thesis by A5,Def13;
end;
theorem
f is convergent_in-infty implies abs(f) is convergent_in-infty &
lim_in-infty abs(f)=|.lim_in-infty f.|
proof
assume
A1: f is convergent_in-infty;
A2: now
let seq;
assume that
A3: seq is divergent_to-infty and
A4: rng seq c=dom abs(f);
A5: rng seq c=dom f by A4,VALUED_1:def 11;
then
A6: lim(f/*seq)=lim_in-infty f by A1,A3,Def13;
A7: f/*seq is convergent by A1,A3,A5;
then abs(f/*seq) is convergent;
hence (abs f)/*seq is convergent by A5,RFUNCT_2:10;
thus lim((abs f)/*seq)=lim abs(f/*seq) by A5,RFUNCT_2:10
.=|.lim_in-infty f.| by A7,A6,SEQ_4:14;
end;
now
let r;
consider g such that
A8: g<r & g in dom f by A1;
take g;
thus g<r & g in dom abs(f) by A8,VALUED_1:def 11;
end;
hence abs(f) is convergent_in-infty by A2;
hence thesis by A2,Def13;
end;
theorem Th95:
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 that
A1: f is convergent_in-infty and
A2: lim_in-infty f<>0 and
A3: for r ex g st g<r & g in dom f & f.g<>0;
A4: now
let seq such that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f^);
dom(f^)=dom f\f"{0} & dom f\f"{0}c=dom f by RFUNCT_1:def 2,XBOOLE_1:36;
then rng seq c=dom f by A6;
then
A7: f/*seq is convergent & lim(f/*seq)=lim_in-infty f by A1,A5,Def13;
then (f/*seq)" is convergent by A2,A6,RFUNCT_2:11,SEQ_2:21;
hence (f^)/*seq is convergent by A6,RFUNCT_2:12;
thus lim((f^)/*seq)=lim((f/*seq)") by A6,RFUNCT_2:12
.=(lim_in-infty f)" by A2,A6,A7,RFUNCT_2:11,SEQ_2:22;
end;
now
let r;
consider g such that
A8: g<r and
A9: g in dom f and
A10: f.g<>0 by A3;
take g;
not f.g in {0} by A10,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
then g in dom f\f"{0} by A9,XBOOLE_0:def 5;
hence g<r & g in dom(f^) by A8,RFUNCT_1:def 2;
end;
hence f^ is convergent_in-infty by A4;
hence thesis by A4,Def13;
end;
theorem Th96:
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 that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty and
A3: for r ex g st g<r & g in dom(f1(#)f2);
A4: now
let seq;
assume that
A5: seq is divergent_to-infty and
A6: rng seq c=dom(f1(#)f2);
A7: dom(f1(#)f2)=dom f1/\dom f2 by VALUED_1:def 4;
dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
then
A8: rng seq c=dom f2 by A6,A7;
then
A9: lim(f2/*seq)=lim_in-infty f2 by A2,A5,Def13;
A10: f2/*seq is convergent by A2,A5,A8;
dom f1/\dom f2 c=dom f1 by XBOOLE_1:17;
then
A11: rng seq c=dom f1 by A6,A7;
then
A12: lim(f1/*seq)=lim_in-infty f1 by A1,A5,Def13;
A13: f1/*seq is convergent by A1,A5,A11;
then (f1/*seq)(#)(f2/*seq) is convergent by A10;
hence (f1(#)f2)/*seq is convergent by A6,A7,RFUNCT_2:8;
thus lim((f1(#)f2)/*seq)=lim((f1/*seq)(#)(f2/*seq)) by A6,A7,RFUNCT_2:8
.=(lim_in-infty f1)*(lim_in-infty f2) by A13,A12,A10,A9,SEQ_2:15;
end;
hence f1(#) f2 is convergent_in-infty by A3;
hence thesis by A4,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 that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty & lim_in-infty f2<>0 and
A3: 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 1;
then
A4: dom(f1/f2)=dom f1/\dom(f2^) by RFUNCT_1:def 2;
A5: dom f1/\dom(f2^) c=dom(f2^) by XBOOLE_1:17;
A6: now
let r;
consider g such that
A7: g<r and
A8: g in dom(f1/f2) by A3;
take g;
g in dom(f2^) by A4,A5,A8;
then
A9: g in dom f2\f2"{0} by RFUNCT_1:def 2;
then g in dom f2 & not g in f2"{0} by XBOOLE_0:def 5;
then not f2.g in {0} by FUNCT_1:def 7;
hence g<r & g in dom f2 & f2.g<>0 by A7,A9,TARSKI:def 1,XBOOLE_0:def 5;
end;
then
A10: f2^ is convergent_in-infty by A2,Th95;
A11: lim_in-infty(f2^)=(lim_in-infty f2)" by A2,A6,Th95;
A12: now
let r;
consider g such that
A13: g<r & g in dom(f1/f2) by A3;
take g;
thus g<r & g in dom(f1(#)(f2^)) by A4,A13,VALUED_1:def 4;
end;
then f1(#)(f2^) is convergent_in-infty by A1,A10,Th96;
hence f1/f2 is convergent_in-infty by RFUNCT_1:31;
thus lim_in-infty(f1/f2)=lim_in-infty(f1(#)(f2^)) by RFUNCT_1:31
.=(lim_in-infty f1)*((lim_in-infty f2)") by A1,A12,A10,A11,Th96
.=(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|right_open_halfline r is bounded) implies f1(#)
f2 is convergent_in+infty & lim_in+infty(f1(#)f2)=0
proof
assume that
A1: f1 is convergent_in+infty & lim_in+infty f1=0 and
A2: for r ex g st r<g & g in dom(f1(#)f2);
given r such that
A3: f2|right_open_halfline r is bounded;
consider g be Real such that
A4: for r1 being object st r1 in right_open_halfline(r)/\dom f2 holds |.
f2.r1.|<=g by A3,RFUNCT_1:73;
A5: now
let s be Real_Sequence;
assume that
A6: s is divergent_to+infty and
A7: rng s c=dom(f1(#)f2);
consider k such that
A8: for n st k<=n holds r<s.n by A6;
A9: rng(s^\k)c=rng s by VALUED_0:21;
A10: rng s c=dom f2 by A7,Lm3;
then
A11: rng(s^\k)c=dom f2 by A9;
now
set t=|.g.|+1;
0<=|.g.| by COMPLEX1:46;
hence 0<t;
let n;
A12: n in NAT by ORDINAL1:def 12;
r<s.(n+k) by A8,NAT_1:12;
then r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: r<g1};
then (s^\k).n in rng(s^\k) & (s^\k).n in right_open_halfline(r) by
VALUED_0:28,XXREAL_1:230;
then (s^\k).n in right_open_halfline(r)/\dom f2 by A11,XBOOLE_0:def 4;
then |.f2.((s^\k).n).|<=g by A4;
then
A13: |.(f2/*(s^\k)).n.|<= g by A10,A9,FUNCT_2:108,XBOOLE_1:1,A12;
g<=|.g.| by ABSVALUE:4;
then g<t by Lm1;
hence |.(f2/*(s^\k)).n.|<t by A13,XXREAL_0:2;
end;
then
A14: f2/*(s^\k) is bounded by SEQ_2:3;
dom(f1(#)f2)=dom f1/\dom f2 by A7,Lm3;
then rng(s^\k)c=dom f1/\dom f2 by A7,A9;
then
A15: (f1/*(s^\k))(#)(f2/*(s^\k))=(f1(#)f2)/*(s^\k) by RFUNCT_2:8
.=((f1(#)f2)/*s)^\k by A7,VALUED_0:27;
rng s c=dom f1 by A7,Lm3;
then
A16: rng(s^\k)c=dom f1 by A9;
s^\k is divergent_to+infty by A6,Th26;
then
A17: f1/*(s^\k) is convergent & lim(f1/*(s^\k))=0 by A1,A16,Def12;
then
A18: (f1/*(s^\k))(#)(f2/*(s^\k)) is convergent by A14,SEQ_2:25;
hence (f1(#)f2)/*s is convergent by A15,SEQ_4:21;
lim((f1/*(s^\k))(#)(f2/*(s^\k)))=0 by A17,A14,SEQ_2:26;
hence lim((f1(#)f2)/*s)=0 by A18,A15,SEQ_4:22;
end;
hence f1(#) f2 is convergent_in+infty by A2;
hence thesis by A5,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|left_open_halfline r is bounded) implies f1(#)f2
is convergent_in-infty & lim_in-infty(f1(#)f2)=0
proof
assume that
A1: f1 is convergent_in-infty & lim_in-infty f1=0 and
A2: for r ex g st g<r & g in dom(f1(#)f2);
given r such that
A3: f2|left_open_halfline r is bounded;
consider g be Real such that
A4: for r1 being object st r1 in left_open_halfline(r)/\dom f2 holds |.f2
.r1.|<=g by A3,RFUNCT_1:73;
A5: now
let s be Real_Sequence;
assume that
A6: s is divergent_to-infty and
A7: rng s c=dom(f1(#)f2);
consider k such that
A8: for n st k<=n holds s.n<r by A6;
A9: rng(s^\k)c=rng s by VALUED_0:21;
A10: rng s c=dom f2 by A7,Lm3;
then
A11: rng(s^\k)c=dom f2 by A9;
now
set t=|.g.|+1;
0<=|.g.| by COMPLEX1:46;
hence 0<t;
let n;
A12: n in NAT by ORDINAL1:def 12;
s.(n+k)<r by A8,NAT_1:12;
then (s^\k).n<r by NAT_1:def 3;
then (s^\k).n in {g1: g1<r};
then (s^\k).n in rng(s^\k) & (s^\k).n in left_open_halfline(r) by
VALUED_0:28,XXREAL_1:229;
then (s^\k).n in left_open_halfline(r)/\dom f2 by A11,XBOOLE_0:def 4;
then |.f2.((s^\k).n).|<=g by A4;
then
A13: |.(f2/*(s^\k)).n.|<= g by A10,A9,FUNCT_2:108,XBOOLE_1:1,A12;
g<=|.g.| by ABSVALUE:4;
then g<t by Lm1;
hence |.(f2/*(s^\k)).n.|<t by A13,XXREAL_0:2;
end;
then
A14: f2/*(s^\k) is bounded by SEQ_2:3;
dom(f1(#)f2)=dom f1/\dom f2 by A7,Lm3;
then rng(s^\k)c=dom f1/\dom f2 by A7,A9;
then
A15: (f1/*(s^\k))(#)(f2/*(s^\k))=(f1(#)f2)/*(s^\k) by RFUNCT_2:8
.=((f1(#)f2)/*s)^\k by A7,VALUED_0:27;
rng s c=dom f1 by A7,Lm3;
then
A16: rng(s^\k)c=dom f1 by A9;
s^\k is divergent_to-infty by A6,Th27;
then
A17: f1/*(s^\k) is convergent & lim(f1/*(s^\k))=0 by A1,A16,Def13;
then
A18: (f1/*(s^\k))(#)(f2/*(s^\k)) is convergent by A14,SEQ_2:25;
hence (f1(#)f2)/*s is convergent by A15,SEQ_4:21;
lim((f1/*(s^\k))(#)(f2/*(s^\k)))=0 by A17,A14,SEQ_2:26;
hence lim((f1(#)f2)/*s)=0 by A18,A15,SEQ_4:22;
end;
hence f1(#) f2 is convergent_in-infty by A2;
hence thesis by A5,Def13;
end;
theorem Th100:
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 that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty and
A3: lim_in+infty f1=lim_in+infty f2 and
A4: for r ex g st r<g & g in dom f;
given r1 such that
A5: 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
A6: for g st g in dom f/\right_open_halfline(r1) holds f1.g<=f.g & f.g<= f2.g;
now
per cases by A5;
suppose
A7: 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);
A8: now
let seq;
assume that
A9: seq is divergent_to+infty and
A10: rng seq c=dom f;
consider k such that
A11: for n st k<=n holds r1<seq.n by A9;
A12: seq^\k is divergent_to+infty by A9,Th26;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A13: x=(seq^\k).n by FUNCT_2:113;
r1<seq.(n+k) by A11,NAT_1:12;
then r1<(seq^\k).n by NAT_1:def 3;
then x in {g: r1<g} by A13;
hence x in right_open_halfline(r1) by XXREAL_1:230;
end;
then
A14: rng(seq^\k)c=right_open_halfline(r1);
A15: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A10;
then
A16: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A14,XBOOLE_1:19;
then
A17: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A7;
then
A18: rng(seq^\k)c=dom f2/\right_open_halfline(r1) by A7;
A19: dom f2/\right_open_halfline(r1) c=dom f2 by XBOOLE_1:17;
then rng(seq^\k)c=dom f2 by A18;
then
A20: f2/*(seq^\k) is convergent & lim(f2/*(seq^\k))=lim_in+infty f1 by A2,A3
,A12,Def12;
A21: dom f1/\right_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
then rng(seq^\k)c=dom f1 by A17;
then
A22: f1/*(seq^\k) is convergent & lim(f1/*(seq^\k))=lim_in+infty f1 by A1,
A12,Def12;
A23: now
let n;
A24: n in NAT by ORDINAL1:def 12;
A25: (seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A16;
then
A26: (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A10,A15,FUNCT_2:108,XBOOLE_1:1,A24;
f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A16,A25;
then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A10,A15,FUNCT_2:108,A24
,XBOOLE_1:1;
hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
^\k)).n by A17,A21,A18,A19,A26,FUNCT_2:108,XBOOLE_1:1,A24;
end;
A27: f/*(seq^\k)=(f/*seq)^\k by A10,VALUED_0:27;
then
A28: (f/*seq)^\k is convergent by A22,A20,A23,SEQ_2:19;
hence f/*seq is convergent by SEQ_4:21;
lim((f/*seq)^\k)=lim_in+infty f1 by A22,A20,A23,A27,SEQ_2:20;
hence lim(f/*seq)=lim_in+infty f1 by A28,SEQ_4:20,21;
end;
hence f is convergent_in+infty by A4;
hence thesis by A8,Def12;
end;
suppose
A29: 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);
A30: now
let seq;
assume that
A31: seq is divergent_to+infty and
A32: rng seq c=dom f;
consider k such that
A33: for n st k<=n holds r1<seq.n by A31;
A34: seq^\k is divergent_to+infty by A31,Th26;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A35: x=(seq^\k).n by FUNCT_2:113;
r1<seq.(n+k) by A33,NAT_1:12;
then r1<(seq^\k).n by NAT_1:def 3;
then x in {g: r1<g} by A35;
hence x in right_open_halfline(r1) by XXREAL_1:230;
end;
then
A36: rng(seq^\k)c=right_open_halfline(r1);
A37: rng(seq^\k) c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A32;
then
A38: rng(seq^\k)c=dom f/\right_open_halfline(r1) by A36,XBOOLE_1:19;
then
A39: rng(seq^\k)c=dom f2/\right_open_halfline(r1) by A29;
then
A40: rng(seq^\k)c=dom f1/\right_open_halfline(r1) by A29;
A41: dom f1/\right_open_halfline(r1) c=dom f1 by XBOOLE_1:17;
then rng(seq^\k)c=dom f1 by A40;
then
A42: f1/*(seq^\k) is convergent & lim(f1/*(seq^\k))=lim_in+infty f1 by A1,
A34,Def12;
A43: dom f2/\right_open_halfline(r1)c=dom f2 by XBOOLE_1:17;
then rng(seq^\k)c=dom f2 by A39;
then
A44: f2/*(seq^\k) is convergent & lim(f2/*(seq^\k))=lim_in+infty f1 by A2,A3
,A34,Def12;
A45: now
let n;
A46: n in NAT by ORDINAL1:def 12;
A47: (seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A38;
then
A48: (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A32,A37,FUNCT_2:108,XBOOLE_1:1,A46;
f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A38,A47;
then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A32,A37,FUNCT_2:108,A46
,XBOOLE_1:1;
hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
^\k)).n by A39,A43,A40,A41,A48,FUNCT_2:108,XBOOLE_1:1,A46;
end;
A49: f/*(seq^\k)=(f/*seq)^\k by A32,VALUED_0:27;
then
A50: (f/*seq)^\k is convergent by A44,A42,A45,SEQ_2:19;
hence f/*seq is convergent by SEQ_4:21;
lim((f/*seq)^\k)=lim_in+infty f1 by A44,A42,A45,A49,SEQ_2:20;
hence lim(f/*seq)=lim_in+infty f1 by A50,SEQ_4:20,21;
end;
hence f is convergent_in+infty by A4;
hence thesis by A30,Def12;
end;
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 and
A3: for g st g in right_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g;
dom f1/\dom f2/\dom f c=dom f by XBOOLE_1:17;
then
A4: right_open_halfline(r1)c=dom f by A2;
A5: now
let r;
consider g being Real such that
A6: |.r.|+|.r1.|<g by XREAL_1:1;
take g;
r<=|.r.| & 0<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then r+0<=|.r.|+|.r1.| by XREAL_1:7;
hence r<g by A6,XXREAL_0:2;
r1<=|.r1.| & 0<=|.r.| by ABSVALUE:4,COMPLEX1:46;
then 0+r1<=|.r.|+|.r1.| by XREAL_1:7;
then r1<g by A6,XXREAL_0:2;
then g in {g1: r1<g1};
then g in right_open_halfline(r1) by XXREAL_1:230;
hence g in dom f by A4;
end;
A7: dom f1/\dom f2/\dom f c=dom f1/\dom f2 by XBOOLE_1:17;
now
dom f1/\dom f2 c=dom f1 by XBOOLE_1:17;
then dom f1/\dom f2/\dom f c=dom f1 by A7;
then
A8: dom f1/\right_open_halfline(r1)=right_open_halfline(r1) by A2,XBOOLE_1:1,28
;
dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
then dom f1/\dom f2/\ dom f c=dom f2 by A7;
hence dom f1/\right_open_halfline(r1)c=dom f2/\right_open_halfline(r1) by
A2,A8,XBOOLE_1:1,28;
thus dom f/\right_open_halfline(r1)c=dom f1/\ right_open_halfline(r1) by A8
,XBOOLE_1:17;
let g;
assume g in dom f/\right_open_halfline(r1);
then g in right_open_halfline(r1) by XBOOLE_0:def 4;
hence f1.g<=f.g & f.g<=f2.g by A3;
end;
hence thesis by A1,A5,Th100;
end;
theorem Th102:
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 that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty and
A3: lim_in-infty f1=lim_in-infty f2 and
A4: for r ex g st g<r & g in dom f;
given r1 such that
A5: 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
A6: for g st g in dom f/\left_open_halfline(r1) holds f1.g<=f.g & f.g<= f2.g;
now
per cases by A5;
suppose
A7: 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);
A8: now
let seq;
assume that
A9: seq is divergent_to-infty and
A10: rng seq c=dom f;
consider k such that
A11: for n st k<=n holds seq.n<r1 by A9;
A12: seq^\k is divergent_to-infty by A9,Th27;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A13: x=(seq^\k).n by FUNCT_2:113;
seq.(n+k)<r1 by A11,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then x in {g: g<r1} by A13;
hence x in left_open_halfline(r1) by XXREAL_1:229;
end;
then
A14: rng(seq^\k)c=left_open_halfline(r1);
A15: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A10;
then
A16: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A14,XBOOLE_1:19;
then
A17: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A7;
then
A18: rng(seq^\k)c=dom f2/\left_open_halfline(r1) by A7;
A19: dom f2/\left_open_halfline(r1)c=dom f2 by XBOOLE_1:17;
then rng(seq^\k)c=dom f2 by A18;
then
A20: f2/*(seq^\k) is convergent & lim(f2/*(seq^\k))=lim_in-infty f1 by A2,A3
,A12,Def13;
A21: dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
then rng(seq^\k)c=dom f1 by A17;
then
A22: f1/*(seq^\k) is convergent & lim(f1/*(seq^\k))=lim_in-infty f1 by A1,
A12,Def13;
A23: now
let n;
A24: n in NAT by ORDINAL1:def 12;
A25: (seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A16;
then
A26: (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A10,A15,FUNCT_2:108,XBOOLE_1:1,A24;
f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A16,A25;
then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A10,A15,FUNCT_2:108,A24
,XBOOLE_1:1;
hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
^\k)).n by A17,A21,A18,A19,A26,FUNCT_2:108,XBOOLE_1:1,A24;
end;
A27: f/*(seq^\k)=(f/*seq)^\k by A10,VALUED_0:27;
then
A28: (f/*seq)^\k is convergent by A22,A20,A23,SEQ_2:19;
hence f/*seq is convergent by SEQ_4:21;
lim((f/*seq)^\k)=lim_in-infty f1 by A22,A20,A23,A27,SEQ_2:20;
hence lim(f/*seq)=lim_in-infty f1 by A28,SEQ_4:20,21;
end;
hence f is convergent_in-infty by A4;
hence thesis by A8,Def13;
end;
suppose
A29: 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);
A30: now
let seq;
assume that
A31: seq is divergent_to-infty and
A32: rng seq c=dom f;
consider k such that
A33: for n st k<=n holds seq.n<r1 by A31;
A34: seq^\k is divergent_to-infty by A31,Th27;
now
let x be object;
assume x in rng(seq^\k);
then consider n being Element of NAT such that
A35: x=(seq^\k).n by FUNCT_2:113;
seq.(n+k)<r1 by A33,NAT_1:12;
then (seq^\k).n<r1 by NAT_1:def 3;
then x in {g: g<r1} by A35;
hence x in left_open_halfline(r1) by XXREAL_1:229;
end;
then
A36: rng(seq^\k)c=left_open_halfline(r1);
A37: rng(seq^\k)c=rng seq by VALUED_0:21;
then rng(seq^\k)c=dom f by A32;
then
A38: rng(seq^\k)c=dom f/\left_open_halfline(r1) by A36,XBOOLE_1:19;
then
A39: rng(seq^\k)c=dom f2/\left_open_halfline(r1) by A29;
then
A40: rng(seq^\k)c=dom f1/\left_open_halfline(r1) by A29;
A41: dom f1/\left_open_halfline(r1)c=dom f1 by XBOOLE_1:17;
then rng(seq^\k)c=dom f1 by A40;
then
A42: f1/*(seq^\k) is convergent & lim(f1/*(seq^\k))=lim_in-infty f1 by A1,
A34,Def13;
A43: dom f2/\left_open_halfline(r1)c=dom f2 by XBOOLE_1:17;
then rng(seq^\k)c=dom f2 by A39;
then
A44: f2/*(seq^\k) is convergent & lim(f2/*(seq^\k))=lim_in-infty f1 by A2,A3
,A34,Def13;
A45: now
let n;
A46: n in NAT by ORDINAL1:def 12;
A47: (seq^\k).n in rng(seq^\k) by VALUED_0:28;
then f.((seq^\k).n)<=f2.((seq^\k).n) by A6,A38;
then
A48: (f/*(seq^\k)).n<=f2.((seq^\k).n)
by A32,A37,FUNCT_2:108,XBOOLE_1:1,A46;
f1.((seq^\k).n)<=f.((seq^\k).n) by A6,A38,A47;
then f1.((seq^\k).n)<=(f/*(seq^\k)).n by A32,A37,FUNCT_2:108,A46
,XBOOLE_1:1;
hence (f1/*(seq^\k)).n<=(f/*(seq^\k)).n & (f/*(seq^\k)).n<=(f2/*(seq
^\k)).n by A39,A43,A40,A41,A48,FUNCT_2:108,XBOOLE_1:1,A46;
end;
A49: f/*(seq^\k)=(f/*seq)^\k by A32,VALUED_0:27;
then
A50: (f/*seq)^\k is convergent by A44,A42,A45,SEQ_2:19;
hence f/*seq is convergent by SEQ_4:21;
lim((f/*seq)^\k)=lim_in-infty f1 by A44,A42,A45,A49,SEQ_2:20;
hence lim(f/*seq)=lim_in-infty f1 by A50,SEQ_4:20,21;
end;
hence f is convergent_in-infty by A4;
hence thesis by A30,Def13;
end;
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 and
A3: for g st g in left_open_halfline(r1) holds f1.g<=f.g & f.g<=f2.g;
dom f1/\dom f2/\dom f c=dom f by XBOOLE_1:17;
then
A4: left_open_halfline(r1) c=dom f by A2;
A5: now
let r;
consider g being Real such that
A6: g<-|.r.|-|.r1.| by XREAL_1:2;
take g;
-|.r.|<=r & 0<=|.r1.| by ABSVALUE:4,COMPLEX1:46;
then -|.r.|-|.r1.|<=r-0 by XREAL_1:13;
hence g<r by A6,XXREAL_0:2;
-|.r1.|<=r1 & 0<=|.r.| by ABSVALUE:4,COMPLEX1:46;
then -|.r1.|-|.r.|<=r1-0 by XREAL_1:13;
then g<r1 by A6,XXREAL_0:2;
then g in {g1: g1<r1};
then g in left_open_halfline(r1) by XXREAL_1:229;
hence g in dom f by A4;
end;
A7: dom f1/\dom f2/\dom f c=dom f1/\dom f2 by XBOOLE_1:17;
now
dom f1/\dom f2 c=dom f1 by XBOOLE_1:17;
then dom f1/\dom f2/\dom f c=dom f1 by A7;
then
A8: dom f1/\left_open_halfline(r1)=left_open_halfline(r1) by A2,XBOOLE_1:1,28;
dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
then dom f1/\dom f2/\ dom f c=dom f2 by A7;
hence
dom f1/\left_open_halfline(r1) c=dom f2/\left_open_halfline(r1) by A2,A8,
XBOOLE_1:1,28;
thus dom f/\left_open_halfline(r1)c=dom f1/\left_open_halfline(r1) by A8,
XBOOLE_1:17;
let g;
assume g in dom f/\left_open_halfline(r1);
then g in left_open_halfline(r1) by XBOOLE_0:def 4;
hence f1.g<=f.g & f.g<=f2.g by A3;
end;
hence thesis by A1,A5,Th102;
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 that
A1: f1 is convergent_in+infty and
A2: f2 is convergent_in+infty;
given r such that
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) 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 A3;
suppose
A4: 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] means $1<$2 & $2 in dom f1/\
right_open_halfline r;
A5: now
let n being Element of NAT ;
0<=|.r.| by COMPLEX1:46;
then
A6: n+0<=n+|.r.| by XREAL_1:7;
consider g such that
A7: n+|.r.|<g and
A8: g in dom f1 by A1;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
0<=n & r<=|.r.| by ABSVALUE:4;
then 0+r<=n+|.r.| by XREAL_1:7;
then r<g by A7,XXREAL_0:2;
then g in {g2: r<g2};
then g in right_open_halfline(r) by XXREAL_1:230;
hence X[n,g] by A7,A8,A6,XBOOLE_0:def 4,XXREAL_0:2;
end;
consider s2 be Real_Sequence such that
A9: for n being Element of NAT holds X[n,s2.n] from FUNCT_2:sch 3(A5);
now
let n being Nat;
A10: n in NAT by ORDINAL1:def 12;
then n<s2.n by A9;
hence s1.n<=s2.n by FUNCT_1:18,A10;
end;
then
A11: s2 is divergent_to+infty by Lm5,Th20,Th42;
A12: rng s2 c=dom f2
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f1/\right_open_halfline(r) by A9;
hence thesis by A4,XBOOLE_0:def 4;
end;
then
A13: lim(f2/*s2)=lim_in+infty f2 by A2,A11,Def12;
A14: rng s2 c=dom f1
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f1/\right_open_halfline(r) by A9;
hence thesis by XBOOLE_0:def 4;
end;
A15: now
let n;
A16: n in NAT by ORDINAL1:def 12;
f1.(s2.n)<=f2.(s2.n) by A4,A9,A16;
then (f1/*s2).n<=f2.(s2.n) by A14,FUNCT_2:108,A16;
hence (f1/*s2).n<=(f2/*s2).n by A12,FUNCT_2:108,A16;
end;
A17: f2/*s2 is convergent by A2,A11,A12;
A18: f1/*s2 is convergent by A1,A11,A14;
lim(f1/*s2)=lim_in+infty f1 by A1,A11,A14,Def12;
hence thesis by A18,A17,A13,A15,SEQ_2:18;
end;
suppose
A19: 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] means $1<$2 & $2 in dom f2/\
right_open_halfline r;
A20: now
let n being Element of NAT ;
0<=|.r.| by COMPLEX1:46;
then
A21: n+0<=n+|.r.| by XREAL_1:7;
consider g such that
A22: n+|.r.|<g and
A23: g in dom f2 by A2;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
0<=n & r<=|.r.| by ABSVALUE:4;
then 0+r<=n+|.r.| by XREAL_1:7;
then r<g by A22,XXREAL_0:2;
then g in {g2: r<g2};
then g in right_open_halfline(r) by XXREAL_1:230;
hence X[n,g] by A22,A23,A21,XBOOLE_0:def 4,XXREAL_0:2;
end;
consider s2 be Real_Sequence such that
A24: for n being Element of NAT holds X[n,s2.n] from FUNCT_2:sch 3(A20);
now
let n;
A25: n in NAT by ORDINAL1:def 12;
then n<s2.n by A24;
hence s1.n<=s2.n by FUNCT_1:18,A25;
end;
then
A26: s2 is divergent_to+infty by Lm5,Th20,Th42;
A27: rng s2 c=dom f1
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f2/\right_open_halfline(r) by A24;
hence thesis by A19,XBOOLE_0:def 4;
end;
then
A28: lim(f1/*s2)=lim_in+infty f1 by A1,A26,Def12;
A29: rng s2 c=dom f2
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f2/\right_open_halfline(r) by A24;
hence thesis by XBOOLE_0:def 4;
end;
A30: now
let n;
A31: n in NAT by ORDINAL1:def 12;
f1.(s2.n)<=f2.(s2.n) by A19,A24,A31;
then (f1/*s2).n<=f2.(s2.n) by A27,FUNCT_2:108,A31;
hence (f1/*s2).n<=(f2/*s2).n by A29,FUNCT_2:108,A31;
end;
A32: f1/*s2 is convergent by A1,A26,A27;
A33: f2/*s2 is convergent by A2,A26,A29;
lim(f2/*s2)=lim_in+infty f2 by A2,A26,A29,Def12;
hence thesis by A33,A32,A28,A30,SEQ_2:18;
end;
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 that
A1: f1 is convergent_in-infty and
A2: f2 is convergent_in-infty;
given r such that
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) 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 A3;
suppose
A4: 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;
deffunc U(Nat) = -$1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f1/\
left_open_halfline r;
consider s1 be Real_Sequence such that
A5: for n holds s1.n=U(n) from SEQ_1:sch 1;
A6: now
let n being Element of NAT ;
0<=|.r.| by COMPLEX1:46;
then
A7: -n-|.r.|<=-n-0 by XREAL_1:13;
consider g such that
A8: g<-n-|.r.| and
A9: g in dom f1 by A1;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
0<=n & -|.r.|<=r by ABSVALUE:4;
then -|.r.|-n<=r-0 by XREAL_1:13;
then g<r by A8,XXREAL_0:2;
then g in {g2: g2<r};
then g in left_open_halfline(r) by XXREAL_1:229;
hence X[n,g] by A8,A9,A7,XBOOLE_0:def 4,XXREAL_0:2;
end;
consider s2 be Real_Sequence such that
A10: for n being Element of NAT holds X[n,s2.n] from FUNCT_2:sch 3(A6);
now
let n;
n in NAT by ORDINAL1:def 12;
then s2.n<-n by A10;
hence s2.n<=s1.n by A5;
end;
then
A11: s2 is divergent_to-infty by A5,Th21,Th43;
A12: rng s2 c=dom f2
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f1/\left_open_halfline(r) by A10;
hence thesis by A4,XBOOLE_0:def 4;
end;
then
A13: lim(f2/*s2)=lim_in-infty f2 by A2,A11,Def13;
A14: rng s2 c=dom f1
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f1/\left_open_halfline(r) by A10;
hence thesis by XBOOLE_0:def 4;
end;
A15: now
let n;
A16: n in NAT by ORDINAL1:def 12;
f1.(s2.n)<=f2.(s2.n) by A4,A10,A16;
then (f1/*s2).n<=f2.(s2.n) by A14,FUNCT_2:108,A16;
hence (f1/*s2).n<=(f2/*s2).n by A12,FUNCT_2:108,A16;
end;
A17: f2/*s2 is convergent by A2,A11,A12;
A18: f1/*s2 is convergent by A1,A11,A14;
lim(f1/*s2)=lim_in-infty f1 by A1,A11,A14,Def13;
hence thesis by A18,A17,A13,A15,SEQ_2:18;
end;
suppose
A19: 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;
deffunc U(Nat) = -$1;
defpred X[Nat,Real] means $2<-$1 & $2 in dom f2/\
left_open_halfline r;
consider s1 be Real_Sequence such that
A20: for n holds s1.n=U(n) from SEQ_1:sch 1;
A21: now
let n being Element of NAT ;
0<=|.r.| by COMPLEX1:46;
then
A22: -n-|.r.|<=-n-0 by XREAL_1:13;
consider g such that
A23: g<-n-|.r.| and
A24: g in dom f2 by A2;
reconsider g as Element of REAL by XREAL_0:def 1;
take g;
0<=n & -|.r.|<=r by ABSVALUE:4;
then -|.r.|-n<=r-0 by XREAL_1:13;
then g<r by A23,XXREAL_0:2;
then g in {g2: g2<r};
then g in left_open_halfline(r) by XXREAL_1:229;
hence X[n,g] by A23,A24,A22,XBOOLE_0:def 4,XXREAL_0:2;
end;
consider s2 be Real_Sequence such that
A25: for n being Element of NAT holds X[n,s2.n] from FUNCT_2:sch 3(A21);
now
let n;
n in NAT by ORDINAL1:def 12;
then s2.n<-n by A25;
hence s2.n<=s1.n by A20;
end;
then
A26: s2 is divergent_to-infty by A20,Th21,Th43;
A27: rng s2 c=dom f1
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f2/\left_open_halfline(r) by A25;
hence thesis by A19,XBOOLE_0:def 4;
end;
then
A28: lim(f1/*s2)=lim_in-infty f1 by A1,A26,Def13;
A29: rng s2 c=dom f2
proof
let x be Real;
assume x in rng s2;
then ex n being Element of NAT st x=s2.n by FUNCT_2:113;
then x in dom f2/\left_open_halfline(r) by A25;
hence thesis by XBOOLE_0:def 4;
end;
A30: now
let n;
A31: n in NAT by ORDINAL1:def 12;
f1.(s2.n)<=f2.(s2.n) by A19,A25,A31;
then (f1/*s2).n<=f2.(s2.n) by A27,FUNCT_2:108,A31;
hence (f1/*s2).n<=(f2/*s2).n by A29,FUNCT_2:108,A31;
end;
A32: f1/*s2 is convergent by A1,A26,A27;
A33: f2/*s2 is convergent by A2,A26,A29;
lim(f2/*s2)=lim_in-infty f2 by A2,A26,A29,Def13;
hence thesis by A33,A32,A28,A30,SEQ_2:18;
end;
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 2;
A4: now
let r;
consider g such that
A5: r<g & g in dom f and
A6: f.g<>0 by A2;
take g;
not f.g in {0} by A6,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
hence r<g & g in dom(f^) by A3,A5,XBOOLE_0:def 5;
end;
now
per cases by A1;
suppose
A7: f is divergent_in+infty_to+infty;
A8: now
let seq such that
A9: seq is divergent_to+infty and
A10: rng seq c=dom(f^);
dom(f^) c=dom f by A3,XBOOLE_1:36;
then rng seq c=dom f by A10;
then f/*seq is divergent_to+infty by A7,A9;
then (f/*seq)" is convergent & lim((f/*seq)")=0 by Th34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A10,RFUNCT_2:12;
end;
hence f^ is convergent_in+infty by A4;
hence thesis by A8,Def12;
end;
suppose
A11: f is divergent_in+infty_to-infty;
A12: now
let seq such that
A13: seq is divergent_to+infty and
A14: rng seq c=dom(f^);
dom(f^) c=dom f by A3,XBOOLE_1:36;
then rng seq c=dom f by A14;
then f/*seq is divergent_to-infty by A11,A13;
then (f/*seq)" is convergent & lim((f/*seq)")=0 by Th34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A14,RFUNCT_2:12;
end;
hence f^ is convergent_in+infty by A4;
hence thesis by A12,Def12;
end;
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 2;
A4: now
let r;
consider g such that
A5: g<r & g in dom f and
A6: f.g<>0 by A2;
take g;
not f.g in {0} by A6,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
hence g<r & g in dom(f^) by A3,A5,XBOOLE_0:def 5;
end;
now
per cases by A1;
suppose
A7: f is divergent_in-infty_to+infty;
A8: now
let seq such that
A9: seq is divergent_to-infty and
A10: rng seq c=dom(f^);
dom(f^) c=dom f by A3,XBOOLE_1:36;
then rng seq c=dom f by A10;
then f/*seq is divergent_to+infty by A7,A9;
then (f/*seq)" is convergent & lim((f/*seq)")=0 by Th34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A10,RFUNCT_2:12;
end;
hence f^ is convergent_in-infty by A4;
hence thesis by A8,Def13;
end;
suppose
A11: f is divergent_in-infty_to-infty;
A12: now
let seq such that
A13: seq is divergent_to-infty and
A14: rng seq c=dom(f^);
dom(f^) c=dom f by A3,XBOOLE_1:36;
then rng seq c=dom f by A14;
then f/*seq is divergent_to-infty by A11,A13;
then (f/*seq)" is convergent & lim((f/*seq)")=0 by Th34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A14,RFUNCT_2:12;
end;
hence f^ is convergent_in-infty by A4;
hence thesis by A12,Def13;
end;
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 that
A1: f is convergent_in+infty & lim_in+infty f=0 and
A2: for r ex g st r<g & g in dom f & f.g<>0;
given r such that
A3: 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
A4: r1<g1 and
A5: g1 in dom f and
A6: f.g1<>0 by A2;
take g1;
thus r1<g1 by A4;
not f.g1 in {0} by A6,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
then g1 in dom f\f"{0} by A5,XBOOLE_0:def 5;
hence thesis by RFUNCT_1:def 2;
end;
let s be Real_Sequence;
assume that
A7: s is divergent_to+infty and
A8: rng s c=dom(f^);
consider k such that
A9: for n st k<=n holds r<s.n by A7;
A10: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A11: dom(f^)c=dom f by XBOOLE_1:36;
then
A12: rng s c=dom f by A8;
then
A13: rng(s^\k)c=dom f by A10;
A14: f/*(s^\k) is non-zero by A8,A10,RFUNCT_2:11,XBOOLE_1:1;
now
let n;
A15: n in NAT by ORDINAL1:def 12;
r<s.(n+k) by A9,NAT_1:12;
then r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: r<g2};
then (s^\k).n in rng(s^\k) & (s^\k).n in right_open_halfline(r) by
VALUED_0:28,XXREAL_1:230;
then (s^\k).n in dom f/\right_open_halfline(r) by A13,XBOOLE_0:def 4;
then
A16: 0<= f.((s^\k).n) by A3;
(f/*(s^\k)).n<>0 by A14,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies 0<(f/*(s^\k)).n;
s^\k is divergent_to+infty by A7,Th26;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def12;
then
A18: (f/*(s^\k))" is divergent_to+infty by A17,Th35;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
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 that
A1: f is convergent_in+infty & lim_in+infty f=0 and
A2: for r ex g st r<g & g in dom f & f.g<>0;
given r such that
A3: 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
A4: r1<g1 and
A5: g1 in dom f and
A6: f.g1<>0 by A2;
take g1;
thus r1<g1 by A4;
not f.g1 in {0} by A6,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
then g1 in dom f\f"{0} by A5,XBOOLE_0:def 5;
hence thesis by RFUNCT_1:def 2;
end;
let s be Real_Sequence;
assume that
A7: s is divergent_to+infty and
A8: rng s c=dom(f^);
consider k such that
A9: for n st k<=n holds r<s.n by A7;
A10: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A11: dom(f^)c=dom f by XBOOLE_1:36;
then
A12: rng s c=dom f by A8;
then
A13: rng(s^\k)c=dom f by A10;
A14: f/*(s^\k) is non-zero by A8,A10,RFUNCT_2:11,XBOOLE_1:1;
now
let n;
A15: n in NAT by ORDINAL1:def 12;
r<s.(n+k) by A9,NAT_1:12;
then r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: r<g2};
then (s^\k).n in rng(s^\k) & (s^\k).n in right_open_halfline(r) by
VALUED_0:28,XXREAL_1:230;
then (s^\k).n in dom f/\right_open_halfline(r) by A13,XBOOLE_0:def 4;
then
A16: f.((s^\k).n)<=0 by A3;
(f/*(s^\k)).n<>0 by A14,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies (f/*(s^\k)).n<0;
s^\k is divergent_to+infty by A7,Th26;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def12;
then
A18: (f/*(s^\k))" is divergent_to-infty by A17,Th36;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
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 that
A1: f is convergent_in-infty & lim_in-infty f=0 and
A2: for r ex g st g<r & g in dom f & f.g<>0;
given r such that
A3: 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
A4: g1<r1 and
A5: g1 in dom f and
A6: f.g1<>0 by A2;
take g1;
thus g1<r1 by A4;
not f.g1 in {0} by A6,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
then g1 in dom f\f"{0} by A5,XBOOLE_0:def 5;
hence thesis by RFUNCT_1:def 2;
end;
let s be Real_Sequence;
assume that
A7: s is divergent_to-infty and
A8: rng s c=dom (f^);
consider k such that
A9: for n st k<=n holds s.n<r by A7;
A10: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A11: dom(f^)c=dom f by XBOOLE_1:36;
then
A12: rng s c=dom f by A8;
then
A13: rng(s^\k)c=dom f by A10;
A14: f/*(s^\k) is non-zero by A8,A10,RFUNCT_2:11,XBOOLE_1:1;
now
let n;
A15: n in NAT by ORDINAL1:def 12;
s.(n+k)<r by A9,NAT_1:12;
then (s^\k).n<r by NAT_1:def 3;
then (s^\k).n in {g2: g2<r};
then (s^\k).n in rng(s^\k) & (s^\k).n in left_open_halfline(r) by
VALUED_0:28,XXREAL_1:229;
then (s^\k).n in dom f/\left_open_halfline(r) by A13,XBOOLE_0:def 4;
then
A16: 0<=f.((s^\k).n) by A3;
0<>(f/*(s^\k)).n by A14,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies 0<(f/*(s^\k)).n;
s^\k is divergent_to-infty by A7,Th27;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def13;
then
A18: (f/*(s^\k))" is divergent_to+infty by A17,Th35;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
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 that
A1: f is convergent_in-infty & lim_in-infty f=0 and
A2: for r ex g st g<r & g in dom f & f.g<>0;
given r such that
A3: 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
A4: g1<r1 and
A5: g1 in dom f and
A6: f.g1<>0 by A2;
take g1;
thus g1<r1 by A4;
not f.g1 in {0} by A6,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
then g1 in dom f\f"{0} by A5,XBOOLE_0:def 5;
hence thesis by RFUNCT_1:def 2;
end;
let s be Real_Sequence;
assume that
A7: s is divergent_to-infty and
A8: rng s c=dom (f^);
consider k such that
A9: for n st k<=n holds s.n<r by A7;
A10: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A11: dom(f^)c=dom f by XBOOLE_1:36;
then
A12: rng s c=dom f by A8;
then
A13: rng(s^\k)c=dom f by A10;
A14: f/*(s^\k) is non-zero by A8,A10,RFUNCT_2:11,XBOOLE_1:1;
now
let n;
A15: n in NAT by ORDINAL1:def 12;
s.(n+k)<r by A9,NAT_1:12;
then (s^\k).n<r by NAT_1:def 3;
then (s^\k).n in {g2: g2<r};
then (s^\k).n in rng(s^\k) & (s^\k).n in left_open_halfline(r) by
VALUED_0:28,XXREAL_1:229;
then (s^\k).n in dom f/\left_open_halfline(r) by A13,XBOOLE_0:def 4;
then
A16: f.((s^\k).n)<=0 by A3;
(f/*(s^\k)).n<>0 by A14,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A12,A10,A16,FUNCT_2:108,XBOOLE_1:1,A15;
end;
then
A17: for n holds 0<=n implies (f/*(s^\k)).n<0;
s^\k is divergent_to-infty by A7,Th27;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A13,Def13;
then
A18: (f/*(s^\k))" is divergent_to-infty by A17,Th36;
(f/*(s^\k))"=((f/*s)^\k)" by A8,A11,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A8,RFUNCT_2:12;
hence thesis by A18,Th7;
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 that
A1: f is convergent_in+infty and
A2: lim_in+infty f=0;
given r such that
A3: 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
A4: r1<g1 and
g1 in dom f by A1;
now
per cases;
suppose
A5: g1<=r;
consider g2 such that
A6: r<g2 and
A7: g2 in dom f by A1;
take g2;
g1<g2 by A5,A6,XXREAL_0:2;
hence r1<g2 by A4,XXREAL_0:2;
g2 in {r2: r<r2} by A6;
then g2 in right_open_halfline(r) by XXREAL_1:230;
then g2 in dom f/\right_open_halfline(r) by A7,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g1<g2 and
A10: g2 in dom f by A1;
take g2;
thus r1<g2 by A4,A9,XXREAL_0:2;
r<g2 by A8,A9,XXREAL_0:2;
then g2 in {r2: r<r2};
then g2 in right_open_halfline(r) by XXREAL_1:230;
then g2 in dom f/\right_open_halfline(r) by A10,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to+infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds r<s.n by A11;
A14: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A15: dom(f^)c=dom f by XBOOLE_1:36;
then
A16: rng s c=dom f by A12;
then
A17: rng(s^\k)c=dom f by A14;
now
let n;
A18: n in NAT by ORDINAL1:def 12;
r<s.(n+k) by A13,NAT_1:12;
then r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: r<g2};
then (s^\k).n in rng(s^\k) & (s^\k).n in right_open_halfline(r) by
VALUED_0:28,XXREAL_1:230;
then (s^\k).n in dom f/\right_open_halfline(r) by A17,XBOOLE_0:def 4;
then 0<f.((s^\k).n) by A3;
hence 0<(f/*(s^\k)).n by A16,A14,FUNCT_2:108,XBOOLE_1:1,A18;
end;
then
A19: for n holds 0<=n implies 0<(f/*(s^\k)).n;
s^\k is divergent_to+infty by A11,Th26;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A2,A17,Def12;
then
A20: (f/*(s^\k))" is divergent_to+infty by A19,Th35;
(f/*(s^\k))"=((f/*s)^\k)" by A12,A15,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,RFUNCT_2:12;
hence thesis by A20,Th7;
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 that
A1: f is convergent_in+infty and
A2: lim_in+infty f=0;
given r such that
A3: 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
A4: r1<g1 and
g1 in dom f by A1;
now
per cases;
suppose
A5: g1<=r;
consider g2 such that
A6: r<g2 and
A7: g2 in dom f by A1;
take g2;
g1<g2 by A5,A6,XXREAL_0:2;
hence r1<g2 by A4,XXREAL_0:2;
g2 in {r2: r<r2} by A6;
then g2 in right_open_halfline(r) by XXREAL_1:230;
then g2 in dom f/\right_open_halfline(r) by A7,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g1<g2 and
A10: g2 in dom f by A1;
take g2;
thus r1<g2 by A4,A9,XXREAL_0:2;
r<g2 by A8,A9,XXREAL_0:2;
then g2 in {r2: r<r2};
then g2 in right_open_halfline(r) by XXREAL_1:230;
then g2 in dom f/\right_open_halfline(r) by A10,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to+infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds r<s.n by A11;
A14: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A15: dom(f^)c=dom f by XBOOLE_1:36;
then
A16: rng s c=dom f by A12;
then
A17: rng(s^\k)c=dom f by A14;
now
let n;
A18: n in NAT by ORDINAL1:def 12;
r<s.(n+k) by A13,NAT_1:12;
then r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: r<g2};
then (s^\k).n in rng(s^\k) & (s^\k).n in right_open_halfline(r) by
VALUED_0:28,XXREAL_1:230;
then (s^\k).n in dom f/\right_open_halfline(r) by A17,XBOOLE_0:def 4;
then f.((s^\k).n)<0 by A3;
hence (f/*(s^\k)).n<0 by A16,A14,FUNCT_2:108,XBOOLE_1:1,A18;
end;
then
A19: for n holds 0<=n implies (f/*(s^\k)).n<0;
s^\k is divergent_to+infty by A11,Th26;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A2,A17,Def12;
then
A20: (f/*(s^\k))" is divergent_to-infty by A19,Th36;
(f/*(s^\k))"=((f/*s)^\k)" by A12,A15,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,RFUNCT_2:12;
hence thesis by A20,Th7;
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 that
A1: f is convergent_in-infty and
A2: lim_in-infty f=0;
given r such that
A3: 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
A4: g1<r1 and
g1 in dom f by A1;
now
per cases;
suppose
A5: g1<=r;
consider g2 such that
A6: g2<g1 and
A7: g2 in dom f by A1;
take g2;
thus g2<r1 by A4,A6,XXREAL_0:2;
g2<r by A5,A6,XXREAL_0:2;
then g2 in {r2: r2<r};
then g2 in left_open_halfline(r) by XXREAL_1:229;
then g2 in dom f/\left_open_halfline(r) by A7,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g2<r and
A10: g2 in dom f by A1;
take g2;
g2<g1 by A8,A9,XXREAL_0:2;
hence g2<r1 by A4,XXREAL_0:2;
g2 in {r2: r2<r} by A9;
then g2 in left_open_halfline(r) by XXREAL_1:229;
then g2 in dom f/\left_open_halfline(r) by A10,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to-infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds s.n<r by A11;
A14: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A15: dom(f^)c=dom f by XBOOLE_1:36;
then
A16: rng s c=dom f by A12;
then
A17: rng(s^\k)c=dom f by A14;
now
let n;
A18: n in NAT by ORDINAL1:def 12;
s.(n+k)<r by A13,NAT_1:12;
then (s^\k).n<r by NAT_1:def 3;
then (s^\k).n in {g2: g2<r};
then (s^\k).n in rng(s^\k) & (s^\k).n in left_open_halfline(r) by
VALUED_0:28,XXREAL_1:229;
then (s^\k).n in dom f/\left_open_halfline(r) by A17,XBOOLE_0:def 4;
then 0<f.((s^\k).n) by A3;
hence 0<(f/*(s^\k)).n by A16,A14,FUNCT_2:108,XBOOLE_1:1,A18;
end;
then
A19: for n holds 0<=n implies 0<(f/*(s^\k)).n;
s^\k is divergent_to-infty by A11,Th27;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A2,A17,Def13;
then
A20: (f/*(s^\k))" is divergent_to+infty by A19,Th35;
(f/*(s^\k))"=((f/*s)^\k)" by A12,A15,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,RFUNCT_2:12;
hence thesis by A20,Th7;
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 that
A1: f is convergent_in-infty and
A2: lim_in-infty f=0;
given r such that
A3: 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
A4: g1<r1 and
g1 in dom f by A1;
now
per cases;
suppose
A5: g1<=r;
consider g2 such that
A6: g2<g1 and
A7: g2 in dom f by A1;
take g2;
thus g2<r1 by A4,A6,XXREAL_0:2;
g2<r by A5,A6,XXREAL_0:2;
then g2 in {r2: r2<r};
then g2 in left_open_halfline(r) by XXREAL_1:229;
then g2 in dom f/\left_open_halfline(r) by A7,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A7,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A8: r<=g1;
consider g2 such that
A9: g2<r and
A10: g2 in dom f by A1;
take g2;
g2<g1 by A8,A9,XXREAL_0:2;
hence g2<r1 by A4,XXREAL_0:2;
g2 in {r2: r2<r} by A9;
then g2 in left_open_halfline(r) by XXREAL_1:229;
then g2 in dom f/\left_open_halfline(r) by A10,XBOOLE_0:def 4;
then 0<>f.g2 by A3;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence;
assume that
A11: s is divergent_to-infty and
A12: rng s c=dom (f^);
consider k such that
A13: for n st k<=n holds s.n<r by A11;
A14: rng(s^\k)c=rng s by VALUED_0:21;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A15: dom(f^)c=dom f by XBOOLE_1:36;
then
A16: rng s c=dom f by A12;
then
A17: rng(s^\k)c=dom f by A14;
now
let n;
A18: n in NAT by ORDINAL1:def 12;
s.(n+k)<r by A13,NAT_1:12;
then (s^\k).n<r by NAT_1:def 3;
then (s^\k).n in {g2: g2<r};
then (s^\k).n in rng(s^\k) & (s^\k).n in left_open_halfline(r) by
VALUED_0:28,XXREAL_1:229;
then (s^\k).n in dom f/\left_open_halfline(r) by A17,XBOOLE_0:def 4;
then f.((s^\k).n)<0 by A3;
hence (f/*(s^\k)).n<0 by A16,A14,FUNCT_2:108,XBOOLE_1:1,A18;
end;
then
A19: for n holds 0<=n implies (f/*(s^\k)).n<0;
s^\k is divergent_to-infty by A11,Th27;
then f/*(s^\k) is convergent & lim(f/*(s^\k))=0 by A1,A2,A17,Def13;
then
A20: (f/*(s^\k))" is divergent_to-infty by A19,Th36;
(f/*(s^\k))"=((f/*s)^\k)" by A12,A15,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,RFUNCT_2:12;
hence thesis by A20,Th7;
end;