Copyright (c) 1990 Association of Mizar Users
environ
vocabulary SEQ_1, PARTFUN1, ARYTM, ARYTM_1, RELAT_1, BOOLE, ARYTM_3, SEQ_2,
ORDINAL2, FUNCT_1, SEQM_3, LIMFUNC1, RCOMP_1, ABSVALUE, RFUNCT_1,
RFUNCT_2, FINSEQ_1, LATTICES, LIMFUNC2;
notation TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, RELSET_1, RCOMP_1,
PARTFUN1, RFUNCT_1, RFUNCT_2, LIMFUNC1;
constructors REAL_1, NAT_1, ABSVALUE, SEQ_2, SEQM_3, PROB_1, RCOMP_1,
RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, MEMBERED, XBOOLE_0;
clusters RELSET_1, XREAL_0, SEQ_1, NAT_1, MEMBERED, ZFMISC_1, XBOOLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
theorems TARSKI, AXIOMS, REAL_1, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4,
SQUARE_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PROB_1, RCOMP_1, FUNCT_1,
XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1;
schemes SEQ_1, RCOMP_1;
begin
reserve r,r1,r2,g,g1,g2,x0 for Real;
reserve n,k for Nat;
reserve seq for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;
Lm1: for r,g,r1 be real number holds 0<g & r<=r1 implies r-g<r1 & r<r1+g
proof
let r,g,r1 be real number;
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;
Lm2: for X be Subset of REAL st rng seq c=dom(f1(#)f2)/\X holds
rng seq c=dom(f1(#)f2) & rng seq c= X & dom(f1(#)f2)=dom f1/\dom f2 &
rng seq c=dom f1 & rng seq c=dom f2 & rng seq c=dom f1/\X & rng seq c=dom f2/\X
proof let X be Subset of REAL such that A1: rng seq c=dom(f1(#)f2)/\X;
dom(f1(#)f2)/\X c=dom(f1(#)f2) & dom(f1(#)f2)/\X c=X by XBOOLE_1:17;
hence A2: rng seq c=dom(f1(#)f2) & rng seq c=X by A1,XBOOLE_1:1;
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 rng seq c=dom f1 & rng seq c=dom f2 by A2,XBOOLE_1:1;
hence rng seq c=dom f1/\X & rng seq c=dom f2/\X by A2,XBOOLE_1:19;
end;
Lm3: r-1/(n+1)<r & r<r+1/(n+1)
proof
0<n+1 by NAT_1:19;
then 0<1/(n+1) by SEQ_2:6; hence thesis by Lm1;
end;
Lm4: for X be Subset of REAL st rng seq c=dom(f1+f2)/\X holds
rng seq c=dom(f1+f2) & rng seq c= X & dom(f1+f2)=dom f1/\dom f2 &
rng seq c=dom f1/\X & rng seq c=dom f2/\X
proof let X be Subset of REAL such that A1: rng seq c=dom(f1+f2)/\X;
dom(f1+f2)/\X c=dom(f1+f2) & dom(f1+f2)/\X c=X by XBOOLE_1:17;
hence A2: rng seq c=dom(f1+f2) & rng seq c=X by A1,XBOOLE_1:1;
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;
then rng seq c=dom f1 & rng seq c=dom f2 by A2,XBOOLE_1:1;
hence rng seq c=dom f1/\X & rng seq c=dom f2/\X by A2,XBOOLE_1:19;
end;
theorem Th1:
seq is convergent & r<lim seq implies ex n st for k st n<=k holds r<seq.k
proof assume A1: seq is convergent & r<lim seq;
deffunc U(Nat) = r;
consider s be Real_Sequence such that A2: for n holds s.n= U(n)
from ExRealSeq;
now let n; s.n=r & s.(n+1)=r by A2; hence s.n=s.(n+1); end;
then A3: s is constant by SEQM_3:16; then A4: s is convergent by SEQ_4:39;
then A5: seq-s is convergent by A1,SEQ_2:25;
s.0=r by A2; then lim s=r by A3,SEQ_4:40;
then lim(seq-s)=lim seq -r by A1,A4,SEQ_2:26; then 0<lim(seq-s) by A1,SQUARE_1
:11;
then consider n such that A6: for k st n<=
k holds 0<(seq-s).k by A5,LIMFUNC1:29;
take n; let k; assume n<=k; then 0<(seq-s).k by A6;
then 0<seq.k-s.k by RFUNCT_2:6; then 0<seq.k-r by A2; then 0+r<seq.k by REAL_1
:86;
hence r<seq.k;
end;
theorem Th2:
seq is convergent & lim seq<r implies ex n st for k st n<=k holds seq.k<r
proof assume A1: seq is convergent & lim seq<r;
deffunc U(Nat) = r;
consider s be Real_Sequence such that
A2: for n holds s.n= U(n) from ExRealSeq;
now let n; s.n=r & s.(n+1)=r by A2; hence s.n=s.(n+1); end;
then A3: s is constant by SEQM_3:16; then A4: s is convergent by SEQ_4:39;
then A5: s-seq is convergent by A1,SEQ_2:25; s.0=r by A2;
then lim s=r by A3,SEQ_4:40; then lim(s-seq)=r-lim seq by A1,A4,SEQ_2:26;
then 0<lim(s-seq) by A1,SQUARE_1:11; then consider n such that
A6: for k st n<=k holds 0<(s-seq).k by A5,LIMFUNC1:29
; take n; let k;assume n<=k;
then 0<(s-seq).k by A6; then 0<s.k-seq.k by RFUNCT_2:6; then 0<r-seq.k by A2;
then 0+seq.k<r by REAL_1:86; hence seq.k<r;
end;
Lm5: (for g1 ex r st x0<r &
for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1) &
seq is convergent & lim seq=x0 & rng seq c=dom f/\right_open_halfline(x0)
implies f*seq is divergent_to-infty
proof assume that
A1: for g1 ex r st x0<r &
for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1 and
A2: seq is convergent & lim seq=x0 & rng seq c=dom f/\right_open_halfline(x0);
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A3: rng seq c=dom f by A2,XBOOLE_1:1;
now let g1; consider r such that
A4: x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1 by A1;
consider n such that A5: for k st n<=k holds seq.k<r by A2,A4,Th2; take n;
let k; assume n<=k; then A6: seq.k<r by A5; seq.k in rng seq by RFUNCT_2:10
;
then A7: seq.k in right_open_halfline(x0) & seq.k in dom f by A2,XBOOLE_0:def
3
;
then seq.k in {g2: x0<g2} by LIMFUNC1:def 3; then ex g2 st g2=seq.k & x0<g2
;
then f.(seq.k)<g1 by A4,A6,A7; hence (f*seq).k<g1 by A3,RFUNCT_2:21;
end; hence thesis by LIMFUNC1:def 5;
end;
theorem Th3:
0<r2 & ].r1-r2,r1.[ c= dom f implies
for r st r<r1 ex g st r<g & g<r1 & g in dom f
proof assume A1: 0<r2 & ].r1-r2,r1.[c=dom f; let r such that A2: r<r1;
now per cases;
suppose A3: r1-r2<=r; consider g being real number such that
A4: r<g & g<r1 by A2,REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g; thus r<g & g<r1 by A4; r1-r2<g by A3,A4,AXIOMS:22;
then g in {g2: r1-r2<g2 & g2<r1} by A4; then g in ].r1-r2,r1.[ by RCOMP_1:def
2;
hence g in dom f by A1;
suppose A5: r<=r1-r2; r1-r2<r1 by A1,Lm1;
then consider g being real number such that
A6: r1-r2<g & g<r1 by REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus r<g & g<r1 by A5,A6,AXIOMS:22; g in {g2: r1-r2<g2 & g2<r1} by A6;
then g in ].r1-r2,r1.[ by RCOMP_1:def 2; hence g in dom f by A1;
end; hence thesis;
end;
theorem Th4:
0<r2 & ].r1,r1+r2.[ c= dom f implies
for r st r1<r ex g st g<r & r1<g & g in dom f
proof assume A1: 0<r2 & ].r1,r1+r2.[ c=dom f; let r such that A2: r1<r;
now per cases;
suppose A3: r1+r2<=r; r1<r1+r2 by A1,Lm1;
then consider g being real number such that
A4: r1<g & g<r1+r2 by REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus g<r & r1<g by A3,A4,AXIOMS:22; g in {g2: r1<g2 & g2<r1+r2} by A4;
then g in ].r1,r1+r2.[ by RCOMP_1:def 2; hence g in dom f by A1;
suppose
A5: r<=r1+r2;
consider g being real number such that A6: r1<g & g<r by A2,REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus g<r & r1<g by A6; r1<g & g<r1+r2 by A5,A6,AXIOMS:22;
then g in {g2: r1<g2 & g2<r1+r2}; then g in ].r1,r1+r2.[ by RCOMP_1:def 2;
hence g in dom f by A1;
end; hence thesis;
end;
theorem Th5:
(for n holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f) implies
seq is convergent & lim seq=x0 & rng seq c= dom f &
rng seq c= dom f /\ left_open_halfline(x0)
proof assume A1: for n holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f;
deffunc U(Nat) = 1/($1+1);
consider s1 be Real_Sequence such that
A2: for n holds s1.n=U(n) from ExRealSeq;
deffunc U(Nat) = x0;
consider s2 be Real_Sequence such that
A3: for n holds s2.n=U(n) from ExRealSeq;
now let n; s2.n=x0 & s2.(n+1)=x0 by A3; hence s2.n=s2.(n+1); end;
then A4: s2 is constant by SEQM_3:16;
then A5: s2 is convergent by SEQ_4:39; s2.0=x0 by A3;
then A6: lim s2=x0 by A4,SEQ_4:40;
A7: s1 is convergent & lim s1=0 by A2,SEQ_4:45;
then A8: s2-s1 is convergent by A5,SEQ_2:25;
A9: lim(s2-s1)=x0-0 by A5,A6,A7,SEQ_2:26
.=x0;
A10: now let n; A11: x0-1/(n+1)<=seq.n & seq.n<=x0 by A1;
(s2-s1).n=s2.n-s1.n by RFUNCT_2:6
.=x0-s1.n by A3
.=x0-1/(n+1) by A2;
hence (s2-s1).n<=seq.n & seq.n<=s2.n by A3,A11;
end; hence seq is convergent by A5,A6,A8,A9,SEQ_2:33;
thus lim seq=x0 by A5,A6,A8,A9,A10,SEQ_2:34;
now let x be set; assume x in rng seq; then consider n such that
A12: x=seq.n by RFUNCT_2:9; seq.n<x0 by A1;
then seq.n in {g2:g2<x0}; hence x in left_open_halfline(x0) by A12,PROB_1:def
15;
end; then A13: rng seq c=left_open_halfline(x0) by TARSKI:def 3;
now let x be set; assume x in rng seq; then ex n st
seq.n=x by RFUNCT_2:9; hence x in dom f by A1;
end; hence rng seq c=dom f by TARSKI:def 3; hence thesis by A13,XBOOLE_1:19;
end;
theorem Th6:
(for n holds x0<seq.n & seq.n<x0+1/(n+1) & seq.n in dom f) implies
seq is convergent & lim seq=x0 & rng seq c= dom f &
rng seq c= dom f /\ right_open_halfline(x0)
proof assume A1: for n holds x0<seq.n & seq.n<x0+1/(n+1) & seq.n in dom f;
deffunc U(Nat) = 1/($1+1);
consider s1 be Real_Sequence such that
A2: for n holds s1.n=U(n) from ExRealSeq;
deffunc U(Nat) = x0;
consider s2 be Real_Sequence such that
A3: for n holds s2.n=U(n)from ExRealSeq;
now let n; s2.n=x0 & s2.(n+1)=x0 by A3; hence s2.n=s2.(n+1); end;
then A4: s2 is constant by SEQM_3:16;
then A5: s2 is convergent by SEQ_4:39; s2.0=x0 by A3;
then A6: lim s2=x0 by A4,SEQ_4:40;
A7: s1 is convergent & lim s1=0 by A2,SEQ_4:45;
then A8: s2+s1 is convergent by A5,SEQ_2:19;
A9: lim(s2+s1)=x0+0 by A5,A6,A7,SEQ_2:20
.=x0;
A10: now let n; A11: x0<=seq.n & seq.n<=x0+1/(n+1) by A1;
(s2+s1).n=s2.n+s1.n by SEQ_1:11
.=x0+s1.n by A3
.=x0+1/(n+1) by A2;
hence s2.n<=seq.n & seq.n<=(s2+s1).n by A3,A11;
end; hence seq is convergent by A5,A6,A8,A9,SEQ_2:33;
thus lim seq=x0 by A5,A6,A8,A9,A10,SEQ_2:34;
now let x be set; assume x in rng seq; then consider n such that
A12: x=seq.n by RFUNCT_2:9; x0<seq.n by A1;
then seq.n in {g2:x0<g2};
hence x in right_open_halfline(x0) by A12,LIMFUNC1:def 3;
end; then A13: rng seq c=right_open_halfline(x0) by TARSKI:def 3;
now let x be set; assume x in rng seq; then ex n st
seq.n=x by RFUNCT_2:9; hence x in dom f by A1;
end; hence rng seq c=dom f by TARSKI:def 3; hence thesis by A13,XBOOLE_1:19;
end;
definition let f,x0;
pred f is_left_convergent_in x0 means :Def1:
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
ex g st for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g;
pred f is_left_divergent_to+infty_in x0 means :Def2:
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is divergent_to+infty;
pred f is_left_divergent_to-infty_in x0 means :Def3:
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is divergent_to-infty;
pred f is_right_convergent_in x0 means :Def4:
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
ex g st for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ right_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g;
pred f is_right_divergent_to+infty_in x0 means :Def5:
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\
right_open_halfline(x0) holds f*seq is divergent_to+infty;
pred f is_right_divergent_to-infty_in x0 means :Def6:
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\
right_open_halfline(x0) holds f*seq is divergent_to-infty;
end;
canceled 6;
theorem
f is_left_convergent_in x0 iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
ex g st for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds
abs(f.r1-g)<g1
proof thus f is_left_convergent_in x0 implies
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
ex g st for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds
abs(f.r1-g)<g1
proof assume that A1: f is_left_convergent_in x0 and
A2: (not for r st r<x0 ex g st r<g & g<x0 & g in dom f) or
for g ex g1 st 0<g1 & for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f &
abs(f.r1-g)>=g1; consider g such that
A3: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f/\
left_open_halfline(x0) holds f*seq is convergent & lim(f*seq)=g by A1,Def1;
consider g1 such that A4: 0<g1 & for r st r<x0
ex r1 st r<r1 & r1<x0 & r1 in dom f & abs(f.r1-g)>=g1 by A1,A2,Def1;
defpred X[Nat,real number] means
x0-1/($1+1)<$2 & $2<x0 & $2 in dom f & abs(f.($2)-g)>=g1;
A5: now let n; x0-1/(n+1)<x0 by Lm3; then consider g2 such that
A6: x0-1/(n+1)<g2 & g2<x0 & g2 in dom f & abs(f.g2-g)>=g1 by A4;
reconsider g2 as real number;
take g2;
thus X[n,g2] by A6;
end; consider s be Real_Sequence such that
A7: for n holds X[n,s.n]
from RealSeqChoice(A5);
A8: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\left_open_halfline(x0) by A7,Th5;
then f*s is convergent & lim(f*s)=g by A3; then consider n such that
A9: for k st n<=k holds abs((f*s).k-g)<g1 by A4,SEQ_2:def 7;
abs((f*s).n-g)<g1 by A9;
then abs(f.(s.n)-g)<g1 by A8,RFUNCT_2:21; hence contradiction by A7;
end;
assume A10: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
given g such that A11: for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds abs(f.r1-g)<g1;
now let s be Real_Sequence such that
A12: s is convergent & lim s=x0 & rng s c=dom f/\left_open_halfline(x0);
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A13: rng s c=dom f by A12,XBOOLE_1:1;
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: r<x0 & for r1 st r<r1 & r1<x0 &
r1 in dom f holds abs(f.r1-g)<g1 by A11,A15;
consider n such that A17: for k st n<=k holds r<s.k by A12,A16,Th1;
take n; let k; assume n<=k; then A18: r<s.k by A17;
s.k in rng s by RFUNCT_2:10;
then A19: s.k in left_open_halfline(x0) & s.k in dom f by A12,XBOOLE_0:def 3
;
then s.k in {g2: g2<x0} by PROB_1:def 15; then ex g2 st g2=s.k & g2<x0;
then abs(f.(s.k)-g)<g1 by A16,A18,A19;
hence abs((f*s).k-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 A10,Def1;
end;
theorem
f is_left_divergent_to+infty_in x0 iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds g1<f.r1
proof thus f is_left_divergent_to+infty_in x0 implies
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds g1<f.r1
proof assume that A1: f is_left_divergent_to+infty_in x0 and
A2: (not for r st r<x0 ex g st r<g & g<x0 & g in dom f) or
ex g1 st for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & g1>=f.r1;
consider g1 such that A3: for r st r<x0
ex r1 st r<r1 & r1<x0 & r1 in dom f & g1>=f.r1 by A1,A2,Def2;
defpred X[Nat,real number] means
x0-1/($1+1)<$2 & $2<x0 & $2 in dom f & f.($2)<=g1;
A4: now let n; x0-1/(n+1)<x0 by Lm3; then consider g2 such that
A5: x0-1/(n+1)<g2 & g2<x0 & g2 in dom f & f.g2<=g1 by A3;
reconsider g2 as real number;
take g2;
thus X[n,g2] by A5;
end; consider s be Real_Sequence such that
A6: for n holds X[n,s.n]
from RealSeqChoice(A4);
A7: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\left_open_halfline(x0) by A6,Th5;
then f*s is divergent_to+infty by A1,Def2; then consider n such that
A8: for k st n<=k holds g1<(f*s).k by LIMFUNC1:def 4; g1<(f*s).n by A8;
then g1<f.(s.n) by A7,RFUNCT_2:21; hence contradiction by A6;
end;
assume that A9: for r st r<x0 ex g st r<g & g<x0 & g in dom f and
A10: for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds g1<f.r1;
now let s be Real_Sequence such that
A11: s is convergent & lim s=x0 & rng s c=dom f/\left_open_halfline(x0);
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
now let g1; consider r such that
A13: r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds g1<f.r1 by A10;
consider n such that A14: for k st n<=k holds r<s.k by A11,A13,Th1;
take n; let k; assume n<=k; then A15: r<s.k by A14
; s.k in rng s by RFUNCT_2:10;
then A16: s.k in left_open_halfline(x0) & s.k in dom f by A11,XBOOLE_0:def 3
;
then s.k in {g2: g2<x0} by PROB_1:def 15; then ex g2 st g2=s.k & g2<x0;
then g1<f.(s.k) by A13,A15,A16; hence g1<(f*s).k by A12,RFUNCT_2:21;
end; hence f*s is divergent_to+infty by LIMFUNC1:def 4;
end; hence thesis by A9,Def2;
end;
theorem
f is_left_divergent_to-infty_in x0 iff
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds f.r1<g1
proof thus f is_left_divergent_to-infty_in x0 implies
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) &
for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds f.r1<g1
proof assume that A1: f is_left_divergent_to-infty_in x0 and
A2: (not for r st r<x0 ex g st r<g & g<x0 & g in dom f) or
ex g1 st for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f & g1<=f.r1;
consider g1 such that A3: for r st r<x0
ex r1 st r<r1 & r1<x0 & r1 in dom f & g1<=f.r1 by A1,A2,Def3;
defpred X[Nat,real number] means
x0-1/($1+1)<$2 & $2<x0 & $2 in dom f & g1<=f.($2);
A4: now let n; x0-1/(n+1)<x0 by Lm3; then consider g2 such that
A5: x0-1/(n+1)<g2 & g2<x0 & g2 in dom f & g1<=f.g2 by A3;
reconsider g2 as real number;
take g2;
thus X[n,g2] by A5;
end; consider s be Real_Sequence such that
A6: for n holds X[n,s.n]
from RealSeqChoice(A4);
A7: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\left_open_halfline(x0) by A6,Th5;
then f*s is divergent_to-infty by A1,Def3; then consider n such that
A8: for k st n<=k holds (f*s).k<g1 by LIMFUNC1:def 5; (f*s).n<g1 by A8;
then f.(s.n)<g1 by A7,RFUNCT_2:21; hence contradiction by A6;
end;
assume that A9: for r st r<x0 ex g st r<g & g<x0 & g in dom f and
A10: for g1 ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds f.r1<g1;
now let s be Real_Sequence such that
A11: s is convergent & lim s=x0 & rng s c=dom f/\left_open_halfline(x0);
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
now let g1; consider r such that
A13: r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds f.r1<g1 by A10;
consider n such that A14: for k st n<=k holds r<s.k by A11,A13,Th1;
take n; let k; assume n<=k; then A15: r<s.k by A14
; s.k in rng s by RFUNCT_2:10;
then A16: s.k in left_open_halfline(x0) & s.k in dom f by A11,XBOOLE_0:def 3
;
then s.k in {g2: g2<x0} by PROB_1:def 15; then ex g2 st g2=s.k & g2<x0;
then f.(s.k)<g1 by A13,A15,A16; hence (f*s).k<g1 by A12,RFUNCT_2:21;
end; hence f*s is divergent_to-infty by LIMFUNC1:def 5;
end; hence thesis by A9,Def3;
end;
theorem
f is_right_convergent_in x0 iff
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
ex g st for g1 st 0<g1
ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds
abs(f.r1-g)<g1
proof thus f is_right_convergent_in x0 implies
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
ex g st for g1 st 0<g1
ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds
abs(f.r1-g)<g1
proof assume that A1: f is_right_convergent_in x0 and
A2: (not for r st x0<r ex g st g<r & x0<g & g in dom f) or
for g ex g1 st 0<g1 & for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f &
abs(f.r1-g)>=g1; consider g such that
A3: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f/\
right_open_halfline(x0) holds f*seq is convergent & lim(f*seq)=g by A1,Def4;
consider g1 such that A4: 0<g1 & for r st x0<r
ex r1 st r1<r & x0<r1 & r1 in dom f & abs(f.r1-g)>=g1 by A1,A2,Def4;
defpred X[Nat,real number] means
x0<$2 & $2<x0+1/($1+1) & $2 in dom f & g1<=abs(f.($2)-g);
A5: now let n; x0<x0+1/(n+1) by Lm3; then consider r1 such that
A6: r1<x0+(1/(n+1)) & x0<r1 & r1 in dom f & g1<=abs(f.r1-g) by A4;
reconsider r1 as real number;
take r1;
thus X[n,r1] by A6;
end; consider s be Real_Sequence such that
A7: for n holds X[n,s.n]
from RealSeqChoice(A5);
A8: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\right_open_halfline(x0) by A7,Th6;
then f*s is convergent & lim(f*s)=g by A3; then consider n such that
A9: for k st n<=k holds abs((f*s).k-g)<g1 by A4,SEQ_2:def 7;
abs((f*s).n-g)<g1 by A9;
then abs(f.(s.n)-g)<g1 by A8,RFUNCT_2:21; hence contradiction by A7;
end;
assume A10: for r st x0<r ex g st g<r & x0<g & g in dom f;
given g such that A11: for g1 st 0<g1 ex r st x0<r &
for r1 st r1<r & x0<r1 & r1 in dom f holds abs(f.r1-g)<g1;
now let s be Real_Sequence such that
A12: s is convergent & lim s=x0 & rng s c=dom f/\right_open_halfline(x0);
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A13: rng s c=dom f by A12,XBOOLE_1:1;
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: x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds
abs(f.r1-g)<g1 by A11,A15;
consider n such that A17: for k st n<=k holds s.k<r by A12,A16,Th2;
take n; let k; assume n<=k; then A18: s.k<r by A17;
s.k in rng s by RFUNCT_2:10;
then A19: s.k in right_open_halfline(x0) & s.k in dom f by A12,XBOOLE_0:def
3
;
then s.k in {g2: x0<g2} by LIMFUNC1:def 3; then ex g2 st g2=s.k & x0<g2;
then abs(f.(s.k)-g)<g1 by A16,A18,A19;
hence abs((f*s).k-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 A10,Def4;
end;
theorem
f is_right_divergent_to+infty_in x0 iff
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds g1<f.r1
proof thus f is_right_divergent_to+infty_in x0 implies
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds g1<f.r1
proof assume that A1: f is_right_divergent_to+infty_in x0 and
A2: (not for r st x0<r ex g st g<r & x0<g & g in dom f) or
ex g1 st for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & f.r1<=g1;
consider g1 such that A3: for r st x0<r
ex r1 st r1<r & x0<r1 & r1 in dom f & f.r1<=g1 by A1,A2,Def5;
defpred X[Nat,real number] means
x0<$2 & $2<x0+1/($1+1) & $2 in dom f & f.($2)<=g1;
A4: now let n; x0<x0+1/(n+1) by Lm3; then consider r1 such that
A5: r1<x0+(1/(n+1)) & x0<r1 & r1 in dom f & f.r1<=g1 by A3;
reconsider r1 as real number;
take r1;
thus X[n,r1] by A5;
end; consider s be Real_Sequence such that
A6: for n holds X[n,s.n]
from RealSeqChoice(A4);
A7: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\right_open_halfline(x0) by A6,Th6;
then f*s is divergent_to+infty by A1,Def5; then consider n such that
A8: for k st n<=k holds g1<(f*s).k by LIMFUNC1:def 4; g1<(f*s).n by A8;
then g1<f.(s.n) by A7,RFUNCT_2:21; hence contradiction by A6;
end;
assume that A9: for r st x0<r ex g st g<r & x0<g & g in dom f and
A10: for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds g1<f.r1;
now let s be Real_Sequence such that
A11: s is convergent & lim s=x0 & rng s c=dom f/\right_open_halfline(x0);
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
now let g1; consider r such that
A13: x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds g1<f.r1 by A10;
consider n such that A14: for k st n<=k holds s.k<r by A11,A13,Th2;
take n; let k; assume n<=k; then A15: s.k<r by A14
; s.k in rng s by RFUNCT_2:10;
then A16: s.k in right_open_halfline(x0) & s.k in dom f by A11,XBOOLE_0:def
3
;
then s.k in {g2: x0<g2} by LIMFUNC1:def 3; then ex g2 st g2=s.k & x0<g2;
then g1<f.(s.k) by A13,A15,A16; hence g1<(f*s).k by A12,RFUNCT_2:21;
end; hence f*s is divergent_to+infty by LIMFUNC1:def 4;
end; hence thesis by A9,Def5;
end;
theorem
f is_right_divergent_to-infty_in x0 iff
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1
proof thus f is_right_divergent_to-infty_in x0 implies
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1
proof assume that A1: f is_right_divergent_to-infty_in x0 and
A2: (not for r st x0<r ex g st g<r & x0<g & g in dom f) or
ex g1 st for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f & g1<=f.r1;
consider g1 such that A3: for r st x0<r
ex r1 st r1<r & x0<r1 & r1 in dom f & g1<=f.r1 by A1,A2,Def6;
defpred X[Nat,real number] means
x0<$2 & $2<x0+1/($1+1) & $2 in dom f & g1<=f.($2);
A4: now let n; x0<x0+1/(n+1) by Lm3; then consider r1 such that
A5: r1<x0+(1/(n+1)) & x0<r1 & r1 in dom f & g1<=f.r1 by A3;
reconsider r1 as real number;
take r1;
thus X[n,r1] by A5;
end; consider s be Real_Sequence such that
A6: for n holds X[n,s.n]
from RealSeqChoice(A4);
A7: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\right_open_halfline(x0) by A6,Th6;
then f*s is divergent_to-infty by A1,Def6; then consider n such that
A8: for k st n<=k holds (f*s).k<g1 by LIMFUNC1:def 5; (f*s).n<g1 by A8;
then f.(s.n)<g1 by A7,RFUNCT_2:21; hence contradiction by A6;
end;
assume that A9: for r st x0<r ex g st g<r & x0<g & g in dom f and
A10: for g1 ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds f.r1<g1;
for s be Real_Sequence holds
s is convergent & lim s=x0 & rng s c=dom f/\right_open_halfline(x0) implies
f*s is divergent_to-infty by A10,Lm5; hence thesis by A9,Def6;
end;
theorem
f1 is_left_divergent_to+infty_in x0 & f2 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f1 /\ dom f2) implies
f1+f2 is_left_divergent_to+infty_in x0 & f1(#)
f2 is_left_divergent_to+infty_in x0
proof assume A1: f1 is_left_divergent_to+infty_in x0 &
f2 is_left_divergent_to+infty_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom f1/\dom f2;
A2: now let r; assume r<x0; then consider g such that
A3: r<g & g<x0 & g in dom f1/\dom f2 by A1; take g;
thus r<g & g<x0 & g in dom(f1+f2) by A3,SEQ_1:def 3;
end;
now let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\left_open_halfline(x0);
then A5: rng seq c=dom(f1+f2) & rng seq c=left_open_halfline(x0) &
dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\left_open_halfline(x0) &
rng seq c=dom f2/\left_open_halfline(x0) by Lm4;
then A6: f1*seq is divergent_to+infty by A1,A4,Def2;
f2*seq is divergent_to+infty by A1,A4,A5,Def2;
then f1*seq+f2*seq is divergent_to+infty by A6,LIMFUNC1:35;
hence (f1+f2)*seq is divergent_to+infty by A5,RFUNCT_2:23;
end; hence f1+f2 is_left_divergent_to+infty_in x0 by A2,Def2;
A7: now let r; assume r<x0; then consider g such that
A8: r<g & g<x0 & g in dom f1/\dom f2 by A1; take g;
thus r<g & g<x0 & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
end;
now let seq; assume A9: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
then A10: rng seq c=dom(f1(#)f2) & rng seq c=left_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1/\left_open_halfline(x0) &
rng seq c=dom f2/\left_open_halfline(x0) by Lm2;
then A11: f1*seq is divergent_to+infty by A1,A9,Def2;
f2*seq is divergent_to+infty by A1,A9,A10,Def2;
then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,LIMFUNC1:37;
hence (f1(#)f2)*seq is divergent_to+infty by A10,RFUNCT_2:23;
end; hence thesis by A7,Def2;
end;
theorem
f1 is_left_divergent_to-infty_in x0 & f2 is_left_divergent_to-infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f1 /\ dom f2) implies
f1+f2 is_left_divergent_to-infty_in x0 &
f1(#)f2 is_left_divergent_to+infty_in x0
proof assume A1: f1 is_left_divergent_to-infty_in x0 &
f2 is_left_divergent_to-infty_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom f1/\dom f2;
A2: now let r; assume r<x0; then consider g such that
A3: r<g & g<x0 & g in dom f1/\dom f2 by A1; take g;
thus r<g & g<x0 & g in dom(f1+f2) by A3,SEQ_1:def 3;
end;
now let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\left_open_halfline(x0);
then A5: rng seq c=dom(f1+f2) & rng seq c=left_open_halfline(x0) &
dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\left_open_halfline(x0) &
rng seq c=dom f2/\left_open_halfline(x0) by Lm4;
then A6: f1*seq is divergent_to-infty by A1,A4,Def3;
f2*seq is divergent_to-infty by A1,A4,A5,Def3;
then f1*seq+f2*seq is divergent_to-infty by A6,LIMFUNC1:38;
hence (f1+f2)*seq is divergent_to-infty by A5,RFUNCT_2:23;
end; hence f1+f2 is_left_divergent_to-infty_in x0 by A2,Def3;
A7: now let r; assume r<x0; then consider g such that
A8: r<g & g<x0 & g in dom f1/\dom f2 by A1; take g;
thus r<g & g<x0 & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
end;
now let seq; assume A9: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
then A10: rng seq c=dom(f1(#)f2) & rng seq c=left_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1/\left_open_halfline(x0) &
rng seq c=dom f2/\left_open_halfline(x0) by Lm2;
then A11: f1*seq is divergent_to-infty by A1,A9,Def3;
f2*seq is divergent_to-infty by A1,A9,A10,Def3;
then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,LIMFUNC1:51;
hence (f1(#)f2)*seq is divergent_to+infty by A10,RFUNCT_2:23;
end; hence thesis by A7,Def2;
end;
theorem
f1 is_right_divergent_to+infty_in x0 & f2 is_right_divergent_to+infty_in x0
&
(for r st x0<r ex g st g<r & x0<g & g in dom f1 /\ dom f2) implies
f1+f2 is_right_divergent_to+infty_in x0 &
f1(#)f2 is_right_divergent_to+infty_in x0
proof assume A1: f1 is_right_divergent_to+infty_in x0 &
f2 is_right_divergent_to+infty_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom f1/\dom f2;
A2: now let r; assume x0<r; then consider g such that
A3: g<r & x0<g & g in dom f1/\dom f2 by A1; take g;
thus g<r & x0<g & g in dom(f1+f2) by A3,SEQ_1:def 3;
end;
now let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\right_open_halfline(x0);
then A5: rng seq c=dom(f1+f2) & rng seq c=right_open_halfline(x0) &
dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\right_open_halfline(x0) &
rng seq c=dom f2/\right_open_halfline(x0) by Lm4;
then A6: f1*seq is divergent_to+infty by A1,A4,Def5;
f2*seq is divergent_to+infty by A1,A4,A5,Def5;
then f1*seq+f2*seq is divergent_to+infty by A6,LIMFUNC1:35;
hence (f1+f2)*seq is divergent_to+infty by A5,RFUNCT_2:23;
end; hence f1+f2 is_right_divergent_to+infty_in x0 by A2,Def5;
A7: now let r; assume x0<r; then consider g such that
A8: g<r & x0<g & g in dom f1/\dom f2 by A1; take g;
thus g<r & x0<g & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
end;
now let seq; assume A9: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
then A10: rng seq c=dom(f1(#)f2) & rng seq c=right_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1/\right_open_halfline(x0) &
rng seq c=dom f2/\right_open_halfline(x0) by Lm2;
then A11: f1*seq is divergent_to+infty by A1,A9,Def5;
f2*seq is divergent_to+infty by A1,A9,A10,Def5;
then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,LIMFUNC1:37;
hence (f1(#)f2)*seq is divergent_to+infty by A10,RFUNCT_2:23;
end; hence thesis by A7,Def5;
end;
theorem
f1 is_right_divergent_to-infty_in x0 & f2 is_right_divergent_to-infty_in x0
&
(for r st x0<r ex g st g<r & x0<g & g in dom f1 /\ dom f2) implies
f1+f2 is_right_divergent_to-infty_in x0 &
f1(#)f2 is_right_divergent_to+infty_in x0
proof assume A1: f1 is_right_divergent_to-infty_in x0 &
f2 is_right_divergent_to-infty_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom f1/\dom f2;
A2: now let r; assume x0<r; then consider g such that
A3: g<r & x0<g & g in dom f1/\dom f2 by A1; take g;
thus g<r & x0<g & g in dom(f1+f2) by A3,SEQ_1:def 3;
end;
now let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\right_open_halfline(x0);
then A5: rng seq c=dom(f1+f2) & rng seq c=right_open_halfline(x0) &
dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\right_open_halfline(x0) &
rng seq c=dom f2/\right_open_halfline(x0) by Lm4;
then A6: f1*seq is divergent_to-infty by A1,A4,Def6;
f2*seq is divergent_to-infty by A1,A4,A5,Def6;
then f1*seq+f2*seq is divergent_to-infty by A6,LIMFUNC1:38;
hence (f1+f2)*seq is divergent_to-infty by A5,RFUNCT_2:23;
end; hence f1+f2 is_right_divergent_to-infty_in x0 by A2,Def6;
A7: now let r; assume x0<r; then consider g such that
A8: g<r & x0<g & g in dom f1/\dom f2 by A1; take g;
thus g<r & x0<g & g in dom(f1(#)f2) by A8,SEQ_1:def 5;
end;
now let seq; assume A9: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
then A10: rng seq c=dom(f1(#)f2) & rng seq c=right_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1/\right_open_halfline(x0) &
rng seq c=dom f2/\right_open_halfline(x0) by Lm2;
then A11: f1*seq is divergent_to-infty by A1,A9,Def6;
f2*seq is divergent_to-infty by A1,A9,A10,Def6;
then (f1*seq)(#)(f2*seq) is divergent_to+infty by A11,LIMFUNC1:51;
hence (f1(#)f2)*seq is divergent_to+infty by A10,RFUNCT_2:23;
end; hence thesis by A7,Def5;
end;
theorem
f1 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2)) &
(ex r st 0<r & f2 is_bounded_below_on ].x0-r,x0.[) implies
f1+f2 is_left_divergent_to+infty_in x0
proof assume A1: f1 is_left_divergent_to+infty_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2); given r such that
A2: 0<r & f2 is_bounded_below_on ].x0-r,x0.[;
now let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\left_open_halfline(x0);
x0-r<x0 by A2,Lm1; then consider k such that
A4: for n st k<=n holds x0-r<seq.n by A3,Th1;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
rng(seq^\k)c=rng seq by RFUNCT_2:7;
then A6: rng(seq^\k)c=dom(f1+f2)/\left_open_halfline(x0) by A3,XBOOLE_1:1;
A7: dom(f1+f2)/\left_open_halfline(x0) c=dom(f1+f2) &
dom(f1+f2)/\left_open_halfline(x0) c=left_open_halfline(x0) by XBOOLE_1:17
;
then A8: rng(seq^\k)c=dom(f1+f2) & rng(seq^\k)c=left_open_halfline(x0)
by A6,XBOOLE_1:1;
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;
then A9: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A8,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A8,XBOOLE_1:19;
then A10: f1*(seq^\k) is divergent_to+infty by A1,A5,Def2;
A11: rng(seq^\k)c=dom f1/\dom f2 by A9,XBOOLE_1:19;
A12: rng seq c=dom(f1+f2) by A3,A7,XBOOLE_1:1;
now consider r1 be real number such that
A13: for g st g in ].x0-r,x0.[/\dom f2 holds r1<=f2.g by A2,RFUNCT_1:def 10;
take r2=r1-1; let n; k<=n+k by NAT_1:37;
then x0-r<seq.(n+k) by A4; then A14: x0-r<(seq^\k).n by SEQM_3:def 9;
A15: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
then (seq^\k).n in left_open_halfline(x0) by A8;
then (seq^\k).n in {g1: g1<x0} by PROB_1:def 15;
then ex g st g=(seq^\k).n & g<x0;
then (seq^\k).n in {g2: x0-r<g2 & g2<x0} by A14;
then (seq^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (seq^\k).n in ].x0-r,x0.[/\dom f2 by A9,A15,XBOOLE_0:def 3;
then r1<=f2.((seq^\k).n) by A13; then r1-1<f2.((seq^\k).n)-0
by REAL_1:92;
hence r2<(f2*(seq^\k)).n by A9,RFUNCT_2:21;
end; then f2*(seq^\k) is bounded_below by SEQ_2:def 4;
then A16: f1*(seq^\k)+f2*(seq^\k) is divergent_to+infty by A10,LIMFUNC1:36;
f1*(seq^\k)+f2*(seq^\k)=(f1+f2)*(seq^\k) by A11,RFUNCT_2:23
.=((f1+f2)*seq)^\k by A12,RFUNCT_2:22;
hence (f1+f2)*seq is divergent_to+infty by A16,LIMFUNC1:34;
end; hence thesis by A1,Def2;
end;
theorem
f1 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ ].x0-r,x0.[ holds r1<=
f2.g) implies
f1(#)f2 is_left_divergent_to+infty_in x0
proof assume A1: f1 is_left_divergent_to+infty_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2);
given r,t be Real such that
A2: 0<r & 0<t & for g st g in dom f2/\].x0-r,x0.[ holds t<=f2.g;
now let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
x0-r<x0 by A2,Lm1; then consider k such that
A4: for n st k<=n holds x0-r<seq.n by A3,Th1;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
rng(seq^\k)c=rng seq by RFUNCT_2:7;
then rng(seq^\k)c=dom(f1(#)f2)/\left_open_halfline(x0) by A3,XBOOLE_1:1;
then A6: rng(seq^\k)c=dom(f1(#)f2) & rng(seq^\k)c=left_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 &
rng(seq^\k)c=dom f1/\left_open_halfline(x0) by Lm2;
then A7: f1*(seq^\k) is divergent_to+infty by A1,A5,Def2;
A8: rng seq c=dom(f1(#)f2) by A3,Lm2;
now thus 0<t by A2; let n; k<=n+k by NAT_1:37;
then x0-r<seq.(n+k) by A4; then A9: x0-r<(seq^\k).n by SEQM_3:def 9;
A10: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
then (seq^\k).n in left_open_halfline(x0) by A6;
then (seq^\k).n in {g1: g1<x0} by PROB_1:def 15;
then ex g st g=(seq^\k).n & g<x0;
then (seq^\k).n in {g2: x0-r<g2 & g2<x0} by A9;
then (seq^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (seq^\k).n in dom f2/\].x0-r,x0.[ by A6,A10,XBOOLE_0:def 3;
then t<=f2.((seq^\k).n) by A2; hence t<=(f2*(seq^\k)).n by A6,RFUNCT_2:21;
end; then A11: (f1*(seq^\k))(#)(f2*(seq^\k)) is divergent_to+infty
by A7,LIMFUNC1:49;
(f1*(seq^\k))(#)(f2*(seq^\k))=(f1(#)f2)*(seq^\k) by A6,RFUNCT_2:23
.=((f1(#)f2)*seq)^\k by A8,RFUNCT_2:22;
hence (f1(#)f2)*seq is divergent_to+infty by A11,LIMFUNC1:34;
end; hence thesis by A1,Def2;
end;
theorem
f1 is_right_divergent_to+infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2)) &
(ex r st 0<r & f2 is_bounded_below_on ].x0,x0+r.[) implies
f1+f2 is_right_divergent_to+infty_in x0
proof assume A1: f1 is_right_divergent_to+infty_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2); given r such that
A2: 0<r & f2 is_bounded_below_on ].x0,x0+r.[;
now let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\right_open_halfline(x0);
x0<x0+r by A2,Lm1; then consider k such that
A4: for n st k<=n holds seq.n<x0+r by A3,Th2;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
rng(seq^\k)c=rng seq by RFUNCT_2:7;
then A6: rng(seq^\k)c=dom(f1+f2)/\right_open_halfline(x0) by A3,XBOOLE_1:1;
A7: dom(f1+f2)/\right_open_halfline(x0) c=dom(f1+f2) &
dom(f1+f2)/\
right_open_halfline(x0) c=right_open_halfline(x0) by XBOOLE_1:17;
then A8: rng(seq^\k)c=dom(f1+f2) & rng(seq^\k)c=right_open_halfline(x0)
by A6,XBOOLE_1:1;
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;
then A9: rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 by A8,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A8,XBOOLE_1:19;
then A10: f1*(seq^\k) is divergent_to+infty by A1,A5,Def5;
A11: rng(seq^\k)c=dom f1/\dom f2 by A9,XBOOLE_1:19;
A12: rng seq c=dom(f1+f2) by A3,A7,XBOOLE_1:1;
now consider r1 be real number such that
A13: for g st g in ].x0,x0+r.[/\dom f2 holds r1<=f2.g by A2,RFUNCT_1:def 10;
take r2=r1-1; let n; k<=n+k by NAT_1:37;
then seq.(n+k)<x0+r by A4; then A14: (seq^\k).n<x0+r by SEQM_3:def 9;
A15: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
then (seq^\k).n in right_open_halfline(x0) by A8;
then (seq^\k).n in {g1: x0<g1} by LIMFUNC1:def 3;
then ex g st g=(seq^\k).n & x0<g;
then (seq^\k).n in {g2: x0<g2 & g2<x0+r} by A14;
then (seq^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (seq^\k).n in ].x0,x0+r.[/\dom f2 by A9,A15,XBOOLE_0:def 3;
then r1<=f2.((seq^\k).n) by A13; then r1-1<f2.((seq^\k).n)-0
by REAL_1:92;
hence r2<(f2*(seq^\k)).n by A9,RFUNCT_2:21;
end; then f2*(seq^\k) is bounded_below by SEQ_2:def 4;
then A16: f1*(seq^\k)+f2*(seq^\k) is divergent_to+infty by A10,LIMFUNC1:36;
f1*(seq^\k)+f2*(seq^\k)=(f1+f2)*(seq^\k) by A11,RFUNCT_2:23
.=((f1+f2)*seq)^\k by A12,RFUNCT_2:22;
hence (f1+f2)*seq is divergent_to+infty by A16,LIMFUNC1:34;
end; hence thesis by A1,Def5;
end;
theorem
f1 is_right_divergent_to+infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) &
(ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ ].x0,x0+r.[ holds r1<=
f2.g) implies
f1(#)f2 is_right_divergent_to+infty_in x0
proof assume A1: f1 is_right_divergent_to+infty_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2);
given r,t be Real such that
A2: 0<r & 0<t & for g st g in dom f2/\].x0,x0+r.[ holds t<=f2.g;
now let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
x0<x0+r by A2,Lm1;
then consider k such that A4: for n st k<=n holds seq.n<x0+r by A3,Th2;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
rng(seq^\k)c=rng seq by RFUNCT_2:7;
then rng(seq^\k)c=dom(f1(#)f2)/\right_open_halfline(x0) by A3,XBOOLE_1:1;
then A6: rng(seq^\k)c=dom(f1(#)f2) & rng(seq^\k)c=right_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng(seq^\k)c=dom f1 & rng(seq^\k)c=dom f2 &
rng(seq^\k)c=dom f1/\right_open_halfline(x0) by Lm2;
then A7: f1*(seq^\k) is divergent_to+infty by A1,A5,Def5;
A8: rng seq c=dom(f1(#)f2) by A3,Lm2;
now thus 0<t by A2; let n; k<=n+k by NAT_1:37;
then seq.(n+k)<x0+r by A4; then A9: (seq^\k).n<x0+r by SEQM_3:def 9;
A10: (seq^\k).n in rng(seq^\k) by RFUNCT_2:10;
then (seq^\k).n in right_open_halfline(x0) by A6;
then (seq^\k).n in {g1: x0<g1} by LIMFUNC1:def 3;
then ex g st g=(seq^\k).n & x0<g;
then (seq^\k).n in {g2: x0<g2 & g2<x0+r} by A9;
then (seq^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (seq^\k).n in dom f2/\].x0,x0+r.[ by A6,A10,XBOOLE_0:def 3;
then t<=f2.((seq^\k).n) by A2; hence t<=(f2*(seq^\k)).n by A6,RFUNCT_2:21;
end; then A11: (f1*(seq^\k))(#)(f2*(seq^\k)) is divergent_to+infty
by A7,LIMFUNC1:49;
(f1*(seq^\k))(#)(f2*(seq^\k))=(f1(#)f2)*(seq^\k) by A6,RFUNCT_2:23
.=((f1(#)f2)*seq)^\k by A8,RFUNCT_2:22;
hence (f1(#)f2)*seq is divergent_to+infty by A11,LIMFUNC1:34;
end; hence thesis by A1,Def5;
end;
theorem
(f is_left_divergent_to+infty_in x0 & r>0 implies
r(#)f is_left_divergent_to+infty_in x0 ) &
(f is_left_divergent_to+infty_in x0 & r<0 implies
r(#)f is_left_divergent_to-infty_in x0 ) &
(f is_left_divergent_to-infty_in x0 & r>0 implies
r(#)f is_left_divergent_to-infty_in x0 ) &
(f is_left_divergent_to-infty_in x0 & r<0 implies
r(#)f is_left_divergent_to+infty_in x0 )
proof thus f is_left_divergent_to+infty_in x0 & r>0 implies
r(#)f is_left_divergent_to+infty_in x0
proof assume A1: f is_left_divergent_to+infty_in x0 & r>0;
thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
proof let r1; assume r1<x0; then consider g such that
A2: r1<g & g<x0 & g in dom f by A1,Def2; take g;
thus thesis by A2,SEQ_1:def 6;
end;
let seq; assume A3: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\left_open_halfline(x0);
then A4: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to+infty by A1,A3,Def2;
then A5: r(#)(f*seq) is divergent_to+infty by A1,LIMFUNC1:40;
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A4,XBOOLE_1:1; hence thesis by A5,RFUNCT_2:24;
end;
thus f is_left_divergent_to+infty_in x0 & r<0 implies
r(#)f is_left_divergent_to-infty_in x0
proof assume A6: f is_left_divergent_to+infty_in x0 & r<0;
thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
proof let r1; assume r1<x0; then consider g such that
A7: r1<g & g<x0 & g in dom f by A6,Def2; take g;
thus thesis by A7,SEQ_1:def 6;
end;
let seq; assume A8: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\left_open_halfline(x0);
then A9: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to+infty by A6,A8,Def2;
then A10: r(#)(f*seq) is divergent_to-infty by A6,LIMFUNC1:40;
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A9,XBOOLE_1:1; hence thesis by A10,RFUNCT_2:24;
end;
thus f is_left_divergent_to-infty_in x0 & r>0 implies
r(#)f is_left_divergent_to-infty_in x0
proof assume A11: f is_left_divergent_to-infty_in x0 & r>0;
thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
proof let r1; assume r1<x0; then consider g such that
A12: r1<g & g<x0 & g in dom f by A11,Def3; take g; thus thesis by A12,SEQ_1:
def 6;
end;
let seq; assume A13: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\left_open_halfline(x0);
then A14: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to-infty by A11,A13,Def3;
then A15: r(#)(f*seq) is divergent_to-infty by A11,LIMFUNC1:41;
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A14,XBOOLE_1:1; hence thesis by A15,RFUNCT_2:24;
end;
assume A16: f is_left_divergent_to-infty_in x0 & r<0;
thus for r1 st r1<x0 ex g st r1<g & g<x0 & g in dom(r(#)f)
proof let r1; assume r1<x0; then consider g such that
A17: r1<g & g<x0 & g in dom f by A16,Def3;
take g;thus thesis by A17,SEQ_1:def 6;
end;
let seq; assume A18: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\left_open_halfline(x0);
then A19: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to-infty by A16,A18,Def3;
then A20: r(#)(f*seq) is divergent_to+infty by A16,LIMFUNC1:41;
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A19,XBOOLE_1:1; hence thesis by A20,RFUNCT_2:24;
end;
theorem
(f is_right_divergent_to+infty_in x0 & r>0 implies
r(#)f is_right_divergent_to+infty_in x0 ) &
(f is_right_divergent_to+infty_in x0 & r<0 implies
r(#)f is_right_divergent_to-infty_in x0 ) &
(f is_right_divergent_to-infty_in x0 & r>0 implies
r(#)f is_right_divergent_to-infty_in x0 ) &
(f is_right_divergent_to-infty_in x0 & r<0 implies
r(#)f is_right_divergent_to+infty_in x0)
proof thus f is_right_divergent_to+infty_in x0 & r>0 implies
r(#)f is_right_divergent_to+infty_in x0
proof assume A1: f is_right_divergent_to+infty_in x0 & r>0;
thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
proof let r1; assume x0<r1; then consider g such that
A2: g<r1 & x0<g & g in dom f by A1,Def5;
take g; thus thesis by A2,SEQ_1:def 6;
end;
let seq; assume A3: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\right_open_halfline(x0);
then A4: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to+infty by A1,A3,Def5;
then A5: r(#)(f*seq) is divergent_to+infty by A1,LIMFUNC1:40;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A4,XBOOLE_1:1; hence thesis by A5,RFUNCT_2:24;
end;
thus f is_right_divergent_to+infty_in x0 & r<0 implies
r(#)f is_right_divergent_to-infty_in x0
proof assume A6: f is_right_divergent_to+infty_in x0 & r<0;
thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
proof let r1; assume x0<r1; then consider g such that
A7: g<r1 & x0<g & g in dom f by A6,Def5;
take g; thus thesis by A7,SEQ_1:def 6;
end;
let seq; assume A8: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\right_open_halfline(x0);
then A9: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to+infty by A6,A8,Def5;
then A10: r(#)(f*seq) is divergent_to-infty by A6,LIMFUNC1:40;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A9,XBOOLE_1:1; hence thesis by A10,RFUNCT_2:24;
end;
thus f is_right_divergent_to-infty_in x0 & r>0 implies
r(#)f is_right_divergent_to-infty_in x0
proof assume A11: f is_right_divergent_to-infty_in x0 & r>0;
thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
proof let r1; assume x0<r1; then consider g such that
A12: g<r1 & x0<g & g in dom f by A11,Def6; take g; thus thesis by A12,SEQ_1:
def 6;
end;
let seq; assume A13: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\right_open_halfline(x0);
then A14: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to-infty by A11,A13,Def6;
then A15: r(#)(f*seq) is divergent_to-infty by A11,LIMFUNC1:41;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A14,XBOOLE_1:1; hence thesis by A15,RFUNCT_2:24;
end;
assume A16: f is_right_divergent_to-infty_in x0 & r<0;
thus for r1 st x0<r1 ex g st g<r1 & x0<g & g in dom(r(#)f)
proof let r1; assume x0<r1; then consider g such that
A17: g<r1 & x0<g & g in dom f by A16,Def6;
take g; thus thesis by A17,SEQ_1:def 6;
end;
let seq; assume A18: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\right_open_halfline(x0);
then A19: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 6;
then f*seq is divergent_to-infty by A16,A18,Def6;
then A20: r(#)(f*seq) is divergent_to+infty by A16,LIMFUNC1:41;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A19,XBOOLE_1:1; hence thesis by A20,RFUNCT_2:24;
end;
theorem
(f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0)
implies abs(f) is_left_divergent_to+infty_in x0
proof assume A1: f is_left_divergent_to+infty_in x0 or
f is_left_divergent_to-infty_in x0;
now per cases by A1;
suppose A2: f is_left_divergent_to+infty_in x0;
A3: now let r; assume r<x0; then consider g such that
A4: r<g & g<x0 & g in dom f by A2,Def2; take g;
thus r<g & g<x0 & g in dom abs(f) by A4,SEQ_1:def 10;
end;
now let seq; assume A5: seq is convergent & lim seq=x0 &
rng seq c=dom abs(f)/\left_open_halfline(x0);
then A6: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 10;
then f*seq is divergent_to+infty by A2,A5,Def2;
then A7: abs(f*seq) is divergent_to+infty by LIMFUNC1:52;
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A6,XBOOLE_1:1;
hence abs(f)*seq is divergent_to+infty by A7,RFUNCT_2:25;
end; hence thesis by A3,Def2;
suppose A8: f is_left_divergent_to-infty_in x0;
A9: now let r; assume r<x0; then consider g such that
A10: r<g & g<x0 & g in dom f by A8,Def3; take g;
thus r<g & g<x0 & g in dom abs(f) by A10,SEQ_1:def 10;
end;
now let seq; assume A11: seq is convergent & lim seq=x0 &
rng seq c=dom abs(f)/\left_open_halfline(x0);
then A12: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 10;
then f*seq is divergent_to-infty by A8,A11,Def3;
then A13: abs(f*seq) is divergent_to+infty by LIMFUNC1:52;
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A12,XBOOLE_1:1;
hence abs(f)*seq is divergent_to+infty by A13,RFUNCT_2:25;
end; hence thesis by A9,Def2;
end; hence thesis;
end;
theorem
(f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0)
implies abs(f) is_right_divergent_to+infty_in x0
proof assume A1: f is_right_divergent_to+infty_in x0 or
f is_right_divergent_to-infty_in x0;
now per cases by A1;
suppose A2: f is_right_divergent_to+infty_in x0;
A3: now let r; assume x0<r; then consider g such that
A4: g<r & x0<g & g in dom f by A2,Def5; take g;
thus g<r & x0<g & g in dom abs(f) by A4,SEQ_1:def 10;
end;
now let seq; assume A5: seq is convergent & lim seq=x0 &
rng seq c=dom abs(f)/\right_open_halfline(x0);
then A6: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 10;
then f*seq is divergent_to+infty by A2,A5,Def5;
then A7: abs(f*seq) is divergent_to+infty by LIMFUNC1:52;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A6,XBOOLE_1:1;
hence abs(f)*seq is divergent_to+infty by A7,RFUNCT_2:25;
end; hence thesis by A3,Def5;
suppose A8: f is_right_divergent_to-infty_in x0;
A9: now let r; assume x0<r; then consider g such that
A10: g<r & x0<g & g in dom f by A8,Def6; take g;
thus g<r & x0<g & g in dom abs(f) by A10,SEQ_1:def 10;
end;
now let seq; assume A11: seq is convergent & lim seq=x0 &
rng seq c=dom abs(f)/\right_open_halfline(x0);
then A12: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 10;
then f*seq is divergent_to-infty by A8,A11,Def6;
then A13: abs(f*seq) is divergent_to+infty by LIMFUNC1:52;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A12,XBOOLE_1:1;
hence abs(f)*seq is divergent_to+infty by A13,RFUNCT_2:25;
end; hence thesis by A9,Def5;
end; hence thesis;
end;
theorem Th31:
(ex r st 0<r & f is_non_decreasing_on ].x0-r,x0.[ &
not f is_bounded_above_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to+infty_in x0
proof given r such that A1: 0<r & f is_non_decreasing_on ].x0-r,x0.[ &
not f is_bounded_above_on ].x0-r,x0.[;
assume for r st r<x0 ex g st r<g & g<x0 & g in dom f;
hence for r st r<x0 ex g st r<g & g<x0 & g in dom f;
let seq such that A2: seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0);
now let t be Real;
consider g1 such that A3: g1 in ].x0-r,x0.[/\dom f &
t<f.g1 by A1,RFUNCT_1:def 9;
g1 in ].x0-r,x0.[ by A3,XBOOLE_0:def 3
; then g1 in {r1: x0-r<r1 & r1<x0} by RCOMP_1:def 2;
then A4: ex r1 st r1=g1 & x0-r<r1 & r1<x0;
then consider n such that A5: for k st n<=k holds g1<seq.k by A2,Th1;
take n; let k; seq.k in rng seq by RFUNCT_2:10;
then A6: seq.k in dom f/\left_open_halfline(x0) by A2; assume n<=k;
then A7: g1<seq.k by A5; then A8: x0-r<seq.k by A4,AXIOMS:22;
A9: dom f/\left_open_halfline(x0)c=dom f &
dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then seq.k in dom f & seq.k in left_open_halfline(x0) by A6;
then seq.k in {r2: r2<x0} by PROB_1:def 15; then ex r2 st r2=seq.k & r2<x0;
then seq.k in {g2: x0-r<g2 & g2<x0} by A8;
then seq.k in ].x0-r,x0.[ by RCOMP_1:def 2
; then seq.k in ].x0-r,x0.[/\dom f by A6,A9,XBOOLE_0:def 3;
then f.g1<=f.(seq.k) by A1,A3,A7,RFUNCT_2:def 4;
then A10: t<f.(seq.k) by A3,AXIOMS:22; rng seq c=dom f by A2,A9,XBOOLE_1:1;
hence t<(f*seq).k by A10,RFUNCT_2:21;
end; hence thesis by LIMFUNC1:def 4;
end;
theorem
(ex r st 0<r & f is_increasing_on ].x0-r,x0.[ &
not f is_bounded_above_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to+infty_in x0
proof given r such that A1: 0<r & f is_increasing_on ].x0-r,x0.[ &
not f is_bounded_above_on ].x0-r,x0.[;
assume A2: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
f is_non_decreasing_on ].x0-r,x0.[ by A1,RFUNCT_2:55; hence thesis by A1,A2,
Th31
;
end;
theorem Th33:
(ex r st 0<r & f is_non_increasing_on ].x0-r,x0.[ &
not f is_bounded_below_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to-infty_in x0
proof given r such that A1: 0<r & f is_non_increasing_on ].x0-r,x0.[ &
not f is_bounded_below_on ].x0-r,x0.[;
assume for r st r<x0 ex g st r<g & g<x0 & g in dom f;
hence for r st r<x0 ex g st r<g & g<x0 & g in dom f;
let seq such that A2: seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0);
now let t be Real;
consider g1 such that A3: g1 in ].x0-r,x0.[/\dom f &
f.g1<t by A1,RFUNCT_1:def 10
;
g1 in ].x0-r,x0.[ by A3,XBOOLE_0:def 3
; then g1 in {r1: x0-r<r1 & r1<x0} by RCOMP_1:def 2;
then A4: ex r1 st r1=g1 & x0-r<r1 & r1<x0;
then consider n such that A5: for k st n<=k holds g1<seq.k by A2,Th1;
take n; let k; seq.k in rng seq by RFUNCT_2:10;
then A6: seq.k in dom f/\left_open_halfline(x0) by A2; assume n<=k;
then A7: g1<seq.k by A5; then A8: x0-r<seq.k by A4,AXIOMS:22;
A9: dom f/\left_open_halfline(x0)c=dom f &
dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then seq.k in dom f & seq.k in left_open_halfline(x0) by A6;
then seq.k in {r2: r2<x0} by PROB_1:def 15; then ex r2 st r2=seq.k & r2<x0;
then seq.k in {g2: x0-r<g2 & g2<x0} by A8;
then seq.k in ].x0-r,x0.[ by RCOMP_1:def 2
; then seq.k in ].x0-r,x0.[/\dom f by A6,A9,XBOOLE_0:def 3;
then f.(seq.k)<=f.g1 by A1,A3,A7,RFUNCT_2:def 5;
then A10: f.(seq.k)<t by A3,AXIOMS:22; rng seq c=dom f by A2,A9,XBOOLE_1:1;
hence (f*seq).k<t by A10,RFUNCT_2:21;
end; hence thesis by LIMFUNC1:def 5;
end;
theorem
(ex r st 0<r & f is_decreasing_on ].x0-r,x0.[ &
not f is_bounded_below_on ].x0-r,x0.[) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f) implies
f is_left_divergent_to-infty_in x0
proof given r such that A1: 0<r & f is_decreasing_on ].x0-r,x0.[ &
not f is_bounded_below_on ].x0-r,x0.[;
assume A2: for r st r<x0 ex g st r<g & g<x0 & g in dom f;
f is_non_increasing_on ].x0-r,x0.[ by A1,RFUNCT_2:56; hence thesis by A1,A2,
Th33
;
end;
theorem Th35:
(ex r st 0<r & f is_non_increasing_on ].x0,x0+r.[ &
not f is_bounded_above_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to+infty_in x0
proof given r such that A1: 0<r & f is_non_increasing_on ].x0,x0+r.[ &
not f is_bounded_above_on ].x0,x0+r.[;
assume for r st x0<r ex g st g<r & x0<g & g in dom f;
hence for r st x0<r ex g st g<r & x0<g & g in dom f;
let seq such that A2: seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0);
now let t be Real; consider g1 such that
A3: g1 in ].x0,x0+r.[/\dom f & t<f.g1 by A1,RFUNCT_1:def 9;
g1 in ].x0,x0+r.[ by A3,XBOOLE_0:def 3
; then g1 in {r1: x0<r1 & r1<x0+r} by RCOMP_1:def 2;
then A4: ex r1 st r1=g1 & x0<r1 & r1<x0+r;
then consider n such that A5: for k st n<=k holds seq.k<g1 by A2,Th2;
take n; let k; seq.k in rng seq by RFUNCT_2:10;
then A6: seq.k in dom f/\right_open_halfline(x0) by A2; assume n<=k;
then A7: seq.k<g1 by A5; then A8: seq.k<x0+r by A4,AXIOMS:22;
A9: dom f/\right_open_halfline(x0)c=dom f &
dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then seq.k in dom f & seq.k in right_open_halfline(x0) by A6;
then seq.k in {r2: x0<r2} by LIMFUNC1:def 3; then ex r2 st r2=seq.k & x0<r2
;
then seq.k in {g2: x0<g2 & g2<x0+r} by A8;
then seq.k in ].x0,x0+r.[ by RCOMP_1:def 2
; then seq.k in ].x0,x0+r.[/\dom f by A6,A9,XBOOLE_0:def 3;
then f.g1<=f.(seq.k) by A1,A3,A7,RFUNCT_2:def 5;
then A10: t<f.(seq.k) by A3,AXIOMS:22; rng seq c=dom f by A2,A9,XBOOLE_1:1;
hence t<(f*seq).k by A10,RFUNCT_2:21;
end; hence thesis by LIMFUNC1:def 4;
end;
theorem
(ex r st 0<r & f is_decreasing_on ].x0,x0+r.[ &
not f is_bounded_above_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to+infty_in x0
proof given r such that A1: 0<r & f is_decreasing_on ].x0,x0+r.[ &
not f is_bounded_above_on ].x0,x0+r.[;
assume A2: for r st x0<r ex g st g<r & x0<g & g in dom f;
f is_non_increasing_on ].x0,x0+r.[ by A1,RFUNCT_2:56; hence thesis by A1,A2,
Th35
;
end;
theorem Th37:
(ex r st 0<r & f is_non_decreasing_on ].x0,x0+r.[ &
not f is_bounded_below_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to-infty_in x0
proof given r such that A1: 0<r & f is_non_decreasing_on ].x0,x0+r.[ &
not f is_bounded_below_on ].x0,x0+r.[;
assume for r st x0<r ex g st g<r & x0<g & g in dom f;
hence for r st x0<r ex g st g<r & x0<g & g in dom f;
let seq such that A2: seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0);
now let t be Real; consider g1 such that
A3: g1 in ].x0,x0+r.[/\dom f & f.g1<t by A1,RFUNCT_1:def 10;
g1 in ].x0,x0+r.[ by A3,XBOOLE_0:def 3
; then g1 in {r1: x0<r1 & r1<x0+r} by RCOMP_1:def 2;
then A4: ex r1 st r1=g1 & x0<r1 & r1<x0+r;
then consider n such that A5: for k st n<=k holds seq.k<g1 by A2,Th2;
take n; let k; seq.k in rng seq by RFUNCT_2:10;
then A6: seq.k in dom f/\right_open_halfline(x0) by A2; assume n<=k;
then A7: seq.k<g1 by A5; then A8: seq.k<x0+r by A4,AXIOMS:22;
A9: dom f/\right_open_halfline(x0)c=dom f &
dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then seq.k in dom f & seq.k in right_open_halfline(x0) by A6;
then seq.k in {r2: x0<r2} by LIMFUNC1:def 3; then ex r2 st r2=seq.k & x0<r2
;
then seq.k in {g2: x0<g2 & g2<x0+r} by A8;
then seq.k in ].x0,x0+r.[ by RCOMP_1:def 2
; then seq.k in ].x0,x0+r.[/\dom f by A6,A9,XBOOLE_0:def 3;
then f.(seq.k)<=f.g1 by A1,A3,A7,RFUNCT_2:def 4;
then A10: f.(seq.k)<t by A3,AXIOMS:22; rng seq c=dom f by A2,A9,XBOOLE_1:1;
hence (f*seq).k<t by A10,RFUNCT_2:21;
end; hence thesis by LIMFUNC1:def 5;
end;
theorem
(ex r st 0<r & f is_increasing_on ].x0,x0+r.[ &
not f is_bounded_below_on ].x0,x0+r.[) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) implies
f is_right_divergent_to-infty_in x0
proof given r such that A1: 0<r & f is_increasing_on ].x0,x0+r.[ &
not f is_bounded_below_on ].x0,x0+r.[;
assume A2: for r st x0<r ex g st g<r & x0<g & g in dom f;
f is_non_decreasing_on ].x0,x0+r.[ by A1,RFUNCT_2:55; hence thesis by A1,A2,
Th37
;
end;
theorem Th39:
f1 is_left_divergent_to+infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f)
& (ex r st 0<r & dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
for g st g in dom f /\ ].x0-r,x0.[ holds f1.g<=f.g) implies
f is_left_divergent_to+infty_in x0
proof assume A1: f1 is_left_divergent_to+infty_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom f;
given r such that A2: 0<r & dom f/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ &
for g st g in dom f/\].x0-r,x0.[ holds f1.g<=f.g;
thus for r st r<x0 ex g st r<g & g<x0 & g in dom f by A1;
let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0);
x0-r<x0 by A2,Lm1; then consider k such that
A4: for n st k<=n holds x0-r<seq.n by A3,Th1;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
dom f/\left_open_halfline(x0)c=dom f &
dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A6: rng seq c=dom f & rng seq c=left_open_halfline(x0) by A3,XBOOLE_1:1;
rng(seq^\k)c= rng seq by RFUNCT_2:7;
then A7: rng(seq^\k)c=dom f & rng(seq^\k)c=left_open_halfline(x0) by A6,
XBOOLE_1:1;
now let x be set; assume A8: x in rng(seq^\k); then consider n such that
A9: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then x0-r<seq.(n+k) by A4; then A10: x0-r<(seq^\k).n by SEQM_3:def 9;
(seq^\k).n in left_open_halfline(x0) by A7,A8,A9;
then (seq^\k).n in {g: g<x0} by PROB_1:def 15;
then ex r1 st r1=(seq^\k).n & r1<x0;
then x in {g1: x0-r<g1 & g1<x0} by A9,A10;
hence x in ].x0-r,x0.[ by RCOMP_1:def 2;
end; then rng(seq^\k)c=].x0-r,x0.[ by TARSKI:def 3;
then A11: rng(seq^\k)c=dom f/\].x0-r,x0.[ by A7,XBOOLE_1:19;
then A12: rng(seq^\k)c=dom f1/\].x0-r,x0.[ by A2,XBOOLE_1:1;
dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
then A13: rng(seq^\k)c=dom f1 by A12,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A7,XBOOLE_1:19;
then A14: f1*(seq^\k) is divergent_to+infty by A1,A5,Def2;
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,A11;
then (f1*(seq^\k)).n<=f.((seq^\k).n) by A13,RFUNCT_2:21;
hence (f1*(seq^\k)).n<=(f*(seq^\k)).n by A7,RFUNCT_2:21;
end; then f*(seq^\k) is divergent_to+infty by A14,LIMFUNC1:69;
then (f*seq)^\k is divergent_to+infty by A6,RFUNCT_2:22;
hence thesis by LIMFUNC1:34;
end;
theorem Th40:
f1 is_left_divergent_to-infty_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f)
& (ex r st 0<r & dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
for g st g in dom f /\ ].x0-r,x0.[ holds f.g<=f1.g) implies
f is_left_divergent_to-infty_in x0
proof assume A1: f1 is_left_divergent_to-infty_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom f;
given r such that A2: 0<r & dom f/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ &
for g st g in dom f/\].x0-r,x0.[ holds f.g<=f1.g;
thus for r st r<x0 ex g st r<g & g<x0 & g in dom f by A1;
let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0);
x0-r<x0 by A2,Lm1; then consider k such that
A4: for n st k<=n holds x0-r<seq.n by A3,Th1;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
dom f/\left_open_halfline(x0)c=dom f &
dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A6: rng seq c=dom f & rng seq c=left_open_halfline(x0) by A3,XBOOLE_1:1;
rng(seq^\k)c= rng seq by RFUNCT_2:7;
then A7: rng(seq^\k)c=dom f & rng(seq^\k)c=left_open_halfline(x0) by A6,
XBOOLE_1:1;
now let x be set; assume A8: x in rng(seq^\k); then consider n such that
A9: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then x0-r<seq.(n+k) by A4; then A10: x0-r<(seq^\k).n by SEQM_3:def 9;
(seq^\k).n in left_open_halfline(x0) by A7,A8,A9;
then (seq^\k).n in {g: g<x0} by PROB_1:def 15;
then ex r1 st r1=(seq^\k).n & r1<x0;
then x in {g1: x0-r<g1 & g1<x0} by A9,A10;
hence x in ].x0-r,x0.[ by RCOMP_1:def 2;
end; then rng(seq^\k)c=].x0-r,x0.[ by TARSKI:def 3;
then A11: rng(seq^\k)c=dom f/\].x0-r,x0.[ by A7,XBOOLE_1:19;
then A12: rng(seq^\k)c=dom f1/\].x0-r,x0.[ by A2,XBOOLE_1:1;
dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
then A13: rng(seq^\k)c=dom f1 by A12,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A7,XBOOLE_1:19;
then A14: f1*(seq^\k) is divergent_to-infty by A1,A5,Def3;
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,A11;
then (f*(seq^\k)).n<=f1.((seq^\k).n) by A7,RFUNCT_2:21;
hence (f*(seq^\k)).n<=(f1*(seq^\k)).n by A13,RFUNCT_2:21;
end; then f*(seq^\k) is divergent_to-infty by A14,LIMFUNC1:70;
then (f*seq)^\k is divergent_to-infty by A6,RFUNCT_2:22;
hence thesis by LIMFUNC1:34;
end;
theorem Th41:
f1 is_right_divergent_to+infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
(ex r st 0<r & dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
for g st g in dom f /\ ].x0,x0+r.[ holds f1.g<=f.g) implies
f is_right_divergent_to+infty_in x0
proof assume A1: f1 is_right_divergent_to+infty_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom f;
given r such that A2: 0<r & dom f/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ &
for g st g in dom f/\].x0,x0+r.[ holds f1.g<=f.g;
thus for r st x0<r ex g st g<r & x0<g & g in dom f by A1;
let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0);
x0<x0+r by A2,Lm1; then consider k such that
A4: for n st k<=n holds seq.n<x0+r by A3,Th2;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
dom f/\right_open_halfline(x0)c=dom f &
dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A6: rng seq c=dom f & rng seq c=right_open_halfline(x0) by A3,XBOOLE_1:1;
rng(seq^\k)c= rng seq by RFUNCT_2:7;
then A7: rng(seq^\k)c=dom f & rng(seq^\k)c=right_open_halfline(x0) by A6,
XBOOLE_1:1
;
now let x be set; assume A8: x in rng(seq^\k); then consider n such that
A9: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then seq.(n+k)<x0+r by A4; then A10: (seq^\k).n<x0+r by SEQM_3:def 9;
(seq^\k).n in right_open_halfline(x0) by A7,A8,A9;
then (seq^\k).n in {g: x0<g} by LIMFUNC1:def 3;
then ex r1 st r1=(seq^\k).n & x0<r1;
then x in {g1: x0<g1 & g1<x0+r} by A9,A10;
hence x in ].x0,x0+r.[ by RCOMP_1:def 2;
end; then rng(seq^\k)c=].x0,x0+r.[ by TARSKI:def 3;
then A11: rng(seq^\k)c=dom f/\].x0,x0+r.[ by A7,XBOOLE_1:19;
then A12: rng(seq^\k)c=dom f1/\].x0,x0+r.[ by A2,XBOOLE_1:1;
dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
then A13: rng(seq^\k)c=dom f1 by A12,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A7,XBOOLE_1:19;
then A14: f1*(seq^\k) is divergent_to+infty by A1,A5,Def5;
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,A11;
then (f1*(seq^\k)).n<=f.((seq^\k).n) by A13,RFUNCT_2:21;
hence (f1*(seq^\k)).n<=(f*(seq^\k)).n by A7,RFUNCT_2:21;
end; then f*(seq^\k) is divergent_to+infty by A14,LIMFUNC1:69;
then (f*seq)^\k is divergent_to+infty by A6,RFUNCT_2:22;
hence thesis by LIMFUNC1:34;
end;
theorem Th42:
f1 is_right_divergent_to-infty_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
(ex r st 0<r & dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
for g st g in dom f /\ ].x0,x0+r.[ holds f.g<=f1.g) implies
f is_right_divergent_to-infty_in x0
proof assume A1: f1 is_right_divergent_to-infty_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom f;
given r such that A2: 0<r & dom f/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ &
for g st g in dom f/\].x0,x0+r.[ holds f.g<=f1.g;
thus for r st x0<r ex g st g<r & x0<g & g in dom f by A1;
let seq such that A3: seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0);
x0<x0+r by A2,Lm1; then consider k such that
A4: for n st k<=n holds seq.n<x0+r by A3,Th2;
A5: seq^\k is convergent & lim(seq^\k)=x0 by A3,SEQ_4:33;
dom f/\right_open_halfline(x0)c=dom f &
dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A6: rng seq c=dom f & rng seq c=right_open_halfline(x0) by A3,XBOOLE_1:1;
rng(seq^\k)c= rng seq by RFUNCT_2:7;
then A7: rng(seq^\k)c=dom f & rng(seq^\k)c=right_open_halfline(x0) by A6,
XBOOLE_1:1
;
now let x be set; assume A8: x in rng(seq^\k); then consider n such that
A9: (seq^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then seq.(n+k)<x0+r by A4; then A10: (seq^\k).n<x0+r by SEQM_3:def 9;
(seq^\k).n in right_open_halfline(x0) by A7,A8,A9;
then (seq^\k).n in {g: x0<g} by LIMFUNC1:def 3;
then ex r1 st r1=(seq^\k).n & x0<r1;
then x in {g1: x0<g1 & g1<x0+r} by A9,A10;
hence x in ].x0,x0+r.[ by RCOMP_1:def 2;
end; then rng(seq^\k)c=].x0,x0+r.[ by TARSKI:def 3;
then A11: rng(seq^\k)c=dom f/\].x0,x0+r.[ by A7,XBOOLE_1:19;
then A12: rng(seq^\k)c=dom f1/\].x0,x0+r.[ by A2,XBOOLE_1:1;
dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
then A13: rng(seq^\k)c=dom f1 by A12,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A7,XBOOLE_1:19;
then A14: f1*(seq^\k) is divergent_to-infty by A1,A5,Def6;
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,A11;
then (f*(seq^\k)).n<=f1.((seq^\k).n) by A7,RFUNCT_2:21;
hence (f*(seq^\k)).n<=(f1*(seq^\k)).n by A13,RFUNCT_2:21;
end; then f*(seq^\k) is divergent_to-infty by A14,LIMFUNC1:70;
then (f*seq)^\k is divergent_to-infty by A6,RFUNCT_2:22;
hence thesis by LIMFUNC1:34;
end;
theorem
f1 is_left_divergent_to+infty_in x0 & (ex r st 0<r &
].x0-r,x0.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ holds f1.g<=
f.g) implies
f is_left_divergent_to+infty_in x0
proof assume A1: f1 is_left_divergent_to+infty_in x0;
given r such that A2: 0<r & ].x0-r,x0.[ c=dom f/\dom f1 &
for g st g in ].x0-r,x0.[ holds f1.g<=f.g;
dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
then A3: ].x0-r,x0.[c=dom f & ].x0-r,x0.[c=dom f1 by A2,XBOOLE_1:1;
then A4: ].x0-r,x0.[=dom f/\].x0-r,x0.[ & ].x0-r,x0.[=dom f1/\].x0-r,x0.[ by
XBOOLE_1:28;
for r st r<x0 ex g st r<g & g<x0 & g in dom f by A2,A3,Th3;
hence thesis by A1,A2,A4,Th39;
end;
theorem
f1 is_left_divergent_to-infty_in x0 & (ex r st 0<r &
].x0-r,x0.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ holds f.g<=
f1.g) implies
f is_left_divergent_to-infty_in x0
proof assume A1: f1 is_left_divergent_to-infty_in x0;
given r such that A2: 0<r & ].x0-r,x0.[c=dom f/\dom f1 &
for g st g in ].x0-r,x0.[ holds f.g<=f1.g;
dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
then A3: ].x0-r,x0.[c=dom f & ].x0-r,x0.[c=dom f1 by A2,XBOOLE_1:1;
then A4: ].x0-r,x0.[=dom f/\].x0-r,x0.[ & ].x0-r,x0.[=dom f1/\].x0-r,x0.[ by
XBOOLE_1:28;
for r st r<x0 ex g st r<g & g<x0 & g in dom f by A2,A3,Th3;
hence thesis by A1,A2,A4,Th40;
end;
theorem
f1 is_right_divergent_to+infty_in x0 & (ex r st 0<r &
].x0,x0+r.[ c= dom f /\ dom f1 & for g st g in ].x0,x0+r.[ holds f1.g<=
f.g) implies
f is_right_divergent_to+infty_in x0
proof assume A1: f1 is_right_divergent_to+infty_in x0;
given r such that A2: 0<r & ].x0,x0+r.[c=dom f/\dom f1 &
for g st g in ].x0,x0+r.[ holds f1.g<=f.g;
dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
then A3: ].x0,x0+r.[c=dom f & ].x0,x0+r.[c=dom f1 by A2,XBOOLE_1:1;
then A4: ].x0,x0+r.[=dom f/\].x0,x0+r.[ & ].x0,x0+r.[=dom f1/\].x0,x0+r.[ by
XBOOLE_1:28;
for r st x0<r ex g st g<r & x0<g & g in dom f by A2,A3,Th4;
hence thesis by A1,A2,A4,Th41;
end;
theorem
f1 is_right_divergent_to-infty_in x0 & (ex r st 0<r &
].x0,x0+r.[ c= dom f /\ dom f1 & for g st g in ].x0,x0+r.[ holds f.g<=
f1.g) implies
f is_right_divergent_to-infty_in x0
proof assume A1: f1 is_right_divergent_to-infty_in x0;
given r such that A2: 0<r & ].x0,x0+r.[c=dom f/\dom f1 &
for g st g in ].x0,x0+r.[ holds f.g<=f1.g;
dom f/\dom f1 c=dom f & dom f/\dom f1 c=dom f1 by XBOOLE_1:17;
then A3: ].x0,x0+r.[c=dom f & ].x0,x0+r.[c=dom f1 by A2,XBOOLE_1:1;
then A4: ].x0,x0+r.[=dom f/\].x0,x0+r.[ & ].x0,x0+r.[=dom f1/\].x0,x0+r.[ by
XBOOLE_1:28;
for r st x0<r ex g st g<r & x0<g & g in dom f by A2,A3,Th4;
hence thesis by A1,A2,A4,Th42;
end;
definition let f,x0;
assume A1: f is_left_convergent_in x0;
func lim_left(f,x0)->Real means :Def7:
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ left_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=it;
existence by A1,Def1;
uniqueness
proof
defpred X[Nat,real number] means
x0-1/($1+1)<$2 & $2<x0 & $2 in dom f;
A2: now let n; x0-1/(n+1)<x0 by Lm3; then consider g such that
A3: x0-1/(n+1)<g & g<x0 & g in dom f by A1,Def1;
reconsider g as real number;
take g;
thus X[n,g] by A3;
end;
consider s be Real_Sequence such that
A4: for n holds X[n,s.n] from RealSeqChoice(A2);
A5: s is convergent & lim s=x0 &
rng s c=dom f/\left_open_halfline(x0) by A4,Th5; let g1,g2 such that
A6: for seq st seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g1 and
A7: for seq st seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g2;
lim(f*s)=g1 by A5,A6; hence thesis by A5,A7;
end;
end;
definition let f,x0;
assume A1: f is_right_convergent_in x0;
func lim_right(f,x0)->Real means :Def8:
for seq st seq is convergent & lim seq=x0 &
rng seq c= dom f /\ right_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=it;
existence by A1,Def4;
uniqueness
proof
defpred X[Nat,real number] means
x0<$2 & $2<x0+1/($1+1) & $2 in dom f;
A2: now let n; x0<x0+1/(n+1) by Lm3; then consider g such that
A3: g<x0+(1/(n+1)) & x0<g & g in dom f by A1,Def4;
reconsider g as real number;
take g;
thus X[n,g] by A3;
end;
consider s be Real_Sequence such that
A4: for n holds X[n,s.n] from RealSeqChoice(A2);
A5: s is convergent & lim s=x0 &
rng s c=dom f/\right_open_halfline(x0) by A4,Th6; let g1,g2 such that
A6: for seq st seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g1 and
A7: for seq st seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0) holds f*seq is convergent &
lim(f*seq)=g2;
lim(f*s)=g1 by A5,A6; hence thesis by A5,A7;
end;
end;
canceled 2;
theorem
f is_left_convergent_in x0 implies
(lim_left(f,x0)=g iff for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds abs(f.r1-g)<g1)
proof assume A1: f is_left_convergent_in x0;
thus lim_left(f,x0)=g implies for g1 st 0<g1
ex r st r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds abs(f.r1-g)<g1
proof assume that A2: lim_left(f,x0)=g and
A3: ex g1 st 0<g1 & for r st r<x0 ex r1 st r<r1 & r1<x0 & r1 in dom f &
abs(f.r1-g)>=g1;
consider g1 such that A4: 0<g1 & for r st r<x0
ex r1 st r<r1 & r1<x0 & r1 in dom f & abs(f.r1-g)>=g1 by A3;
defpred X[Nat,real number] means
x0-1/($1+1)<$2 & $2<x0 & $2 in dom f & abs(f.($2)-g)>=g1;
A5: now let n; x0-1/(n+1)<x0 by Lm3; then consider g2 such that
A6: x0-1/(n+1)<g2 & g2<x0 & g2 in dom f & abs(f.g2-g)>=g1 by A4;
reconsider g2 as real number;
take g2;
thus X[n,g2] by A6;
end; consider s be Real_Sequence such that
A7: for n holds X[n,s.n]
from RealSeqChoice(A5);
A8: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\left_open_halfline(x0) by A7,Th5;
then f*s is convergent & lim(f*s)=g by A1,A2,Def7; then consider n such that
A9: for k st n<=k holds abs((f*s).k-g)<g1 by A4,SEQ_2:def 7;
abs((f*s).n-g)<g1 by A9;
then abs(f.(s.n)-g)<g1 by A8,RFUNCT_2:21; hence contradiction by A7;
end;
assume A10: for g1 st 0<g1 ex r st r<x0 &
for r1 st r<r1 & r1<x0 & r1 in dom f holds abs(f.r1-g)<g1;
now let s be Real_Sequence such that
A11: s is convergent & lim s=x0 & rng s c=dom f/\left_open_halfline(x0);
dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
A13: now let g1 be real number;
A14: g1 is Real by XREAL_0:def 1;
assume 0<g1; then consider r such that
A15: r<x0 & for r1 st r<r1 & r1<x0 & r1 in dom f holds
abs(f.r1-g)<g1 by A10,A14;
consider n such that A16: for k st n<=k holds r<s.k by A11,A15,Th1;
take n; let k; assume n<=k; then A17: r<s.k by A16
; s.k in rng s by RFUNCT_2:10;
then A18: s.k in left_open_halfline(x0) & s.k in dom f by A11,XBOOLE_0:def 3
;
then s.k in {g2: g2<x0} by PROB_1:def 15; then ex g2 st g2=s.k & g2<x0;
then abs(f.(s.k)-g)<g1 by A15,A17,A18; hence abs((f*s).k-g)<g1 by A12,
RFUNCT_2:21;
end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A13,SEQ_2:
def 7;
end; hence thesis by A1,Def7;
end;
theorem
f is_right_convergent_in x0 implies
(lim_right(f,x0)=g iff for g1 st 0<g1 ex r st x0<r &
for r1 st r1<r & x0<r1 & r1 in dom f holds abs(f.r1-g)<g1)
proof assume A1: f is_right_convergent_in x0;
thus lim_right(f,x0)=g implies for g1 st 0<g1
ex r st x0<r & for r1 st r1<r & x0<r1 & r1 in dom f holds abs(f.r1-g)<g1
proof assume that A2: lim_right(f,x0)=g and
A3: ex g1 st 0<g1 & for r st x0<r ex r1 st r1<r & x0<r1 & r1 in dom f &
abs(f.r1-g)>=g1;
consider g1 such that A4: 0<g1 & for r st x0<r
ex r1 st r1<r & x0<r1 & r1 in dom f & abs(f.r1-g)>=g1 by A3;
defpred X[Nat,real number] means
x0<$2 & $2<x0+1/($1+1) & $2 in dom f & g1<=abs(f.($2)-g);
A5: now let n; x0<x0+1/(n+1) by Lm3; then consider r1 such that
A6: r1<x0+(1/(n+1)) & x0<r1 & r1 in dom f & g1<=abs(f.r1-g) by A4;
reconsider r1 as real number;
take r1;
thus X[n,r1] by A6;
end; consider s be Real_Sequence such that
A7: for n holds X[n,s.n]
from RealSeqChoice(A5);
A8: s is convergent & lim s=x0 & rng s c=dom f &
rng s c=dom f/\right_open_halfline(x0) by A7,Th6;
then f*s is convergent & lim(f*s)=g by A1,A2,Def8; then consider n such that
A9: for k st n<=k holds abs((f*s).k-g)<g1 by A4,SEQ_2:def 7;
abs((f*s).n-g)<g1 by A9;
then abs(f.(s.n)-g)<g1 by A8,RFUNCT_2:21; hence contradiction by A7;
end;
assume A10: for g1 st 0<g1 ex r st x0<r &
for r1 st r1<r & x0<r1 & r1 in dom f holds abs(f.r1-g)<g1;
now let s be Real_Sequence such that
A11: s is convergent & lim s=x0 & rng s c=dom f/\right_open_halfline(x0);
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
A13: now let g1 be real number;
A14: g1 is Real by XREAL_0:def 1;
assume 0<g1; then consider r such that
A15: x0<r & for r1 st r1<r & x0<r1 &
r1 in dom f holds abs(f.r1-g)<g1 by A10,A14
;
consider n such that A16: for k st n<=k holds s.k<r by A11,A15,Th2;
take n; let k; assume n<=k; then A17: s.k<r by A16
; s.k in rng s by RFUNCT_2:10;
then A18: s.k in right_open_halfline(x0) & s.k in dom f by A11,XBOOLE_0:def
3
;
then s.k in {g2: x0<g2} by LIMFUNC1:def 3; then ex g2 st g2=s.k & x0<g2;
then abs(f.(s.k)-g)<g1 by A15,A17,A18; hence abs((f*s).k-g)<g1 by A12,
RFUNCT_2:21;
end; hence f*s is convergent by SEQ_2:def 6; hence lim(f*s)=g by A13,SEQ_2:
def 7;
end; hence thesis by A1,Def8;
end;
theorem Th51:
f is_left_convergent_in x0 implies r(#)f is_left_convergent_in x0 &
lim_left(r(#)f,x0)=r*(lim_left(f,x0))
proof assume A1: f is_left_convergent_in x0;
A2: now let r1; assume r1<x0; then consider g such that
A3: r1<g & g<x0 & g in dom f by A1,Def1; take g;
thus r1<g & g<x0 & g in dom(r(#)f) by A3,SEQ_1:def 6;
end;
A4: now let seq; A5: lim_left(f,x0)=lim_left(f,x0);
assume A6: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\left_open_halfline(x0);
then A7: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 6;
then A8: f*seq is convergent & lim(f*seq)=lim_left(f,x0) by A1,A5,A6,Def7;
then A9: r(#)(f*seq) is convergent by SEQ_2:21;
dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
then A10:
rng seq c=dom f by A7,XBOOLE_1:1; then A11: r(#)(f*seq)=(r(#)
f)*seq by RFUNCT_2:24;
thus (r(#)f)*seq is convergent by A9,A10,RFUNCT_2:24;
thus lim((r(#)f)*seq)=r*(lim_left(f,x0)) by A8,A11,SEQ_2:22;
end; hence r(#)f is_left_convergent_in x0 by A2,Def1; hence thesis by A4,Def7;
end;
theorem Th52:
f is_left_convergent_in x0 implies -f is_left_convergent_in x0 &
lim_left(-f,x0)=-(lim_left(f,x0))
proof assume A1: f is_left_convergent_in x0; A2: (-1)(#)f=-f by RFUNCT_1:38;
hence -f is_left_convergent_in x0 by A1,Th51;
thus lim_left(-f,x0)=(-1)*(lim_left(f,x0)) by A1,A2,Th51
.=-(1*(lim_left(f,x0))) by XCMPLX_1:175
.=-(lim_left(f,x0));
end;
theorem Th53:
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2)) implies
f1+f2 is_left_convergent_in x0 &
lim_left(f1+f2,x0)=lim_left(f1,x0)+lim_left(f2,x0)
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom(f1+f2);
A2: now A3: lim_left(f1,x0)=lim_left(f1,x0) & lim_left(f2,x0)=lim_left(f2,x0);
let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\left_open_halfline(x0);
then A5: rng seq c=dom(f1+f2) & rng seq c=left_open_halfline(x0) &
dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\left_open_halfline(x0) &
rng seq c=dom f2/\left_open_halfline(x0) by Lm4;
then A6: f1*seq is convergent & lim(f1*seq)=lim_left(f1,x0) by A1,A3,A4,Def7;
A7: f2*seq is convergent & lim(f2*seq)=lim_left(f2,x0) by A1,A3,A4,A5,Def7;
A8: f1*seq+f2*seq=(f1+f2)*seq by A5,RFUNCT_2:23;
hence (f1+f2)*seq is convergent by A6,A7,SEQ_2:19;
thus lim((f1+f2)*seq)=lim_left(f1,x0)+lim_left(f2,x0) by A6,A7,A8,SEQ_2:20;
end; hence f1+f2 is_left_convergent_in x0 by A1,Def1; hence thesis by A2,Def7;
end;
theorem
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1-f2)) implies
f1-f2 is_left_convergent_in x0 &
lim_left(f1-f2,x0)=(lim_left(f1,x0))-(lim_left(f2,x0))
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom(f1-f2);
A2: f1-f2=f1+-f2 by RFUNCT_1:40;
A3: -f2 is_left_convergent_in x0 by A1,Th52;
hence f1-f2 is_left_convergent_in x0 by A1,A2,Th53;
thus lim_left(f1-f2,x0)=lim_left(f1,x0)+lim_left(-f2,x0) by A1,A2,A3,Th53
.=(lim_left(f1,x0))+-lim_left(f2,x0) by A1,Th52
.=(lim_left(f1,x0))-lim_left(f2,x0) by XCMPLX_0:def 8;
end;
theorem
f is_left_convergent_in x0 & f"{0}={} & lim_left(f,x0)<>0 implies
f^ is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))"
proof assume A1: f is_left_convergent_in x0 & f"{0}={} & lim_left(f,x0)<>0;
then A2: dom f=dom f\f"{0}
.=dom(f^) by RFUNCT_1:def 8;
then A3: for r st r<x0
ex g st r<g & g<x0 & g in dom(f^) by A1,Def1;
A4: now let seq; assume A5: seq is convergent & lim seq=x0 &
rng seq c=dom(f^)/\left_open_halfline(x0);
then A6: f*seq is convergent & lim(f*seq)=lim_left(f,x0) by A1,A2,Def7;
dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
then A7: rng seq c=dom f by A2,A5,XBOOLE_1:1;
then A8: f*seq is_not_0 by A2,RFUNCT_2:26;
A9: (f*seq)"=(f^)*seq by A2,A7,RFUNCT_2:27;
hence (f^)*seq is convergent by A1,A6,A8,SEQ_2:35;
thus lim((f^)*seq)=(lim_left(f,x0))" by A1,A6,A8,A9,SEQ_2:36;
end; hence f^ is_left_convergent_in x0 by A3,Def1; hence thesis by A4,Def7;
end;
theorem
f is_left_convergent_in x0 implies abs(f) is_left_convergent_in x0 &
lim_left(abs(f),x0)=abs(lim_left(f,x0))
proof assume A1: f is_left_convergent_in x0;
A2: now let r; assume r<x0; then consider g such that
A3: r<g & g<x0 & g in dom f by A1,Def1; take g;
thus r<g & g<x0 & g in dom abs(f) by A3,SEQ_1:def 10;
end;
A4: now A5: lim_left(f,x0)=lim_left(f,x0); let seq; assume
A6: seq is convergent & lim seq=x0 &
rng seq c=dom(abs(f))/\left_open_halfline(x0);
then A7: rng seq c=dom f/\left_open_halfline(x0) by SEQ_1:def 10;
then A8: f*seq is convergent & lim(f*seq)=lim_left(f,x0) by A1,A5,A6,Def7;
dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A7,XBOOLE_1:1;
then A9: abs(f*seq)=abs(f)*seq by RFUNCT_2:25;
hence abs(f)*seq is convergent by A8,SEQ_4:26;
thus lim(abs(f)*seq)=abs(lim_left(f,x0)) by A8,A9,SEQ_4:27;
end; hence abs(f) is_left_convergent_in x0 by A2,Def1;
hence thesis by A4,Def7;
end;
theorem Th57:
f is_left_convergent_in x0 & lim_left(f,x0)<>0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) implies
f^ is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))"
proof assume A1: f is_left_convergent_in x0 & lim_left(f,x0)<>0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0);
A2: dom f\f"{0}=dom(f^) by RFUNCT_1:def 8;
A3: now let r; assume r<x0; then consider g such that
A4: r<g & g<x0 & g in dom f & f.g<>0 by A1;
take g; not f.g in {0} by A4,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 13;
hence r<g & g<x0 & g in dom(f^) by A2,A4,XBOOLE_0:def 4;
end;
A5: now let seq such that A6: seq is convergent & lim seq=x0 &
rng seq c=dom(f^)/\left_open_halfline(x0);
dom(f^)/\left_open_halfline(x0)c=dom(f^) &
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A7: rng seq c=dom(f^) & rng seq c=left_open_halfline(x0) by A6,XBOOLE_1:
1;
dom(f^)c=dom f by A2,XBOOLE_1:36; then rng seq c=dom f by A7,XBOOLE_1:1;
then rng seq c=dom f/\left_open_halfline(x0) by A7,XBOOLE_1:19;
then A8: f*seq is convergent & lim(f*seq)=lim_left(f,x0) by A1,A6,Def7;
A9: f*seq is_not_0 by A7,RFUNCT_2:26;
A10: (f*seq)"=(f^)*seq by A7,RFUNCT_2:27;
hence (f^)*seq is convergent by A1,A8,A9,SEQ_2:35;
thus lim((f^)*seq)=(lim_left(f,x0))" by A1,A8,A9,A10,SEQ_2:36;
end; hence f^ is_left_convergent_in x0 by A3,Def1; hence thesis by A5,Def7;
end;
theorem Th58:
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) implies
f1(#)f2 is_left_convergent_in x0 &
lim_left(f1(#)f2,x0)=(lim_left(f1,x0))*(lim_left(f2,x0))
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2);
A2: now A3: lim_left(f1,x0)=lim_left(f1,x0) & lim_left(f2,x0)=lim_left(f2,x0);
let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\left_open_halfline(x0);
then A5: rng seq c=dom(f1(#)f2) & rng seq c=left_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1/\left_open_halfline(x0) &
rng seq c=dom f2/\left_open_halfline(x0) by Lm2;
then A6: f1*seq is convergent & lim(f1*seq)=lim_left(f1,x0) by A1,A3,A4,Def7;
A7: f2*seq is convergent & lim(f2*seq)=lim_left(f2,x0) by A1,A3,A4,A5,Def7;
A8: (f1*seq)(#)(f2*seq)=(f1(#)f2)*seq by A5,RFUNCT_2:23;
hence (f1(#)f2)*seq is convergent by A6,A7,SEQ_2:28;
thus lim((f1(#)f2)*seq)=lim_left(f1,x0)*lim_left(f2,x0) by A6,A7,A8,SEQ_2:29
;
end; hence f1(#)
f2 is_left_convergent_in x0 by A1,Def1; hence thesis by A2,Def7;
end;
theorem
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & lim_left(f2,x0)<>
0
& (for r st r<x0 ex g st r<g & g<x0 & g in dom(f1/f2)) implies
f1/f2 is_left_convergent_in x0 &
lim_left(f1/f2,x0)=(lim_left(f1,x0))/(lim_left(f2,x0))
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f2,x0)<>0 & for r st r<x0 ex g st r<g & g<x0 & g in dom(f1/f2);
A2: f1/f2=f1(#)(f2^) by RFUNCT_1:47;
now let r; assume r<x0; then consider g such that
A3: r<g & g<x0 & g in dom(f1/f2) by A1; take g; thus r<g & g<x0 by A3;
dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 4;
then A4: g in dom f2\f2"{0} by A3,XBOOLE_0:def 3;
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 in dom f2 & f2.g<>0 by A4,TARSKI:def 1,XBOOLE_0:def 4;
end;
then A5: f2^ is_left_convergent_in x0 & lim_left(f2^,x0)=(lim_left(f2,x0))"
by A1,Th57; hence f1/f2 is_left_convergent_in x0 by A1,A2,Th58;
thus lim_left(f1/f2,x0)=lim_left(f1,x0)*((lim_left(f2,x0))") by A1,A2,A5,Th58
.=lim_left(f1,x0)/(lim_left(f2,x0)) by XCMPLX_0:def 9;
end;
theorem Th60:
f is_right_convergent_in x0 implies r(#)f is_right_convergent_in x0 &
lim_right(r(#)f,x0)=r*(lim_right(f,x0))
proof assume A1: f is_right_convergent_in x0;
A2: now let r1; assume x0<r1; then consider g such that
A3: g<r1 & x0<g & g in dom f by A1,Def4; take g;
thus g<r1 & x0<g & g in dom(r(#)f) by A3,SEQ_1:def 6;
end;
A4: now let seq; A5: lim_right(f,x0)=lim_right(f,x0);
assume A6: seq is convergent & lim seq=x0 &
rng seq c=dom(r(#)f)/\right_open_halfline(x0);
then A7: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 6;
then A8: f*seq is convergent & lim(f*seq)=lim_right(f,x0) by A1,A5,A6,Def8;
then A9: r(#)(f*seq) is convergent by SEQ_2:21;
dom f/\right_open_halfline(x0) c=dom f by XBOOLE_1:17;
then A10:
rng seq c=dom f by A7,XBOOLE_1:1; then A11: r(#)(f*seq)=(r(#)
f)*seq by RFUNCT_2:24;
thus (r(#)f)*seq is convergent by A9,A10,RFUNCT_2:24;
thus lim((r(#)f)*seq)=r*(lim_right(f,x0)) by A8,A11,SEQ_2:22;
end; hence r(#)
f is_right_convergent_in x0 by A2,Def4; hence thesis by A4,Def8;
end;
theorem Th61:
f is_right_convergent_in x0 implies -f is_right_convergent_in x0 &
lim_right(-f,x0)=-(lim_right(f,x0))
proof assume A1: f is_right_convergent_in x0; A2: (-1)(#)f=-f by RFUNCT_1:38;
hence -f is_right_convergent_in x0 by A1,Th60;
thus lim_right(-f,x0)=(-1)*(lim_right(f,x0)) by A1,A2,Th60
.=-(1*(lim_right(f,x0))) by XCMPLX_1:175
.=-(lim_right(f,x0));
end;
theorem Th62:
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2)) implies
f1+f2 is_right_convergent_in x0 &
lim_right(f1+f2,x0)=(lim_right(f1,x0))+(lim_right(f2,x0))
proof assume A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom(f1+f2);
A2: now A3: lim_right(f1,x0)=lim_right(f1,x0) &
lim_right(f2,x0)=lim_right(f2,x0);
let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1+f2)/\right_open_halfline(x0);
then A5: rng seq c=dom(f1+f2) & rng seq c=right_open_halfline(x0) &
dom(f1+f2)=dom f1/\dom f2 & rng seq c=dom f1/\right_open_halfline(x0) &
rng seq c=dom f2/\right_open_halfline(x0) by Lm4;
then A6: f1*seq is convergent & lim(f1*seq)=lim_right(f1,x0) by A1,A3,A4,Def8
;
A7: f2*seq is convergent & lim(f2*seq)=lim_right(f2,x0) by A1,A3,A4,A5,Def8;
A8: f1*seq+f2*seq=(f1+f2)*seq by A5,RFUNCT_2:23;
hence (f1+f2)*seq is convergent by A6,A7,SEQ_2:19;
thus lim((f1+f2)*seq)=lim_right(f1,x0)+lim_right(f2,x0) by A6,A7,A8,SEQ_2:20
;
end; hence f1+f2 is_right_convergent_in x0 by A1,Def4; hence thesis by A2,Def8
;
end;
theorem
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1-f2)) implies
f1-f2 is_right_convergent_in x0 &
lim_right(f1-f2,x0)=(lim_right(f1,x0))-(lim_right(f2,x0))
proof assume A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom(f1-f2);
A2: f1-f2=f1+-f2 by RFUNCT_1:40;
A3: -f2 is_right_convergent_in x0 by A1,Th61;
hence f1-f2 is_right_convergent_in x0 by A1,A2,Th62;
thus lim_right(f1-f2,x0)=lim_right(f1,x0)+lim_right(-f2,x0) by A1,A2,A3,Th62
.=(lim_right(f1,x0))+-lim_right(f2,x0) by A1,Th61
.=(lim_right(f1,x0))-lim_right(f2,x0) by XCMPLX_0:def 8;
end;
theorem
f is_right_convergent_in x0 & f"{0}={} & lim_right(f,x0)<>0 implies
f^ is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))"
proof assume A1: f is_right_convergent_in x0 & f"{0}={} & lim_right(f,x0)<>0;
then A2: dom f=dom f\f"{0}
.=dom(f^) by RFUNCT_1:def 8;
then A3: for r st x0<r ex g st g<r & x0<g & g in dom(f^) by A1,Def4;
A4: now let seq; assume A5: seq is convergent & lim seq=x0 &
rng seq c=dom(f^)/\right_open_halfline(x0);
then A6: f*seq is convergent & lim(f*seq)=lim_right(f,x0) by A1,A2,Def8;
dom f/\right_open_halfline(x0) c=dom f by XBOOLE_1:17;
then A7: rng seq c=dom f by A2,A5,XBOOLE_1:1;
then A8: f*seq is_not_0 by A2,RFUNCT_2:26;
A9: (f*seq)"=(f^)*seq by A2,A7,RFUNCT_2:27;
hence (f^)*seq is convergent by A1,A6,A8,SEQ_2:35;
thus lim((f^)*seq)=(lim_right(f,x0))" by A1,A6,A8,A9,SEQ_2:36;
end; hence f^ is_right_convergent_in x0 by A3,Def4; hence thesis by A4,Def8;
end;
theorem
f is_right_convergent_in x0 implies abs(f) is_right_convergent_in x0 &
lim_right(abs(f),x0)=abs(lim_right(f,x0))
proof assume A1: f is_right_convergent_in x0;
A2: now let r; assume x0<r; then consider g such that
A3: g<r & x0<g & g in dom f by A1,Def4; take g;
thus g<r & x0<g & g in dom abs(f) by A3,SEQ_1:def 10;
end;
A4: now A5: lim_right(f,x0)=lim_right(f,x0); let seq; assume
A6: seq is convergent & lim seq=x0 &
rng seq c=dom(abs(f))/\right_open_halfline(x0);
then A7: rng seq c=dom f/\right_open_halfline(x0) by SEQ_1:def 10;
then A8: f*seq is convergent & lim(f*seq)=lim_right(f,x0) by A1,A5,A6,Def8;
dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
then rng seq c=dom f by A7,XBOOLE_1:1;
then A9: abs(f*seq)=abs(f)*seq by RFUNCT_2:25;
hence abs(f)*seq is convergent by A8,SEQ_4:26;
thus lim(abs(f)*seq)=abs(lim_right(f,x0)) by A8,A9,SEQ_4:27;
end; hence abs(f) is_right_convergent_in x0 by A2,Def4;
hence thesis by A4,Def8
;
end;
theorem Th66:
f is_right_convergent_in x0 & lim_right(f,x0)<>0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) implies
f^ is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))"
proof assume A1: f is_right_convergent_in x0 & lim_right(f,x0)<>0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0);
A2: dom f\f"{0}=dom(f^) by RFUNCT_1:def 8;
A3: now let r; assume x0<r; then consider g such that
A4: g<r & x0<g & g in dom f & f.g<>0 by A1;
take g; not f.g in {0} by A4,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 13;
hence g<r & x0<g & g in dom(f^) by A2,A4,XBOOLE_0:def 4;
end;
A5: now let seq such that A6: seq is convergent & lim seq=x0 &
rng seq c=dom(f^)/\right_open_halfline(x0);
dom(f^)/\right_open_halfline(x0)c=dom(f^) &
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17
;
then A7: rng seq c=dom(f^) & rng seq c=right_open_halfline(x0) by A6,XBOOLE_1
:1;
dom(f^) c=dom f by A2,XBOOLE_1:36; then rng seq c=dom f by A7,XBOOLE_1:1
;
then rng seq c=dom f/\right_open_halfline(x0) by A7,XBOOLE_1:19;
then A8: f*seq is convergent & lim(f*seq)=lim_right(f,x0) by A1,A6,Def8;
A9: f*seq is_not_0 by A7,RFUNCT_2:26;
A10: (f*seq)"=(f^)*seq by A7,RFUNCT_2:27;
hence (f^)*seq is convergent by A1,A8,A9,SEQ_2:35;
thus lim((f^)*seq)=(lim_right(f,x0))" by A1,A8,A9,A10,SEQ_2:36;
end; hence f^ is_right_convergent_in x0 by A3,Def4; hence thesis by A5,Def8;
end;
theorem Th67:
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) implies
f1(#)f2 is_right_convergent_in x0 &
lim_right(f1(#)f2,x0)=(lim_right(f1,x0))*(lim_right(f2,x0))
proof assume A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2);
A2: now A3: lim_right(f1,x0)=lim_right(f1,x0) &
lim_right(f2,x0)=lim_right(f2,x0);
let seq; assume A4: seq is convergent & lim seq=x0 &
rng seq c=dom(f1(#)f2)/\right_open_halfline(x0);
then A5: rng seq c=dom(f1(#)f2) & rng seq c=right_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng seq c=dom f1/\right_open_halfline(x0) &
rng seq c=dom f2/\right_open_halfline(x0) by Lm2;
then A6: f1*seq is convergent & lim(f1*seq)=lim_right(f1,x0) by A1,A3,A4,Def8
;
A7: f2*seq is convergent & lim(f2*seq)=lim_right(f2,x0) by A1,A3,A4,A5,Def8;
A8: (f1*seq)(#)(f2*seq)=(f1(#)f2)*seq by A5,RFUNCT_2:23;
hence (f1(#)f2)*seq is convergent by A6,A7,SEQ_2:28;
thus lim((f1(#)
f2)*seq)=lim_right(f1,x0)*lim_right(f2,x0) by A6,A7,A8,SEQ_2:29;
end; hence f1(#)
f2 is_right_convergent_in x0 by A1,Def4; hence thesis by A2,Def8
;
end;
theorem
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f2,x0)<>0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1/f2)) implies
f1/f2 is_right_convergent_in x0 &
lim_right(f1/f2,x0)=(lim_right(f1,x0))/(lim_right(f2,x0))
proof assume
A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f2,x0)<>0 & for r st x0<r ex g st g<r & x0<g & g in dom(f1/f2);
A2: f1/f2=f1(#)(f2^) by RFUNCT_1:47;
now let r; assume x0<r; then consider g such that
A3: g<r & x0<g & g in dom(f1/f2) by A1; take g; thus g<r & x0<g by A3;
dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 4;
then A4: g in dom f2\f2"{0} by A3,XBOOLE_0:def 3;
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 in dom f2 & f2.g<>0 by A4,TARSKI:def 1,XBOOLE_0:def 4;
end;
then A5: f2^ is_right_convergent_in x0 & lim_right(f2^,x0)=(lim_right(f2,x0))"
by A1,Th66; hence f1/f2 is_right_convergent_in x0 by A1,A2,Th67;
thus lim_right(f1/f2,x0)=lim_right(f1,x0)*((lim_right(f2,x0))") by A1,A2,A5,
Th67
.=lim_right(f1,x0)/(lim_right(f2,x0)) by XCMPLX_0:def 9;
end;
theorem
f1 is_left_convergent_in x0 & lim_left(f1,x0)=0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2)) &
(ex r st 0<r & f2 is_bounded_on ].x0-r,x0.[) implies
f1(#)f2 is_left_convergent_in x0 & lim_left(f1(#)f2,x0)=0
proof assume A1: f1 is_left_convergent_in x0 & lim_left(f1,x0)=0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom(f1(#)f2);
given r such that A2: 0<r & f2 is_bounded_on ].x0-r,x0.[;
consider g be real number such that
A3: for r1 st r1 in ].x0-r,x0.[/\dom f2 holds
abs(f2.r1)<=g by A2,RFUNCT_1:90;
A4: now let s be Real_Sequence; assume A5: s is convergent &
lim s=x0 & rng s c=dom(f1(#)f2)/\left_open_halfline(x0);
then A6: rng s c=dom(f1(#)f2) & rng s c=left_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng s c=dom f1 & rng s c=dom f2 &
rng s c=dom f1/\left_open_halfline(x0) &
rng s c=dom f2/\left_open_halfline(x0) by Lm2;
x0-r<x0 by A2,Lm1; then consider k such that
A7: for n st k<=n holds x0-r<s.n by A5,Th1;
A8: s^\k is convergent & lim(s^\k)=x0 by A5,SEQ_4:33;
set L=left_open_halfline(x0); 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 &
rng(s^\k)c=dom f1/\L & rng(s^\k)c=L & rng(s^\k)c=dom f2/\
L by A6,XBOOLE_1:1;
then A10: f1*(s^\k) is convergent & lim(f1*(s^\k))=0 by A1,A8,Def7;
now set t=abs(g)+1; 0<=abs(g) by ABSVALUE:5; hence 0<t by Lm1;
let n; A11: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then A12: (s^\k).n in dom f2 & (s^\k).n in L by A9;
k<=n+k by NAT_1:37; then x0-r<s.(n+k) by A7;
then A13: x0-r<(s^\k).n by SEQM_3:def 9;
(s^\k).n in {g1: g1<x0} by A12,PROB_1:def 15;
then ex g1 st g1=(s^\k).n & g1<x0; then (s^\k).n in {g2: x0-r<g2 & g2<x0}
by A13;
then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (s^\k).n in ].x0-r,x0.[/\dom f2 by A9,A11,XBOOLE_0:def 3;
then abs(f2.((s^\k).n))<=g by A3; then A14: abs((f2*(s^\k)).n)<=
g by A9,RFUNCT_2:21;
g<=abs(g) by ABSVALUE:11; then g<t by Lm1;
hence abs((f2*(s^\k)).n)<t by A14,AXIOMS:22;
end; then A15: f2*(s^\k) is bounded by SEQ_2:15;
then A16: (f1*(s^\k))(#)(f2*(s^\k)) is convergent by A10,SEQ_2:39;
A17: lim((f1*(s^\k))(#)(f2*(s^\k)))=0 by A10,A15,SEQ_2:40;
A18: (f1*(s^\k))(#)(f2*(s^\k))=(f1(#)f2)*(s^\k) by A9,RFUNCT_2:23
.=((f1(#)f2)*s)^\k by A6,RFUNCT_2:22;
hence (f1(#)f2)*s is convergent by A16,SEQ_4:35;
thus lim((f1(#)f2)*s)=0 by A16,A17,A18,SEQ_4:36;
end; hence f1(#)
f2 is_left_convergent_in x0 by A1,Def1; hence thesis by A4,Def7;
end;
theorem
f1 is_right_convergent_in x0 & lim_right(f1,x0)=0 &
(for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2)) &
(ex r st 0<r & f2 is_bounded_on ].x0,x0+r.[) implies
f1(#)f2 is_right_convergent_in x0 & lim_right(f1(#)f2,x0)=0
proof assume A1: f1 is_right_convergent_in x0 & lim_right(f1,x0)=0 &
for r st x0<r ex g st g<r & x0<g & g in dom(f1(#)f2);
given r such that A2: 0<r & f2 is_bounded_on ].x0,x0+r.[;
consider g be real number such that
A3: for r1 st r1 in ].x0,x0+r.[/\dom f2 holds
abs(f2.r1)<=g by A2,RFUNCT_1:90;
A4: now let s be Real_Sequence; assume A5: s is convergent &
lim s=x0 & rng s c=dom(f1(#)f2)/\right_open_halfline(x0);
then A6: rng s c=dom(f1(#)f2) & rng s c=right_open_halfline(x0) &
dom(f1(#)f2)=dom f1/\dom f2 & rng s c=dom f1 & rng s c=dom f2 &
rng s c=dom f1/\right_open_halfline(x0) &
rng s c=dom f2/\right_open_halfline(x0) by Lm2;
x0<x0+r by A2,Lm1; then consider k such that
A7: for n st k<=n holds s.n<x0+r by A5,Th2;
A8: s^\k is convergent & lim(s^\k)=x0 by A5,SEQ_4:33;
set L=right_open_halfline(x0); 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 &
rng(s^\k)c=dom f1/\L & rng(s^\k)c=L & rng(s^\k)c=dom f2/\
L by A6,XBOOLE_1:1;
then A10: f1*(s^\k) is convergent & lim(f1*(s^\k))=0 by A1,A8,Def8;
now set t=abs(g)+1; 0<=abs(g) by ABSVALUE:5; hence 0<t by Lm1;
let n; A11: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then A12: (s^\k).n in dom f2 & (s^\k).n in L by A9;
k<=n+k by NAT_1:37; then s.(n+k)<x0+r by A7;
then A13: (s^\k).n<x0+r by SEQM_3:def 9;
(s^\k).n in {g1: x0<g1} by A12,LIMFUNC1:def 3
; then ex g1 st g1=(s^\k).n & x0<g1;
then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A13;
then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (s^\k).n in ].x0,x0+r.[/\dom f2 by A9,A11,XBOOLE_0:def 3;
then abs(f2.((s^\k).n))<=g by A3; then A14: abs((f2*(s^\k)).n)<=
g by A9,RFUNCT_2:21;
g<=abs(g) by ABSVALUE:11; then g<t by Lm1;
hence abs((f2*(s^\k)).n)<t by A14,AXIOMS:22;
end; then A15: f2*(s^\k) is bounded by SEQ_2:15;
then A16: (f1*(s^\k))(#)(f2*(s^\k)) is convergent by A10,SEQ_2:39;
A17: lim((f1*(s^\k))(#)(f2*(s^\k)))=0 by A10,A15,SEQ_2:40;
A18: (f1*(s^\k))(#)(f2*(s^\k))=(f1(#)f2)*(s^\k) by A9,RFUNCT_2:23
.=((f1(#)f2)*s)^\k by A6,RFUNCT_2:22;
hence (f1(#)f2)*s is convergent by A16,SEQ_4:35;
thus lim((f1(#)f2)*s)=0 by A16,A17,A18,SEQ_4:36;
end; hence f1(#)
f2 is_right_convergent_in x0 by A1,Def4; hence thesis by A4,Def8
;
end;
theorem Th71:
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f)
& (ex r st 0<r & (for g st g in dom f /\ ].x0-r,x0.[ holds
f1.g<=f.g & f.g<=f2.g) &
((dom f1 /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[ &
dom f /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[) or
(dom f2 /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
dom f /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[))) implies
f is_left_convergent_in x0 & lim_left(f,x0)=lim_left(f1,x0)
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0) &
for r st r<x0 ex g st r<g & g<x0 & g in dom f;
given r1 such that
A2: 0<r1 & (for g st g in dom f/\].x0-r1,x0.[ holds f1.g<=f.g & f.g<=f2.g) and
A3: (dom f1/\].x0-r1,x0.[c=dom f2/\].x0-r1,x0.[ &
dom f/\].x0-r1,x0.[c=dom f1/\].x0-r1,x0.[) or
(dom f2/\].x0-r1,x0.[c=dom f1/\].x0-r1,x0.[ &
dom f/\].x0-r1,x0.[c=dom f2/\].x0-r1,x0.[);
now per cases by A3;
suppose A4: dom f1/\].x0-r1,x0.[c=dom f2/\].x0-r1,x0.[ &
dom f/\].x0-r1,x0.[c=dom f1/\].x0-r1,x0.[;
A5: now let seq; assume A6: seq is convergent & lim seq=x0 &
rng seq c=dom f/\left_open_halfline(x0);
then x0-r1<lim seq by A2,Lm1; then consider k such that
A7: for n st k<=n holds x0-r1<seq.n by A6,Th1;
A8: seq^\k is convergent & lim(seq^\k)= x0 by A6,SEQ_4:33;
A9: rng(seq^\k)c=rng seq by RFUNCT_2:7;
dom f/\left_open_halfline(x0)c=dom f &
dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A10: rng seq c=dom f & rng seq c=left_open_halfline(x0) by A6,XBOOLE_1:
1
;
then A11: rng(seq^\k)c=dom f & rng(seq^\k)c=left_open_halfline(x0) by A9,
XBOOLE_1:1
;
A12: dom f1/\].x0-r1,x0.[c=dom f1 by XBOOLE_1:17;
A13: dom f2/\].x0-r1,x0.[c=dom f2 by XBOOLE_1:17;
now let x be set; assume A14: x in rng(seq^\k); then consider n such that
A15: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then x0-r1<seq.(n+k) by A7;
then A16: x0-r1<(seq^\k).n by SEQM_3:def 9;
(seq^\k).n in left_open_halfline(x0) by A11,A14,A15;
then (seq^\k).n in {g: g<x0} by PROB_1:def 15
; then ex g st g=(seq^\k).n & g<x0;
then x in {g1: x0-r1<g1 & g1<x0} by A15,A16;
hence x in ].x0-r1,x0.[ by RCOMP_1:def 2;
end;
then A17: rng(seq^\k)c=].x0-r1,x0.[ by TARSKI:def 3;
then A18: rng(seq^\k)c=dom f/\].x0-r1,x0.[ by A11,XBOOLE_1:19;
then A19: rng(seq^\k)c=dom f1/\].x0-r1,x0.[ by A4,XBOOLE_1:1;
then A20: rng(seq^\k)c=dom f1 by A12,XBOOLE_1:1;
rng(seq^\k)c=dom f2/\].x0-r1,x0.[ by A4,A19,XBOOLE_1:1;
then A21: rng(seq^\k)c=dom f2 by A13,XBOOLE_1:1;
].x0-r1,x0.[c=left_open_halfline(x0) by LIMFUNC1:16;
then A22: rng(seq^\k)c=left_open_halfline(x0) by A17,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A20,XBOOLE_1:19;
then A23: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_left(f1,x0)
by A1,A8,Def7;
rng(seq^\k) c=dom f2/\left_open_halfline(x0) by A21,A22,XBOOLE_1:19;
then A24: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_left(f2,x0)
by A1,A8,Def7;
A25: 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 A2,A18
;
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 A20,A21,RFUNCT_2:21;
end; then A26: f*(seq^\k) is convergent by A1,A23,A24,SEQ_2:33;
lim(f*(seq^\k))=lim_left(f1,x0) by A1,A23,A24,A25,SEQ_2:34;
then A27: (f*seq)^\k is convergent & lim((f*seq)^\k)=lim_left(f1,x0)
by A10,A26,RFUNCT_2:22; hence f*seq is convergent by SEQ_4:35;
thus lim(f*seq)=lim_left(f1,x0) by A27,SEQ_4:36;
end; hence f is_left_convergent_in x0 by A1,Def1; hence thesis by A5,Def7;
suppose A28: dom f2/\].x0-r1,x0.[c=dom f1/\].x0-r1,x0.[ &
dom f/\].x0-r1,x0.[c=dom f2/\].x0-r1,x0.[;
A29: now let seq; assume A30: seq is convergent & lim seq=x0 &
rng seq c= dom f/\left_open_halfline(x0);
then x0-r1<lim seq by A2,Lm1; then consider k such that
A31: for n st k<=n holds x0-r1<seq.n by A30,Th1;
A32: seq^\k is convergent & lim(seq^\k)= x0 by A30,SEQ_4:33;
A33: rng(seq^\k)c=rng seq by RFUNCT_2:7;
dom f/\left_open_halfline(x0)c=dom f &
dom f/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A34: rng seq c=dom f & rng seq c=left_open_halfline(x0) by A30,XBOOLE_1
:1
;
then A35: rng(seq^\k)c=dom f & rng(seq^\k)c=left_open_halfline(x0) by A33,
XBOOLE_1:1;
A36: dom f1/\].x0-r1,x0.[c=dom f1 by XBOOLE_1:17;
A37: dom f2/\].x0-r1,x0.[c=dom f2 by XBOOLE_1:17;
now let x be set; assume A38: x in rng(seq^\k); then consider n such that
A39: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then x0-r1<seq.(n+k) by A31;
then A40: x0-r1<(seq^\k).n by SEQM_3:def 9;
(seq^\k).n in left_open_halfline(x0) by A35,A38,A39;
then (seq^\k).n in {g: g<x0} by PROB_1:def 15
; then ex g st g=(seq^\k).n & g<x0;
then x in {g1: x0-r1<g1 & g1<x0} by A39,A40;
hence x in ].x0-r1,x0.[ by RCOMP_1:def 2;
end; then A41: rng(seq^\k)c=].x0-r1,x0.[ by TARSKI:def 3;
then A42: rng(seq^\k)c=dom f/\].x0-r1,x0.[ by A35,XBOOLE_1:19;
then A43: rng(seq^\k)c=dom f2/\].x0-r1,x0.[ by A28,XBOOLE_1:1;
then A44: rng(seq^\k)c=dom f2 by A37,XBOOLE_1:1;
rng(seq^\k)c=dom f1/\].x0-r1,x0.[ by A28,A43,XBOOLE_1:1;
then A45: rng(seq^\k)c=dom f1 by A36,XBOOLE_1:1;
].x0-r1,x0.[c=left_open_halfline(x0) by LIMFUNC1:16;
then A46: rng(seq^\k)c=left_open_halfline(x0) by A41,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\left_open_halfline(x0) by A45,XBOOLE_1:19;
then A47: f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_left(f1,x0)
by A1,A32,Def7;
rng(seq^\k)c=dom f2/\left_open_halfline(x0) by A44,A46,XBOOLE_1:19;
then A48: f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_left(f2,x0)
by A1,A32,Def7;
A49: 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 A2,A42
;
then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n)
by A35,RFUNCT_2:21;
hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n
by A44,A45,RFUNCT_2:21;
end; then A50: f*(seq^\k) is convergent by A1,A47,A48,SEQ_2:33;
lim(f*(seq^\k))=lim_left(f1,x0) by A1,A47,A48,A49,SEQ_2:34;
then A51: (f*seq)^\k is convergent & lim((f*seq)^\k)=lim_left(f1,x0)
by A34,A50,RFUNCT_2:22; hence f*seq is convergent by SEQ_4:35;
thus lim(f*seq)=lim_left(f1,x0) by A51,SEQ_4:36;
end; hence f is_left_convergent_in x0 by A1,Def1; hence thesis by A29,Def7;
end; hence thesis;
end;
theorem
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0) & (ex r st 0<r &
].x0-r,x0.[ c= dom f1 /\ dom f2 /\ dom f &
for g st g in ].x0-r,x0.[ holds f1.g<=f.g & f.g<=f2.g) implies
f is_left_convergent_in x0 & lim_left(f,x0)=lim_left(f1,x0)
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 &
lim_left(f1,x0)=lim_left(f2,x0);
given r such that A2: 0<r & ].x0-r,x0.[c=dom f1/\dom f2/\dom f &
for g st g in ].x0-r,x0.[ holds f1.g<=f.g & f.g<=f2.g;
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 A3: ].x0-r,x0.[c=dom f & ].x0-r,x0.[c=dom f1/\dom f2 by A2,XBOOLE_1:1;
then A4: dom f/\].x0-r,x0.[=].x0-r,x0.[ by XBOOLE_1:28;
dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
then ].x0-r,x0.[c=dom f1 & ].x0-r,x0.[c=dom f2 by A3,XBOOLE_1:1;
then A5: dom f1/\].x0-r,x0.[=].x0-r,x0.[ & dom f2/\].x0-r,x0.[=].x0-r,x0.[
by XBOOLE_1:28;
now let r1 such that A6: r1<x0;
now per cases;
suppose A7: r1<=x0-r;
now x0-r<x0 by A2,Lm1;
then consider g being real number such that A8: x0-r<g & g<x0 by REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus r1<g & g<x0 by A7,A8,AXIOMS:22; g in {g2: x0-r<g2 & g2<x0} by A8;
then g in ].x0-r,x0.[ by RCOMP_1:def 2; hence g in dom f by A3;
end; hence ex g st r1<g & g<x0 & g in dom f;
suppose A9: x0-r<=r1;
now consider g being real number such that
A10: r1<g & g<x0 by A6,REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus r1<g & g<x0 by A10; x0-r<g by A9,A10,AXIOMS:22;
then g in {g2: x0-r<g2 & g2<x0} by A10;
then g in ].x0-r,x0.[ by RCOMP_1:def 2; hence g in dom f by A3;
end; hence ex g st r1<g & g<x0 & g in dom f;
end; hence ex g st r1<g & g<x0 & g in dom f;
end; hence thesis by A1,A2,A4,A5,Th71;
end;
theorem Th73:
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0) &
(for r st x0<r ex g st g<r & x0<g & g in dom f) &
(ex r st 0<r & (for g st g in dom f /\ ].x0,x0+r.[ holds
f1.g<=f.g & f.g<=f2.g) &
((dom f1 /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[ &
dom f /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[) or
(dom f2 /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
dom f /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[))) implies
f is_right_convergent_in x0 & lim_right(f,x0)=lim_right(f1,x0)
proof assume A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0) &
for r st x0<r ex g st g<r & x0<g & g in dom f;
given r1 such that
A2: 0<r1 & for g st g in dom f/\].x0,x0+r1.[ holds f1.g<=f.g & f.g<=f2.g and
A3: (dom f1/\].x0,x0+r1.[c=dom f2/\].x0,x0+r1.[ &
dom f/\].x0,x0+r1.[c=dom f1/\].x0,x0+r1.[) or
(dom f2/\].x0,x0+r1.[c=dom f1/\].x0,x0+r1.[ &
dom f/\].x0,x0+r1.[c=dom f2/\].x0,x0+r1.[);
now per cases by A3;
suppose A4: dom f1/\].x0,x0+r1.[c=dom f2/\].x0,x0+r1.[ &
dom f/\].x0,x0+r1.[c=dom f1/\].x0,x0+r1.[;
A5: now let seq; assume A6: seq is convergent & lim seq=x0 &
rng seq c=dom f/\right_open_halfline(x0);
then x0<lim seq+r1 by A2,Lm1; then consider k such that
A7: for n st k<=n holds seq.n<x0+r1 by A6,Th2;
A8: seq^\k is convergent & lim(seq^\k)= x0 by A6,SEQ_4:33;
A9: rng(seq^\k)c=rng seq by RFUNCT_2:7;
dom f/\right_open_halfline(x0)c=dom f &
dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A10: rng seq c=dom f & rng seq c=right_open_halfline(x0) by A6,XBOOLE_1
:1
;
then A11:rng(seq^\k)c=dom f & rng(seq^\k)c=right_open_halfline(x0) by A9,
XBOOLE_1:1
;
A12: dom f1/\].x0,x0+r1.[c=dom f1 by XBOOLE_1:17;
A13: dom f2/\].x0,x0+r1.[c=dom f2 by XBOOLE_1:17;
now let x be set; assume A14: x in rng(seq^\k); then consider n such that
A15: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then seq.(n+k)<x0+r1 by A7;
then A16: (seq^\k).n<x0+r1 by SEQM_3:def 9;
(seq^\k).n in right_open_halfline(x0) by A11,A14,A15;
then (seq^\k).n in {g: x0<g} by LIMFUNC1:def 3
; then ex g st g=(seq^\k).n & x0<g;
then x in {g1: x0<g1 & g1<x0+r1} by A15,A16;
hence x in ].x0,x0+r1.[ by RCOMP_1:def 2;
end; then A17: rng(seq^\k)c=].x0,x0+r1.[ by TARSKI:def 3;
then A18: rng(seq^\k)c=dom f/\].x0,x0+r1.[ by A11,XBOOLE_1:19;
then A19: rng(seq^\k)c=dom f1/\].x0,x0+r1.[ by A4,XBOOLE_1:1;
then A20: rng(seq^\k)c=dom f1 by A12,XBOOLE_1:1;
rng(seq^\k)c=dom f2/\].x0,x0+r1.[ by A4,A19,XBOOLE_1:1;
then A21: rng(seq^\k)c=dom f2 by A13,XBOOLE_1:1;
].x0,x0+r1.[c=right_open_halfline(x0) by LIMFUNC1:11;
then A22: rng(seq^\k)c=right_open_halfline(x0) by A17,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A20,XBOOLE_1:19;
then A23:f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_right(f1,x0)
by A1,A8,Def8;
rng(seq^\k)c=dom f2/\right_open_halfline(x0) by A21,A22,XBOOLE_1:19;
then A24:f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_right(f2,x0)
by A1,A8,Def8;
A25: 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 A2,A18
;
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 A20,A21,RFUNCT_2:21;
end; then A26: f*(seq^\k) is convergent by A1,A23,A24,SEQ_2:33;
lim(f*(seq^\k))=lim_right(f1,x0) by A1,A23,A24,A25,SEQ_2:34;
then A27: (f*seq)^\k is convergent & lim((f*seq)^\k)=lim_right(f1,x0)
by A10,A26,RFUNCT_2:22; hence f*seq is convergent by SEQ_4:35;
thus lim(f*seq)=lim_right(f1,x0) by A27,SEQ_4:36;
end; hence f is_right_convergent_in x0 by A1,Def4; hence thesis by A5,Def8;
suppose A28: dom f2/\].x0,x0+r1.[c=dom f1/\].x0,x0+r1.[ &
dom f/\].x0,x0+r1.[ c=dom f2/\].x0,x0+r1.[;
A29: now let seq; assume A30: seq is convergent & lim seq=x0 &
rng seq c= dom f/\right_open_halfline(x0);
then x0<lim seq+r1 by A2,Lm1; then consider k such that
A31: for n st k<=n holds seq.n<x0+r1 by A30,Th2;
A32: seq^\k is convergent & lim(seq^\k)= x0 by A30,SEQ_4:33;
A33: rng(seq^\k)c=rng seq by RFUNCT_2:7;
dom f/\right_open_halfline(x0)c=dom f &
dom f/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A34: rng seq c=dom f & rng seq c=right_open_halfline(x0) by A30,
XBOOLE_1:1
;
then A35: rng(seq^\k)c=dom f & rng(seq^\k)c=right_open_halfline(x0)
by A33,XBOOLE_1:1;
A36: dom f1/\].x0,x0+r1.[c=dom f1 by XBOOLE_1:17;
A37: dom f2/\].x0,x0+r1.[c=dom f2 by XBOOLE_1:17;
now let x be set; assume A38: x in rng(seq^\k); then consider n such that
A39: x=(seq^\k).n by RFUNCT_2:9; k<=n+k by NAT_1:37
; then seq.(n+k)<x0+r1 by A31;
then A40: (seq^\k).n<x0+r1 by SEQM_3:def 9;
(seq^\k).n in right_open_halfline(x0) by A35,A38,A39;
then (seq^\k).n in {g: x0<g} by LIMFUNC1:def 3
; then ex g st g=(seq^\k).n & x0<g;
then x in {g1: x0<g1 & g1<x0+r1} by A39,A40;
hence x in ].x0,x0+r1.[ by RCOMP_1:def 2;
end; then A41: rng(seq^\k)c=].x0,x0+r1.[ by TARSKI:def 3;
then A42: rng(seq^\k)c=dom f/\].x0,x0+r1.[ by A35,XBOOLE_1:19;
then A43: rng(seq^\k)c=dom f2/\].x0,x0+r1.[ by A28,XBOOLE_1:1;
then A44: rng(seq^\k)c=dom f2 by A37,XBOOLE_1:1;
rng(seq^\k)c=dom f1/\].x0,x0+r1.[ by A28,A43,XBOOLE_1:1;
then A45: rng(seq^\k)c=dom f1 by A36,XBOOLE_1:1;
].x0,x0+r1.[c=right_open_halfline(x0) by LIMFUNC1:11;
then A46: rng(seq^\k)c=right_open_halfline(x0) by A41,XBOOLE_1:1;
then rng(seq^\k)c=dom f1/\right_open_halfline(x0) by A45,XBOOLE_1:19;
then A47:f1*(seq^\k) is convergent & lim(f1*(seq^\k))=lim_right(f1,x0)
by A1,A32,Def8;
rng(seq^\k)c=dom f2/\right_open_halfline(x0) by A44,A46,XBOOLE_1:19;
then A48:f2*(seq^\k) is convergent & lim(f2*(seq^\k))=lim_right(f2,x0)
by A1,A32,Def8;
A49: 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 A2,A42
;
then f1.((seq^\k).n)<=(f*(seq^\k)).n & (f*(seq^\k)).n<=f2.((seq^\k).n)
by A35,RFUNCT_2:21;
hence (f1*(seq^\k)).n<=(f*(seq^\k)).n & (f*(seq^\k)).n<=(f2*(seq^\k)).n
by A44,A45,RFUNCT_2:21;
end; then A50: f*(seq^\k) is convergent by A1,A47,A48,SEQ_2:33;
lim(f*(seq^\k))=lim_right(f1,x0) by A1,A47,A48,A49,SEQ_2:34;
then A51: (f*seq)^\k is convergent & lim((f*seq)^\k)=lim_right(f1,x0)
by A34,A50,RFUNCT_2:22; hence f*seq is convergent by SEQ_4:35;
thus lim(f*seq)=lim_right(f1,x0) by A51,SEQ_4:36;
end; hence f is_right_convergent_in x0 by A1,Def4; hence thesis by A29,Def8
;
end; hence thesis;
end;
theorem
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0) &
(ex r st 0<r & ].x0,x0+r.[ c= dom f1 /\ dom f2 /\ dom f &
for g st g in ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g) implies
f is_right_convergent_in x0 & lim_right(f,x0)=lim_right(f1,x0)
proof assume A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 &
lim_right(f1,x0)=lim_right(f2,x0);
given r such that A2: 0<r & ].x0,x0+r.[c=dom f1/\dom f2/\dom f &
for g st g in ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g;
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 A3: ].x0,x0+r.[c=dom f & ].x0,x0+r.[c=dom f1/\dom f2 by A2,XBOOLE_1:1;
then A4: dom f/\].x0,x0+r.[=].x0,x0+r.[ by XBOOLE_1:28;
dom f1/\dom f2 c=dom f1 & dom f1/\dom f2 c=dom f2 by XBOOLE_1:17;
then ].x0,x0+r.[c=dom f1 & ].x0,x0+r.[c=dom f2 by A3,XBOOLE_1:1;
then A5: dom f1/\].x0,x0+r.[=].x0,x0+r.[ & dom f2/\].x0,x0+r.[=].x0,x0+r.[
by XBOOLE_1:28;
now let r1 such that A6: x0<r1;
now per cases;
suppose A7: r1<=x0+r;
now consider g being real number such that
A8: x0<g & g<r1 by A6,REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus g<r1 & x0<g by A8; g<x0+r by A7,A8,AXIOMS:22;
then g in {g2: x0<g2 & g2<x0+r} by A8;
then g in ].x0,x0+r.[ by RCOMP_1:def 2; hence g in dom f by A3;
end; hence ex g st g<r1 & x0<g & g in dom f;
suppose A9: x0+r<=r1;
now x0+0<x0+r by A2,REAL_1:67;
then consider g being real number such that
A10: x0<g & g<x0+r by REAL_1:75;
reconsider g as Real by XREAL_0:def 1;
take g;
thus g<r1 & x0<g by A9,A10,AXIOMS:22;
g in {g2: x0<g2 & g2<x0+r} by A10;
then g in ].x0,x0+r.[ by RCOMP_1:def 2; hence g in dom f by A3;
end; hence ex g st g<r1 & x0<g & g in dom f;
end; hence ex g st g<r1 & x0<g & g in dom f;
end; hence thesis by A1,A2,A4,A5,Th73;
end;
theorem
f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0 & (ex r st 0<r &
((dom f1 /\ ].x0-r,x0.[ c= dom f2 /\ ].x0-r,x0.[ &
for g st g in dom f1 /\ ].x0-r,x0.[ holds f1.g<=f2.g) or
(dom f2 /\ ].x0-r,x0.[ c= dom f1 /\ ].x0-r,x0.[ &
for g st g in dom f2 /\ ].x0-r,x0.[ holds f1.g<=f2.g))) implies
lim_left(f1,x0)<=lim_left(f2,x0)
proof assume A1: f1 is_left_convergent_in x0 & f2 is_left_convergent_in x0;
given r such that A2: 0<r and
A3: (dom f1/\].x0-r,x0.[c=dom f2/\].x0-r,x0.[ &
for g st g in dom f1/\].x0-r,x0.[ holds f1.g<=f2.g) or
(dom f2/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ &
for g st g in dom f2/\].x0-r,x0.[ holds f1.g<=f2.g);
A4: lim_left(f1,x0)=lim_left(f1,x0) & lim_left(f2,x0)=lim_left(f2,x0);
now per cases by A3;
suppose A5: dom f1/\].x0-r,x0.[c=dom f2/\].x0-r,x0.[ &
for g st g in dom f1/\].x0-r,x0.[ holds f1.g<=f2.g;
defpred X[Nat,real number] means x0-1/($1+1)<$2 &
$2<x0 & $2 in dom f1;
A6: now let n; x0-1/(n+1)<x0 by Lm3; then consider g such that
A7: x0-1/(n+1)<g & g<x0 & g in dom f1 by A1,Def1;
reconsider g as real number;
take g;
thus X[n,g] by A7;
end; consider s be Real_Sequence such that
A8: for n holds X[n,s.n] from RealSeqChoice(A6);
A9: s is convergent & lim s=x0 & rng s c=dom f1/\left_open_halfline(x0)
by A8,Th5; x0-r<x0 by A2,Lm1; then consider k such that
A10: for n st k<=n holds x0-r<s.n by A9,Th1;
A11: s^\k is convergent & lim(s^\k)=x0 by A9,SEQ_4:33;
rng(s^\k)c=rng s by RFUNCT_2:7;
then rng(s^\k)c=dom f1/\left_open_halfline(x0) by A9,XBOOLE_1:1;
then A12: f1*(s^\k) is convergent & lim(f1*(s^\k))=lim_left(f1,x0) by A1,A4,
A11,Def7;
now let x be set; assume x in rng(s^\k); then consider n such that
A13: (s^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then x0-r<s.(n+k) by A10; then A14: x0-r<(s^\k).n by SEQM_3:def 9;
s.(n+k)<x0 & s.(n+k) in dom f1 by A8;
then A15: (s^\k).n<x0 & (s^\k).n in dom f1 by SEQM_3:def 9;
then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A14; then (s^\k).n in ].x0-r,x0
.[
by RCOMP_1:def 2;
hence x in dom f1/\].x0-r,x0.[ by A13,A15,XBOOLE_0:def 3;
end; then A16: rng(s^\k)c=dom f1/\].x0-r,x0.[ by TARSKI:def 3;
then A17: rng(s^\k)c=dom f2/\].x0-r,x0.[ by A5,XBOOLE_1:1;
dom f2/\].x0-r,x0.[c=dom f2 & dom f2/\
].x0-r,x0.[c=].x0-r,x0.[ by XBOOLE_1:17;
then A18: rng(s^\k)c=dom f2 & rng(s^\k)c=].x0-r,x0.[ by A17,XBOOLE_1:1;
].x0-r,x0.[c=left_open_halfline(x0) by LIMFUNC1:16;
then rng(s^\k)c=left_open_halfline(x0) by A18,XBOOLE_1:1;
then rng(s^\k)c=dom f2/\left_open_halfline(x0) by A18,XBOOLE_1:19;
then A19: f2*(s^\k) is convergent & lim(f2*(s^\k))=lim_left(f2,x0) by A1,A4,
A11,Def7;
dom f1/\].x0-r,x0.[c=dom f1 by XBOOLE_1:17;
then A20: rng(s^\k)c=dom f1 by A16,XBOOLE_1:1;
now let n; (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then f1.((s^\k).n)<=f2.((s^\k).n) by A5,A16;
then f1.((s^\k).n)<=(f2*(s^\k)).n by A18,RFUNCT_2:21;
hence (f1*(s^\k)).n<=(f2*(s^\k)).n by A20,RFUNCT_2:21;
end; hence thesis by A12,A19,SEQ_2:32;
suppose A21: dom f2/\].x0-r,x0.[c=dom f1/\].x0-r,x0.[ &
for g st g in dom f2/\].x0-r,x0.[ holds f1.g<=f2.g;
defpred X[Nat,real number] means x0-1/($1+1)<$2 &
$2<x0 & $2 in dom f2;
A22: now let n;
0<n+1 by NAT_1:19;
then 0<1/(n+1) by SEQ_2:6; then x0-1/(n+1)<x0-0 by REAL_1:92;
then consider g such that
A23: x0-1/(n+1)<g & g<x0 & g in dom f2 by A1,Def1;
reconsider g as real number;
take g;
thus X[n,g] by A23;
end; consider s be Real_Sequence such that
A24: for n holds X[n,s.n] from RealSeqChoice(A22
);
A25: s is convergent & lim s=x0 & rng s c=dom f2/\left_open_halfline(x0)
by A24,Th5; x0-r<x0 by A2,Lm1; then consider k such that A26:
for n st k<=n holds x0-r<s.n by A25,Th1;
A27: s^\k is convergent & lim(s^\k)=x0 by A25,SEQ_4:33;
rng(s^\k)c=rng s by RFUNCT_2:7;
then rng(s^\k)c=dom f2/\left_open_halfline(x0) by A25,XBOOLE_1:1;
then A28: f2*(s^\k) is convergent & lim(f2*(s^\k))=lim_left(f2,x0) by A1,A4,
A27,Def7;
A29: now let x be set; assume x in rng(s^\k); then consider n such that
A30: (s^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then x0-r<s.(n+k) by A26; then A31: x0-r<(s^\k).n by SEQM_3:def 9;
s.(n+k)<x0 & s.(n+k) in dom f2 by A24;
then A32: (s^\k).n<x0 & (s^\k).n in dom f2 by SEQM_3:def 9;
then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A31; then (s^\k).n in ].x0-r,x0
.[
by RCOMP_1:def 2;
hence x in dom f2/\].x0-r,x0.[ by A30,A32,XBOOLE_0:def 3;
end; then A33: rng(s^\k)c=dom f2/\].x0-r,x0.[ by TARSKI:def 3;
then A34: rng(s^\k)c=dom f1/\].x0-r,x0.[ by A21,XBOOLE_1:1;
dom f1/\].x0-r,x0.[c=dom f1 & dom f1/\
].x0-r,x0.[c=].x0-r,x0.[ by XBOOLE_1:17;
then A35: rng(s^\k)c=dom f1 & rng(s^\k)c=].x0-r,x0.[ by A34,XBOOLE_1:1;
].x0-r,x0.[c=left_open_halfline(x0) by LIMFUNC1:16;
then rng(s^\k)c=left_open_halfline(x0) by A35,XBOOLE_1:1;
then rng(s^\k)c=dom f1/\left_open_halfline(x0) by A35,XBOOLE_1:19;
then A36: f1*(s^\k) is convergent & lim(f1*(s^\k))=lim_left(f1,x0) by A1,A4,
A27,Def7;
dom f2/\].x0-r,x0.[c=dom f2 by XBOOLE_1:17;
then A37: rng(s^\k)c=dom f2 by A33,XBOOLE_1:1;
now let n; (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in dom f2/\].x0-r,x0.[ by A29;
then f1.((s^\k).n)<=f2.((s^\k).n) by A21;
then f1.((s^\k).n)<=(f2*(s^\k)).n by A37,RFUNCT_2:21;
hence (f1*(s^\k)).n<=(f2*(s^\k)).n by A35,RFUNCT_2:21;
end; hence thesis by A28,A36,SEQ_2:32;
end; hence thesis;
end;
theorem
f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0 & (ex r st 0<r &
((dom f1 /\ ].x0,x0+r.[ c= dom f2 /\ ].x0,x0+r.[ &
for g st g in dom f1 /\ ].x0,x0+r.[ holds f1.g<=f2.g) or
(dom f2 /\ ].x0,x0+r.[ c= dom f1 /\ ].x0,x0+r.[ &
for g st g in dom f2 /\ ].x0,x0+r.[ holds f1.g<=f2.g))) implies
lim_right(f1,x0)<=lim_right(f2,x0)
proof assume A1: f1 is_right_convergent_in x0 & f2 is_right_convergent_in x0;
given r such that A2: 0<r and
A3: (dom f1/\].x0,x0+r.[c=dom f2/\].x0,x0+r.[ &
for g st g in dom f1/\].x0,x0+r.[ holds f1.g<=f2.g) or
(dom f2/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ &
for g st g in dom f2/\].x0,x0+r.[ holds f1.g<=f2.g);
A4: lim_right(f1,x0)=lim_right(f1,x0) & lim_right(f2,x0)=lim_right(f2,x0);
now per cases by A3;
suppose A5: dom f1/\].x0,x0+r.[c=dom f2/\].x0,x0+r.[ &
for g st g in dom f1/\].x0,x0+r.[ holds f1.g<=f2.g;
defpred X[Nat,real number] means x0<$2 & $2<x0+1/($1+1) &
$2 in dom f1;
A6: now let n; x0<x0+1/(n+1) by Lm3; then consider g such that
A7: g<x0+(1/(n+1)) & x0<g & g in dom f1 by A1,Def4;
reconsider g as real number;
take g;
thus X[n,g] by A7;
end; consider s be Real_Sequence such that
A8: for n holds X[n,s.n] from RealSeqChoice(A6);
A9: s is convergent & lim s=x0 & rng s c=dom f1/\right_open_halfline(x0)
by A8,Th6; x0<x0+r by A2,Lm1; then consider k such that
A10: for n st k<=n holds s.n<x0+r by A9,Th2;
A11: s^\k is convergent & lim(s^\k)=x0 by A9,SEQ_4:33;
rng(s^\k)c=rng s by RFUNCT_2:7;
then rng(s^\k)c=dom f1/\right_open_halfline(x0) by A9,XBOOLE_1:1;
then A12: f1*(s^\k) is convergent & lim(f1*(s^\k))=lim_right(f1,x0)
by A1,A4,A11,Def8;
now let x be set; assume x in rng(s^\k); then consider n such that
A13: (s^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then s.(n+k)<x0+r by A10; then A14: (s^\k).n<x0+r by SEQM_3:def 9;
x0<s.(n+k) & s.(n+k) in dom f1 by A8;
then A15: x0<(s^\k).n & (s^\k).n in dom f1 by SEQM_3:def 9;
then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A14; then (s^\k).n in ].x0,x0+r
.[
by RCOMP_1:def 2;
hence x in dom f1/\].x0,x0+r.[ by A13,A15,XBOOLE_0:def 3;
end; then A16: rng(s^\k)c=dom f1/\].x0,x0+r.[ by TARSKI:def 3;
then A17: rng(s^\k)c=dom f2/\].x0,x0+r.[ by A5,XBOOLE_1:1;
dom f2/\].x0,x0+r.[c=dom f2 & dom f2/\
].x0,x0+r.[c=].x0,x0+r.[ by XBOOLE_1:17;
then A18: rng(s^\k)c=dom f2 & rng(s^\k)c=].x0,x0+r.[ by A17,XBOOLE_1:1;
].x0,x0+r.[c=right_open_halfline(x0) by LIMFUNC1:11;
then rng(s^\k)c=right_open_halfline(x0) by A18,XBOOLE_1:1;
then rng(s^\k)c=dom f2/\right_open_halfline(x0) by A18,XBOOLE_1:19;
then A19: f2*(s^\k) is convergent & lim(f2*(s^\k))=lim_right(f2,x0)
by A1,A4,A11,Def8;
dom f1/\].x0,x0+r.[c=dom f1 by XBOOLE_1:17;
then A20: rng(s^\k)c=dom f1 by A16,XBOOLE_1:1;
now let n; (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then f1.((s^\k).n)<=f2.((s^\k).n) by A5,A16;
then f1.((s^\k).n)<=(f2*(s^\k)).n by A18,RFUNCT_2:21;
hence (f1*(s^\k)).n<=(f2*(s^\k)).n by A20,RFUNCT_2:21;
end; hence thesis by A12,A19,SEQ_2:32;
suppose A21: dom f2/\].x0,x0+r.[c=dom f1/\].x0,x0+r.[ &
for g st g in dom f2/\].x0,x0+r.[ holds f1.g<=f2.g;
defpred X[Nat,real number] means x0<$2 & $2<x0+1/($1+1) & $2 in dom f2;
A22: now let n;
0<n+1 by NAT_1:19;
then 0<1/(n+1) by SEQ_2:6; then x0+0<x0+1/(n+1) by REAL_1:67;
then consider g such that
A23: g<x0+(1/(n+1)) & x0<g & g in dom f2 by A1,Def4;
reconsider g as real number;
take g;
thus X[n,g] by A23;
end;
consider s be Real_Sequence such that
A24: for n holds X[n,s.n] from RealSeqChoice(A22);
A25: s is convergent & lim s=x0 & rng s c=dom f2/\right_open_halfline(x0)
by A24,Th6; x0<x0+r by A2,Lm1; then consider k such that
A26: for n st k<=n holds s.n<x0+r by A25,Th2;
A27: s^\k is convergent & lim(s^\k)=x0 by A25,SEQ_4:33;
rng(s^\k)c=rng s by RFUNCT_2:7;
then rng(s^\k)c=dom f2/\right_open_halfline(x0) by A25,XBOOLE_1:1;
then A28: f2*(s^\k) is convergent & lim(f2*(s^\k))=lim_right(f2,x0)
by A1,A4,A27,Def8;
A29: now let x be set; assume x in rng(s^\k); then consider n such that
A30: (s^\k).n=x by RFUNCT_2:9; k<=n+k by NAT_1:37;
then s.(n+k)<x0+r by A26; then A31: (s^\k).n<x0+r by SEQM_3:def 9;
x0<s.(n+k) & s.(n+k) in dom f2 by A24;
then A32: x0<(s^\k).n & (s^\k).n in dom f2 by SEQM_3:def 9;
then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A31; then (s^\k).n in ].x0,x0+r
.[
by RCOMP_1:def 2;
hence x in dom f2/\].x0,x0+r.[ by A30,A32,XBOOLE_0:def 3;
end; then A33: rng(s^\k)c=dom f2/\].x0,x0+r.[ by TARSKI:def 3;
then A34: rng(s^\k)c=dom f1/\].x0,x0+r.[ by A21,XBOOLE_1:1;
dom f1/\].x0,x0+r.[c=dom f1 & dom f1/\
].x0,x0+r.[c=].x0,x0+r.[ by XBOOLE_1:17;
then A35: rng(s^\k)c=dom f1 & rng(s^\k)c=].x0,x0+r.[ by A34,XBOOLE_1:1;
].x0,x0+r.[c=right_open_halfline(x0) by LIMFUNC1:11;
then rng(s^\k)c=right_open_halfline(x0) by A35,XBOOLE_1:1;
then rng(s^\k)c=dom f1/\right_open_halfline(x0) by A35,XBOOLE_1:19;
then A36: f1*(s^\k) is convergent & lim(f1*(s^\k))=lim_right(f1,x0)
by A1,A4,A27,Def8;
dom f2/\].x0,x0+r.[c=dom f2 by XBOOLE_1:17;
then A37: rng(s^\k)c=dom f2 by A33,XBOOLE_1:1;
now let n; (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in dom f2/\].x0,x0+r.[ by A29;
then f1.((s^\k).n)<=f2.((s^\k).n) by A21;
then f1.((s^\k).n)<=(f2*(s^\k)).n by A37,RFUNCT_2:21;
hence (f1*(s^\k)).n<=(f2*(s^\k)).n by A35,RFUNCT_2:21;
end; hence thesis by A28,A36,SEQ_2:32;
end; hence thesis;
end;
theorem
(f is_left_divergent_to+infty_in x0 or f is_left_divergent_to-infty_in x0) &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) implies
f^ is_left_convergent_in x0 & lim_left(f^,x0)=0
proof assume A1: f is_left_divergent_to+infty_in x0 or
f is_left_divergent_to-infty_in x0;
assume A2: for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
A3: now let r; assume r<x0; then consider g such that
A4: r<g & g<x0 & g in dom f & f.g<>0 by A2; take g; thus r<g & g<x0 by A4;
not f.g in {0} by A4,TARSKI:def 1; then not g in f"{0} by FUNCT_1:def 13
;
then g in dom f\f"{0} by A4,XBOOLE_0:def 4; hence g in dom(f^) by RFUNCT_1:
def 8;
end;
A5: now let seq such that A6: seq is convergent & lim seq=x0 &
rng seq c=dom(f^)/\left_open_halfline(x0);
dom(f^)/\left_open_halfline(x0)c=dom(f^) &
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A7: rng seq c=dom(f^) & rng seq c=left_open_halfline(x0) by A6,XBOOLE_1:
1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8
;
then dom(f^)c=dom f by XBOOLE_1:36; then rng seq c=dom f by A7,XBOOLE_1:1;
then A8: rng seq c=dom f/\left_open_halfline(x0) by A7,XBOOLE_1:19;
now per cases by A1;
suppose f is_left_divergent_to+infty_in x0;
then f*seq is divergent_to+infty by A6,A8,Def2;
then (f*seq)" is convergent & lim((f*seq)")=0 by LIMFUNC1:61;
hence (f^)*seq is convergent & lim((f^)*seq)=0 by A7,RFUNCT_2:27;
suppose f is_left_divergent_to-infty_in x0;
then f*seq is divergent_to-infty by A6,A8,Def3;
then (f*seq)" is convergent & lim((f*seq)")=0 by LIMFUNC1:61;
hence (f^)*seq is convergent & lim((f^)*seq)=0 by A7,RFUNCT_2:27;
end; hence (f^)*seq is convergent & lim((f^)*seq)=0;
end; hence f^ is_left_convergent_in x0 by A3,Def1;
hence thesis by A5,Def7;
end;
theorem
(f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0)
&
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) implies
f^ is_right_convergent_in x0 & lim_right(f^,x0)=0
proof assume A1: f is_right_divergent_to+infty_in x0 or
f is_right_divergent_to-infty_in x0;
assume A2: for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
A3: now let r; assume x0<r; then consider g such that
A4: g<r & x0<g & g in dom f & f.g<>0 by A2; take g; thus g<r & x0<g by A4;
not f.g in {0} by A4,TARSKI:def 1; then not g in f"{0} by FUNCT_1:def 13
;
then g in dom f\f"{0} by A4,XBOOLE_0:def 4; hence g in dom(f^) by RFUNCT_1:
def 8;
end;
A5: now let seq such that A6: seq is convergent & lim seq=x0 &
rng seq c=dom(f^)/\right_open_halfline(x0);
dom(f^)/\right_open_halfline(x0)c=dom(f^) &
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17
;
then A7: rng seq c=dom(f^) & rng seq c=right_open_halfline(x0) by A6,XBOOLE_1
:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8
;
then dom(f^)c=dom f by XBOOLE_1:36; then rng seq c=dom f by A7,XBOOLE_1:1;
then A8: rng seq c=dom f/\right_open_halfline(x0) by A7,XBOOLE_1:19;
now per cases by A1;
suppose f is_right_divergent_to+infty_in x0;
then f*seq is divergent_to+infty by A6,A8,Def5;
then (f*seq)" is convergent & lim((f*seq)")=0 by LIMFUNC1:61;
hence (f^)*seq is convergent & lim((f^)*seq)=0 by A7,RFUNCT_2:27;
suppose f is_right_divergent_to-infty_in x0;
then f*seq is divergent_to-infty by A6,A8,Def6;
then (f*seq)" is convergent & lim((f*seq)")=0 by LIMFUNC1:61;
hence (f^)*seq is convergent & lim((f^)*seq)=0 by A7,RFUNCT_2:27;
end; hence (f^)*seq is convergent & lim((f^)*seq)=0;
end; hence f^ is_right_convergent_in x0 by A3,Def4; hence thesis by A5,Def8;
end;
theorem
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds 0<f.g) implies
f^ is_left_divergent_to+infty_in x0
proof assume A1: f is_left_convergent_in x0 & lim_left(f,x0)=0;
given r such that A2: 0<r & for g st g in dom f/\].x0-r,x0.[ holds 0<f.g;
thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
proof let r1; assume r1<x0; then consider g1 such that
A3: r1<g1 & g1<x0 & g1 in dom f by A1,Def1;
now per cases;
suppose A4: g1<=x0-r; x0-r<x0 by A2,Lm1; then consider g2 such that
A5: x0-r<g2 & g2<x0 & g2 in dom f by A1,Def1; take g2;
g1<g2 by A4,A5,AXIOMS:22; hence r1<g2 & g2<x0 by A3,A5,AXIOMS:22;
g2 in {r2: x0-r<r2 & r2<x0} by A5;
then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0-r,x0.[ 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: x0-r<=g1; consider g2 such that
A7: g1<g2 & g2<x0 & g2 in dom f by A1,A3,Def1; take g2;
thus r1<g2 & g2<x0 by A3,A7,AXIOMS:22; x0-r<g2 by A6,A7,AXIOMS:22;
then g2 in {r2: x0-r<r2 & r2<x0} by A7;
then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0-r,x0.[ 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 such that A8: s is convergent & lim s=x0 &
rng s c=dom(f^)/\left_open_halfline(x0); x0-r<x0 by A2,Lm1;
then consider k such that A9: for n st k<=n holds x0-r<s.n by A8,Th1;
A10: s^\k is convergent & lim(s^\k)=x0 by A8,SEQ_4:33;
dom(f^)/\left_open_halfline(x0)c=dom(f^) &
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A11: rng s c=dom(f^) & rng s c=left_open_halfline(x0) by A8,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A13: rng(s^\k)c=dom (f^)/\left_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=left_open_halfline(x0) & rng(s^\k)c=dom f by A8,A11,A12,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\left_open_halfline(x0) by XBOOLE_1:19;
then A14: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def7;
A15: now let n; A16: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in left_open_halfline(x0) by A13;
then (s^\k).n in {g1: g1<x0} by PROB_1:def 15; then A17:
ex g1 st g1=(s^\k).n & g1<x0; k<=n+k by NAT_1:37
; then x0-r<s.(n+k) by A9;
then x0-r<(s^\k).n by SEQM_3:def 9
; then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A17;
then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0-r,x0.[ by A13,A16,XBOOLE_0:def 3
; then 0<f.((s^\k).n) by A2;
hence 0<(f*(s^\k)).n by A13,RFUNCT_2:21;
end; then for n holds 0<>(f*(s^\k)).n; then A18: f*(s^\k) is_not_0 by SEQ_1:7
;
for n holds 0<=n implies 0<(f*(s^\k)).n by A15;
then A19: (f*(s^\k))" is divergent_to+infty by A14,A18,LIMFUNC1:62;
(f*(s^\k))"=((f*s)^\k)" by A12,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A11,RFUNCT_2:27; hence thesis by A19,LIMFUNC1:34;
end;
theorem
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds f.g<0) implies
f^ is_left_divergent_to-infty_in x0
proof assume A1: f is_left_convergent_in x0 & lim_left(f,x0)=0;
given r such that A2: 0<r & for g st g in dom f/\].x0-r,x0.[ holds f.g<0;
thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
proof let r1; assume r1<x0; then consider g1 such that
A3: r1<g1 & g1<x0 & g1 in dom f by A1,Def1;
now per cases;
suppose A4: g1<=x0-r; x0-r<x0 by A2,Lm1; then consider g2 such that
A5: x0-r<g2 & g2<x0 & g2 in dom f by A1,Def1; take g2;
g1<g2 by A4,A5,AXIOMS:22; hence r1<g2 & g2<x0 by A3,A5,AXIOMS:22;
g2 in {r2: x0-r<r2 & r2<x0} by A5;
then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0-r,x0.[ 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: x0-r<=g1; consider g2 such that
A7: g1<g2 & g2<x0 & g2 in dom f by A1,A3,Def1; take g2;
thus r1<g2 & g2<x0 by A3,A7,AXIOMS:22; x0-r<g2 by A6,A7,AXIOMS:22;
then g2 in {r2: x0-r<r2 & r2<x0} by A7;
then g2 in ].x0-r,x0.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0-r,x0.[ 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 such that A8: s is convergent & lim s=x0 &
rng s c=dom(f^)/\left_open_halfline(x0); x0-r<x0 by A2,Lm1;
then consider k such that A9: for n st k<=n holds x0-r<s.n by A8,Th1;
A10: s^\k is convergent & lim(s^\k)=x0 by A8,SEQ_4:33;
dom(f^)/\left_open_halfline(x0)c=dom(f^) &
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A11: rng s c=dom(f^) & rng s c=left_open_halfline(x0) by A8,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A13: rng(s^\k)c=dom (f^)/\left_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=left_open_halfline(x0) & rng(s^\k)c=dom f by A8,A11,A12,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\left_open_halfline(x0) by XBOOLE_1:19;
then A14: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def7;
A15: now let n; A16: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in left_open_halfline(x0) by A13;
then (s^\k).n in {g1: g1<x0} by PROB_1:def 15; then A17:
ex g1 st g1=(s^\k).n & g1<x0; k<=n+k by NAT_1:37
; then x0-r<s.(n+k) by A9;
then x0-r<(s^\k).n by SEQM_3:def 9
; then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A17;
then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0-r,x0.[ by A13,A16,XBOOLE_0:def 3
; then f.((s^\k).n)<0 by A2;
hence (f*(s^\k)).n<0 by A13,RFUNCT_2:21;
end; then for n holds 0<>(f*(s^\k)).n; then A18: f*(s^\k) is_not_0 by SEQ_1:7
;
for n holds 0<=n implies (f*(s^\k)).n<0 by A15;
then A19: (f*(s^\k))" is divergent_to-infty by A14,A18,LIMFUNC1:63;
(f*(s^\k))"=((f*s)^\k)" by A12,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A11,RFUNCT_2:27; hence thesis by A19,LIMFUNC1:34;
end;
theorem
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds 0<f.g) implies
f^ is_right_divergent_to+infty_in x0
proof assume A1: f is_right_convergent_in x0 & lim_right(f,x0)=0;
given r such that A2: 0<r & for g st g in dom f/\].x0,x0+r.[ holds 0<f.g;
thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
proof let r1; assume x0<r1; then consider g1 such that
A3: g1<r1 & x0<g1 & g1 in dom f by A1,Def4;
now per cases;
suppose A4: g1<=x0+r; consider g2 such that
A5: g2<g1 & x0<g2 & g2 in dom f by A1,A3,Def4; take g2;
thus g2<r1 & x0<g2 by A3,A5,AXIOMS:22; g2<x0+r by A4,A5,AXIOMS:22;
then g2 in {r2: x0<r2 & r2<x0+r} by A5;
then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0,x0+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: x0+r<=g1; x0<x0+r by A2,Lm1; then consider g2 such that
A7: g2<x0+r & x0<g2 & g2 in dom f by A1,Def4; take g2;
g2<g1 by A6,A7,AXIOMS:22; hence g2<r1 & x0<g2 by A3,A7,AXIOMS:22;
g2 in {r2: x0<r2 & r2<x0+r} by A7;
then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0,x0+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 such that A8: s is convergent & lim s=x0 &
rng s c=dom(f^)/\right_open_halfline(x0); x0<x0+r by A2,Lm1;
then consider k such that A9: for n st k<=n holds s.n<x0+r by A8,Th2;
A10: s^\k is convergent & lim(s^\k)=x0 by A8,SEQ_4:33;
dom(f^)/\right_open_halfline(x0)c=dom(f^) &
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A11: rng s c=dom(f^) & rng s c=right_open_halfline(x0) by A8,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A12: rng s c=dom f by A11,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A13: rng(s^\k)c=dom (f^)/\right_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=right_open_halfline(x0) & rng(s^\k)c=dom f by A8,A11,A12,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\right_open_halfline(x0) by XBOOLE_1:19;
then A14: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def8;
A15: now let n; A16: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in right_open_halfline(x0) by A13;
then (s^\k).n in {g1: x0<g1} by LIMFUNC1:def 3; then A17:
ex g1 st g1=(s^\k).n & x0<g1; k<=n+k by NAT_1:37
; then s.(n+k)<x0+r by A9;
then (s^\k).n<x0+r by SEQM_3:def 9
; then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A17;
then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0,x0+r.[ by A13,A16,XBOOLE_0:def 3
; then 0<f.((s^\k).n) by A2;
hence 0<(f*(s^\k)).n by A13,RFUNCT_2:21;
end;
then for n holds 0<>(f*(s^\k)).n;
then A18: f*(s^\k) is_not_0 by SEQ_1:7;
for n holds 0<=n implies 0<(f*(s^\k)).n by A15;
then A19: (f*(s^\k))" is divergent_to+infty by A14,A18,LIMFUNC1:62;
(f*(s^\k))"=((f*s)^\k)" by A12,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A11,RFUNCT_2:27; hence thesis by A19,LIMFUNC1:34;
end;
theorem
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds f.g<0) implies
f^ is_right_divergent_to-infty_in x0
proof assume A1: f is_right_convergent_in x0 & lim_right(f,x0)=0;
given r such that A2: 0<r & for g st g in dom f/\].x0,x0+r.[ holds f.g<0;
thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
proof let r1; assume x0<r1; then consider g1 such that
A3: g1<r1 & x0<g1 & g1 in dom f by A1,Def4;
now per cases;
suppose A4: g1<=x0+r; consider g2 such that
A5: g2<g1 & x0<g2 & g2 in dom f by A1,A3,Def4; take g2;
thus g2<r1 & x0<g2 by A3,A5,AXIOMS:22; g2<x0+r by A4,A5,AXIOMS:22;
then g2 in {r2: x0<r2 & r2<x0+r} by A5;
then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0,x0+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: x0+r<=g1; x0<x0+r by A2,Lm1; then consider g2 such that
A7: g2<x0+r & x0<g2 & g2 in dom f by A1,Def4; take g2;
g2<g1 by A6,A7,AXIOMS:22; hence g2<r1 & x0<g2 by A3,A7,AXIOMS:22;
g2 in {r2: x0<r2 & r2<x0+r} by A7;
then g2 in ].x0,x0+r.[ by RCOMP_1:def 2;
then g2 in dom f/\].x0,x0+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 such that A8: s is convergent & lim s=x0 &
rng s c=dom(f^)/\right_open_halfline(x0); x0<x0+r by A2,Lm1;
then consider k such that A9: for n st k<=n holds s.n<x0+r by A8,Th2;
A10: s^\k is convergent & lim(s^\k)=x0 by A8,SEQ_4:33;
dom(f^)/\right_open_halfline(x0)c=dom(f^) &
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A11: rng s c=dom(f^) & rng s c=right_open_halfline(x0) by A8,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A12: rng s c=dom f by A11,XBOOLE_1:1; rng(s^\k)c=rng s by RFUNCT_2:7;
then A13: rng(s^\k)c=dom (f^)/\right_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=right_open_halfline(x0) & rng(s^\k)c=dom f by A8,A11,A12,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\right_open_halfline(x0) by XBOOLE_1:19;
then A14: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A10,Def8;
A15: now let n; A16: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in right_open_halfline(x0) by A13;
then (s^\k).n in {g1: x0<g1} by LIMFUNC1:def 3; then A17:
ex g1 st g1=(s^\k).n & x0<g1; k<=n+k by NAT_1:37
; then s.(n+k)<x0+r by A9;
then (s^\k).n<x0+r by SEQM_3:def 9
; then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A17;
then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0,x0+r.[ by A13,A16,XBOOLE_0:def 3
; then f.((s^\k).n)<0 by A2;
hence (f*(s^\k)).n<0 by A13,RFUNCT_2:21;
end; then for n holds 0<>(f*(s^\k)).n;
then A18: f*(s^\k) is_not_0 by SEQ_1:7;
for n holds 0<=n implies (f*(s^\k)).n<0 by A15;
then A19: (f*(s^\k))" is divergent_to-infty by A14,A18,LIMFUNC1:63;
(f*(s^\k))"=((f*s)^\k)" by A12,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A11,RFUNCT_2:27; hence thesis by A19,LIMFUNC1:34;
end;
theorem
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds 0<=f.g) implies
f^ is_left_divergent_to+infty_in x0
proof assume A1: f is_left_convergent_in x0 & lim_left(f,x0)=0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
given r such that A2: 0<r & for g st g in dom f/\].x0-r,x0.[ holds 0<=f.g;
thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
proof let r1; assume r1<x0; then consider g1 such that
A3: r1<g1 & g1<x0 & g1 in dom f & f.g1<>0 by A1; take g1;
thus r1<g1 & g1<x0 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 such that A4: s is convergent & lim s=x0 &
rng s c=dom(f^)/\left_open_halfline(x0); x0-r<x0 by A2,Lm1;
then consider k such that A5: for n st k<=n holds x0-r<s.n by A4,Th1;
A6: s^\k is convergent & lim(s^\k)=x0 by A4,SEQ_4:33;
dom (f^)/\left_open_halfline(x0)c=dom(f^) &
dom (f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A7: rng s c=dom(f^) & rng s c=left_open_halfline(x0) by A4,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A8: rng s c=dom f by A7,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A9: rng(s^\k)c=dom (f^)/\left_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=left_open_halfline(x0) & rng(s^\k)c=dom f by A4,A7,A8,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\left_open_halfline(x0) by XBOOLE_1:19;
then A10: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def7;
A11: f*(s^\k) is_not_0 by A9,RFUNCT_2:26;
A12: now let n; A13: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in left_open_halfline(x0) by A9;
then (s^\k).n in {g1: g1<x0} by PROB_1:def 15; then A14:
ex g1 st g1=(s^\k).n & g1<x0; k<=n+k by NAT_1:37
; then x0-r<s.(n+k) by A5;
then x0-r<(s^\k).n by SEQM_3:def 9
; then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A14;
then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0-r,x0.[ by A9,A13,XBOOLE_0:def 3
; then A15: 0<=f.((s^\k).n) by A2
; (f*(s^\k)).n<>0 by A11,SEQ_1:7;
hence 0<(f*(s^\k)).n by A9,A15,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 A12;
then A17: (f*(s^\k))" is divergent_to+infty by A10,A16,LIMFUNC1:62;
(f*(s^\k))"=((f*s)^\k)" by A8,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A7,RFUNCT_2:27; hence thesis by A17,LIMFUNC1:34;
end;
theorem
f is_left_convergent_in x0 & lim_left(f,x0)=0 &
(for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0-r,x0.[ holds f.g<=0) implies
f^ is_left_divergent_to-infty_in x0
proof assume A1: f is_left_convergent_in x0 & lim_left(f,x0)=0 &
for r st r<x0 ex g st r<g & g<x0 & g in dom f & f.g<>0;
given r such that A2: 0<r & for g st g in dom f/\].x0-r,x0.[ holds f.g<=0;
thus for r1 st r1<x0 ex g1 st r1<g1 & g1<x0 & g1 in dom(f^)
proof let r1; assume r1<x0; then consider g1 such that
A3: r1<g1 & g1<x0 & g1 in dom f & f.g1<>0 by A1; take g1;
thus r1<g1 & g1<x0 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 such that A4: s is convergent & lim s=x0 &
rng s c=dom(f^)/\left_open_halfline(x0); x0-r<x0 by A2,Lm1;
then consider k such that A5: for n st k<=n holds x0-r<s.n by A4,Th1;
A6: s^\k is convergent & lim(s^\k)=x0 by A4,SEQ_4:33;
dom(f^)/\left_open_halfline(x0)c=dom(f^) &
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then A7: rng s c=dom(f^) & rng s c=left_open_halfline(x0) by A4,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A8: rng s c=dom f by A7,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A9: rng(s^\k)c=dom (f^)/\left_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=left_open_halfline(x0) & rng(s^\k)c=dom f by A4,A7,A8,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\left_open_halfline(x0) by XBOOLE_1:19;
then A10: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def7;
A11: f*(s^\k) is_not_0 by A9,RFUNCT_2:26;
A12: now let n; A13: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in left_open_halfline(x0) by A9;
then (s^\k).n in {g1: g1<x0} by PROB_1:def 15; then A14:
ex g1 st g1=(s^\k).n & g1<x0; k<=n+k by NAT_1:37
; then x0-r<s.(n+k) by A5;
then x0-r<(s^\k).n by SEQM_3:def 9
; then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A14;
then (s^\k).n in ].x0-r,x0.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0-r,x0.[ by A9,A13,XBOOLE_0:def 3
; then A15: f.((s^\k).n)<=0 by A2
; (f*(s^\k)).n<>0 by A11,SEQ_1:7;
hence (f*(s^\k)).n<0 by A9,A15,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 A12;
then A17: (f*(s^\k))" is divergent_to-infty by A10,A16,LIMFUNC1:63;
(f*(s^\k))"=((f*s)^\k)" by A8,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A7,RFUNCT_2:27; hence thesis by A17,LIMFUNC1:34;
end;
theorem
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds 0<=f.g) implies
f^ is_right_divergent_to+infty_in x0
proof assume A1: f is_right_convergent_in x0 & lim_right(f,x0)=0 &
for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
given r such that A2: 0<r & for g st g in dom f/\].x0,x0+r.[ holds 0<=f.g;
thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
proof let r1; assume x0<r1; then consider g1 such that
A3: g1<r1 & x0<g1 & g1 in dom f & f.g1<>0 by A1; take g1;
thus g1<r1 & x0<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 such that A4: s is convergent & lim s=x0 &
rng s c=dom(f^)/\right_open_halfline(x0); x0<x0+r by A2,Lm1;
then consider k such that A5: for n st k<=n holds s.n<x0+r by A4,Th2;
A6: s^\k is convergent & lim(s^\k)=x0 by A4,SEQ_4:33;
dom(f^)/\right_open_halfline(x0)c=dom(f^) &
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A7: rng s c=dom(f^) & rng s c=right_open_halfline(x0) by A4,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A8: rng s c=dom f by A7,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A9: rng(s^\k)c=dom (f^)/\right_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=right_open_halfline(x0) & rng(s^\k)c=dom f by A4,A7,A8,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\right_open_halfline(x0) by XBOOLE_1:19;
then A10: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def8;
A11: f*(s^\k) is_not_0 by A9,RFUNCT_2:26;
A12: now let n; A13: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in right_open_halfline(x0) by A9;
then (s^\k).n in {g1: x0<g1} by LIMFUNC1:def 3; then A14:
ex g1 st g1=(s^\k).n & x0<g1; k<=n+k by NAT_1:37
; then s.(n+k)<x0+r by A5;
then (s^\k).n<x0+r by SEQM_3:def 9
; then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A14;
then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0,x0+r.[ by A9,A13,XBOOLE_0:def 3
; then A15: 0<=f.((s^\k).n) by A2
; 0<>(f*(s^\k)).n by A11,SEQ_1:7;
hence 0<(f*(s^\k)).n by A9,A15,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 A12;
then A17: (f*(s^\k))" is divergent_to+infty by A10,A16,LIMFUNC1:62;
(f*(s^\k))"=((f*s)^\k)" by A8,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A7,RFUNCT_2:27; hence thesis by A17,LIMFUNC1:34;
end;
theorem
f is_right_convergent_in x0 & lim_right(f,x0)=0 &
(for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0) &
(ex r st 0<r & for g st g in dom f /\ ].x0,x0+r.[ holds f.g<=0) implies
f^ is_right_divergent_to-infty_in x0
proof assume A1: f is_right_convergent_in x0 & lim_right(f,x0)=0 &
for r st x0<r ex g st g<r & x0<g & g in dom f & f.g<>0;
given r such that A2: 0<r & for g st g in dom f/\].x0,x0+r.[ holds f.g<=0;
thus for r1 st x0<r1 ex g1 st g1<r1 & x0<g1 & g1 in dom(f^)
proof let r1; assume x0<r1; then consider g1 such that
A3: g1<r1 & x0<g1 & g1 in dom f & f.g1<>0 by A1; take g1;
thus g1<r1 & x0<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 such that A4: s is convergent & lim s=x0 &
rng s c=dom(f^)/\right_open_halfline(x0); x0<x0+r by A2,Lm1;
then consider k such that A5: for n st k<=n holds s.n<x0+r by A4,Th2;
A6: s^\k is convergent & lim(s^\k)=x0 by A4,SEQ_4:33;
dom(f^)/\right_open_halfline(x0)c=dom(f^) &
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then A7: rng s c=dom(f^) & rng s c=right_open_halfline(x0) by A4,XBOOLE_1:1;
dom(f^)=dom f\f"{0} by RFUNCT_1:def 8; then dom(f^)c=dom f by XBOOLE_1:36
;
then A8: rng s c=dom f by A7,XBOOLE_1:1;
rng(s^\k)c=rng s by RFUNCT_2:7;
then A9: rng(s^\k)c=dom (f^)/\right_open_halfline(x0) & rng(s^\k)c=dom(f^) &
rng(s^\k)c=right_open_halfline(x0) & rng(s^\k)c=dom f by A4,A7,A8,XBOOLE_1:1
;
then rng(s^\k)c=dom f/\right_open_halfline(x0) by XBOOLE_1:19;
then A10: f*(s^\k) is convergent & lim(f*(s^\k))=0 by A1,A6,Def8;
A11: f*(s^\k) is_not_0 by A9,RFUNCT_2:26;
A12: now let n; A13: (s^\k).n in rng(s^\k) by RFUNCT_2:10;
then (s^\k).n in right_open_halfline(x0) by A9;
then (s^\k).n in {g1: x0<g1} by LIMFUNC1:def 3; then A14:
ex g1 st g1=(s^\k).n & x0<g1; k<=n+k by NAT_1:37
; then s.(n+k)<x0+r by A5;
then (s^\k).n<x0+r by SEQM_3:def 9
; then (s^\k).n in {g2: x0<g2 & g2<x0+r} by A14;
then (s^\k).n in ].x0,x0+r.[ by RCOMP_1:def 2;
then (s^\k).n in dom f/\].x0,x0+r.[ by A9,A13,XBOOLE_0:def 3
; then A15: f.((s^\k).n)<=0 by A2
; (f*(s^\k)).n<>0 by A11,SEQ_1:7;
hence (f*(s^\k)).n<0 by A9,A15,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 A12;
then A17: (f*(s^\k))" is divergent_to-infty by A10,A16,LIMFUNC1:63;
(f*(s^\k))"=((f*s)^\k)" by A8,RFUNCT_2:22
.=((f*s)")^\k by SEQM_3:41
.=((f^)*s)^\k by A7,RFUNCT_2:27; hence thesis by A17,LIMFUNC1:34;
end;