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