:: One-Side Limits of a Real Function at a Point
:: by Jaros{\l}aw Kotowicz
::
:: Received August 20, 1990
:: Copyright (c) 1990-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, SEQ_1, PARTFUN1, CARD_1, ARYTM_3,
XXREAL_0, ARYTM_1, RELAT_1, TARSKI, VALUED_1, XBOOLE_0, SEQ_2, ORDINAL2,
FUNCT_1, LIMFUNC1, FUNCT_2, XXREAL_1, COMPLEX1, XXREAL_2, NAT_1,
VALUED_0, ORDINAL4, LIMFUNC2, ASYMPT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0,
COMPLEX1, REAL_1, NAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1,
SEQ_1, COMSEQ_2, SEQ_2, RELSET_1, RCOMP_1, PARTFUN1, RFUNCT_1, LIMFUNC1,
XXREAL_0;
constructors FUNCOP_1, REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1,
RCOMP_1, RFUNCT_1, RFUNCT_2, LIMFUNC1, PARTFUN1, VALUED_1, RELSET_1,
BINOP_2, RVSUM_1, COMSEQ_2, SEQ_1;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, XBOOLE_0,
VALUED_0, VALUED_1, FUNCT_2, SEQ_4, SEQ_1, SEQ_2;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities LIMFUNC1, PROB_1, VALUED_1;
expansions LIMFUNC1;
theorems TARSKI, NAT_1, ABSVALUE, SEQ_1, SEQ_2, SEQM_3, SEQ_4, RFUNCT_1,
RFUNCT_2, LIMFUNC1, RCOMP_1, FUNCT_1, XREAL_0, XBOOLE_0, XBOOLE_1,
XCMPLX_0, XREAL_1, COMPLEX1, XXREAL_0, VALUED_1, XXREAL_1, FUNCT_2,
VALUED_0, ORDINAL1;
schemes SEQ_1, FUNCT_2;
begin
reserve r,r1,r2,g,g1,g2,x0,t 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 holds 0=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;
consider g1 such that
A4: 0=
g1 by A1,A2;
defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2=g1;
A6: now
let n be Element of NAT;
x0-1/(n+1)=g1 by A5;
reconsider g2 as Element of REAL by XREAL_0:def 1;
take g2;
thus X[n,g2] by A7,A8,A9,A10;
end;
consider s be Real_Sequence such that
A11: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: for n being Nat holds X[n,s.n]
proof let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A11;
end;
A13: rng s c=dom f/\left_open_halfline(x0) by A12,Th5;
A14: lim s=x0 by A12,Th5;
A15: s is convergent by A12,Th5;
then
A16: lim(f/*s)=g by A3,A14,A13;
f/*s is convergent by A3,A15,A14,A13;
then consider n such that
A17: for k st n<=k holds |.(f/*s).k-g.|=f.r1;
consider g1 such that
A3: for r st r=f.r1 by A1,A2;
defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2=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;
consider g1 such that
A4: 0=
g1 by A1,A2;
defpred X[Nat,Real] means x0<$2 & $20 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
A1: dom f/\left_open_halfline(x0)c=dom f by XBOOLE_1:17;
thus f is_left_divergent_to+infty_in x0 & r>0 implies r(#)f
is_left_divergent_to+infty_in x0
proof
assume that
A2: f is_left_divergent_to+infty_in x0 and
A3: r>0;
thus for r1 st r10 implies r(#)f
is_left_divergent_to-infty_in x0
proof
assume that
A22: f is_left_divergent_to-infty_in x0 and
A23: r>0;
thus for r1 st r10 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
A1: dom f/\right_open_halfline(x0)c=dom f by XBOOLE_1:17;
thus f is_right_divergent_to+infty_in x0 & r>0 implies r(#)f
is_right_divergent_to+infty_in x0
proof
assume that
A2: f is_right_divergent_to+infty_in x0 and
A3: r>0;
thus for r1 st x00 implies r(#)f
is_right_divergent_to-infty_in x0
proof
assume that
A22: f is_right_divergent_to-infty_in x0 and
A23: r>0;
thus for r1 st 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;
uniqueness
proof
defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2 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;
uniqueness
proof
defpred X[Nat,Real] means x0<$2 & $2=g1;
consider g1 such that
A4: 0= g1 by A3;
defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2=g1;
A6: now
let n be Element of NAT;
x0-1/(n+1)=g1 by A5;
reconsider g2 as Element of REAL by XREAL_0:def 1;
take g2;
thus X[n,g2] by A7,A8,A9,A10;
end;
consider s be Real_Sequence such that
A11: for n being Element of NAT holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: for n being Nat holds X[n,s.n]
proof let n;
n in NAT by ORDINAL1:def 12;
hence thesis by A11;
end;
A13: rng s c=dom f/\left_open_halfline(x0) by A12,Th5;
A14: lim s=x0 by A12,Th5;
A15: s is convergent by A12,Th5;
then
A16: lim(f/*s)=g by A1,A2,A14,A13,Def7;
f/*s is convergent by A1,A15,A14,A13;
then consider n such that
A17: for k st n<=k holds |.(f/*s).k-g.|=g1;
consider g1 such that
A4: 0= g1 by A3;
defpred X[Nat,Real] means x0<$2 & $20 implies f^
is_left_convergent_in x0 & lim_left(f^,x0)=(lim_left(f,x0))"
proof
assume that
A1: f is_left_convergent_in x0 and
A2: f"{0}={} and
A3: lim_left(f,x0)<>0;
A4: dom f=dom f\f"{0} by A2
.=dom(f^) by RFUNCT_1:def 2;
A5: now
let seq;
assume that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom(f^)/\left_open_halfline(x0);
A9: lim(f/*seq)=lim_left(f,x0) by A1,A4,A6,A7,A8,Def7;
A10: dom f/\left_open_halfline(x0) c=dom f by XBOOLE_1:17;
then
A11: rng seq c=dom f by A4,A8,XBOOLE_1:1;
A12: f/*seq is convergent by A1,A4,A6,A7,A8;
A13: (f/*seq)"=(f^)/*seq by A4,A8,A10,RFUNCT_2:12,XBOOLE_1:1;
hence (f^)/*seq is convergent by A3,A4,A12,A9,A11,RFUNCT_2:11,SEQ_2:21;
thus lim((f^)/*seq)=(lim_left(f,x0))" by A3,A4,A12,A9,A11,A13,RFUNCT_2:11
,SEQ_2:22;
end;
for r st r0 & (for r st r0) implies f^ is_left_convergent_in x0 &
lim_left(f^,x0)=(lim_left(f,x0))"
proof
assume that
A1: f is_left_convergent_in x0 and
A2: lim_left(f,x0)<>0 and
A3: for r st r0;
A4: dom f\f"{0}=dom(f^) by RFUNCT_1:def 2;
A5: now
A6: dom(f^)c=dom f by A4,XBOOLE_1:36;
let seq such that
A7: seq is convergent and
A8: lim seq=x0 and
A9: rng seq c=dom(f^)/\left_open_halfline(x0);
A10: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
then
A11: f/*seq is non-zero by A9,RFUNCT_2:11,XBOOLE_1:1;
rng seq c=dom(f^) by A9,A10,XBOOLE_1:1;
then
A12: rng seq c=dom f by A6,XBOOLE_1:1;
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then rng seq c=left_open_halfline(x0) by A9,XBOOLE_1:1;
then
A13: rng seq c=dom f/\left_open_halfline(x0) by A12,XBOOLE_1:19;
then
A14: lim(f/*seq)=lim_left(f,x0) by A1,A7,A8,Def7;
A15: (f/*seq)"=(f^)/*seq by A9,A10,RFUNCT_2:12,XBOOLE_1:1;
A16: f/*seq is convergent by A1,A7,A8,A13;
hence (f^)/*seq is convergent by A2,A14,A11,A15,SEQ_2:21;
thus lim((f^)/*seq)=(lim_left(f,x0))" by A2,A16,A14,A11,A15,SEQ_2:22;
end;
now
let r;
assume r0 by A3;
take g;
not f.g in {0} by A20,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
hence r 0 & (for r st r0 and
A4: for r st r0 by A9,TARSKI:def 1,XBOOLE_0:def 5;
end;
then
A11: f2^ is_left_convergent_in x0 by A2,A3,Th49;
A12: f1/f2=f1(#)(f2^) by RFUNCT_1:31;
hence f1/f2 is_left_convergent_in x0 by A1,A4,A11,Th50;
lim_left(f2^,x0)=(lim_left(f2,x0))" by A2,A3,A5,Th49;
hence
lim_left(f1/f2,x0)=lim_left(f1,x0)*((lim_left(f2,x0))") by A1,A4,A12,A11,Th50
.=lim_left(f1,x0)/(lim_left(f2,x0)) by XCMPLX_0:def 9;
end;
theorem Th52:
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 seq;
assume that
A3: seq is convergent and
A4: lim seq=x0 and
A5: rng seq c=dom(r(#)f)/\right_open_halfline(x0);
A6: rng seq c=dom f/\right_open_halfline(x0) by A5,VALUED_1:def 5;
A7: dom f/\right_open_halfline(x0) c=dom f by XBOOLE_1:17;
then
A8: r (#)(f/*seq)=(r(#)f)/*seq by A6,RFUNCT_2:9,XBOOLE_1:1;
A9: f/*seq is convergent by A1,A3,A4,A6;
then r(#)(f/*seq) is convergent;
hence (r(#)f)/*seq is convergent by A6,A7,RFUNCT_2:9,XBOOLE_1:1;
lim(f/*seq)=lim_right(f,x0) by A1,A3,A4,A6,Def8;
hence lim((r(#)f)/*seq)=r*(lim_right(f,x0)) by A9,A8,SEQ_2:8;
end;
now
let r1;
assume x00 implies f^
is_right_convergent_in x0 & lim_right(f^,x0)=(lim_right(f,x0))"
proof
assume that
A1: f is_right_convergent_in x0 and
A2: f"{0}={} and
A3: lim_right(f,x0)<>0;
A4: dom f=dom f\f"{0} by A2
.=dom(f^) by RFUNCT_1:def 2;
A5: now
let seq;
assume that
A6: seq is convergent and
A7: lim seq=x0 and
A8: rng seq c=dom(f^)/\right_open_halfline(x0);
A9: lim(f/*seq)=lim_right(f,x0) by A1,A4,A6,A7,A8,Def8;
A10: dom f/\right_open_halfline(x0) c=dom f by XBOOLE_1:17;
then
A11: rng seq c=dom f by A4,A8,XBOOLE_1:1;
A12: f/*seq is convergent by A1,A4,A6,A7,A8;
A13: (f/*seq)"=(f^)/*seq by A4,A8,A10,RFUNCT_2:12,XBOOLE_1:1;
hence (f^)/*seq is convergent by A3,A4,A12,A9,A11,RFUNCT_2:11,SEQ_2:21;
thus lim((f^)/*seq)=(lim_right(f,x0))" by A3,A4,A12,A9,A11,A13,RFUNCT_2:11
,SEQ_2:22;
end;
for r st x00 & (for r st x0<
r ex g st g0) implies f^ is_right_convergent_in
x0 & lim_right(f^,x0)=(lim_right(f,x0))"
proof
assume that
A1: f is_right_convergent_in x0 and
A2: lim_right(f,x0)<>0 and
A3: for r st x00;
A4: dom f\f"{0}=dom(f^) by RFUNCT_1:def 2;
A5: now
A6: dom(f^) c=dom f by A4,XBOOLE_1:36;
let seq such that
A7: seq is convergent and
A8: lim seq=x0 and
A9: rng seq c=dom(f^)/\right_open_halfline(x0);
A10: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
then
A11: f/*seq is non-zero by A9,RFUNCT_2:11,XBOOLE_1:1;
rng seq c=dom(f^) by A9,A10,XBOOLE_1:1;
then
A12: rng seq c=dom f by A6,XBOOLE_1:1;
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then rng seq c=right_open_halfline(x0) by A9,XBOOLE_1:1;
then
A13: rng seq c=dom f/\right_open_halfline(x0) by A12,XBOOLE_1:19;
then
A14: lim(f/*seq)=lim_right(f,x0) by A1,A7,A8,Def8;
A15: (f/*seq)"=(f^)/*seq by A9,A10,RFUNCT_2:12,XBOOLE_1:1;
A16: f/*seq is convergent by A1,A7,A8,A13;
hence (f^)/*seq is convergent by A2,A14,A11,A15,SEQ_2:21;
thus lim((f^)/*seq)=(lim_right(f,x0))" by A2,A16,A14,A11,A15,SEQ_2:22;
end;
now
let r;
assume x00 by A3;
take g;
not f.g in {0} by A20,TARSKI:def 1;
then not g in f"{0} by FUNCT_1:def 7;
hence g0 & (for r st x00 and
A4: for r st x00 by A9,TARSKI:def 1,XBOOLE_0:def 5;
end;
then
A11: f2^ is_right_convergent_in x0 by A2,A3,Th58;
A12: f1/f2=f1(#)(f2^) by RFUNCT_1:31;
hence f1/f2 is_right_convergent_in x0 by A1,A4,A11,Th59;
lim_right(f2^,x0)=(lim_right(f2,x0)) " by A2,A3,A5,Th58;
hence lim_right(f1/f2,x0)=lim_right(f1,x0)*((lim_right(f2,x0))") by A1,A4,A12
,A11,Th59
.=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 r0) 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;
A2: now
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A3: dom(f^)c=dom f by XBOOLE_1:36;
let seq such that
A4: seq is convergent and
A5: lim seq=x0 and
A6: rng seq c=dom(f^)/\left_open_halfline(x0);
dom(f^)/\left_open_halfline(x0)c=left_open_halfline(x0) by XBOOLE_1:17;
then
A7: rng seq c=left_open_halfline(x0) by A6,XBOOLE_1:1;
A8: dom(f^)/\left_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
then rng seq c=dom(f^) by A6,XBOOLE_1:1;
then rng seq c=dom f by A3,XBOOLE_1:1;
then
A9: 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
A10: f/*seq is divergent_to+infty by A4,A5,A9;
then
A11: lim((f/*seq)")=0 by LIMFUNC1:34;
(f/*seq)" is convergent by A10,LIMFUNC1:34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A6,A8,A11,
RFUNCT_2:12,XBOOLE_1:1;
end;
suppose
f is_left_divergent_to-infty_in x0;
then
A12: f/*seq is divergent_to-infty by A4,A5,A9;
then
A13: lim((f/*seq)")=0 by LIMFUNC1:34;
(f/*seq)" is convergent by A12,LIMFUNC1:34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A6,A8,A13,
RFUNCT_2:12,XBOOLE_1:1;
end;
end;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0;
end;
assume
A14: for r st r0;
now
let r;
assume r0 by A14;
take g;
thus r0) 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;
A2: now
dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A3: dom(f^)c=dom f by XBOOLE_1:36;
let seq such that
A4: seq is convergent and
A5: lim seq=x0 and
A6: rng seq c=dom(f^)/\right_open_halfline(x0);
dom(f^)/\right_open_halfline(x0)c=right_open_halfline(x0) by XBOOLE_1:17;
then
A7: rng seq c=right_open_halfline(x0) by A6,XBOOLE_1:1;
A8: dom(f^)/\right_open_halfline(x0)c=dom(f^) by XBOOLE_1:17;
then rng seq c=dom(f^) by A6,XBOOLE_1:1;
then rng seq c=dom f by A3,XBOOLE_1:1;
then
A9: 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
A10: f/*seq is divergent_to+infty by A4,A5,A9;
then
A11: lim((f/*seq)")=0 by LIMFUNC1:34;
(f/*seq)" is convergent by A10,LIMFUNC1:34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A6,A8,A11,
RFUNCT_2:12,XBOOLE_1:1;
end;
suppose
f is_right_divergent_to-infty_in x0;
then
A12: f/*seq is divergent_to-infty by A4,A5,A9;
then
A13: lim((f/*seq)")=0 by LIMFUNC1:34;
(f/*seq)" is convergent by A12,LIMFUNC1:34;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0 by A6,A8,A13,
RFUNCT_2:12,XBOOLE_1:1;
end;
end;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0;
end;
assume
A14: for r st x00;
now
let r;
assume x00 by A14;
take g;
thus gf.g2 by A4;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A11: x0-r<=g1;
consider g2 such that
A12: g1f.g2 by A4;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A14,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom(f^)/\left_open_halfline(x0);
x0-rf.g2 by A4;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
suppose
A11: x0+r<=g1;
x0f.g2 by A4;
then not f.g2 in {0} by TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then g2 in dom f\f"{0} by A14,XBOOLE_0:def 5;
hence g2 in dom(f^) by RFUNCT_1:def 2;
end;
end;
hence thesis;
end;
let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom(f^)/\right_open_halfline(x0);
x00) & (ex r st 00;
given r such that
A4: 00 by A3;
take g1;
thus r10 by A24,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
end;
then
A29: for n holds 0<=n implies 0<(f/*(s^\k)).n;
f/*(s^\k) is convergent by A1,A10,A14,A22;
then
A30: (f/*(s^\k))" is divergent_to+infty by A23,A29,LIMFUNC1:35;
(f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
hence thesis by A30,LIMFUNC1:7;
end;
theorem
f is_left_convergent_in x0 & lim_left(f,x0)=0 & (for r st r0) & (ex r st 00;
given r such that
A4: 00 by A3;
take g1;
thus r10 by A24,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
end;
then
A29: for n holds 0<=n implies (f/*(s^\k)).n<0;
f/*(s^\k) is convergent by A1,A10,A14,A22;
then
A30: (f/*(s^\k))" is divergent_to-infty by A23,A29,LIMFUNC1:36;
(f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
hence thesis by A30,LIMFUNC1:7;
end;
theorem
f is_right_convergent_in x0 & lim_right(f,x0)=0 & (for r st x00) & (ex r st 00;
given r such that
A4: 00 by A3;
take g1;
thus g1(f/*(s^\k)).n by A24,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
end;
then
A29: for n holds 0<=n implies 0<(f/*(s^\k)).n;
f/*(s^\k) is convergent by A1,A10,A14,A22;
then
A30: (f/*(s^\k))" is divergent_to+infty by A23,A29,LIMFUNC1:35;
(f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
hence thesis by A30,LIMFUNC1:7;
end;
theorem
f is_right_convergent_in x0 & lim_right(f,x0)=0 & (for r st x00) & (ex r st 00;
given r such that
A4: 00 by A3;
take g1;
thus g10 by A24,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A19,A17,A28,FUNCT_2:108,XBOOLE_1:1,A25;
end;
then
A29: for n holds 0<=n implies (f/*(s^\k)).n<0;
f/*(s^\k) is convergent by A1,A10,A14,A22;
then
A30: (f/*(s^\k))" is divergent_to-infty by A23,A29,LIMFUNC1:36;
(f/*(s^\k))"=((f/*s)^\k)" by A16,A18,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A12,A15,RFUNCT_2:12,XBOOLE_1:1;
hence thesis by A30,LIMFUNC1:7;
end;