:: The Limit of a Real Function at a Point
:: by Jaros{\l}aw Kotowicz
::
:: Received September 5, 1990
:: Copyright (c) 1990-2021 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, LIMFUNC1,
FUNCT_1, COMPLEX1, SEQ_2, ORDINAL2, XXREAL_1, FUNCT_2, LIMFUNC2, NAT_1,
VALUED_0, XXREAL_2, ORDINAL4, LIMFUNC3;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0,
XREAL_0, COMPLEX1, REAL_1, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, VALUED_0,
VALUED_1, SEQ_1, PARTFUN1, COMSEQ_2, SEQ_2, RCOMP_1, RFUNCT_1, LIMFUNC1,
LIMFUNC2, RECDEF_1;
constructors REAL_1, NAT_1, COMPLEX1, SEQ_2, SEQM_3, PROB_1, RCOMP_1,
PARTFUN1, RFUNCT_1, RFUNCT_2, LIMFUNC1, LIMFUNC2, VALUED_1, RECDEF_1,
RELSET_1, COMSEQ_2, NUMBERS;
registrations ORDINAL1, RELSET_1, NUMBERS, XREAL_0, NAT_1, MEMBERED, VALUED_0,
VALUED_1, FUNCT_2, SEQ_4;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities XBOOLE_0, VALUED_1, PROB_1, LIMFUNC1;
expansions TARSKI, LIMFUNC1;
theorems TARSKI, NAT_1, FUNCT_1, FUNCT_2, ABSVALUE, SEQ_1, SEQ_2, SEQM_3,
SEQ_4, RFUNCT_1, RCOMP_1, RFUNCT_2, LIMFUNC1, LIMFUNC2, RELSET_1,
XREAL_0, XBOOLE_0, XBOOLE_1, XCMPLX_0, XCMPLX_1, XREAL_1, COMPLEX1,
XXREAL_0, ORDINAL1, VALUED_1, XXREAL_1, VALUED_0, RELAT_1, NUMBERS;
schemes NAT_1, RECDEF_1, FUNCT_2;
begin
reserve r,r1,r2,g,g1,g2,x0,t for Real;
reserve n,k,m for Element of NAT;
reserve seq for Real_Sequence;
reserve f,f1,f2 for PartFunc of REAL,REAL;
Lm1: for g,r,r1 be Real holds 0|.x0-seq.n.| by A1;
then x0-seq.n+seq.n<>0+seq.n by ABSVALUE:2;
then not x in {x0} by A9,TARSKI:def 1;
hence thesis by A7,A8,XBOOLE_0:def 5;
end;
theorem Th3:
seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} implies
for r st 00 by TARSKI:def 1;
end;
then seq.k-x0<>0;
then 0<|.-(x0-seq.k).| by COMPLEX1:47;
hence 0<|.x0-seq.k.| by COMPLEX1:52;
thus |.x0-seq.k.|x0 by A3,TARSKI:def 1;
now
per cases by A5,XXREAL_0:1;
suppose
r1=g1;
consider g such that
A3: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f\{x0}
holds f/*seq is convergent & lim(f/*seq)=g by A1;
consider g1 such that
A4: 0= g1 by A1,A2;
defpred X[Element of NAT,Real] means 0<|.x0-$2.| & |.x0-$2.|<1/(
$1+1) & $2 in dom f & |.f.($2)-g.|>=g1;
A6: for n ex r1 being Element of REAL st X[n,r1]
proof let n;
consider r1 such that
A7: X[n,r1] by A5,XREAL_1:139;
reconsider r1 as Element of REAL by XREAL_0:def 1;
take r1;
thus thesis by A7;
end;
consider s be Real_Sequence such that
A8: for n holds X[n,s.n] from FUNCT_2:sch 3(A6);
A9: rng s c=dom f\{x0} by A8,Th2;
A10: lim s=x0 by A8,Th2;
A11: s is convergent by A8,Th2;
then
A12: lim(f/*s)=g by A3,A10,A9;
f/*s is convergent by A3,A11,A10,A9;
then consider n being Nat such that
A13: for k being Nat st n<=k holds |.(f/*s).k-g.|=x0;
now
per cases;
suppose
ex k st for n st k<=n holds x0x0;
A26: rng s c=dom f by A17,XBOOLE_1:1;
A27: rng(s^\k)c=dom f/\right_open_halfline(x0)
proof
let x be object;
assume x in rng(s^\k);
then consider n such that
A28: (s^\k).n=x by FUNCT_2:113;
x0=s.n;
defpred X[Nat] means s.$1x0 by TARSKI:def 1;
hence s.nx0;
defpred P[set,set] means for n,m st $1=n & $2=m holds n$1;
assume ex n st X[n];
then
A53: ex n be Nat st X[n];
consider M1 be Nat such that
A54: X[M1] & for n be Nat st X[n] holds M1<=n from NAT_1:sch
5(A53);
defpred X[Nat] means $1 M1 by A43,A54;
M<=M1 by A36,A54;
hence M=x0
proof
given k such that
A60: MXk;
hence contradiction by A54,A61,A62;
end;
end;
hence contradiction;
end;
consider m such that
A63: F.m=MX by A58;
M1 in NAT by ORDINAL1:def 12;
then
A64: F.(m+1)<=M1 by A43,A54,A58,A63;
A65: s.(F.(m+1))M1;
then F.(m+1)=x0 by A24;
take n;
thus k<=n by A68;
s.n in rng s by VALUED_0:28;
then not s.n in {x0} by A17,XBOOLE_0:def 5;
then s.n<>x0 by TARSKI:def 1;
hence s.n>x0 by A69,XXREAL_0:1;
end;
then ex mn be Element of NAT st 0<=mn & s.mn>x0;
then
A70: ex m be Nat st X[m];
consider N be Nat such that
A71: X[N] & for n be Nat st X[n] holds N<=n from NAT_1:sch 5(A70);
defpred X[Nat] means (s*F).$1x0
& for k st nx0 holds m<=k;
defpred X[Nat,set,set] means P[$2,$3];
A79: s*F is convergent by A15,A50,SEQ_4:16;
reconsider N9=N as Element of NAT by ORDINAL1:def 12;
A80: now
let n;
consider m such that
A81: n+1<=m and
A82: s.m>x0 by A67;
take m;
thus nx0 by A81,A82,NAT_1:13;
end;
A83: for n being Nat
for x be Element of NAT ex y be Element of NAT st X[n, x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred X[Nat] means x<$1 & s.$1>x0;
ex m st X[m] by A80;
then
A84: ex m be Nat st X[m];
consider l be Nat such that
A85: X[l] & for k be Nat st X[k] holds l<= k from NAT_1:sch
5(A84);
reconsider l as Element of NAT by ORDINAL1:def 12;
take l;
thus thesis by A85;
end;
consider G be sequence of NAT such that
A86: G.0=N9 & for n being Nat holds X[n,G.n,G.(n+1)] from RECDEF_1:sch
2(A83);
A87: rng G c=NAT by RELAT_1:def 19;
then
A88: rng G c=REAL by NUMBERS:19;
A89: dom G=NAT by FUNCT_2:def 1;
then reconsider G as Real_Sequence by A88,RELSET_1:4;
A90: now
let n;
G.n in rng G by A89,FUNCT_1:def 3;
hence G.n is Element of NAT by A87;
end;
now
let n be Nat;
A91: n in NAT by ORDINAL1:def 12;
A92: G.(n+1) is Element of NAT by A90;
G.n is Element of NAT by A90,A91;
hence G.nx0 & for m holds G.m<>$1;
A95: for n st s.n>x0 ex m st G.m=n
proof
assume ex n st X[n];
then
A96: ex n be Nat st X[n];
consider N1 be Nat such that
A97: X[N1] & for n be Nat st X[n] holds N1<=n from NAT_1:
sch 5(A96);
defpred X[Nat] means $1x0 & ex m st G.m=$1;
A98: ex n be Nat st X[n]
proof
take N;
A99: N <> N1 by A86,A97;
N<=N1 by A71,A97;
hence Nx0 by A71;
take 0;
thus thesis by A86;
end;
A100: for n be Nat st X[n] holds n<=N1;
consider NX be Nat such that
A101: X[NX] & for n be Nat st X[n] holds n<=NX from NAT_1:
sch 6(A100,A98);
A102: for k st NXx0;
now
per cases;
suppose
ex m st G.m=k;
hence contradiction by A101,A103,A104,A105;
end;
suppose
for m holds G.m<>k;
hence contradiction by A97,A104,A105;
end;
end;
hence contradiction;
end;
consider m such that
A106: G.m=NX by A101;
N1 in NAT by ORDINAL1:def 12;
then
A107: G.(m+1)<=N1 by A86,A97,A101,A106;
A108: s.(G.(m+1))>x0 by A86,A106;
A109: NXN1;
then G.(m+1)x0;
A110: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
(s*G).k>x0;
P[G.k,G.(k+1)] by A86;
then s.(G.(k+1))>x0;
hence thesis by FUNCT_2:15;
end;
A111: X[0] by A71,A86,FUNCT_2:15;
A112: for k being Nat holds X[k] from NAT_1:sch 2(A111,A110);
A113: rng(s*G)c=dom f/\right_open_halfline(x0)
proof
let x be object;
assume
A114: x in rng(s*G);
then consider n such that
A115: (s*G).n=x by FUNCT_2:113;
(s*G).n>x0 by A112;
then x in {g1: x0x0 by TARSKI:def 1;
now
per cases by A124,XXREAL_0:1;
suppose
s.k= n1 by A125,SEQM_3:1;
then r<(f/*(s*F)).l by A120;
then rx0;
then consider l be Element of NAT such that
A126: k=G.l by A95,A122;
G.n2<=n by XXREAL_0:25;
then G.n2<=k by A123,XXREAL_0:2;
then l >= n2 by A126,SEQM_3:1;
then r<(f/*(s*G)).l by A121;
then r=x0;
now
per cases;
suppose
ex k st for n st k<=n holds x0x0;
A25: rng s c=dom f by A16,XBOOLE_1:1;
A26: rng(s^\k)c=dom f/\right_open_halfline(x0)
proof
let x be object;
assume x in rng(s^\k);
then consider n such that
A27: (s^\k).n=x by FUNCT_2:113;
x0=s.n;
defpred P[set,set] means for n,m st $1=n & $2=m holds nx0 by TARSKI:def 1;
hence s.n$1;
A51: for n st s.n M1 by A42,A53;
M<=M1 by A35,A53;
hence M=x0
proof
given k such that
A59: MXk;
hence contradiction by A53,A60,A61;
end;
end;
hence contradiction;
end;
consider m such that
A62: F.m=MX by A57;
M1 in NAT by ORDINAL1:def 12;
then
A63: F.(m+1)<=M1 by A42,A53,A57,A62;
A64: s.(F.(m+1))M1;
then F.(m+1)x0;
A66: now
let k;
consider n such that
A67: k<=n and
A68: s.n>=x0 by A23;
take n;
thus k<=n by A67;
s.n in rng s by VALUED_0:28;
then not s.n in {x0} by A16,XBOOLE_0:def 5;
then s.n<>x0 by TARSKI:def 1;
hence s.n>x0 by A68,XXREAL_0:1;
end;
then ex mn be Element of NAT st 0<=mn & s.mn>x0;
then
A69: ex m be Nat st X[m];
consider N be Nat such that
A70: X[N] & for n be Nat st X[n] holds N<=n from NAT_1:sch 5(
A69);
defpred X[Nat] means (s*F).$1x0
& for k st nx0 holds m<=k;
defpred X[Nat,set,set] means P[$2,$3];
A78: s*F is convergent by A14,A49,SEQ_4:16;
lim(s*F)=x0 by A14,A15,A49,SEQ_4:17;
then
A79: f/*(s*F) is divergent_to-infty by A11,A78,A74,LIMFUNC2:def 3;
reconsider N9=N as Element of NAT by ORDINAL1:def 12;
A80: now
let n;
consider m such that
A81: n+1<=m and
A82: s.m>x0 by A66;
take m;
thus nx0 by A81,A82,NAT_1:13;
end;
A83: for n being Nat
for x be Element of NAT ex y be Element of NAT st X[n, x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred X[Nat] means x<$1 & s.$1>x0;
ex m st X[m] by A80;
then
A84: ex m be Nat st X[m];
consider l be Nat such that
A85: X[l] & for k be Nat st X[k] holds l<=k from NAT_1:sch
5 (A84);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A85;
end;
consider G be sequence of NAT such that
A86: G.0=N9 & for n being Nat holds X[n,G.n,G.(n+1)] from RECDEF_1:sch
2(A83);
A87: rng G c=NAT by RELAT_1:def 19;
then
A88: rng G c=REAL by NUMBERS:19;
A89: dom G=NAT by FUNCT_2:def 1;
then reconsider G as Real_Sequence by A88,RELSET_1:4;
A90: now
let n;
G.n in rng G by A89,FUNCT_1:def 3;
hence G.n is Element of NAT by A87;
end;
now
let n be Nat;
A91: n in NAT by ORDINAL1:def 12;
A92: G.(n+1) is Element of NAT by A90;
G.n is Element of NAT by A90,A91;
hence G.nx0 & for m holds G.m<>$1;
A95: for n st s.n>x0 ex m st G.m=n
proof
assume ex n st X[n];
then
A96: ex n be Nat st X[n];
consider N1 be Nat such that
A97: X[N1] & for n be Nat st X[n] holds N1<=n from NAT_1:
sch 5(A96);
defpred X[Nat] means $1x0 & ex m st G.m=$1;
A98: ex n be Nat st X[n]
proof
take N;
A99: N <> N1 by A86,A97;
N<=N1 by A70,A97;
hence Nx0 by A70;
take 0;
thus thesis by A86;
end;
A100: for n be Nat st X[n] holds n<=N1;
consider NX be Nat such that
A101: X[NX] & for n be Nat st X[n] holds n<=NX from NAT_1:
sch 6(A100,A98);
A102: for k st NXx0;
now
per cases;
suppose
ex m st G.m=k;
hence contradiction by A101,A103,A104,A105;
end;
suppose
for m holds G.m<>k;
hence contradiction by A97,A104,A105;
end;
end;
hence contradiction;
end;
consider m such that
A106: G.m=NX by A101;
N1 in NAT by ORDINAL1:def 12;
then
A107: G.(m+1)<=N1 by A86,A97,A101,A106;
A108: s.(G.(m+1))>x0 by A86,A106;
A109: NXN1;
then G.(m+1)x0;
A110: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
(s*G).k>x0;
P[G.k,G.(k+1)] by A86;
then s.(G.(k+1))>x0;
hence thesis by FUNCT_2:15;
end;
A111: X[0] by A70,A86,FUNCT_2:15;
A112: for k being Nat holds X[k] from NAT_1:sch 2(A111,A110);
A113: rng(s*G)c=dom f/\right_open_halfline(x0)
proof
let x be object;
assume
A114: x in rng(s*G);
then consider n such that
A115: (s*G).n=x by FUNCT_2:113;
(s*G).n>x0 by A112;
then x in {g1: x0x0 by TARSKI:def 1;
now
per cases by A123,XXREAL_0:1;
suppose
s.k= n1 by A124,SEQM_3:1;
then (f/*(s*F)).lx0;
then consider l be Element of NAT such that
A125: k=G.l by A95,A121;
G.n2<=n by XXREAL_0:25;
then G.n2<=k by A122,XXREAL_0:2;
then l >= n2 by A125,SEQM_3:1;
then (f/*(s*G)).l0 implies r(#) f
is_divergent_to+infty_in x0)& (f is_divergent_to+infty_in x0 & r<0 implies r(#)
f is_divergent_to-infty_in x0)& (f is_divergent_to-infty_in x0 & r>0 implies r
(#) f is_divergent_to-infty_in x0)& (f is_divergent_to-infty_in x0 & r<0
implies r(#)f is_divergent_to+infty_in x0)
proof
thus f is_divergent_to+infty_in x0 & r>0 implies r(#)f
is_divergent_to+infty_in x0
proof
assume that
A1: f is_divergent_to+infty_in x0 and
A2: r>0;
thus for r1,r2 st r10 implies r(#)f
is_divergent_to-infty_in x0
proof
assume that
A29: f is_divergent_to-infty_in x0 and
A30: r>0;
thus for r1,r2 st r1 Real means
:Def4:
for seq st seq is convergent & lim seq=x0
& rng seq c= dom f \ {x0} holds f/*seq is convergent & lim(f/*seq)=it;
existence
by A1;
uniqueness
proof
defpred X[Element of NAT,Real] means x0-1/($1+1)<$2 & $2=g1;
A6: for n ex r1 being Element of REAL st X[n,r1]
proof let n;
consider r1 such that
A7: X[n,r1] by A5,XREAL_1:139;
reconsider r1 as Element of REAL by XREAL_0:def 1;
take r1;
thus thesis by A7;
end;
consider s be Real_Sequence such that
A8: for n holds X[n,s.n] from FUNCT_2:sch 3(A6);
A9: rng s c=dom f\{x0} by A8,Th2;
A10: lim s=x0 by A8,Th2;
A11: s is convergent by A8,Th2;
then
A12: lim(f/*s)=g by A1,A2,A10,A9,Def4;
f/*s is convergent by A1,A11,A10,A9;
then consider n being Nat such that
A13: for k being Nat st n<=k holds |.(f/*s).k-g.|=x0;
now
per cases;
suppose
ex k st for n st k<=n holds x0x0;
A18: rng s c=dom f by A7,XBOOLE_1:1;
A19: rng(s^\k)c=dom f/\right_open_halfline(x0)
proof
let x be object;
assume x in rng(s^\k);
then consider n such that
A20: (s^\k).n=x by FUNCT_2:113;
x0=s.n;
set GR=lim_left(f,x0);
defpred P[set,set] means for n,m st $1=n & $2=m holds nx0 by TARSKI:def 1;
hence s.n$1;
A46: for n st s.n M1 by A37,A48;
M<=M1 by A30,A48;
hence M=x0
proof
given k such that
A54: MXk;
hence contradiction by A48,A55,A56;
end;
end;
hence contradiction;
end;
consider m such that
A57: F.m=MX by A52;
M1 in NAT by ORDINAL1:def 12;
then
A58: F.(m+1)<=M1 by A37,A48,A52,A57;
A59: s.(F.(m+1))M1;
then F.(m+1)x0;
A61: now
let k;
consider n such that
A62: k<=n and
A63: s.n>=x0 by A16;
take n;
thus k<=n by A62;
s.n in rng s by VALUED_0:28;
then not s.n in {x0} by A7,XBOOLE_0:def 5;
then s.n<>x0 by TARSKI:def 1;
hence s.n>x0 by A63,XXREAL_0:1;
end;
then ex mn be Element of NAT st 0<=mn & s.mn>x0;
then
A64: ex m be Nat st X[m];
consider N be Nat such that
A65: X[N] & for n be Nat st X[n] holds N<=n from NAT_1:sch 5(
A64);
defpred X[Nat] means (s*F).$1x0
& for k st nx0 holds m<=k;
defpred X[Nat,set,set] means P[$2,$3];
A73: s*F is convergent by A5,A44,SEQ_4:16;
reconsider N9=N as Element of NAT by ORDINAL1:def 12;
A74: now
let n;
consider m such that
A75: n+1<=m and
A76: s.m>x0 by A61;
take m;
thus nx0 by A75,A76,NAT_1:13;
end;
A77: for n being Nat
for x be Element of NAT ex y be Element of NAT st X[n, x,y]
proof
let n be Nat;
let x be Element of NAT;
defpred X[Nat] means x<$1 & s.$1>x0;
ex m st X[m] by A74;
then
A78: ex m be Nat st X[m];
consider l be Nat such that
A79: X[l] & for k be Nat st X[k] holds l<=k from NAT_1:sch
5 (A78 );
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A79;
end;
consider G be sequence of NAT such that
A80: G.0=N9 & for n being Nat holds X[n,G.n,G.(n+1)] from RECDEF_1:sch
2(A77);
A81: rng G c=NAT by RELAT_1:def 19;
then
A82: rng G c=REAL by NUMBERS:19;
A83: dom G=NAT by FUNCT_2:def 1;
then reconsider G as Real_Sequence by A82,RELSET_1:4;
A84: now
let n;
G.n in rng G by A83,FUNCT_1:def 3;
hence G.n is Element of NAT by A81;
end;
now
let n be Nat;
A85: n in NAT by ORDINAL1:def 12;
A86: G.(n+1) is Element of NAT by A84;
G.n is Element of NAT by A84,A85;
hence G.nx0 & for m holds G.m<>$1;
A93: for n st s.n>x0 ex m st G.m=n
proof
assume ex n st X[n];
then
A94: ex n be Nat st X[n];
consider N1 be Nat such that
A95: X[N1] & for n be Nat st X[n] holds N1<=n from NAT_1:
sch 5(A94 );
defpred X[Nat] means $1x0 & ex m st G.m=$1;
A96: ex n be Nat st X[n]
proof
take N;
A97: N <> N1 by A80,A95;
N<=N1 by A65,A95;
hence Nx0 by A65;
take 0;
thus thesis by A80;
end;
A98: for n be Nat st X[n] holds n<=N1;
consider NX be Nat such that
A99: X[NX] & for n be Nat st X[n] holds n<=NX from NAT_1:
sch 6(A98,A96);
A100: for k st NXx0;
now
per cases;
suppose
ex m st G.m=k;
hence contradiction by A99,A101,A102,A103;
end;
suppose
for m holds G.m<>k;
hence contradiction by A95,A102,A103;
end;
end;
hence contradiction;
end;
consider m such that
A104: G.m=NX by A99;
N1 in NAT by ORDINAL1:def 12;
then
A105: G.(m+1)<=N1 by A80,A95,A99,A104;
A106: s.(G.(m+1))>x0 by A80,A104;
A107: NXN1;
then G.(m+1)x0;
A108: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
(s*G).k>x0;
P[G.k,G.(k+1)] by A80;
then s.(G.(k+1))>x0;
hence thesis by FUNCT_2:15;
end;
A109: X[0]by A65,A80,FUNCT_2:15;
A110: for k being Nat holds X[k] from NAT_1:sch 2(A109,A108);
A111: rng(s*G)c=dom f/\right_open_halfline(x0)
proof
let x be object;
assume
A112: x in rng(s*G);
then consider n such that
A113: (s*G).n=x by FUNCT_2:113;
(s*G).n>x0 by A110;
then x in {g1: x0x0 by TARSKI:def 1;
now
per cases by A124,XXREAL_0:1;
suppose
s.k= n1 by A125,SEQM_3:1;
then |.(f/*(s*F)).l-GR.|x0;
then consider l be Element of NAT such that
A126: k=G.l by A93,A122;
G.n2<=n by XXREAL_0:25;
then G.n2<=k by A123,XXREAL_0:2;
then l >= n2 by A126,SEQM_3:1;
then |.(f/*(s*G)).l-GR.|0 implies f^
is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))"
proof
assume that
A1: f is_convergent_in x0 and
A2: f"{0}={} and
A3: lim(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^)\{x0};
A9: lim(f/*seq)=lim(f,x0) by A1,A4,A6,A7,A8,Def4;
A10: (f/*seq)"=(f^)/*seq by A8,RFUNCT_2:12,XBOOLE_1:1;
A11: rng seq c=dom f by A4,A8,XBOOLE_1:1;
A12: f/*seq is convergent by A1,A4,A6,A7,A8;
hence (f^)/*seq is convergent by A3,A4,A9,A11,A10,RFUNCT_2:11,SEQ_2:21;
thus lim((f^)/*seq)=(lim(f,x0))" by A3,A4,A12,A9,A11,A10,RFUNCT_2:11
,SEQ_2:22;
end;
for r1,r2 st r10 & (for r1,r2 st r10 & f.g2<>0) implies f^ is_convergent_in x0 & lim(f^,x0)=(lim(f,x0))"
proof
assume that
A1: f is_convergent_in x0 and
A2: lim(f,x0)<>0 and
A3: for r1,r2 st r10 & f.g2<>0;
A4: dom f\f"{0}=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^)\{x0};
A9: f/*seq is non-zero by A8,RFUNCT_2:11,XBOOLE_1:1;
rng seq c=dom(f^) by A8,XBOOLE_1:1;
then
A10: rng seq c=dom f by A4,XBOOLE_1:1;
now
let x be object;
assume
A11: x in rng seq;
then not x in {x0} by A8,XBOOLE_0:def 5;
hence x in dom f\{x0} by A10,A11,XBOOLE_0:def 5;
end;
then
A12: rng seq c=dom f\{x0};
then
A13: lim(f/*seq)=lim(f,x0) by A1,A6,A7,Def4;
A14: (f/*seq)"=(f^)/*seq by A8,RFUNCT_2:12,XBOOLE_1:1;
A15: f/*seq is convergent by A1,A6,A7,A12;
hence (f^)/*seq is convergent by A2,A13,A9,A14,SEQ_2:21;
thus lim((f^)/*seq)=(lim(f,x0))" by A2,A15,A13,A9,A14,SEQ_2:22;
end;
now
let r1,r2;
assume that
A16: r10 and
A25: f.g2<>0 by A3,A16,A17;
take g1,g2;
not f.g2 in {0} by A25,TARSKI:def 1;
then
A26: not g2 in f"{0} by FUNCT_1:def 7;
not f.g1 in {0} by A24,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
hence r10 & (for
r1,r2 st r10 and
A4: for r1,r2 st r10 & f2.g2<>0 by
A10,A11,A12,A13,A14,A15,TARSKI:def 1;
end;
then
A16: f2^ is_convergent_in x0 by A2,A3,Th37;
A17: f1/f2=f1(#)(f2^) by RFUNCT_1:31;
hence f1/f2 is_convergent_in x0 by A1,A4,A16,Th38;
lim(f2^,x0)=(lim(f2,x0))" by A2,A3,A5,Th37;
hence lim(f1/f2,x0)=lim(f1,x0)*((lim(f2,x0))") by A1,A4,A17,A16,Th38
.=lim(f1,x0)/(lim(f2,x0)) by XCMPLX_0:def 9;
end;
theorem
f1 is_convergent_in x0 & lim(f1,x0)=0 & (for r1,r2 st r10 & f.g2<>0) implies f^ is_convergent_in x0 & lim(f^,
x0)=0
proof
A1: dom f\f"{0}=dom(f^) by RFUNCT_1:def 2;
assume
A2: f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0;
A3: now
let seq;
assume that
A4: seq is convergent and
A5: lim seq=x0 and
A6: rng seq c=dom(f^)\{x0};
rng seq c=dom(f^) by A6,XBOOLE_1:1;
then
A7: rng seq c=dom f by A1,XBOOLE_1:1;
A8: rng seq c=dom f\{x0}
proof
let x be object;
assume
A9: x in rng seq;
then not x in {x0} by A6,XBOOLE_0:def 5;
hence thesis by A7,A9,XBOOLE_0:def 5;
end;
now
per cases by A2;
suppose
f is_divergent_to+infty_in x0;
then
A10: f/*seq is divergent_to+infty by A4,A5,A8;
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,A11,RFUNCT_2:12
,XBOOLE_1:1;
end;
suppose
f is_divergent_to-infty_in x0;
then
A12: f/*seq is divergent_to-infty by A4,A5,A8;
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,A13,RFUNCT_2:12
,XBOOLE_1:1;
end;
end;
hence (f^)/*seq is convergent & lim((f^)/*seq)=0;
end;
assume
A14: for r1,r2 st r10 & f.g2<>0;
now
let r1,r2;
assume that
A15: r10 and
A24: f.g2<>0 by A14,A15,A16;
take g1,g2;
not f.g2 in {0} by A24,TARSKI:def 1;
then
A25: not g2 in f"{0} by FUNCT_1:def 7;
not f.g1 in {0} by A23,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
hence r10 &
f.g2<>0) & (ex r st 00 & f.g2<>0;
given r such that
A4: 00 and
A15: f.g2<>0 by A3,A6,A7;
not f.g2 in {0} by A15,TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then
A16: g2 in dom f\f"{0} by A13,XBOOLE_0:def 5;
take g1, g2;
not f.g1 in {0} by A14,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
then g1 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence thesis by A8,A9,A11,A12,A16,RFUNCT_1:def 2;
end;
let s be Real_Sequence;
assume that
A17: s is convergent and
A18: lim s=x0 and
A19: rng s c=dom(f^)\{x0};
consider k such that
A20: for n st k<=n holds x0-r0 by A32,SEQ_1:5;
hence 0<(f/*(s^\k)).n by A25,A24,A38,FUNCT_2:108,XBOOLE_1:1,A33;
end;
then
A39: for n being Nat holds 0<=n implies 0<(f/*(s^\k)).n;
f/*(s^\k) is convergent by A1,A17,A30,A28;
then (f/*(s^\k))" is divergent_to+infty by A31,A39,LIMFUNC1:35;
hence thesis by A23,LIMFUNC1:7;
end;
theorem
f is_convergent_in x0 & lim(f,x0)=0 & (for r1,r2 st r10 &
f.g2<>0) & (ex r st 00 & f.g2<>0;
given r such that
A4: 00 and
A15: f.g2<>0 by A3,A6,A7;
not f.g2 in {0} by A15,TARSKI:def 1;
then not g2 in f"{0} by FUNCT_1:def 7;
then
A16: g2 in dom f\f"{0} by A13,XBOOLE_0:def 5;
take g1,g2;
not f.g1 in {0} by A14,TARSKI:def 1;
then not g1 in f"{0} by FUNCT_1:def 7;
then g1 in dom f\f"{0} by A10,XBOOLE_0:def 5;
hence thesis by A8,A9,A11,A12,A16,RFUNCT_1:def 2;
end;
let s be Real_Sequence;
assume that
A17: s is convergent and
A18: lim s=x0 and
A19: rng s c=dom(f^)\{x0};
consider k such that
A20: for n st k<=n holds x0-r0 by A32,SEQ_1:5;
hence (f/*(s^\k)).n<0 by A25,A24,A38,FUNCT_2:108,XBOOLE_1:1;
end;
A39: for n being Nat holds 0<=n implies (f/*(s^\k)).n<0
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A33;
end;
f/*(s^\k) is convergent by A1,A17,A30,A28;
then (f/*(s^\k))" is divergent_to-infty by A31,A39,LIMFUNC1:36;
hence thesis by A23,LIMFUNC1:7;
end;
theorem
f is_convergent_in x0 & lim(f,x0)=0 & (ex r st 0