:: The Limit of a Real Function at a Point
:: by Jaros{\l}aw Kotowicz
::
:: Received September 5, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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<g & r<=r1 implies r-g<r1 & r<r1+g
proof
let g,r,r1 be Real;
assume that
A1: 0<g and
A2: r<=r1;
r-g<r1-0 by A1,A2,XREAL_1:15;
hence r-g<r1;
r+0<r1+g by A1,A2,XREAL_1:8;
hence thesis;
end;
Lm2: for X be set st rng seq c=dom(f1(#)f2)\X holds rng seq c=dom(f1(#)f2) &
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 set;
assume
A1: rng seq c=dom(f1(#)f2)\X;
hence
A2: rng seq c=dom(f1(#)f2) by XBOOLE_1:1;
thus
A3: dom(f1(#)f2)=dom f1/\dom f2 by VALUED_1:def 4;
then
A4: dom(f1(#)f2)c=dom f2 by XBOOLE_1:17;
dom(f1(#)f2)c=dom f1 by A3,XBOOLE_1:17;
hence rng seq c=dom f1 & rng seq c=dom f2 by A2,A4;
A5: dom(f1(#)f2)\X c=dom f2\X by A3,XBOOLE_1:17,33;
dom(f1(#)f2)\X c=dom f1\X by A3,XBOOLE_1:17,33;
hence thesis by A1,A5;
end;
Lm3: r-1/(n+1)<r & r<r+1/(n+1)
proof
0<1/(n+1) by XREAL_1:139;
hence thesis by Lm1;
end;
Lm4: for X be set st rng seq c=dom(f1+f2)\X holds rng seq c=dom(f1+f2) & 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 set;
assume
A1: rng seq c=dom(f1+f2)\X;
hence
A2: rng seq c=dom(f1+f2) by XBOOLE_1:1;
thus
A3: dom(f1+f2)=dom f1/\dom f2 by VALUED_1:def 1;
then
A4: dom(f1+f2)c=dom f2 by XBOOLE_1:17;
dom(f1+f2)c=dom f1 by A3,XBOOLE_1:17;
hence rng seq c=dom f1 & rng seq c=dom f2 by A2,A4;
A5: dom(f1+f2)\X c=dom f2\X by A3,XBOOLE_1:17,33;
dom(f1+f2)\X c=dom f1\X by A3,XBOOLE_1:17,33;
hence thesis by A1,A5;
end;
theorem Th1:
(rng seq c= dom f /\ left_open_halfline(x0) or rng seq c= dom f
/\ right_open_halfline(x0)) implies rng seq c= dom f \ {x0}
proof
assume
A1: rng seq c=dom f/\left_open_halfline(x0) or rng seq c=dom f/\
right_open_halfline(x0);
let x be object;
assume
A2: x in rng seq;
then consider n such that
A3: seq.n=x by FUNCT_2:113;
now
per cases by A1;
suppose
A4: rng seq c=dom f/\left_open_halfline(x0);
then seq.n in left_open_halfline(x0) by A2,A3,XBOOLE_0:def 4;
then seq.n in {g1: g1<x0} by XXREAL_1:229;
then ex g1 st g1=seq.n & g1<x0;
then
A5: not x in {x0} by A3,TARSKI:def 1;
seq.n in dom f by A2,A3,A4,XBOOLE_0:def 4;
hence thesis by A3,A5,XBOOLE_0:def 5;
end;
suppose
A6: rng seq c=dom f/\right_open_halfline(x0);
then seq.n in right_open_halfline(x0) by A2,A3,XBOOLE_0:def 4;
then seq.n in {g1: x0<g1} by XXREAL_1:230;
then ex g1 st g1=seq.n & x0<g1;
then
A7: not x in {x0} by A3,TARSKI:def 1;
seq.n in dom f by A2,A3,A6,XBOOLE_0:def 4;
hence thesis by A3,A7,XBOOLE_0:def 5;
end;
end;
hence thesis;
end;
theorem Th2:
(for n holds 0<|.x0-seq.n.| & |.x0-seq.n.|<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 \ {x0}
proof
assume
A1: for n holds 0<|.x0-seq.n.| & |.x0-seq.n.|<1/(n+1) & seq.n in dom f;
A2: now
let r be Real such that
A3: 0<r;
consider n being Nat such that
A4: r"<n by SEQ_4:3;
take n;
let k be Nat;
assume n<=k;
then n+1<=k+1 by XREAL_1:6;
then
A5: 1/(k+1)<=1/(n+1) by XREAL_1:118;
n<=n+1 by NAT_1:12;
then r"<n+1 by A4,XXREAL_0:2;
then 1/(n+1)<1/r" by A3,XREAL_1:76;
then 1/(k+1)<1/r" by A5,XXREAL_0:2;
then
A6: 1/(k+1)<r by XCMPLX_1:216;
k in NAT by ORDINAL1:def 12;
then |.x0-seq.k.|<1/(k+1) by A1;
then |.-(seq.k-x0).|<r by A6,XXREAL_0:2;
hence |.seq.k-x0.|<r by COMPLEX1:52;
end;
hence seq is convergent by SEQ_2:def 6;
hence lim seq=x0 by A2,SEQ_2:def 7;
thus
A7: rng seq c=dom f
proof
let x be object;
assume x in rng seq;
then ex n st seq.n=x by FUNCT_2:113;
hence thesis by A1;
end;
let x be object;
assume
A8: x in rng seq;
then consider n such that
A9: seq.n=x by FUNCT_2:113;
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 0<r ex n st for k st n<=k holds 0<|.x0-seq.k.| & |.x0-seq.k.|<r &
seq.k in dom f
proof
assume that
A1: seq is convergent and
A2: lim seq=x0 and
A3: rng seq c=dom f\{x0};
let r;
assume 0<r;
then consider n being Nat such that
A4: for k being Nat st n<=k holds |.seq.k-x0.|<r by A1,A2,SEQ_2:def 7;
reconsider n as Element of NAT by ORDINAL1:def 12;
take n;
let k;
assume n<=k;
then |.seq.k-x0.|<r by A4;
then
A5: |.-(x0-seq.k).|<r;
now
let n;
seq.n in rng seq by VALUED_0:28;
then not seq.n in {x0} by A3,XBOOLE_0:def 5;
hence seq.n-x0<>0 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.|<r by A5,COMPLEX1:52;
seq.k in rng seq by VALUED_0:28;
hence thesis by A3,XBOOLE_0:def 5;
end;
theorem Th4:
0<r implies ].x0-r,x0+r.[ \ {x0} = ].x0-r,x0.[ \/ ].x0,x0+r.[
proof
assume
A1: 0<r;
thus ].x0-r,x0+r.[\{x0}c=].x0-r,x0.[ \/ ].x0,x0+r.[
proof
let x be object;
assume
A2: x in ].x0-r,x0+r.[\{x0};
then consider r1 such that
A3: r1=x;
x in ].x0-r,x0+r.[ by A2,XBOOLE_0:def 5;
then x in {g2: x0-r<g2 & g2<x0+r} by RCOMP_1:def 2;
then
A4: ex g2 st g2=x & x0-r<g2 & g2<x0+r;
not x in {x0} by A2,XBOOLE_0:def 5;
then
A5: r1<>x0 by A3,TARSKI:def 1;
now
per cases by A5,XXREAL_0:1;
suppose
r1<x0;
then r1 in {g1: x0-r<g1 & g1<x0} by A3,A4;
then x in ].x0-r,x0.[ by A3,RCOMP_1:def 2;
hence thesis by XBOOLE_0:def 3;
end;
suppose
x0<r1;
then r1 in {g1: x0<g1 & g1<x0+r} by A3,A4;
then x in ].x0,x0+r.[ by A3,RCOMP_1:def 2;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
let x be object such that
A6: x in ].x0-r,x0.[\/].x0,x0+r.[;
now
per cases by A6,XBOOLE_0:def 3;
suppose
x in ].x0-r,x0.[;
then x in {g1: x0-r<g1 & g1<x0} by RCOMP_1:def 2;
then consider g1 such that
A7: g1=x and
A8: x0-r<g1 and
A9: g1<x0;
g1<x0+r by A1,A9,Lm1;
then x in {g2: x0-r<g2 & g2<x0+r} by A7,A8;
then
A10: x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
not x in {x0} by A7,A9,TARSKI:def 1;
hence thesis by A10,XBOOLE_0:def 5;
end;
suppose
x in ].x0,x0+r.[;
then x in {g1: x0<g1 & g1<x0+r} by RCOMP_1:def 2;
then consider g1 such that
A11: g1=x and
A12: x0<g1 and
A13: g1<x0+r;
x0-r<g1 by A1,A12,Lm1;
then x in {g2: x0-r<g2 & g2<x0+r} by A11,A13;
then
A14: x in ].x0-r,x0+r.[ by RCOMP_1:def 2;
not x in {x0} by A11,A12,TARSKI:def 1;
hence thesis by A14,XBOOLE_0:def 5;
end;
end;
hence thesis;
end;
theorem Th5:
0<r2 & ].x0-r2,x0.[ \/ ].x0,x0+r2.[ c= dom f implies for r1,r2 st
r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in
dom f
proof
assume that
A1: 0<r2 and
A2: ].x0-r2,x0.[\/].x0,x0+r2.[c=dom f;
A3: ].x0-r2,x0.[c=].x0-r2,x0.[\/].x0,x0+r2.[ by XBOOLE_1:7;
A4: ].x0,x0+r2.[c=].x0-r2,x0.[\/].x0,x0+r2.[ by XBOOLE_1:7;
let r1,r2;
assume that
A5: r1<x0 and
A6: x0<r2;
consider g1 such that
A7: r1<g1 and
A8: g1<x0 and
A9: g1 in dom f by A1,A2,A3,A5,LIMFUNC2:3,XBOOLE_1:1;
consider g2 such that
A10: g2<r2 and
A11: x0<g2 and
A12: g2 in dom f by A1,A2,A4,A6,LIMFUNC2:4,XBOOLE_1:1;
take g1;
take g2;
thus thesis by A7,A8,A9,A10,A11,A12;
end;
theorem Th6:
(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 \ {x0}
proof
assume
A1: for n holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f;
A2: for n being Nat holds x0-1/(n+1)<seq.n & seq.n<x0 & seq.n in dom f
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A1;
end;
hence seq is convergent & lim seq=x0 by LIMFUNC2:5;
rng seq c=dom f/\left_open_halfline(x0) by LIMFUNC2:5,A2;
hence thesis by Th1;
end;
theorem Th7:
seq is convergent & lim seq=x0 & 0<g implies ex k st for n st k<=
n holds x0-g<seq.n & seq.n<x0+g
proof
assume that
A1: seq is convergent and
A2: lim seq=x0 and
A3: 0<g;
x0-g<lim seq by A2,A3,Lm1;
then consider k1 be Nat such that
A4: for n being Nat st k1<=n holds x0-g<seq.n by A1,LIMFUNC2:1;
lim seq<x0+g by A2,A3,Lm1;
then consider k2 be Nat such that
A5: for n being Nat st k2<= n holds seq.n<x0+g by A1,LIMFUNC2:2;
reconsider k=max(k1,k2)as Element of NAT by ORDINAL1:def 12;
take k;
let n;
assume
A6: k<=n;
k1<=k by XXREAL_0:25;
then k1<=n by A6,XXREAL_0:2;
hence x0-g<seq.n by A4;
k2<=k by XXREAL_0:25;
then k2<=n by A6,XXREAL_0:2;
hence thesis by A5;
end;
theorem Th8:
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom
f & g2<r2 & x0<g2 & g2 in dom f) iff (for r st r<x0 ex g st r<g & g<x0 & g in
dom f) & for r st x0<r ex g st g<r & x0<g & g in dom f
proof
thus (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f) implies (for r st r<x0 ex g st r<g & g<x0 & g in
dom f) & for r st x0<r ex g st g<r & x0<g & g in dom f
proof
assume
A1: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f
& g2<r2 & x0<g2 & g2 in dom f;
thus for r st r<x0 ex g st r<g & g<x0 & g in dom f
proof
A2: x0<x0+1 by Lm1;
let r;
assume r<x0;
then consider g1,g2 such that
A3: r<g1 and
A4: g1<x0 and
A5: g1 in dom f and
g2<x0+1 and
x0<g2 and
g2 in dom f by A1,A2;
take g1;
thus thesis by A3,A4,A5;
end;
A6: x0-1<x0 by Lm1;
let r;
assume x0<r;
then consider g1,g2 such that
x0-1<g1 and
g1<x0 and
g1 in dom f and
A7: g2<r and
A8: x0<g2 and
A9: g2 in dom f by A1,A6;
take g2;
thus thesis by A7,A8,A9;
end;
assume that
A10: for r st r<x0 ex g st r<g & g<x0 & g in dom f and
A11: for r st x0<r ex g st g<r & x0<g & g in dom f;
let r1,r2;
assume that
A12: r1<x0 and
A13: x0<r2;
consider g2 such that
A14: g2<r2 and
A15: x0<g2 and
A16: g2 in dom f by A11,A13;
consider g1 such that
A17: r1<g1 and
A18: g1<x0 and
A19: g1 in dom f by A10,A12;
take g1;
take g2;
thus thesis by A17,A18,A19,A14,A15,A16;
end;
definition
let f,x0;
pred f is_convergent_in x0 means
(for r1,r2 st r1<x0 & x0<r2 ex g1,g2
st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & ex g st for seq
st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f/*seq is
convergent & lim(f/*seq)=g;
pred f is_divergent_to+infty_in x0 means
(for r1,r2 st r1<x0 & x0<r2
ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for
seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f/*seq is
divergent_to+infty;
pred f is_divergent_to-infty_in x0 means
(for r1,r2 st r1<x0 & x0<r2
ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for
seq st seq is convergent & lim seq=x0 & rng seq c= dom f \ {x0} holds f/*seq is
divergent_to-infty;
end;
theorem
f is_convergent_in x0 iff (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<
g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & ex g st for g1 st 0<
g1 ex g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds
|.f.r1-g.|<g1
proof
thus f is_convergent_in x0 implies (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st
r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & ex g st for g1 st
0<g1 ex g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds
|.f.r1-g.|<g1
proof
assume that
A1: f is_convergent_in x0 and
A2: (not for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) or for g ex g1 st 0<g1 & for g2 st 0<g2 ex
r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f & |.f.r1-g.|>=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 and
A5: for g2 st 0<g2 ex r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f
& |.f.r1-g.|>= 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.|<g1 by A4,A12,SEQ_2:def 7;
A14: |.(f/*s).n-g.|<g1 by A13;
A15: n in NAT by ORDINAL1:def 12;
rng s c=dom f by A8,Th2;
then |.f.(s.n)-g.|<g1 by A14,FUNCT_2:108,A15;
hence contradiction by A8,A15;
end;
assume
A16: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f
& g2<r2 & x0<g2 & g2 in dom f;
given g such that
A17: for g1 st 0<g1 ex g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<
g2 & r1 in dom f holds |.f.r1-g.|<g1;
now
let s be Real_Sequence;
assume that
A18: s is convergent and
A19: lim s=x0 and
A20: rng s c=dom f\{x0};
A21: now
let g1 be Real;
assume
A22: 0<g1;
consider g2 such that
A23: 0<g2 and
A24: for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds
|.f.r1 -g.|<g1 by A17,A22;
consider n such that
A25: for k st n<=k holds 0<|.x0-s.k.| & |.x0-s.k.|<g2 & s.k in dom
f by A18,A19,A20,A23,Th3;
reconsider n as Nat;
take n;
let k be Nat;
A26: k in NAT by ORDINAL1:def 12;
assume
A27: n<=k;
then
A28: |.x0-s.k.|<g2 by A25,A26;
A29: s.k in dom f by A25,A27,A26;
0<|.x0-s.k.| by A25,A27,A26;
then |.f.(s.k)-g.|<g1 by A24,A28,A29;
hence |.(f/*s).k-g.|<g1 by A20,FUNCT_2:108,XBOOLE_1:1,A26;
end;
hence f/*s is convergent by SEQ_2:def 6;
hence lim(f/*s)=g by A21,SEQ_2:def 7;
end;
hence thesis by A16;
end;
theorem
f is_divergent_to+infty_in x0 iff (for r1,r2 st r1<x0 & x0<r2 ex g1,g2
st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for g1 ex g2 st
0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds g1<f.r1
proof
thus f is_divergent_to+infty_in x0 implies (for r1,r2 st r1<x0 & x0<r2 ex g1
,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for g1 ex
g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds g1<f.r1
proof
assume that
A1: f is_divergent_to+infty_in x0 and
A2: (not for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) or ex g1 st for g2 st 0<g2 ex r1 st 0<
|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f & f.r1<=g1;
consider g1 such that
A3: for g2 st 0<g2 ex r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f
& f.r1<=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)<=g1;
A4: for n ex r1 being Element of REAL st X[n,r1]
proof let n;
consider r1 such that
A5: X[n,r1] by A3,XREAL_1:139;
reconsider r1 as Element of REAL by XREAL_0:def 1;
take r1;
thus thesis by A5;
end;
consider s be Real_Sequence such that
A6: for n holds X[n,s.n] from FUNCT_2:sch 3(A4);
A7: rng s c=dom f\{x0} by A6,Th2;
A8: lim s=x0 by A6,Th2;
s is convergent by A6,Th2;
then f/*s is divergent_to+infty by A1,A8,A7;
then consider n being Nat such that
A9: for k being Nat st n<=k holds g1<(f/*s).k;
A10: g1<(f/*s).n by A9;
A11: n in NAT by ORDINAL1:def 12;
rng s c=dom f by A6,Th2;
then g1<f.(s.n) by A10,FUNCT_2:108,A11;
hence contradiction by A6,A11;
end;
assume that
A12: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f
& g2<r2 & x0<g2 & g2 in dom f and
A13: for g1 ex g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1
in dom f holds g1<f.r1;
now
let s be Real_Sequence;
assume that
A14: s is convergent and
A15: lim s=x0 and
A16: rng s c=dom f\{x0};
now
let g1;
consider g2 such that
A17: 0<g2 and
A18: for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds g1<f
.r1 by A13;
consider n such that
A19: for k st n<=k holds 0<|.x0-s.k.| & |.x0-s.k.|<g2 & s.k in dom
f by A14,A15,A16,A17,Th3;
reconsider n as Nat;
take n;
let k be Nat;
A20: k in NAT by ORDINAL1:def 12;
assume
A21: n<=k;
then
A22: |.x0-s.k.|<g2 by A19,A20;
A23: s.k in dom f by A19,A21,A20;
0<|.x0-s.k.| by A19,A21,A20;
then g1<f.(s.k) by A18,A22,A23;
hence g1<(f/*s).k by A16,FUNCT_2:108,XBOOLE_1:1,A20;
end;
hence f/*s is divergent_to+infty;
end;
hence thesis by A12;
end;
theorem
f is_divergent_to-infty_in x0 iff (for r1,r2 st r1<x0 & x0<r2 ex g1,g2
st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for g1 ex g2 st
0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds f.r1<g1
proof
thus f is_divergent_to-infty_in x0 implies (for r1,r2 st r1<x0 & x0<r2 ex g1
,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & for g1 ex
g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds f.r1<g1
proof
assume that
A1: f is_divergent_to-infty_in x0 and
A2: (not for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) or ex g1 st for g2 st 0<g2 ex r1 st 0<
|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f & g1<=f.r1;
consider g1 such that
A3: for g2 st 0<g2 ex r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f
& g1<=f.r1 by A1,A2;
defpred X[Element of NAT,Real] means 0<|.x0-$2.| & |.x0-$2.|<1/(
$1+1) & $2 in dom f & g1<=f.($2);
A4: for n ex r1 being Element of REAL st X[n,r1]
proof let n;
consider r1 such that
A5: X[n,r1] by A3,XREAL_1:139;
reconsider r1 as Element of REAL by XREAL_0:def 1;
take r1;
thus thesis by A5;
end;
consider s be Real_Sequence such that
A6: for n holds X[n,s.n] from FUNCT_2:sch 3(A4);
A7: rng s c=dom f\{x0} by A6,Th2;
A8: lim s=x0 by A6,Th2;
s is convergent by A6,Th2;
then f/*s is divergent_to-infty by A1,A8,A7;
then consider n being Nat such that
A9: for k being Nat st n<=k holds (f/*s).k<g1;
A10: (f/*s).n<g1 by A9;
A11: n in NAT by ORDINAL1:def 12;
rng s c=dom f by A6,Th2;
then f.(s.n)<g1 by A10,FUNCT_2:108,A11;
hence contradiction by A6,A11;
end;
assume that
A12: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f
& g2<r2 & x0<g2 & g2 in dom f and
A13: for g1 ex g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1
in dom f holds f.r1<g1;
now
let s be Real_Sequence;
assume that
A14: s is convergent and
A15: lim s=x0 and
A16: rng s c=dom f\{x0};
now
let g1;
consider g2 such that
A17: 0<g2 and
A18: for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds f.r1
<g1 by A13;
consider n such that
A19: for k st n<=k holds 0<|.x0-s.k.| & |.x0-s.k.|<g2 & s.k in dom
f by A14,A15,A16,A17,Th3;
reconsider n as Nat;
take n;
let k be Nat;
A20: k in NAT by ORDINAL1:def 12;
assume
A21: n<=k;
then
A22: |.x0-s.k.|<g2 by A19,A20;
A23: s.k in dom f by A19,A21,A20;
0<|.x0-s.k.| by A19,A21,A20;
then f.(s.k)<g1 by A18,A22,A23;
hence (f/*s).k<g1 by A16,FUNCT_2:108,XBOOLE_1:1,A20;
end;
hence f/*s is divergent_to-infty;
end;
hence thesis by A12;
end;
theorem Th12:
f is_divergent_to+infty_in x0 iff f
is_left_divergent_to+infty_in x0 & f is_right_divergent_to+infty_in x0
proof
thus f is_divergent_to+infty_in x0 implies f is_left_divergent_to+infty_in
x0 & f is_right_divergent_to+infty_in x0
proof
assume
A1: f is_divergent_to+infty_in x0;
A2: now
let s be Real_Sequence;
assume that
A3: s is convergent and
A4: lim s=x0 and
A5: rng s c=dom f/\left_open_halfline(x0);
rng s c=dom f\{x0} by A5,Th1;
hence f/*s is divergent_to+infty by A1,A3,A4;
end;
A6: now
let s be Real_Sequence;
assume that
A7: s is convergent and
A8: lim s=x0 and
A9: rng s c=dom f/\ right_open_halfline(x0);
rng s c=dom f\{x0} by A9,Th1;
hence f/*s is divergent_to+infty by A1,A7,A8;
end;
A10: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f by A1;
then for r st r<x0 ex g st r<g & g<x0 & g in dom f by Th8;
hence f is_left_divergent_to+infty_in x0 by A2,LIMFUNC2:def 2;
for r st x0<r ex g st g<r & x0<g & g in dom f by A10,Th8;
hence thesis by A6,LIMFUNC2:def 5;
end;
assume that
A11: f is_left_divergent_to+infty_in x0 and
A12: f is_right_divergent_to+infty_in x0;
A13: for r st x0<r ex g st g<r & x0<g & g in dom f by A12,LIMFUNC2:def 5;
A14: now
let s be Real_Sequence such that
A15: s is convergent and
A16: lim s=x0 and
A17: rng s c=dom f\{x0};
now
per cases;
suppose
ex k st for n st k<=n holds s.n<x0;
then consider k such that
A18: for n st k<=n holds s.n<x0;
A19: rng s c=dom f by A17,XBOOLE_1:1;
A20: rng(s^\k)c=dom f/\left_open_halfline(x0)
proof
let x be object;
assume x in rng(s^\k);
then consider n such that
A21: (s^\k).n=x by FUNCT_2:113;
s.(n+k)<x0 by A18,NAT_1:12;
then s.(n+k) in {g1: g1<x0};
then s.(n+k) in left_open_halfline(x0) by XXREAL_1:229;
then
A22: x in left_open_halfline(x0) by A21,NAT_1:def 3;
s.(n+k) in rng s by VALUED_0:28;
then x in rng s by A21,NAT_1:def 3;
hence thesis by A19,A22,XBOOLE_0:def 4;
end;
A23: f/*(s^\k) =(f/*s)^\k by A17,VALUED_0:27,XBOOLE_1:1;
lim(s^\k)=x0 by A15,A16,SEQ_4:20;
then f/*(s^\k) is divergent_to+infty by A11,A15,A20,LIMFUNC2:def 2;
hence f/*s is divergent_to+infty by A23,LIMFUNC1:7;
end;
suppose
A24: for k ex n st k<=n & s.n>=x0;
now
per cases;
suppose
ex k st for n st k<=n holds x0<s.n;
then consider k such that
A25: for n st k<=n holds s.n>x0;
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+k) by A25,NAT_1:12;
then s.(n+k) in {g1: x0<g1};
then s.(n+k) in right_open_halfline(x0) by XXREAL_1:230;
then
A29: x in right_open_halfline(x0) by A28,NAT_1:def 3;
s.(n+k) in rng s by VALUED_0:28;
then x in rng s by A28,NAT_1:def 3;
hence thesis by A26,A29,XBOOLE_0:def 4;
end;
A30: f/*(s^\k) =(f/*s)^\k by A17,VALUED_0:27,XBOOLE_1:1;
lim(s^\k)=x0 by A15,A16,SEQ_4:20;
then f/*(s^\k) is divergent_to+infty by A12,A15,A27,LIMFUNC2:def 5;
hence f/*s is divergent_to+infty by A30,LIMFUNC1:7;
end;
suppose
A31: for k ex n st k<=n & x0>=s.n;
defpred X[Nat] means s.$1<x0;
A32: now
let k;
consider n such that
A33: k<=n and
A34: s.n<=x0 by A31;
take n;
thus k<=n by A33;
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 A34,XXREAL_0:1;
end;
then ex m1 be Element of NAT st 0<=m1 & s.m1<x0;
then
A35: ex m be Nat st X[m];
consider M be Nat such that
A36: X[M] & for n be Nat st X[n] holds M <= n from NAT_1:sch 5
(A35);
defpred X[Nat] means s.$1>x0;
defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s.m<x0
& for k st n<k & s.k<x0 holds m<=k;
defpred X[Nat,set,set] means P[$2,$3];
reconsider M9=M as Element of NAT by ORDINAL1:def 12;
A37: now
let n;
consider m such that
A38: n+1<=m and
A39: s.m<x0 by A32;
take m;
thus n<m & s.m<x0 by A38,A39,NAT_1:13;
end;
A40: 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 A37;
then
A41: ex m be Nat st X[m];
consider l be Nat such that
A42: X[l] & for k be Nat st X[k] holds l <= k from NAT_1:sch
5(A41);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A42;
end;
consider F be sequence of NAT such that
A43: F.0=M9 & for n being Nat holds X[n,F.n,F.(n+1)] from RECDEF_1:sch 2
(A40);
A44: rng F c=NAT by RELAT_1:def 19;
then
A45: rng F c=REAL by NUMBERS:19;
A46: dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A45,RELSET_1:4;
A47: now
let n;
F.n in rng F by A46,FUNCT_1:def 3;
hence F.n is Element of NAT by A44;
end;
now
let n be Nat;
A48: F.(n+1) is Element of NAT by A47;
A49: n in NAT by ORDINAL1:def 12;
F.n is Element of NAT by A47,A49;
hence F.n<F.(n+1) by A43,A48;
end;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A50: s*F is subsequence of s by VALUED_0:def 17;
then rng(s*F)c=rng s by VALUED_0:21;
then
A51: rng(s*F)c=dom f\{x0} by A17;
A52: for n st s.n<x0 ex m st F.m=n
proof
defpred X[Nat] means s.$1<x0 & for m holds F.m<>$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 & s.$1<x0 & ex m st F.m=$1;
A55: ex n be Nat st X[n]
proof
take M;
A56: M <> M1 by A43,A54;
M<=M1 by A36,A54;
hence M<M1 by A56,XXREAL_0:1;
thus s.M<x0 by A36;
take 0;
thus thesis by A43;
end;
A57: for n be Nat st X[n] holds n<=M1;
consider MX be Nat such that
A58: X[MX] & for n be Nat st X[n] holds n<=MX from NAT_1:sch
6(A57,A55);
A59: for k st MX<k & k<M1 holds s.k>=x0
proof
given k such that
A60: MX<k and
A61: k<M1 and
A62: s.k<x0;
now
per cases;
suppose
ex m st F.m=k;
hence contradiction by A58,A60,A61,A62;
end;
suppose
for m holds F.m<>k;
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))<x0 by A43,A63;
A66: MX<F.(m+1) by A43,A63;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A64,XXREAL_0:1;
hence contradiction by A59,A66,A65;
end;
hence contradiction by A54;
end;
A67: now
let k;
consider n such that
A68: k<=n and
A69: s.n>=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).$1<x0;
A72: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
(s*F).k<x0;
P[F.k,F.(k+1)] by A43;
then s.(F.(k+1))<x0;
hence thesis by FUNCT_2:15;
end;
A73: X[0] by A36,A43,FUNCT_2:15;
A74: for k being Nat holds X[k] from NAT_1:sch 2(A73,A72);
A75: rng(s*F)c=dom f/\left_open_halfline(x0)
proof
let x be object;
assume
A76: x in rng(s*F);
then consider n such that
A77: (s*F).n=x by FUNCT_2:113;
(s*F).n<x0 by A74;
then x in {g1: g1<x0} by A77;
then
A78: x in left_open_halfline(x0) by XXREAL_1:229;
x in dom f by A51,A76,XBOOLE_0:def 5;
hence thesis by A78,XBOOLE_0:def 4;
end;
defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s.m>x0
& for k st n<k & s.k>x0 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 n<m & s.m>x0 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.n<G.(n+1) by A86,A92;
end;
then reconsider G as increasing sequence of NAT by SEQM_3:def 6;
A93: s*G is subsequence of s by VALUED_0:def 17;
then rng(s*G)c=rng s by VALUED_0:21;
then
A94: rng(s*G)c=dom f\{x0} by A17;
defpred X[Nat] means s.$1>x0 & 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 $1<N1 & s.$1>x0 & 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 N<N1 by A99,XXREAL_0:1;
thus s.N>x0 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 NX<k & k<N1 holds s.k<=x0
proof
given k such that
A103: NX<k and
A104: k<N1 and
A105: s.k>x0;
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: NX<G.(m+1) by A86,A106;
now
assume G.(m+1)<>N1;
then G.(m+1)<N1 by A107,XXREAL_0:1;
hence contradiction by A102,A109,A108;
end;
hence contradiction by A97;
end;
defpred X[Nat] means (s*G).$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: x0<g1} by A115;
then
A116: x in right_open_halfline(x0) by XXREAL_1:230;
x in dom f by A94,A114,XBOOLE_0:def 5;
hence thesis by A116,XBOOLE_0:def 4;
end;
A117: s*G is convergent by A15,A93,SEQ_4:16;
lim(s*G)=x0 by A15,A16,A93,SEQ_4:17;
then
A118: f/*(s*G) is divergent_to+infty by A12,A117,A113,LIMFUNC2:def 5;
lim(s*F)=x0 by A15,A16,A50,SEQ_4:17;
then
A119: f/*(s*F) is divergent_to+infty by A11,A79,A75,LIMFUNC2:def 2;
now
let r;
consider n1 be Nat such that
A120: for k being Nat st n1<=k holds r<(f/*(s*F)).k
by A119;
consider n2 be Nat such that
A121: for k being Nat st n2<=k holds r<(f/*(s*G)).k
by A118;
reconsider n=max(F.n1,G.n2) as Nat;
take n;
let k be Nat;
A122: k in NAT by ORDINAL1:def 12;
assume
A123: n<=k;
s.k in rng s by VALUED_0:28;
then not s.k in {x0} by A17,XBOOLE_0:def 5;
then
A124: s.k<>x0 by TARSKI:def 1;
now
per cases by A124,XXREAL_0:1;
suppose
s.k<x0;
then consider l be Element of NAT such that
A125: k=F.l by A52,A122;
F.n1<=n by XXREAL_0:25;
then F.n1<=k by A123,XXREAL_0:2;
then l >= n1 by A125,SEQM_3:1;
then r<(f/*(s*F)).l by A120;
then r<f.((s*F).l) by A51,FUNCT_2:108,XBOOLE_1:1;
then r<f.(s.k) by A125,FUNCT_2:15;
hence r<(f/*s).k by A17,FUNCT_2:108,XBOOLE_1:1,A122;
end;
suppose
s.k>x0;
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<f.((s*G).l) by A94,FUNCT_2:108,XBOOLE_1:1;
then r<f.(s.k) by A126,FUNCT_2:15;
hence r<(f/*s).k by A17,FUNCT_2:108,XBOOLE_1:1,A122;
end;
end;
hence r<(f/*s).k;
end;
hence f/*s is divergent_to+infty;
end;
end;
hence f/*s is divergent_to+infty;
end;
end;
hence f/*s is divergent_to+infty;
end;
for r st r<x0 ex g st r<g & g<x0 & g in dom f by A11,LIMFUNC2:def 2;
then
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2
<r2 & x0<g2 & g2 in dom f by A13,Th8;
hence thesis by A14;
end;
theorem Th13:
f is_divergent_to-infty_in x0 iff f
is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0
proof
thus f is_divergent_to-infty_in x0 implies f is_left_divergent_to-infty_in
x0 & f is_right_divergent_to-infty_in x0
proof
assume
A1: f is_divergent_to-infty_in x0;
A2: now
let s be Real_Sequence;
assume that
A3: s is convergent and
A4: lim s=x0 and
A5: rng s c=dom f/\left_open_halfline(x0);
rng s c=dom f\{x0} by A5,Th1;
hence f/*s is divergent_to-infty by A1,A3,A4;
end;
A6: now
let s be Real_Sequence;
assume that
A7: s is convergent and
A8: lim s=x0 and
A9: rng s c=dom f/\ right_open_halfline(x0);
rng s c=dom f\{x0} by A9,Th1;
hence f/*s is divergent_to-infty by A1,A7,A8;
end;
A10: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f by A1;
then for r st r<x0 ex g st r<g & g<x0 & g in dom f by Th8;
hence f is_left_divergent_to-infty_in x0 by A2,LIMFUNC2:def 3;
for r st x0<r ex g st g<r & x0<g & g in dom f by A10,Th8;
hence thesis by A6,LIMFUNC2:def 6;
end;
assume that
A11: f is_left_divergent_to-infty_in x0 and
A12: f is_right_divergent_to-infty_in x0;
A13: now
let s be Real_Sequence such that
A14: s is convergent and
A15: lim s=x0 and
A16: rng s c=dom f\{x0};
now
per cases;
suppose
ex k st for n st k<=n holds s.n<x0;
then consider k such that
A17: for n st k<=n holds s.n<x0;
A18: rng s c=dom f by A16,XBOOLE_1:1;
A19: rng(s^\k)c=dom f/\left_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;
s.(n+k)<x0 by A17,NAT_1:12;
then s.(n+k) in {g1: g1<x0};
then s.(n+k) in left_open_halfline(x0) by XXREAL_1:229;
then
A21: x in left_open_halfline(x0) by A20,NAT_1:def 3;
s.(n+k) in rng s by VALUED_0:28;
then x in rng s by A20,NAT_1:def 3;
hence thesis by A18,A21,XBOOLE_0:def 4;
end;
A22: f/*(s^\k) =(f/*s)^\k by A16,VALUED_0:27,XBOOLE_1:1;
lim(s^\k)=x0 by A14,A15,SEQ_4:20;
then f/*(s^\k) is divergent_to-infty by A11,A14,A19,LIMFUNC2:def 3;
hence f/*s is divergent_to-infty by A22,LIMFUNC1:7;
end;
suppose
A23: for k ex n st k<=n & s.n>=x0;
now
per cases;
suppose
ex k st for n st k<=n holds x0<s.n;
then consider k such that
A24: for n st k<=n holds s.n>x0;
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+k) by A24,NAT_1:12;
then s.(n+k) in {g1: x0<g1};
then s.(n+k) in right_open_halfline(x0) by XXREAL_1:230;
then
A28: x in right_open_halfline(x0) by A27,NAT_1:def 3;
s.(n+k) in rng s by VALUED_0:28;
then x in rng s by A27,NAT_1:def 3;
hence thesis by A25,A28,XBOOLE_0:def 4;
end;
A29: f/*(s^\k) =(f/*s)^\k by A16,VALUED_0:27,XBOOLE_1:1;
lim(s^\k)=x0 by A14,A15,SEQ_4:20;
then f/*(s^\k) is divergent_to-infty by A12,A14,A26,LIMFUNC2:def 6;
hence f/*s is divergent_to-infty by A29,LIMFUNC1:7;
end;
suppose
A30: for k ex n st k<=n & x0>=s.n;
defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s.m<x0
& for k st n<k & s.k<x0 holds m<=k;
defpred X[Nat,set,set] means P[$2,$3];
defpred X[Nat] means s.$1<x0;
A31: now
let k;
consider n such that
A32: k<=n and
A33: s.n<=x0 by A30;
take n;
thus k<=n by A32;
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 A33,XXREAL_0:1;
end;
then ex m1 be Element of NAT st 0<=m1 & s.m1<x0;
then
A34: ex m be Nat st X[m];
consider M be Nat such that
A35: X[M] & for n be Nat st X[n] holds M<=n from NAT_1:sch 5(
A34);
reconsider M9=M as Element of NAT by ORDINAL1:def 12;
A36: now
let n;
consider m such that
A37: n+1<=m and
A38: s.m<x0 by A31;
take m;
thus n<m & s.m<x0 by A37,A38,NAT_1:13;
end;
A39: 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 A36;
then
A40: ex m be Nat st X[m];
consider l be Nat such that
A41: X[l] & for k be Nat st X[k] holds l<=k from NAT_1:sch 5
(A40);
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A41;
end;
consider F be sequence of NAT such that
A42: F.0=M9 & for n being Nat holds X[n,F.n,F.(n+1)] from RECDEF_1:sch 2
(A39);
A43: rng F c=NAT by RELAT_1:def 19;
then
A44: rng F c=REAL by NUMBERS:19;
A45: dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A44,RELSET_1:4;
A46: now
let n;
F.n in rng F by A45,FUNCT_1:def 3;
hence F.n is Element of NAT by A43;
end;
now
let n be Nat;
A47: n in NAT by ORDINAL1:def 12;
A48: F.(n+1) is Element of NAT by A46;
F.n is Element of NAT by A46,A47;
hence F.n<F.(n+1) by A42,A48;
end;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A49: s*F is subsequence of s by VALUED_0:def 17;
then rng(s*F)c=rng s by VALUED_0:21;
then
A50: rng(s*F)c=dom f\{x0} by A16;
defpred X[Nat] means s.$1<x0 & for m holds F.m<>$1;
A51: for n st s.n<x0 ex m st F.m=n
proof
assume ex n st X[n];
then
A52: ex n be Nat st X[n];
consider M1 be Nat such that
A53: X[M1] & for n be Nat st X[n] holds M1<=n from NAT_1:sch
5(A52);
defpred X[Nat] means $1<M1 & s.$1<x0 & ex m st F.m=$1;
A54: ex n be Nat st X[n]
proof
take M;
A55: M <> M1 by A42,A53;
M<=M1 by A35,A53;
hence M<M1 by A55,XXREAL_0:1;
thus s.M<x0 by A35;
take 0;
thus thesis by A42;
end;
A56: for n be Nat st X[n] holds n<=M1;
consider MX be Nat such that
A57: X[MX] & for n be Nat st X[n] holds n<=MX from NAT_1:sch
6(A56,A54);
A58: for k st MX<k & k<M1 holds s.k>=x0
proof
given k such that
A59: MX<k and
A60: k<M1 and
A61: s.k<x0;
now
per cases;
suppose
ex m st F.m=k;
hence contradiction by A57,A59,A60,A61;
end;
suppose
for m holds F.m<>k;
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))<x0 by A42,A62;
A65: MX<F.(m+1) by A42,A62;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A63,XXREAL_0:1;
hence contradiction by A58,A65,A64;
end;
hence contradiction by A53;
end;
defpred X[Nat] means s.$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).$1<x0;
A71: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
(s*F).k<x0;
P[F.k,F.(k+1)] by A42;
then s.(F.(k+1))<x0;
hence thesis by FUNCT_2:15;
end;
A72: X[0] by A35,A42,FUNCT_2:15;
A73: for k being Nat holds X[k] from NAT_1:sch 2(A72,A71);
A74: rng(s*F)c=dom f/\left_open_halfline(x0)
proof
let x be object;
assume
A75: x in rng(s*F);
then consider n such that
A76: (s*F).n=x by FUNCT_2:113;
(s*F).n<x0 by A73;
then x in {g1: g1<x0} by A76;
then
A77: x in left_open_halfline(x0) by XXREAL_1:229;
x in dom f by A50,A75,XBOOLE_0:def 5;
hence thesis by A77,XBOOLE_0:def 4;
end;
defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s.m>x0
& for k st n<k & s.k>x0 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 n<m & s.m>x0 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.n<G.(n+1) by A86,A92;
end;
then reconsider G as increasing sequence of NAT by SEQM_3:def 6;
A93: s*G is subsequence of s by VALUED_0:def 17;
then rng(s*G)c=rng s by VALUED_0:21;
then
A94: rng(s*G)c=dom f\{x0} by A16;
defpred X[Nat] means s.$1>x0 & 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 $1<N1 & s.$1>x0 & 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 N<N1 by A99,XXREAL_0:1;
thus s.N>x0 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 NX<k & k<N1 holds s.k<=x0
proof
given k such that
A103: NX<k and
A104: k<N1 and
A105: s.k>x0;
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: NX<G.(m+1) by A86,A106;
now
assume G.(m+1)<>N1;
then G.(m+1)<N1 by A107,XXREAL_0:1;
hence contradiction by A102,A109,A108;
end;
hence contradiction by A97;
end;
defpred X[Nat] means (s*G).$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: x0<g1} by A115;
then
A116: x in right_open_halfline(x0) by XXREAL_1:230;
x in dom f by A94,A114,XBOOLE_0:def 5;
hence thesis by A116,XBOOLE_0:def 4;
end;
A117: s*G is convergent by A14,A93,SEQ_4:16;
lim(s*G)=x0 by A14,A15,A93,SEQ_4:17;
then
A118: f/*(s*G) is divergent_to-infty by A12,A117,A113,LIMFUNC2:def 6;
now
let r;
consider n1 be Nat such that
A119: for k being Nat st n1<=k holds (f/*(s*F)).k<r
by A79;
consider n2 be Nat such that
A120: for k being Nat st n2<=k holds (f/*(s*G)).k<r
by A118;
reconsider n=max(F.n1,G.n2) as Nat;
take n;
let k be Nat;
A121: k in NAT by ORDINAL1:def 12;
assume
A122: n<=k;
s.k in rng s by VALUED_0:28;
then not s.k in {x0} by A16,XBOOLE_0:def 5;
then
A123: s.k<>x0 by TARSKI:def 1;
now
per cases by A123,XXREAL_0:1;
suppose
s.k<x0;
then consider l be Element of NAT such that
A124: k=F.l by A51,A121;
F.n1<=n by XXREAL_0:25;
then F.n1<=k by A122,XXREAL_0:2;
then l >= n1 by A124,SEQM_3:1;
then (f/*(s*F)).l<r by A119;
then f.((s*F).l)<r by A50,FUNCT_2:108,XBOOLE_1:1;
then f.(s.k)<r by A124,FUNCT_2:15;
hence (f/*s).k<r by A16,FUNCT_2:108,XBOOLE_1:1,A121;
end;
suppose
s.k>x0;
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)).l<r by A120;
then f.((s*G).l)<r by A94,FUNCT_2:108,XBOOLE_1:1;
then f.(s.k)<r by A125,FUNCT_2:15;
hence (f/*s).k<r by A16,FUNCT_2:108,XBOOLE_1:1,A121;
end;
end;
hence (f/*s).k<r;
end;
hence f/*s is divergent_to-infty;
end;
end;
hence f/*s is divergent_to-infty;
end;
end;
hence f/*s is divergent_to-infty;
end;
now
let r1,r2;
assume that
A126: r1<x0 and
A127: x0<r2;
consider g1 such that
A128: r1<g1 and
A129: g1<x0 and
A130: g1 in dom f by A11,A126,LIMFUNC2:def 3;
consider g2 such that
A131: g2<r2 and
A132: x0<g2 and
A133: g2 in dom f by A12,A127,LIMFUNC2:def 6;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f by A128,A129
,A130,A131,A132,A133;
end;
hence thesis by A13;
end;
theorem
f1 is_divergent_to+infty_in x0 & f2 is_divergent_to+infty_in x0 & (for
r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f1 /\ dom f2 & g2<
r2 & x0<g2 & g2 in dom f1 /\ dom f2) implies f1+f2 is_divergent_to+infty_in x0
& f1(#)f2 is_divergent_to+infty_in x0
proof
assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: f2 is_divergent_to+infty_in x0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f1
/\dom f2 & g2<r2 & x0<g2 & g2 in dom f1/\dom f2;
A4: now
let s be Real_Sequence;
assume that
A5: s is convergent and
A6: lim s=x0 and
A7: rng s c=dom(f1+f2)\{x0};
rng s c=dom f2\{x0} by A7,Lm4;
then
A8: f2/*s is divergent_to+infty by A2,A5,A6;
rng s c=dom f1\{ x0} by A7,Lm4;
then f1/*s is divergent_to+infty by A1,A5,A6;
then
A9: f1/*s+f2/*s is divergent_to+infty by A8,LIMFUNC1:8;
A10: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
rng s c=dom(f1+f2) by A7,Lm4;
hence (f1+f2)/*s is divergent_to+infty by A10,A9,RFUNCT_2:8;
end;
A11: now
let s be Real_Sequence;
assume that
A12: s is convergent and
A13: lim s=x0 and
A14: rng s c=dom(f1(#)f2)\{x0};
rng s c=dom f2\{x0} by A14,Lm2;
then
A15: f2/*s is divergent_to+infty by A2,A12,A13;
rng s c=dom f1\{x0} by A14,Lm2;
then f1/*s is divergent_to+infty by A1,A12,A13;
then
A16: (f1/*s)(#)(f2/*s) is divergent_to+infty by A15,LIMFUNC1:10;
A17: dom(f1(#) f2)=dom f1/\dom f2 by A14,Lm2;
rng s c=dom(f1(#)f2) by A14,Lm2;
hence (f1(#)f2)/*s is divergent_to+infty by A17,A16,RFUNCT_2:8;
end;
now
let r1,r2;
assume that
A18: r1<x0 and
A19: x0<r2;
consider g1,g2 such that
A20: r1<g1 and
A21: g1<x0 and
A22: g1 in dom f1/\dom f2 and
A23: g2<r2 and
A24: x0<g2 and
A25: g2 in dom f1/\dom f2 by A3,A18,A19;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)
by A20,A21,A22,A23,A24,A25,VALUED_1:def 1;
end;
hence f1+f2 is_divergent_to+infty_in x0 by A4;
now
let r1,r2;
assume that
A26: r1<x0 and
A27: x0<r2;
consider g1,g2 such that
A28: r1<g1 and
A29: g1<x0 and
A30: g1 in dom f1/\dom f2 and
A31: g2<r2 and
A32: x0<g2 and
A33: g2 in dom f1/\dom f2 by A3,A26,A27;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)
f2) by A28,A29,A30,A31,A32,A33,VALUED_1:def 4;
end;
hence thesis by A11;
end;
theorem
f1 is_divergent_to-infty_in x0 & f2 is_divergent_to-infty_in x0 & (for
r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f1 /\ dom f2 & g2<
r2 & x0<g2 & g2 in dom f1 /\ dom f2) implies f1+f2 is_divergent_to-infty_in x0
& f1(#) f2 is_divergent_to+infty_in x0
proof
assume that
A1: f1 is_divergent_to-infty_in x0 and
A2: f2 is_divergent_to-infty_in x0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f1
/\dom f2 & g2<r2 & x0<g2 & g2 in dom f1/\dom f2;
A4: now
let s be Real_Sequence;
assume that
A5: s is convergent and
A6: lim s=x0 and
A7: rng s c=dom(f1+f2)\{x0};
rng s c=dom f2\{x0} by A7,Lm4;
then
A8: f2/*s is divergent_to-infty by A2,A5,A6;
rng s c=dom f1\{ x0} by A7,Lm4;
then f1/*s is divergent_to-infty by A1,A5,A6;
then
A9: f1/*s+f2/*s is divergent_to-infty by A8,LIMFUNC1:11;
A10: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
rng s c=dom(f1+f2) by A7,Lm4;
hence (f1+f2)/*s is divergent_to-infty by A10,A9,RFUNCT_2:8;
end;
A11: now
let s be Real_Sequence;
assume that
A12: s is convergent and
A13: lim s=x0 and
A14: rng s c=dom(f1(#)f2)\{x0};
rng s c=dom f2\{x0} by A14,Lm2;
then
A15: f2/*s is divergent_to-infty by A2,A12,A13;
rng s c=dom f1\{x0} by A14,Lm2;
then f1/*s is divergent_to-infty by A1,A12,A13;
then
A16: (f1/*s)(#)(f2/*s) is divergent_to+infty by A15,LIMFUNC1:24;
A17: dom(f1(#) f2)=dom f1/\dom f2 by A14,Lm2;
rng s c=dom(f1(#)f2) by A14,Lm2;
hence (f1(#)f2)/*s is divergent_to+infty by A17,A16,RFUNCT_2:8;
end;
now
let r1,r2;
assume that
A18: r1<x0 and
A19: x0<r2;
consider g1,g2 such that
A20: r1<g1 and
A21: g1<x0 and
A22: g1 in dom f1/\dom f2 and
A23: g2<r2 and
A24: x0<g2 and
A25: g2 in dom f1/\dom f2 by A3,A18,A19;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)
by A20,A21,A22,A23,A24,A25,VALUED_1:def 1;
end;
hence f1+f2 is_divergent_to-infty_in x0 by A4;
now
let r1,r2;
assume that
A26: r1<x0 and
A27: x0<r2;
consider g1,g2 such that
A28: r1<g1 and
A29: g1<x0 and
A30: g1 in dom f1/\dom f2 and
A31: g2<r2 and
A32: x0<g2 and
A33: g2 in dom f1/\dom f2 by A3,A26,A27;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)
f2) by A28,A29,A30,A31,A32,A33,VALUED_1:def 4;
end;
hence thesis by A11;
end;
theorem
f1 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2
st r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2)) & (ex r
st 0<r & f2|(].x0-r,x0.[ \/ ].x0,x0+r.[) is bounded_below ) implies f1+f2
is_divergent_to+infty_in x0
proof
assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1+
f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2);
given r such that
A3: 0<r and
A4: f2|(].x0-r,x0.[ \/ ].x0,x0+r.[) is bounded_below;
now
let s be Real_Sequence;
assume that
A5: s is convergent and
A6: lim s=x0 and
A7: rng s c=dom(f1+f2)\{x0};
consider k such that
A8: for n st k<=n holds x0-r<s.n & s.n<x0+r by A3,A5,A6,Th7;
rng(s^\k)c=rng s by VALUED_0:21;
then
A9: rng(s^\k)c=dom(f1+f2)\{x0} by A7;
then
A10: rng(s^\k)c=dom f1\{x0} by Lm4;
A11: rng(s^\k)c=dom f2 by A9,Lm4;
now
consider r1 be Real such that
A12: for g being object st g in (].x0-r,x0.[\/].x0,x0+r.[)/\dom f2
holds r1<=f2.g by A4,RFUNCT_1:71;
take r2=r1-1;
let n be Nat;
A13: n in NAT by ORDINAL1:def 12;
A14: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A8;
then
A15: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A8,A14;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: x0-r<g2 & g2<x0+r} by A15;
then
A16: (s^\k).n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A17: (s^\k).n in rng(s ^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A9,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A16,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by A3,Th4;
then (s^\k).n in (].x0-r,x0.[\/].x0,x0+r.[)/\dom f2 by A11,A17,
XBOOLE_0:def 4;
then r1-1<f2.((s^\k).n)-0 by A12,XREAL_1:15;
hence r2<(f2/*(s^\k)).n by A11,FUNCT_2:108,A13;
end;
then
A18: f2/*(s^\k) is bounded_below by SEQ_2:def 4;
lim(s^\k)=x0 by A5,A6,SEQ_4:20;
then f1/*(s^\k) is divergent_to+infty by A1,A5,A10;
then
A19: f1/*(s^\k)+f2/*(s^\k) is divergent_to+infty by A18,LIMFUNC1:9;
A20: rng s c=dom(f1+f2) by A7,Lm4;
rng(s^\k)c=dom(f1+f2) by A9,Lm4;
then rng(s^\k)c=dom f1/\dom f2 by VALUED_1:def 1;
then f1/*(s^\k)+f2/*(s^\k)=(f1+f2)/*(s^\k) by RFUNCT_2:8
.=((f1+f2)/*s)^\k by A20,VALUED_0:27;
hence (f1+f2)/*s is divergent_to+infty by A19,LIMFUNC1:7;
end;
hence thesis by A2;
end;
theorem
f1 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2
st r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2)) & (
ex r,r1 st 0<r & 0<r1 & for g st g in dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)
holds r1<=f2.g) implies f1(#)f2 is_divergent_to+infty_in x0
proof
assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1
(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2);
given r,t such that
A3: 0<r and
A4: 0<t and
A5: for g st g in dom f2/\(].x0-r,x0.[\/ ].x0,x0+r.[) holds t<=f2.g;
now
let s be Real_Sequence;
assume that
A6: s is convergent and
A7: lim s=x0 and
A8: rng s c=dom(f1(#)f2)\{x0};
consider k such that
A9: for n st k<=n holds x0-r<s.n & s.n<x0+r by A3,A6,A7,Th7;
A10: rng s c=dom(f1(#)f2) by A8,Lm2;
A11: dom(f1(#)f2)=dom f1/\dom f2 by A8,Lm2;
rng(s^\k)c=rng s by VALUED_0:21;
then
A12: rng(s^\k)c=dom(f1(#)f2)\{x0} by A8;
then
A13: rng(s^\k)c=dom f1\{x0} by Lm2;
A14: rng(s^\k)c=dom f2 by A12,Lm2;
A15: now
thus 0<t by A4;
let n be Nat;
A16: n in NAT by ORDINAL1:def 12;
A17: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A9;
then
A18: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A9,A17;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: x0-r<g2 & g2<x0+r} by A18;
then
A19: (s^\k).n in ].x0-r,x0+r.[ by RCOMP_1:def 2;
A20: (s^\k).n in rng(s ^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A12,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A19,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by A3,Th4;
then (s^\k).n in dom f2/\(].x0-r,x0.[\/].x0,x0+r.[) by A14,A20,
XBOOLE_0:def 4;
then t<=f2.((s^\k).n) by A5;
hence t<=(f2/*(s^\k)).n by A14,FUNCT_2:108,A16;
end;
lim(s^\k)=x0 by A6,A7,SEQ_4:20;
then f1/*(s^\k) is divergent_to+infty by A1,A6,A13;
then
A21: (f1/*(s^\k))(#)(f2/*(s^\k)) is divergent_to+infty by A15,LIMFUNC1:22;
rng(s^\k)c=dom(f1(#)f2) by A12,Lm2;
then (f1/*(s^\k))(#)(f2/*(s^\k))=(f1(#)f2)/*(s^\k) by A11,RFUNCT_2:8
.=((f1(#)f2)/*s)^\k by A10,VALUED_0:27;
hence (f1(#)f2)/*s is divergent_to+infty by A21,LIMFUNC1:7;
end;
hence thesis by A2;
end;
theorem
(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)& (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 r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(r(#)
f) & g2<r2 & x0<g2 & g2 in dom(r (#)f)
proof
let r1,r2;
assume that
A3: r1<x0 and
A4: x0<r2;
consider g1,g2 such that
A5: r1<g1 and
A6: g1<x0 and
A7: g1 in dom f and
A8: g2<r2 and
A9: x0<g2 and
A10: g2 in dom f by A1,A3,A4;
take g1;
take g2;
thus thesis by A5,A6,A7,A8,A9,A10,VALUED_1:def 5;
end;
let seq;
assume that
A11: seq is convergent and
A12: lim seq=x0 and
A13: rng seq c=dom(r(#)f)\{x0};
A14: rng seq c=dom f\{x0} by A13,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A1,A11,A12;
then r(#)(f/*seq) is divergent_to+infty by A2,LIMFUNC1:13;
hence thesis by A14,RFUNCT_2:9,XBOOLE_1:1;
end;
thus f is_divergent_to+infty_in x0 & r<0 implies r(#)f
is_divergent_to-infty_in x0
proof
assume that
A15: f is_divergent_to+infty_in x0 and
A16: r<0;
thus for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(r(#)
f) & g2<r2 & x0<g2 & g2 in dom(r (#)f)
proof
let r1,r2;
assume that
A17: r1<x0 and
A18: x0<r2;
consider g1,g2 such that
A19: r1<g1 and
A20: g1<x0 and
A21: g1 in dom f and
A22: g2<r2 and
A23: x0<g2 and
A24: g2 in dom f by A15,A17,A18;
take g1;
take g2;
thus thesis by A19,A20,A21,A22,A23,A24,VALUED_1:def 5;
end;
let seq;
assume that
A25: seq is convergent and
A26: lim seq=x0 and
A27: rng seq c=dom(r(#)f)\{x0};
A28: rng seq c=dom f\{x0} by A27,VALUED_1:def 5;
then f/*seq is divergent_to+infty by A15,A25,A26;
then r(#)(f/*seq) is divergent_to-infty by A16,LIMFUNC1:13;
hence thesis by A28,RFUNCT_2:9,XBOOLE_1:1;
end;
thus f is_divergent_to-infty_in x0 & r>0 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<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(r(#)
f) & g2<r2 & x0<g2 & g2 in dom(r (#)f)
proof
let r1,r2;
assume that
A31: r1<x0 and
A32: x0<r2;
consider g1,g2 such that
A33: r1<g1 and
A34: g1<x0 and
A35: g1 in dom f and
A36: g2<r2 and
A37: x0<g2 and
A38: g2 in dom f by A29,A31,A32;
take g1;
take g2;
thus thesis by A33,A34,A35,A36,A37,A38,VALUED_1:def 5;
end;
let seq;
assume that
A39: seq is convergent and
A40: lim seq=x0 and
A41: rng seq c=dom(r(#)f)\{x0};
A42: rng seq c=dom f\{x0} by A41,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A29,A39,A40;
then r(#)(f/*seq) is divergent_to-infty by A30,LIMFUNC1:14;
hence thesis by A42,RFUNCT_2:9,XBOOLE_1:1;
end;
assume that
A43: f is_divergent_to-infty_in x0 and
A44: r<0;
thus for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(r(#)f)
& g2<r2 & x0<g2 & g2 in dom(r (#)f)
proof
let r1,r2;
assume that
A45: r1<x0 and
A46: x0<r2;
consider g1,g2 such that
A47: r1<g1 and
A48: g1<x0 and
A49: g1 in dom f and
A50: g2<r2 and
A51: x0<g2 and
A52: g2 in dom f by A43,A45,A46;
take g1;
take g2;
thus thesis by A47,A48,A49,A50,A51,A52,VALUED_1:def 5;
end;
let seq;
assume that
A53: seq is convergent and
A54: lim seq=x0 and
A55: rng seq c=dom(r(#)f)\{x0};
A56: rng seq c=dom f\{x0} by A55,VALUED_1:def 5;
then f/*seq is divergent_to-infty by A43,A53,A54;
then r(#)(f/*seq) is divergent_to+infty by A44,LIMFUNC1:14;
hence thesis by A56,RFUNCT_2:9,XBOOLE_1:1;
end;
theorem
(f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0)
implies abs(f) is_divergent_to+infty_in x0
proof
assume
A1: f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0;
now
per cases by A1;
suppose
A2: 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 abs(f)\{x0};
A7: rng seq c=dom f\{x0} by A6,VALUED_1:def 11;
then f/*seq is divergent_to+infty by A2,A4,A5;
then
A8: abs(f/*seq) is divergent_to+infty by LIMFUNC1:25;
rng seq c=dom f by A7,XBOOLE_1:1;
hence (abs f)/*seq is divergent_to+infty by A8,RFUNCT_2:10;
end;
now
let r1,r2;
assume that
A9: r1<x0 and
A10: x0<r2;
consider g1,g2 such that
A11: r1<g1 and
A12: g1<x0 and
A13: g1 in dom f and
A14: g2<r2 and
A15: x0<g2 and
A16: g2 in dom f by A2,A9,A10;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom abs(f) & g2<r2 & x0<g2 & g2 in dom abs(
f) by A11,A12,A13,A14,A15,A16,VALUED_1:def 11;
end;
hence thesis by A3;
end;
suppose
A17: f is_divergent_to-infty_in x0;
A18: now
let seq;
assume that
A19: seq is convergent and
A20: lim seq=x0 and
A21: rng seq c=dom abs(f)\{x0};
A22: rng seq c=dom f\{x0} by A21,VALUED_1:def 11;
then f/*seq is divergent_to-infty by A17,A19,A20;
then
A23: abs(f/*seq) is divergent_to+infty by LIMFUNC1:25;
rng seq c=dom f by A22,XBOOLE_1:1;
hence (abs f)/*seq is divergent_to+infty by A23,RFUNCT_2:10;
end;
now
let r1,r2;
assume that
A24: r1<x0 and
A25: x0<r2;
consider g1,g2 such that
A26: r1<g1 and
A27: g1<x0 and
A28: g1 in dom f and
A29: g2<r2 and
A30: x0<g2 and
A31: g2 in dom f by A17,A24,A25;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom abs(f) & g2<r2 & x0<g2 & g2 in dom abs(
f) by A26,A27,A28,A29,A30,A31,VALUED_1:def 11;
end;
hence thesis by A18;
end;
end;
hence thesis;
end;
theorem Th20:
(ex r st f|].x0-r,x0.[ is non-decreasing & f|].x0,x0+r.[ is
non-increasing & not f|].x0-r,x0.[ is bounded_above & not f|].x0,x0+r.[ is
bounded_above) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to+infty_in x0
proof
given r such that
A1: f|].x0-r,x0.[ is non-decreasing and
A2: f|].x0,x0+r.[ is non-increasing and
A3: not f|].x0-r,x0.[ is bounded_above and
A4: not f|].x0,x0+r.[ is bounded_above;
assume
A5: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f;
then for r st x0<r ex g st g<r & x0<g & g in dom f by Th8;
then
A6: f is_right_divergent_to+infty_in x0 by A2,A4,LIMFUNC2:29;
for r st r<x0 ex g st r<g & g<x0 & g in dom f by A5,Th8;
then f is_left_divergent_to+infty_in x0 by A1,A3,LIMFUNC2:25;
hence thesis by A6,Th12;
end;
theorem
(ex r st 0<r & f|].x0-r,x0.[ is increasing & f|].x0,x0+r.[ is
decreasing & not f|].x0-r,x0.[ is bounded_above & not f|].x0,x0+r.[ is
bounded_above) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to+infty_in x0
by Th20;
theorem Th22:
(ex r st f|].x0-r,x0.[ is non-increasing & f|].x0,x0+r.[ is
non-decreasing & not f|].x0-r,x0.[ is bounded_below & not f|].x0,x0+r.[ is
bounded_below) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to-infty_in x0
proof
given r such that
A1: f|].x0-r,x0.[ is non-increasing and
A2: f|].x0,x0+r.[ is non-decreasing and
A3: not f|].x0-r,x0.[ is bounded_below and
A4: not f|].x0,x0+r.[ is bounded_below;
assume
A5: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f;
then for r st x0<r ex g st g<r & x0<g & g in dom f by Th8;
then
A6: f is_right_divergent_to-infty_in x0 by A2,A4,LIMFUNC2:31;
for r st r<x0 ex g st r<g & g<x0 & g in dom f by A5,Th8;
then f is_left_divergent_to-infty_in x0 by A1,A3,LIMFUNC2:27;
hence thesis by A6,Th13;
end;
theorem
(ex r st 0<r & f|].x0-r,x0.[ is decreasing & f|].x0,x0+r.[ is
increasing & not f|].x0-r,x0.[ is bounded_below & not f|].x0,x0+r.[ is
bounded_below) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in
dom f & g2<r2 & x0<g2 & g2 in dom f) implies f is_divergent_to-infty_in x0
by Th22;
theorem Th24:
f1 is_divergent_to+infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex
g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & (ex r st
0<r & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,
x0+r.[) & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f.g)
implies f is_divergent_to+infty_in x0
proof
assume that
A1: f1 is_divergent_to+infty_in x0 and
A2: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f;
given r such that
A3: 0<r and
A4: dom f/\(].x0-r,x0.[\/].x0,x0+r.[)c=dom f1/\(].x0-r,x0.[\/ ].x0,x0+r .[) and
A5: for g st g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) holds f1.g<=f.g;
thus for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2
<r2 & x0<g2 & g2 in dom f by A2;
let s be Real_Sequence;
assume that
A6: s is convergent and
A7: lim s=x0 and
A8: rng s c=dom f\{x0};
consider k such that
A9: for n st k<=n holds x0-r<s.n & s.n<x0+r by A3,A6,A7,Th7;
A10: rng(s^\k)c= rng s by VALUED_0:21;
then
A11: rng(s^\k)c=dom f\{x0} by A8;
now
let x be object;
assume x in rng(s^\k);
then consider n such that
A12: (s^\k).n=x by FUNCT_2:113;
A13: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A9;
then
A14: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A9,A13;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r<g1 & g1<x0+r} by A14;
then
A15: (s^\k).n in ].x0-r,x0+r .[ by RCOMP_1:def 2;
(s^\k).n in rng(s^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A11,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A15,XBOOLE_0:def 5;
hence x in ].x0-r,x0.[\/].x0,x0+r.[ by A3,A12,Th4;
end;
then
A16: rng(s^\k)c=].x0-r,x0.[\/].x0,x0+r.[;
A17: rng s c=dom f by A8,XBOOLE_1:1;
then rng(s^\k)c=dom f by A10;
then
A18: rng(s^\k)c=dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A16,XBOOLE_1:19;
then
A19: rng(s^\k)c=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) by A4;
A20: now
let n be Nat;
A21: n in NAT by ORDINAL1:def 12;
(s^\k).n in rng(s^\k) by VALUED_0:28;
then f1.((s^\k).n)<=f.((s^\k).n) by A5,A18;
then (f1/*(s^\k)).n<=f.((s^\k).n) by A19,FUNCT_2:108,XBOOLE_1:18,A21;
hence (f1/*(s^\k)).n<=(f/*(s^\k)).n
by A17,A10,FUNCT_2:108,XBOOLE_1:1,A21;
end;
A22: rng(s^\k)c=dom f1 by A19,XBOOLE_1:18;
now
let x be object;
assume
A23: x in rng(s^\k);
then not x in {x0} by A11,XBOOLE_0:def 5;
hence x in dom f1\{x0} by A22,A23,XBOOLE_0:def 5;
end;
then
A24: rng(s^\k)c=dom f1\{x0};
lim(s^\k)=x0 by A6,A7,SEQ_4:20;
then f1/*(s^\k) is divergent_to+infty by A1,A6,A24;
then f/*(s^\k) is divergent_to+infty by A20,LIMFUNC1:42;
then (f/*s)^\k is divergent_to+infty by A8,VALUED_0:27,XBOOLE_1:1;
hence thesis by LIMFUNC1:7;
end;
theorem Th25:
f1 is_divergent_to-infty_in x0 & (for r1,r2 st r1<x0 & x0<r2 ex
g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f) & (ex r st
0<r & dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,
x0+r.[) & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<=f1.g)
implies f is_divergent_to-infty_in x0
proof
assume that
A1: f1 is_divergent_to-infty_in x0 and
A2: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f;
given r such that
A3: 0<r and
A4: dom f/\(].x0-r,x0.[\/].x0,x0+r.[)c=dom f1/\(].x0-r,x0.[\/ ].x0,x0+r .[) and
A5: for g st g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) holds f.g<=f1.g;
thus for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2
<r2 & x0<g2 & g2 in dom f by A2;
let s be Real_Sequence;
assume that
A6: s is convergent and
A7: lim s=x0 and
A8: rng s c=dom f\{x0};
consider k such that
A9: for n st k<=n holds x0-r<s.n & s.n<x0+r by A3,A6,A7,Th7;
A10: rng(s^\k)c= rng s by VALUED_0:21;
then
A11: rng(s^\k)c=dom f\{x0} by A8;
now
let x be object;
assume x in rng(s^\k);
then consider n such that
A12: (s^\k).n=x by FUNCT_2:113;
A13: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A9;
then
A14: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A9,A13;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r<g1 & g1<x0+r} by A14;
then
A15: (s^\k).n in ].x0-r,x0+r .[ by RCOMP_1:def 2;
(s^\k).n in rng(s^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A11,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A15,XBOOLE_0:def 5;
hence x in ].x0-r,x0.[\/].x0,x0+r.[ by A3,A12,Th4;
end;
then
A16: rng(s^\k)c=].x0-r,x0.[\/].x0,x0+r.[;
A17: rng s c=dom f by A8,XBOOLE_1:1;
then rng(s^\k)c=dom f by A10;
then
A18: rng(s^\k)c=dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A16,XBOOLE_1:19;
then
A19: rng(s^\k)c=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) by A4;
A20: now
let n be Nat;
A21: n in NAT by ORDINAL1:def 12;
(s^\k).n in rng(s^\k) by VALUED_0:28;
then f.((s^\k).n)<=f1.((s^\k).n) by A5,A18;
then (f/*(s^\k)).n<=f1.((s^\k).n) by A17,A10,FUNCT_2:108,XBOOLE_1:1,A21;
hence (f/*(s^\k)).n<=(f1/*(s^\k)).n by A19,FUNCT_2:108,XBOOLE_1:18,A21;
end;
A22: rng(s^\k)c=dom f1 by A19,XBOOLE_1:18;
now
let x be object;
assume
A23: x in rng(s^\k);
then not x in {x0} by A11,XBOOLE_0:def 5;
hence x in dom f1\{x0} by A22,A23,XBOOLE_0:def 5;
end;
then
A24: rng(s^\k)c=dom f1\{x0};
lim(s^\k)=x0 by A6,A7,SEQ_4:20;
then f1/*(s^\k) is divergent_to-infty by A1,A6,A24;
then f/*(s^\k) is divergent_to-infty by A20,LIMFUNC1:43;
then (f/*s)^\k is divergent_to-infty by A8,VALUED_0:27,XBOOLE_1:1;
hence thesis by LIMFUNC1:7;
end;
theorem
f1 is_divergent_to+infty_in x0 & (ex r st 0<r & ].x0-r,x0.[ \/ ].x0,x0
+r.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f1.g<=
f.g) implies f is_divergent_to+infty_in x0
proof
assume
A1: f1 is_divergent_to+infty_in x0;
given r such that
A2: 0<r and
A3: ].x0-r,x0.[\/].x0,x0+r.[c=dom f/\dom f1 and
A4: for g st g in ].x0-r,x0.[\/].x0,x0+r.[ holds f1.g<=f.g;
A5: ].x0-r,x0.[\/].x0,x0+r.[=dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A3,
XBOOLE_1:18,28;
A6: ].x0-r,x0.[\/].x0,x0+r.[=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) by A3,
XBOOLE_1:18,28;
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<
r2 & x0<g2 & g2 in dom f by A2,A3,Th5,XBOOLE_1:18;
hence thesis by A1,A2,A4,A5,A6,Th24;
end;
theorem
f1 is_divergent_to-infty_in x0 & (ex r st 0<r & ].x0-r,x0.[ \/ ].x0,x0
+r.[ c= dom f /\ dom f1 & for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f.g<=
f1.g) implies f is_divergent_to-infty_in x0
proof
assume
A1: f1 is_divergent_to-infty_in x0;
given r such that
A2: 0<r and
A3: ].x0-r,x0.[ \/ ].x0,x0+r.[c=dom f/\dom f1 and
A4: for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f.g<=f1.g;
A5: ].x0-r,x0.[\/].x0,x0+r.[=dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A3,
XBOOLE_1:18,28;
A6: ].x0-r,x0.[\/].x0,x0+r.[=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) by A3,
XBOOLE_1:18,28;
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<
r2 & x0<g2 & g2 in dom f by A2,A3,Th5,XBOOLE_1:18;
hence thesis by A1,A2,A4,A5,A6,Th25;
end;
definition
let f,x0;
assume
A1: f is_convergent_in x0;
func lim(f,x0)-> 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<x0 & $2 in
dom f;
A2: now
let n;
A3: x0+0<x0+1 by XREAL_1:8;
x0-1/(n+1)<x0 by Lm3;
then consider g1,g2 such that
A4: x0-1/(n+1)<g1 and
A5: g1<x0 and
A6: g1 in dom f and
g2<x0+1 and
x0<g2 and
g2 in dom f by A1,A3;
reconsider g1 as Element of REAL by XREAL_0:def 1;
take g1;
thus X[n,g1] by A4,A5,A6;
end;
consider s be Real_Sequence such that
A7: for n holds X[n,s.n] from FUNCT_2:sch 3(A2);
A8: rng s c=dom f\{x0} by A7,Th6;
A9: lim s=x0 by A7,Th6;
let g1,g2 be Real such that
A10: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f\{x0}
holds f/*seq is convergent & lim(f/*seq)=g1 and
A11: for seq st seq is convergent & lim seq=x0 & rng seq c=dom f\{x0}
holds f/*seq is convergent & lim(f/*seq)=g2;
A12: s is convergent by A7,Th6;
then lim(f/*s)=g1 by A9,A8,A10;
hence thesis by A12,A9,A8,A11;
end;
end;
theorem
f is_convergent_in x0 implies (lim(f,x0)=g iff for g1 st 0<g1 ex g2 st
0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds |.f.r1-g.|<
g1)
proof
assume
A1: f is_convergent_in x0;
thus lim(f,x0)=g implies for g1 st 0<g1 ex g2 st 0<g2 & for r1 st 0<|.x0-
r1.| & |.x0-r1.|<g2 & r1 in dom f holds |.f.r1-g.|<g1
proof
assume that
A2: lim(f,x0)=g and
A3: ex g1 st 0<g1 & for g2 st 0<g2 ex r1 st 0<|.x0-r1.| & |.x0-r1.|<
g2 & r1 in dom f & g1<=|.f.r1-g.|;
consider g1 such that
A4: 0<g1 and
A5: for g2 st 0<g2 ex r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f
& g1<=|.f.r1-g.| by A3;
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 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.|<g1 by A4,A12,SEQ_2:def 7;
A14: |.(f/*s).n-g.|<g1 by A13;
A15: n in NAT by ORDINAL1:def 12;
rng s c=dom f by A8,Th2;
then |.f.(s.n)-g.|<g1 by A14,FUNCT_2:108,A15;
hence contradiction by A8,A15;
end;
assume
A16: for g1 st 0<g1 ex g2 st 0<g2 & for r1 st 0<|.x0-r1.| & |.x0-r1.|<
g2 & r1 in dom f holds |.f.r1-g.|<g1;
reconsider g as Real;
now
let s be Real_Sequence;
assume that
A17: s is convergent and
A18: lim s=x0 and
A19: rng s c=dom f\{x0};
A20: now
let g1 be Real;
assume
A21: 0<g1;
consider g2 such that
A22: 0<g2 and
A23: for r1 st 0<|.x0-r1.| & |.x0-r1.|<g2 & r1 in dom f holds
|.f.r1 -g.|<g1 by A16,A21;
consider n such that
A24: for k st n<=k holds 0<|.x0-s.k.| & |.x0-s.k.|<g2 & s.k in dom
f by A17,A18,A19,A22,Th3;
reconsider n as Nat;
take n;
let k be Nat;
A25: k in NAT by ORDINAL1:def 12;
assume
A26: n<=k;
then
A27: |.x0-s.k.|<g2 by A24,A25;
A28: s.k in dom f by A24,A26,A25;
0<|.x0-s.k.| by A24,A26,A25;
then |.f.(s.k)-g.|<g1 by A23,A27,A28;
hence |.(f/*s).k-g.|<g1 by A19,FUNCT_2:108,XBOOLE_1:1,A25;
end;
hence f/*s is convergent by SEQ_2:def 6;
hence lim(f/*s)=g by A20,SEQ_2:def 7;
end;
hence thesis by A1,Def4;
end;
theorem Th29:
f is_convergent_in x0 implies f is_left_convergent_in x0 & f
is_right_convergent_in x0 & lim_left(f,x0)=lim_right(f,x0) & lim(f,x0)=lim_left
(f,x0) & lim(f,x0)=lim_right(f,x0)
proof
assume
A1: f is_convergent_in x0;
A2: now
let s be Real_Sequence;
assume that
A3: s is convergent and
A4: lim s=x0 and
A5: rng s c=dom f/\ right_open_halfline(x0);
rng s c=dom f\{x0} by A5,Th1;
hence f/*s is convergent & lim(f/*s)=lim(f,x0) by A1,A3,A4,Def4;
end;
A6: now
let s be Real_Sequence;
assume that
A7: s is convergent and
A8: lim s=x0 and
A9: rng s c=dom f/\left_open_halfline(x0);
rng s c=dom f\{x0} by A9,Th1;
hence f/*s is convergent & lim(f/*s)=lim(f,x0) by A1,A7,A8,Def4;
end;
A10: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<
r2 & x0<g2 & g2 in dom f by A1;
then for r st r<x0 ex g st r<g & g<x0 & g in dom f by Th8;
hence f is_left_convergent_in x0 by A6,LIMFUNC2:def 1;
then
A11: lim_left(f,x0)=lim(f,x0) by A6,LIMFUNC2:def 7;
for r st x0<r ex g st g<r & x0<g & g in dom f by A10,Th8;
hence f is_right_convergent_in x0 by A2,LIMFUNC2:def 4;
hence thesis by A11,A2,LIMFUNC2:def 8;
end;
theorem
f is_left_convergent_in x0 & f is_right_convergent_in x0 & lim_left(f,
x0)=lim_right(f,x0) implies f is_convergent_in x0 & lim(f,x0)=lim_left(f,x0) &
lim(f,x0)=lim_right(f,x0)
proof
assume that
A1: f is_left_convergent_in x0 and
A2: f is_right_convergent_in x0 and
A3: lim_left(f,x0)=lim_right(f,x0);
A4: now
let s be Real_Sequence such that
A5: s is convergent and
A6: lim s=x0 and
A7: rng s c=dom f\{x0};
now
per cases;
suppose
ex k st for n st k<=n holds s.n<x0;
then consider k such that
A8: for n st k<=n holds s.n<x0;
A9: rng s c=dom f by A7,XBOOLE_1:1;
A10: rng(s^\k)c=dom f/\left_open_halfline(x0)
proof
let x be object;
assume x in rng(s^\k);
then consider n such that
A11: (s^\k).n=x by FUNCT_2:113;
s.(n+k)<x0 by A8,NAT_1:12;
then s.(n+k) in {g1: g1<x0};
then s.(n+k) in left_open_halfline(x0) by XXREAL_1:229;
then
A12: x in left_open_halfline(x0) by A11,NAT_1:def 3;
s.(n+k) in rng s by VALUED_0:28;
then x in rng s by A11,NAT_1:def 3;
hence thesis by A9,A12,XBOOLE_0:def 4;
end;
A13: f/*(s^\k) =(f/*s)^\k by A7,VALUED_0:27,XBOOLE_1:1;
A14: lim(s^\k)=x0 by A5,A6,SEQ_4:20;
then
A15: f/*(s^\k) is convergent by A1,A3,A5,A10,LIMFUNC2:def 7;
hence f/*s is convergent by A13,SEQ_4:21;
lim(f/*(s^\k))=lim_left(f,x0) by A1,A5,A14,A10,LIMFUNC2:def 7;
hence lim(f/*s)=lim_left(f,x0) by A15,A13,SEQ_4:22;
end;
suppose
A16: for k ex n st k<=n & s.n>=x0;
now
per cases;
suppose
ex k st for n st k<=n holds x0<s.n;
then consider k such that
A17: for n st k<=n holds s.n>x0;
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+k) by A17,NAT_1:12;
then s.(n+k) in {g1: x0<g1};
then s.(n+k) in right_open_halfline(x0) by XXREAL_1:230;
then
A21: x in right_open_halfline(x0) by A20,NAT_1:def 3;
s.(n+k) in rng s by VALUED_0:28;
then x in rng s by A20,NAT_1:def 3;
hence thesis by A18,A21,XBOOLE_0:def 4;
end;
A22: f/*(s^\k) =(f/*s)^\k by A7,VALUED_0:27,XBOOLE_1:1;
A23: lim(s^\k)=x0 by A5,A6,SEQ_4:20;
then
A24: f/*(s^\k) is convergent by A2,A3,A5,A19,LIMFUNC2:def 8;
hence f/*s is convergent by A22,SEQ_4:21;
lim(f/*(s^\k))=lim_left(f,x0) by A2,A3,A5,A23,A19,LIMFUNC2:def 8;
hence lim(f/*s)=lim_left(f,x0) by A24,A22,SEQ_4:22;
end;
suppose
A25: for k ex n st k<=n & x0>=s.n;
set GR=lim_left(f,x0);
defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s.m<x0
& for k st n<k & s.k<x0 holds m<=k;
defpred X[Nat,set,set] means P[$2,$3];
defpred X[Nat] means s.$1<x0;
A26: now
let k;
consider n such that
A27: k<=n and
A28: s.n<=x0 by A25;
take n;
thus k<=n by A27;
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 A28,XXREAL_0:1;
end;
then ex m1 be Element of NAT st 0<=m1 & s.m1<x0;
then
A29: ex m be Nat st X[m];
consider M be Nat such that
A30: X[M] & for n be Nat st X[n] holds M<=n from NAT_1:sch 5(
A29);
reconsider M9=M as Element of NAT by ORDINAL1:def 12;
A31: now
let n;
consider m such that
A32: n+1<=m and
A33: s.m<x0 by A26;
take m;
thus n<m & s.m<x0 by A32,A33,NAT_1:13;
end;
A34: 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 A31;
then
A35: ex m be Nat st X[m];
consider l be Nat such that
A36: X[l] & for k be Nat st X[k] holds l<=k from NAT_1:sch 5
(A35 );
take l;
l in NAT by ORDINAL1:def 12;
hence thesis by A36;
end;
consider F be sequence of NAT such that
A37: F.0=M9 & for n being Nat holds X[n,F.n,F.(n+1)] from RECDEF_1:sch 2
(A34);
A38: rng F c=NAT by RELAT_1:def 19;
then
A39: rng F c=REAL by NUMBERS:19;
A40: dom F=NAT by FUNCT_2:def 1;
then reconsider F as Real_Sequence by A39,RELSET_1:4;
A41: now
let n;
F.n in rng F by A40,FUNCT_1:def 3;
hence F.n is Element of NAT by A38;
end;
now
let n be Nat;
A42: n in NAT by ORDINAL1:def 12;
A43: F.(n+1) is Element of NAT by A41;
F.n is Element of NAT by A41,A42;
hence F.n<F.(n+1) by A37,A43;
end;
then reconsider F as increasing sequence of NAT by SEQM_3:def 6;
A44: s*F is subsequence of s by VALUED_0:def 17;
then rng(s*F)c=rng s by VALUED_0:21;
then
A45: rng(s*F)c=dom f\{x0} by A7;
defpred X[Nat] means s.$1<x0 & for m holds F.m<>$1;
A46: for n st s.n<x0 ex m st F.m=n
proof
assume ex n st X[n];
then
A47: ex n be Nat st X[n];
consider M1 be Nat such that
A48: X[M1] & for n be Nat st X[n] holds M1<=n from NAT_1:sch
5(A47 );
defpred X[Nat] means $1<M1 & s.$1<x0 & ex m st F.m=$1;
A49: ex n be Nat st X[n]
proof
take M;
A50: M <> M1 by A37,A48;
M<=M1 by A30,A48;
hence M<M1 by A50,XXREAL_0:1;
thus s.M<x0 by A30;
take 0;
thus thesis by A37;
end;
A51: for n be Nat st X[n] holds n<=M1;
consider MX be Nat such that
A52: X[MX] & for n be Nat st X[n] holds n<=MX from NAT_1:sch
6(A51,A49);
A53: for k st MX<k & k<M1 holds s.k>=x0
proof
given k such that
A54: MX<k and
A55: k<M1 and
A56: s.k<x0;
now
per cases;
suppose
ex m st F.m=k;
hence contradiction by A52,A54,A55,A56;
end;
suppose
for m holds F.m<>k;
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))<x0 by A37,A57;
A60: MX<F.(m+1) by A37,A57;
now
assume F.(m+1)<>M1;
then F.(m+1)<M1 by A58,XXREAL_0:1;
hence contradiction by A53,A60,A59;
end;
hence contradiction by A48;
end;
defpred X[Nat] means s.$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).$1<x0;
A66: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat such that
(s*F).k<x0;
P[F.k,F.(k+1)] by A37;
then s.(F.(k+1))<x0;
hence thesis by FUNCT_2:15;
end;
A67: X[0] by A30,A37,FUNCT_2:15;
A68: for k being Nat holds X[k] from NAT_1:sch 2(A67,A66);
A69: rng(s*F)c=dom f/\left_open_halfline(x0)
proof
let x be object;
assume
A70: x in rng(s*F);
then consider n such that
A71: (s*F).n=x by FUNCT_2:113;
(s*F).n<x0 by A68;
then x in {g1: g1<x0} by A71;
then
A72: x in left_open_halfline(x0) by XXREAL_1:229;
x in dom f by A45,A70,XBOOLE_0:def 5;
hence thesis by A72,XBOOLE_0:def 4;
end;
defpred P[set,set] means for n,m st $1=n & $2=m holds n<m & s.m>x0
& for k st n<k & s.k>x0 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 n<m & s.m>x0 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.n<G.(n+1) by A80,A86;
end;
then reconsider G as increasing sequence of NAT by SEQM_3:def 6;
A87: s*G is subsequence of s by VALUED_0:def 17;
then rng(s*G)c=rng s by VALUED_0:21;
then
A88: rng(s*G)c=dom f\{x0} by A7;
A89: lim(s*F)=x0 by A5,A6,A44,SEQ_4:17;
then
A90: lim(f/*(s*F))=lim_left(f,x0 ) by A1,A73,A69,LIMFUNC2:def 7;
A91: f/*(s*F) is convergent by A1,A3,A73,A89,A69,LIMFUNC2:def 7;
A92: s*G is convergent by A5,A87,SEQ_4:16;
defpred X[Nat] means s.$1>x0 & 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 $1<N1 & s.$1>x0 & 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 N<N1 by A97,XXREAL_0:1;
thus s.N>x0 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 NX<k & k<N1 holds s.k<=x0
proof
given k such that
A101: NX<k and
A102: k<N1 and
A103: s.k>x0;
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: NX<G.(m+1) by A80,A104;
now
assume G.(m+1)<>N1;
then G.(m+1)<N1 by A105,XXREAL_0:1;
hence contradiction by A100,A107,A106;
end;
hence contradiction by A95;
end;
defpred X[Nat] means (s*G).$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: x0<g1} by A113;
then
A114: x in right_open_halfline(x0) by XXREAL_1:230;
x in dom f by A88,A112,XBOOLE_0:def 5;
hence thesis by A114,XBOOLE_0:def 4;
end;
A115: lim(s*G)=x0 by A5,A6,A87,SEQ_4:17;
then
A116: lim(f/*(s*G))=lim_left(f,x0 ) by A2,A3,A92,A111,LIMFUNC2:def 8;
A117: f/*(s*G) is convergent by A2,A3,A92,A115,A111,LIMFUNC2:def 8;
A118: now
let r be Real;
assume
A119: 0<r;
then consider n1 be Nat such that
A120: for k being Nat st n1<=k holds |.(f/*(s*F)).k-GR.|<r
by A91,A90,
SEQ_2:def 7;
consider n2 be Nat such that
A121: for k being Nat st n2<=k holds |.(f/*(s*G)).k-GR.|<r
by A117,A116,A119,
SEQ_2:def 7;
reconsider n=max(F.n1,G.n2) as Nat;
take n;
let k be Nat;
A122: k in NAT by ORDINAL1:def 12;
assume
A123: n<=k;
s.k in rng s by VALUED_0:28;
then not s.k in {x0} by A7,XBOOLE_0:def 5;
then
A124: s.k<>x0 by TARSKI:def 1;
now
per cases by A124,XXREAL_0:1;
suppose
s.k<x0;
then consider l be Element of NAT such that
A125: k=F.l by A46,A122;
F.n1<=n by XXREAL_0:25;
then F.n1<=k by A123,XXREAL_0:2;
then l >= n1 by A125,SEQM_3:1;
then |.(f/*(s*F)).l-GR.|<r by A120;
then |.f.((s*F).l)-GR.|<r by A45,FUNCT_2:108,XBOOLE_1:1;
then |.f.(s.k)-GR.|<r by A125,FUNCT_2:15;
hence |.(f/*s).k-GR.|<r by A7,FUNCT_2:108,XBOOLE_1:1,A122;
end;
suppose
s.k>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.|<r by A121;
then |.f.((s*G).l)-GR.|<r by A88,FUNCT_2:108,XBOOLE_1:1;
then |.f.(s.k)-GR.|<r by A126,FUNCT_2:15;
hence |.(f/*s).k-GR.|<r by A7,FUNCT_2:108,XBOOLE_1:1,A122;
end;
end;
hence |.(f/*s).k-GR.|<r;
end;
hence f/*s is convergent by SEQ_2:def 6;
hence lim(f/*s)=lim_left(f,x0) by A118,SEQ_2:def 7;
end;
end;
hence f/*s is convergent & lim(f/*s)=lim_left(f,x0);
end;
end;
hence f/*s is convergent & lim(f/*s)=lim_left(f,x0);
end;
now
let r1,r2;
assume that
A127: r1<x0 and
A128: x0<r2;
consider g1 such that
A129: r1<g1 and
A130: g1<x0 and
A131: g1 in dom f by A1,A127,LIMFUNC2:def 1;
consider g2 such that
A132: g2<r2 and
A133: x0<g2 and
A134: g2 in dom f by A2,A128,LIMFUNC2:def 4;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f by A129,A130
,A131,A132,A133,A134;
end;
hence f is_convergent_in x0 by A4;
hence thesis by A3,A4,Def4;
end;
theorem Th31:
f is_convergent_in x0 implies r(#)f is_convergent_in x0 & lim(r
(#)f,x0)=r*(lim(f,x0))
proof
assume
A1: f is_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)\{x0};
A6: rng seq c=dom f\{x0} by A5,VALUED_1:def 5;
then
A7: r(#)(f/*seq)=(r(#)f)/*seq by RFUNCT_2:9,XBOOLE_1:1;
A8: f/*seq is convergent by A1,A3,A4,A6;
then r(#) (f/*seq) is convergent by SEQ_2:7;
hence (r(#) f)/*seq is convergent by A6,RFUNCT_2:9,XBOOLE_1:1;
lim(f/*seq)=lim(f,x0) by A1,A3,A4,A6,Def4;
hence lim((r(#)f)/*seq)=r*(lim(f,x0)) by A8,A7,SEQ_2:8;
end;
now
let r1,r2;
assume that
A9: r1<x0 and
A10: x0<r2;
consider g1,g2 such that
A11: r1<g1 and
A12: g1<x0 and
A13: g1 in dom f and
A14: g2<r2 and
A15: x0<g2 and
A16: g2 in dom f by A1,A9,A10;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom(r(#)f) & g2<r2 & x0<g2 & g2 in dom(r(#)f)
by A11,A12,A13,A14,A15,A16,VALUED_1:def 5;
end;
hence r(#)f is_convergent_in x0 by A2;
hence thesis by A2,Def4;
end;
theorem Th32:
f is_convergent_in x0 implies -f is_convergent_in x0 & lim(-f,x0
)=-(lim(f,x0))
proof
assume
A1: f is_convergent_in x0;
thus -f is_convergent_in x0 by A1,Th31;
thus lim(-f,x0)=(-1)*(lim(f,x0)) by A1,Th31
.=-(lim(f,x0));
end;
theorem Th33:
f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st
r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1+f2) & g2<r2 & x0<g2 & g2
in dom(f1+f2)) implies f1+f2 is_convergent_in x0 & lim(f1+f2,x0)=lim(f1,x0)+lim
(f2,x0)
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1+
f2) & g2<r2 & x0<g2 & g2 in dom(f1+f2);
A4: now
let seq;
assume that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1+f2)\{x0};
A8: dom(f1+f2)=dom f1/\dom f2 by A7,Lm4;
A9: rng seq c=dom f1\ {x0} by A7,Lm4;
A10: rng seq c=dom f2\{x0} by A7,Lm4;
then
A11: lim(f2/*seq)=lim(f2,x0) by A2,A5,A6,Def4;
A12: f2/*seq is convergent by A2,A5,A6,A10;
rng seq c=dom(f1+f2) by A7,Lm4;
then
A13: f1/*seq+f2/*seq=(f1+f2)/*seq by A8,RFUNCT_2:8;
A14: f1/*seq is convergent by A1,A5,A6,A9;
hence (f1+f2)/*seq is convergent by A12,A13,SEQ_2:5;
lim(f1/*seq)=lim(f1,x0) by A1,A5,A6,A9,Def4;
hence lim((f1+f2)/*seq)=lim(f1,x0)+lim(f2,x0) by A14,A12,A11,A13,SEQ_2:6;
end;
hence f1+f2 is_convergent_in x0 by A3;
hence thesis by A4,Def4;
end;
theorem
f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st r1<x0
& x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1-f2) & g2<r2 & x0<g2 & g2 in
dom(f1-f2)) implies f1-f2 is_convergent_in x0 & lim(f1-f2,x0)=(lim(f1,x0))-(lim
(f2,x0))
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1-
f2) & g2<r2 & x0<g2 & g2 in dom(f1-f2);
A4: -f2 is_convergent_in x0 by A2,Th32;
hence f1-f2 is_convergent_in x0 by A1,A3,Th33;
thus lim(f1-f2,x0)=lim(f1,x0)+lim(-f2,x0) by A1,A3,A4,Th33
.=(lim(f1,x0))+-lim(f2,x0) by A2,Th32
.=(lim(f1,x0))-lim(f2,x0);
end;
theorem
f is_convergent_in x0 & f"{0}={} & lim(f,x0)<>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 r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f^) &
g2<r2 & x0<g2 & g2 in dom(f^) by A1,A4;
hence f^ is_convergent_in x0 by A5;
hence thesis by A5,Def4;
end;
theorem
f is_convergent_in x0 implies abs(f) is_convergent_in x0 & lim(abs(f),
x0)=|.lim(f,x0).|
proof
assume
A1: f is_convergent_in x0;
A2: now
let seq;
assume that
A3: seq is convergent and
A4: lim seq=x0 and
A5: rng seq c=dom abs(f)\{x0};
A6: rng seq c=dom f\{x0} by A5,VALUED_1:def 11;
then rng seq c=dom f by XBOOLE_1:1;
then
A7: abs(f/*seq)=(abs f)/*seq by RFUNCT_2:10;
A8: f/*seq is convergent by A1,A3,A4,A6;
hence (abs f)/*seq is convergent by A7;
lim(f/*seq)=lim(f,x0) by A1,A3,A4,A6,Def4;
hence lim((abs f)/*seq)=|.lim(f,x0).| by A8,A7,SEQ_4:14;
end;
now
let r1,r2;
assume that
A9: r1<x0 and
A10: x0<r2;
consider g1,g2 such that
A11: r1<g1 and
A12: g1<x0 and
A13: g1 in dom f and
A14: g2<r2 and
A15: x0<g2 and
A16: g2 in dom f by A1,A9,A10;
take g1;
take g2;
thus r1<g1 & g1<x0 & g1 in dom abs(f) & g2<r2 & x0<g2 & g2 in dom abs(f)
by A11,A12,A13,A14,A15,A16,VALUED_1:def 11;
end;
hence abs(f) is_convergent_in x0 by A2;
hence thesis by A2,Def4;
end;
theorem Th37:
f is_convergent_in x0 & lim(f,x0)<>0 & (for r1,r2 st r1<x0 & x0<
r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1
<>0 & 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 r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & 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: r1<x0 and
A17: x0<r2;
consider g1,g2 such that
A18: r1<g1 and
A19: g1<x0 and
A20: g1 in dom f and
A21: g2<r2 and
A22: x0<g2 and
A23: g2 in dom f and
A24: f.g1<>0 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 r1<g1 & g1<x0 & g1 in dom(f^) & g2<r2 & x0<g2 & g2 in dom(f^) by A4
,A18,A19,A20,A21,A22,A23,A26,XBOOLE_0:def 5;
end;
hence f^ is_convergent_in x0 by A5;
hence thesis by A5,Def4;
end;
theorem Th38:
f1 is_convergent_in x0 & f2 is_convergent_in x0 & (for r1,r2 st
r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 &
g2 in dom(f1(#) f2)) implies f1(#)f2 is_convergent_in x0 & lim(f1(#)f2,x0)=(lim
(f1,x0))*(lim(f2,x0))
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1
(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2);
A4: now
let seq;
assume that
A5: seq is convergent and
A6: lim seq=x0 and
A7: rng seq c=dom(f1(#)f2)\{x0};
A8: dom(f1(#) f2)=dom f1/\dom f2 by A7,Lm2;
A9: rng seq c=dom f1\{x0} by A7,Lm2;
A10: rng seq c=dom f2\{x0} by A7,Lm2;
then
A11: lim(f2/*seq)=lim(f2,x0) by A2,A5,A6,Def4;
A12: f2/*seq is convergent by A2,A5,A6,A10;
rng seq c=dom(f1(#)f2) by A7,Lm2;
then
A13: (f1/*seq)(#)(f2/*seq)=(f1(#)f2)/*seq by A8,RFUNCT_2:8;
A14: f1/*seq is convergent by A1,A5,A6,A9;
hence (f1(#)f2)/*seq is convergent by A12,A13,SEQ_2:14;
lim(f1/*seq)=lim(f1,x0) by A1,A5,A6,A9,Def4;
hence lim((f1(#)f2)/*seq)=lim(f1,x0)*lim(f2,x0) by A14,A12,A11,A13,SEQ_2:15
;
end;
hence f1(#)f2 is_convergent_in x0 by A3;
hence thesis by A4,Def4;
end;
theorem
f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f2,x0)<>0 & (for
r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1/f2) & g2<r2 &
x0<g2 & g2 in dom(f1/f2)) implies f1/f2 is_convergent_in x0 & lim(f1/f2,x0)=(
lim(f1,x0))/(lim(f2,x0))
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: lim(f2,x0)<>0 and
A4: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1/
f2) & g2<r2 & x0<g2 & g2 in dom(f1/f2);
A5: now
let r1,r2;
assume that
A6: r1<x0 and
A7: x0<r2;
consider g1,g2 such that
A8: r1<g1 and
A9: g1<x0 and
A10: g1 in dom(f1/f2) and
A11: g2<r2 and
A12: x0<g2 and
A13: g2 in dom(f1/f2) by A4,A6,A7;
take g1;
take g2;
thus r1<g1 & g1<x0 by A8,A9;
A14: dom(f1/f2)=dom f1/\(dom f2\f2"{0}) by RFUNCT_1:def 1;
then g2 in dom f2\f2"{0} by A13,XBOOLE_0:def 4;
then not g2 in f2"{0} by XBOOLE_0:def 5;
then
A15: not f2.g2 in {0} by A13,A14,FUNCT_1:def 7;
g1 in dom f2\f2"{0} by A10,A14,XBOOLE_0:def 4;
then not g1 in f2"{0} by XBOOLE_0:def 5;
then not f2.g1 in {0} by A10,A14,FUNCT_1:def 7;
hence g1 in dom f2 & g2<r2 & x0<g2 & g2 in dom f2 & f2.g1<>0 & 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 r1<x0 & x0<r2 ex
g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2
)) & (ex r st 0<r & f2|(].x0-r,x0.[ \/ ].x0,x0+r.[) is bounded ) implies f1(#)
f2 is_convergent_in x0 & lim(f1(#)f2,x0)=0
proof
assume that
A1: f1 is_convergent_in x0 and
A2: lim(f1,x0)=0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f1
(#)f2) & g2<r2 & x0<g2 & g2 in dom(f1(#)f2);
given r such that
A4: 0<r and
A5: f2|(].x0-r,x0.[ \/ ].x0,x0+r.[) is bounded;
consider g be Real such that
A6: for r1 being object st r1 in (].x0-r,x0.[\/].x0,x0+r.[)/\dom f2 holds
|.f2.r1.|<=g by A5,RFUNCT_1:73;
A7: now
let s be Real_Sequence;
assume that
A8: s is convergent and
A9: lim s=x0 and
A10: rng s c=dom(f1(#)f2)\{x0};
consider k such that
A11: for n st k<= n holds x0-r<s.n & s.n<x0+r by A4,A8,A9,Th7;
A12: rng(s^\k)c=rng s by VALUED_0:21;
rng s c=dom f1\{x0} by A10,Lm2;
then
A13: rng(s^\k)c=dom f1\{x0} by A12;
A14: lim(s^\k)=x0 by A8,A9,SEQ_4:20;
then
A15: f1/*(s^\k) is convergent by A1,A8,A13;
A16: rng s c=dom f2 by A10,Lm2;
then
A17: rng(s^\k)c=dom f2 by A12;
now
set t=|.g.|+1;
0<=|.g.| by COMPLEX1:46;
hence 0<t;
let n be Nat;
A18: n in NAT by ORDINAL1:def 12;
A19: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A11;
then
A20: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A11,A19;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r<g1 & g1<x0+r} by A20;
then
A21: (s^\k).n in ].x0-r,x0+r .[ by RCOMP_1:def 2;
A22: (s^\k).n in rng(s^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A13,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A21,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by A4,Th4;
then (s^\k).n in (].x0-r,x0.[\/].x0,x0+r.[)/\dom f2 by A17,A22,
XBOOLE_0:def 4;
then |.f2.((s^\k).n).|<=g by A6;
then
A23: |.(f2/*(s^\k)).n.|<= g by A16,A12,FUNCT_2:108,XBOOLE_1:1,A18;
g<=|.g.| by ABSVALUE:4;
then g<t by Lm1;
hence |.(f2/*(s^\k)).n.|<t by A23,XXREAL_0:2;
end;
then
A24: f2/*(s^\k) is bounded by SEQ_2:3;
A25: rng s c=dom(f1(#)f2) by A10,Lm2;
dom(f1(#)f2)=dom f1/\dom f2 by A10,Lm2;
then rng(s^\k)c=dom f1/\dom f2 by A25,A12;
then
A26: (f1/*(s^\k))(#)(f2/*(s^\k))=(f1(#)f2)/*(s^\k) by RFUNCT_2:8
.=((f1(#)f2)/*s)^\k by A25,VALUED_0:27;
A27: lim(f1/*(s^\k))=0 by A1,A2,A8,A14,A13,Def4;
then
A28: (f1/*(s^\k))(#)(f2/*(s^\k)) is convergent by A15,A24,SEQ_2:25;
hence (f1(#)f2)/*s is convergent by A26,SEQ_4:21;
lim((f1/*(s^\k))(#)(f2/*(s^\k)))=0 by A15,A27,A24,SEQ_2:26;
hence lim((f1(#)f2)/*s)=0 by A28,A26,SEQ_4:22;
end;
hence f1(#)f2 is_convergent_in x0 by A3;
hence thesis by A7,Def4;
end;
theorem Th41:
f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f1,x0)=lim
(f2,x0) & (for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f) & (ex r st 0<r & (for g st g in dom f /\ (].x0-r,
x0.[ \/ ].x0,x0+r.[) holds f1.g<=f.g & f.g<=f2.g) & ((dom f1 /\ (].x0-r,x0.[ \/
].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & dom f /\ (].x0-r,x0.[
\/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)) or (dom f2 /\ (].x0-
r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) & dom f /\ (].
x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)))) implies
f is_convergent_in x0 & lim(f,x0)=lim(f1,x0)
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: lim(f1,x0)=lim(f2,x0) and
A4: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f;
given r1 such that
A5: 0<r1 and
A6: for g st g in dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[) holds f1.g<=f.g &
f.g<=f2.g and
A7: dom f1/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f2/\(].x0-r1,x0.[\/ ].x0,
x0+r1.[) & dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f1/\(].x0-r1,x0.[\/].x0,x0+
r1.[) or dom f2/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f1/\(].x0-r1,x0.[\/].x0,x0+
r1.[) & dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f2/\(].x0-r1,x0.[\/].x0,x0+r1
.[);
now
per cases by A7;
suppose
A8: dom f1/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f2/\(].x0-r1,x0.[\/].
x0,x0+r1.[) & dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f1/\(].x0-r1,x0.[\/].x0,
x0+r1.[);
A9: now
let s be Real_Sequence;
assume that
A10: s is convergent and
A11: lim s=x0 and
A12: rng s c=dom f\{x0};
consider k such that
A13: for n st k<=n holds x0-r1<s.n & s.n<x0+r1 by A5,A10,A11,Th7;
A14: rng(s^\k)c=rng s by VALUED_0:21;
then
A15: rng(s^\k)c=dom f\{x0} by A12;
now
let x be object;
assume
A16: x in rng(s^\k);
then consider n such that
A17: x=(s^\k).n by FUNCT_2:113;
A18: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r1 by A13;
then
A19: (s^\k).n<x0+r1 by NAT_1:def 3;
x0-r1<s.(n+k) by A13,A18;
then x0-r1<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r1<g1 & g1<x0+r1} by A19;
then
A20: (s^\k).n in ].x0-r1,x0+r1.[ by RCOMP_1:def 2;
not (s^\k).n in {x0} by A15,A16,A17,XBOOLE_0:def 5;
then x in ].x0-r1,x0+r1.[\{x0} by A17,A20,XBOOLE_0:def 5;
hence x in ].x0-r1,x0.[\/].x0,x0+r1.[ by A5,Th4;
end;
then
A21: rng(s^\k)c=].x0-r1,x0.[\/].x0,x0+r1.[;
A22: rng s c=dom f by A12,XBOOLE_1:1;
then rng(s^\k)c=dom f by A14;
then
A23: rng(s^\k)c=dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[) by A21,XBOOLE_1:19;
then
A24: rng(s^\k)c=dom f1/\(].x0-r1,x0.[\/].x0,x0+r1.[) by A8;
then
A25: rng(s^\k)c=dom f2/\(].x0-r1,x0.[\/].x0,x0+r1.[) by A8;
A26: lim(s^\k)= x0 by A10,A11,SEQ_4:20;
A27: dom f2/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f2 by XBOOLE_1:17;
then
A28: rng(s^\k)c=dom f2 by A25;
A29: rng(s^\k) c=dom f2\{x0}
proof
let x be object;
assume
A30: x in rng(s^\k);
then not x in {x0} by A15,XBOOLE_0:def 5;
hence thesis by A28,A30,XBOOLE_0:def 5;
end;
then
A31: lim(f2/*(s^\k))=lim(f2,x0) by A2,A10,A26,Def4;
A32: dom f1/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f1 by XBOOLE_1:17;
then
A33: rng(s^\k)c=dom f1 by A24;
A34: rng(s^\k)c=dom f1\{x0}
proof
let x be object;
assume
A35: x in rng(s^\k);
then not x in {x0} by A15,XBOOLE_0:def 5;
hence thesis by A33,A35,XBOOLE_0:def 5;
end;
then
A36: lim(f1/*(s^\k))=lim(f1,x0) by A1,A10,A26,Def4;
A37: now
let n be Nat;
A38: n in NAT by ORDINAL1:def 12;
A39: (s^\k).n in rng(s^\k) by VALUED_0:28;
then f.((s^\k).n)<=f2.((s^\k).n) by A6,A23;
then
A40: (f/*(s^\k)).n<= f2.((s^\k).n)
by A14,A22,FUNCT_2:108,XBOOLE_1:1,A38;
f1.((s^\k).n)<=f.((s^\k).n) by A6,A23,A39;
then f1.((s^\k).n)<=(f/*(s^\k)).n
by A14,A22,FUNCT_2:108,XBOOLE_1:1,A38;
hence (f1/*(s^\k)).n<=(f/*(s^\k)).n & (f/*(s^\k)).n<=(f2/*(s^\k)).n
by A32,A27,A24,A25,A40,FUNCT_2:108,XBOOLE_1:1,A38;
end;
A41: f2/*(s^\k) is convergent by A2,A10,A26,A29;
A42: f1/*(s^\k) is convergent by A1,A10,A26,A34;
then f/*(s^\k) is convergent by A3,A36,A41,A31,A37,SEQ_2:19;
then
A43: (f/*s)^\k is convergent by A12,VALUED_0:27,XBOOLE_1:1;
hence f/*s is convergent by SEQ_4:21;
lim(f/*(s^\k))=lim(f1,x0) by A3,A42,A36,A41,A31,A37,SEQ_2:20;
then lim((f/*s)^\k)=lim(f1,x0) by A12,VALUED_0:27,XBOOLE_1:1;
hence lim(f/*s)=lim(f1,x0) by A43,SEQ_4:22;
end;
hence f is_convergent_in x0 by A4;
hence thesis by A9,Def4;
end;
suppose
A44: dom f2/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f1/\(].x0-r1,x0.[\/].
x0,x0+r1.[) & dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f2/\(].x0-r1,x0.[\/].x0,
x0+r1.[);
A45: now
let s be Real_Sequence;
assume that
A46: s is convergent and
A47: lim s=x0 and
A48: rng s c=dom f\{x0};
consider k such that
A49: for n st k<=n holds x0-r1<s.n & s.n<x0+r1 by A5,A46,A47,Th7;
A50: rng(s^\k)c=rng s by VALUED_0:21;
then
A51: rng(s^\k)c=dom f\{x0} by A48;
now
let x be object;
assume
A52: x in rng(s^\k);
then consider n such that
A53: x=(s^\k).n by FUNCT_2:113;
A54: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r1 by A49;
then
A55: (s^\k).n<x0+r1 by NAT_1:def 3;
x0-r1<s.(n+k) by A49,A54;
then x0-r1<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r1<g1 & g1<x0+r1} by A55;
then
A56: (s^\k).n in ].x0-r1,x0+r1.[ by RCOMP_1:def 2;
not (s^\k).n in {x0} by A51,A52,A53,XBOOLE_0:def 5;
then x in ].x0-r1,x0+r1.[\{x0} by A53,A56,XBOOLE_0:def 5;
hence x in ].x0-r1,x0.[\/].x0,x0+r1.[ by A5,Th4;
end;
then
A57: rng(s^\k)c=].x0-r1,x0.[\/].x0,x0+r1.[;
A58: rng s c=dom f by A48,XBOOLE_1:1;
then rng(s^\k)c=dom f by A50;
then
A59: rng(s^\k)c=dom f/\(].x0-r1,x0.[\/].x0,x0+r1.[) by A57,XBOOLE_1:19;
then
A60: rng(s^\k)c=dom f2/\(].x0-r1,x0.[\/].x0,x0+r1.[) by A44;
then
A61: rng(s^\k)c=dom f1/\(].x0-r1,x0.[\/].x0,x0+r1.[) by A44;
A62: lim(s^\k)= x0 by A46,A47,SEQ_4:20;
A63: dom f2/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f2 by XBOOLE_1:17;
then
A64: rng(s^\k)c=dom f2 by A60;
A65: rng(s^\k) c=dom f2\{x0}
proof
let x be object;
assume
A66: x in rng(s^\k);
then not x in {x0} by A51,XBOOLE_0:def 5;
hence thesis by A64,A66,XBOOLE_0:def 5;
end;
then
A67: lim(f2/*(s^\k))=lim(f2,x0) by A2,A46,A62,Def4;
A68: dom f1/\(].x0-r1,x0.[\/].x0,x0+r1.[)c=dom f1 by XBOOLE_1:17;
then
A69: rng(s^\k)c=dom f1 by A61;
A70: rng(s^\k)c=dom f1\{x0}
proof
let x be object;
assume
A71: x in rng(s^\k);
then not x in {x0} by A51,XBOOLE_0:def 5;
hence thesis by A69,A71,XBOOLE_0:def 5;
end;
then
A72: lim(f1/*(s^\k))=lim(f1,x0) by A1,A46,A62,Def4;
A73: now
let n be Nat;
A74: n in NAT by ORDINAL1:def 12;
A75: (s^\k).n in rng(s^\k) by VALUED_0:28;
then f.((s^\k).n)<=f2.((s^\k).n) by A6,A59;
then
A76: (f/*(s^\k)).n<= f2.((s^\k).n)
by A50,A58,FUNCT_2:108,XBOOLE_1:1,A74;
f1.((s^\k).n)<=f.((s^\k).n) by A6,A59,A75;
then f1.((s^\k).n)<=(f/*(s^\k)).n
by A50,A58,FUNCT_2:108,XBOOLE_1:1,A74;
hence (f1/*(s^\k)).n<=(f/*(s^\k)).n & (f/*(s^\k)).n<=(f2/*(s^\k)).n
by A68,A63,A60,A61,A76,FUNCT_2:108,XBOOLE_1:1,A74;
end;
A77: f2/*(s^\k) is convergent by A2,A46,A62,A65;
A78: f1/*(s^\k) is convergent by A1,A46,A62,A70;
then f/*(s^\k) is convergent by A3,A72,A77,A67,A73,SEQ_2:19;
then
A79: (f/*s)^\k is convergent by A48,VALUED_0:27,XBOOLE_1:1;
hence f/*s is convergent by SEQ_4:21;
lim(f/*(s^\k))=lim(f1,x0) by A3,A78,A72,A77,A67,A73,SEQ_2:20;
then lim((f/*s)^\k)=lim(f1,x0) by A48,VALUED_0:27,XBOOLE_1:1;
hence lim(f/*s)=lim(f1,x0) by A79,SEQ_4:22;
end;
hence f is_convergent_in x0 by A4;
hence thesis by A45,Def4;
end;
end;
hence thesis;
end;
theorem
f1 is_convergent_in x0 & f2 is_convergent_in x0 & lim(f1,x0)=lim(f2,x0
) & (ex r st 0<r & ].x0-r,x0.[ \/ ].x0,x0+r.[ c= dom f1 /\ dom f2 /\ dom f &
for g st g in ].x0-r,x0.[ \/ ].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g) implies f
is_convergent_in x0 & lim(f,x0)=lim(f1,x0)
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0 and
A3: lim(f1,x0)=lim(f2,x0);
given r such that
A4: 0<r and
A5: ].x0-r,x0.[\/].x0,x0+r.[c=dom f1/\dom f2/\dom f and
A6: for g st g in ].x0-r,x0.[\/].x0,x0+r.[ holds f1.g<=f.g & f.g<=f2.g;
A7: dom f/\(].x0-r,x0.[\/].x0,x0+r.[)=].x0-r,x0.[\/].x0,x0+r.[ by A5,
XBOOLE_1:18,28;
A8: ].x0-r,x0.[\/].x0,x0+r.[c=dom f1/\dom f2 by A5,XBOOLE_1:18;
then
A9: dom f1/\(].x0-r,x0.[\/].x0,x0+r.[)=].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_1:18
,28;
A10: dom f2/\(].x0-r,x0.[\/].x0,x0+r.[)=].x0-r,x0.[\/].x0,x0+r.[ by A8,
XBOOLE_1:18,28;
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2
<r2 & x0<g2 & g2 in dom f by A4,A5,Th5,XBOOLE_1:18;
hence thesis by A1,A2,A3,A4,A6,A7,A9,A10,Th41;
end;
theorem
f1 is_convergent_in x0 & f2 is_convergent_in x0 & (ex r st 0<r & ((dom
f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) &
for g st g in dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<=f2.g) or (dom
f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) c= dom f1 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) &
for g st g in dom f2 /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f1.g<= f2.g)))
implies lim(f1,x0)<=lim(f2,x0)
proof
assume that
A1: f1 is_convergent_in x0 and
A2: f2 is_convergent_in x0;
given r such that
A3: 0<r and
A4: (dom f1/\(].x0-r,x0.[\/].x0,x0+r.[)c=dom f2/\(].x0-r,x0.[\/].x0,x0+r
.[) & for g st g in dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) holds f1.g<=f2.g) or (
dom f2/\(].x0-r,x0.[\/].x0,x0+r.[)c=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) & for g
st g in dom f2/\(].x0-r,x0.[\/].x0,x0+r.[) holds f1.g<=f2.g);
now
per cases by A4;
suppose
A5: dom f1/\(].x0-r,x0.[\/].x0,x0+r.[)c=dom f2/\(].x0-r,x0.[\/].x0,
x0+r.[) & for g st g in dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) holds f1.g<=f2.g;
defpred X[Nat,Real] means x0-1/($1+1)<$2 & $2<x0 & $2
in dom f1;
A6: now
let n be Element of NAT;
A7: x0<x0+1 by Lm1;
x0-1/(n+1)<x0 by Lm3;
then consider g1,g2 such that
A8: x0-1/(n+1)<g1 and
A9: g1<x0 and
A10: g1 in dom f1 and
g2<x0+1 and
x0<g2 and
g2 in dom f1 by A1,A7;
reconsider g1 as Element of REAL by XREAL_0:def 1;
take g1;
thus X[n,g1] by A8,A9,A10;
end;
consider s be Real_Sequence such that
A11: for n holds X[n,s.n] from FUNCT_2:sch 3(A6);
A12: lim s=x0 by A11,Th6;
A13: rng s c=dom f1\{x0} by A11,Th6;
A14: s is convergent by A11,Th6;
x0-r<x0 by A3,Lm1;
then consider k being Nat such that
A15: for n being Nat st k<=n holds x0-r<s.n by A14,A12,LIMFUNC2:1;
A16: lim(s^\k)=x0 by A14,A12,SEQ_4:20;
rng(s^\k)c=rng s by VALUED_0:21;
then
A17: rng(s^\k)c=dom f1\{x0} by A13;
then
A18: lim(f1/*(s^\k))=lim(f1,x0) by A1,A14,A16,Def4;
now
let x be object;
assume x in rng(s^\k);
then consider n such that
A19: (s^\k).n=x by FUNCT_2:113;
A20: n+k in NAT by ORDINAL1:def 12;
s.(n+k)<x0 by A11,A20;
then
A21: (s^\k).n<x0 by NAT_1:def 3;
x0-r<s.(n+k) by A15,NAT_1:12;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A21;
then (s^\k).n in ].x0-r,x0 .[ by RCOMP_1:def 2;
then
A22: (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_0:def 3;
s.(n+k) in dom f1 by A11,A20;
then (s^\k).n in dom f1 by NAT_1:def 3;
hence x in dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) by A19,A22,XBOOLE_0:def 4
;
end;
then
A23: rng(s^\k)c=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[);
then
A24: rng(s^\k)c=dom f2/\(].x0-r,x0.[\/].x0,x0+r.[) by A5;
A25: now
let n be Nat;
A26: n in NAT by ORDINAL1:def 12;
(s^\k).n in rng(s^\k) by VALUED_0:28;
then f1.((s^\k).n)<=f2.((s^\k).n) by A5,A23;
then f1.((s^\k).n)<=(f2/*(s^\k)).n
by A24,FUNCT_2:108,XBOOLE_1:18,A26;
hence (f1/*(s^\k)).n<=(f2/*(s^\k)).n
by A23,FUNCT_2:108,XBOOLE_1:18,A26;
end;
A27: rng(s^\k)c=dom f2 by A24,XBOOLE_1:18;
A28: rng(s^\k)c=dom f2\{x0}
proof
let x be object;
assume
A29: x in rng(s^\k);
then not x in {x0} by A17,XBOOLE_0:def 5;
hence thesis by A27,A29,XBOOLE_0:def 5;
end;
then
A30: lim(f2/*(s^\k))=lim(f2,x0) by A2,A14,A16,Def4;
A31: f2/*(s^\k) is convergent by A2,A14,A16,A28;
f1/*(s^\k) is convergent by A1,A14,A16,A17;
hence thesis by A18,A31,A30,A25,SEQ_2:18;
end;
suppose
A32: dom f2/\(].x0-r,x0.[\/].x0,x0+r.[)c=dom f1/\(].x0-r,x0.[\/].x0,
x0+r.[) & for g st g in dom f2/\(].x0-r,x0.[\/].x0,x0+r.[) holds f1.g<=f2.g;
defpred X[Element of NAT,Real] means x0-1/($1+1)<$2 & $2<x0 & $2
in dom f2;
A33: now
let n;
A34: x0<x0+1 by Lm1;
x0-1/(n+1)<x0 by Lm3;
then consider g1,g2 such that
A35: x0-1/(n+1)<g1 and
A36: g1<x0 and
A37: g1 in dom f2 and
g2<x0+1 and
x0<g2 and
g2 in dom f2 by A2,A34;
reconsider g1 as Element of REAL by XREAL_0:def 1;
take g1;
thus X[n,g1] by A35,A36,A37;
end;
consider s be Real_Sequence such that
A38: for n holds X[n,s.n] from FUNCT_2:sch 3(A33 );
A39: lim s=x0 by A38,Th6;
A40: rng s c=dom f2\{x0} by A38,Th6;
A41: s is convergent by A38,Th6;
x0-r<x0 by A3,Lm1;
then consider k being Nat such that
A42: for n being Nat st k<=n holds x0-r<s.n by A41,A39,LIMFUNC2:1;
A43: lim(s^\k)=x0 by A41,A39,SEQ_4:20;
rng(s^\k)c=rng s by VALUED_0:21;
then
A44: rng(s^\k)c=dom f2\{x0} by A40;
then
A45: lim(f2/*(s^\k))=lim(f2,x0) by A2,A41,A43,Def4;
A46: now
let x be object;
assume x in rng(s^\k);
then consider n such that
A47: (s^\k).n=x by FUNCT_2:113;
A48: n+k in NAT by ORDINAL1:def 12;
s.(n+k)<x0 by A38,A48;
then
A49: (s^\k).n<x0 by NAT_1:def 3;
x0-r<s.(n+k) by A42,NAT_1:12;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g2: x0-r<g2 & g2<x0} by A49;
then (s^\k).n in ].x0-r,x0 .[ by RCOMP_1:def 2;
then
A50: (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_0:def 3;
s.(n+k) in dom f2 by A38,A48;
then (s^\k).n in dom f2 by NAT_1:def 3;
hence x in dom f2/\(].x0-r,x0.[\/].x0,x0+r.[) by A47,A50,XBOOLE_0:def 4
;
end;
then
A51: rng(s^\k)c=dom f2/\(].x0-r,x0.[\/].x0,x0+r.[);
then
A52: rng(s^\k)c=dom f1/\(].x0-r,x0.[\/].x0,x0+r.[) by A32;
A53: now
let n be Nat;
A54: n in NAT by ORDINAL1:def 12;
(s^\k).n in rng(s^\k) by VALUED_0:28;
then f1.((s^\k).n)<=f2.((s^\k).n) by A32,A46;
then f1.((s^\k).n)<=(f2/*(s^\k)).n
by A51,FUNCT_2:108,XBOOLE_1:18,A54;
hence (f1/*(s^\k)).n<=(f2/*(s^\k)).n
by A52,FUNCT_2:108,XBOOLE_1:18,A54;
end;
A55: rng(s^\k)c=dom f1 by A52,XBOOLE_1:18;
A56: rng(s^\k)c=dom f1\{x0}
proof
let x be object;
assume
A57: x in rng(s^\k);
then not x in {x0} by A44,XBOOLE_0:def 5;
hence thesis by A55,A57,XBOOLE_0:def 5;
end;
then
A58: lim(f1/*(s^\k))=lim(f1,x0) by A1,A41,A43,Def4;
A59: f1/*(s^\k) is convergent by A1,A41,A43,A56;
f2/*(s^\k) is convergent by A2,A41,A43,A44;
hence thesis by A45,A59,A58,A53,SEQ_2:18;
end;
end;
hence thesis;
end;
theorem
(f is_divergent_to+infty_in x0 or f is_divergent_to-infty_in x0) & (
for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0
<g2 & g2 in dom f & f.g1<>0 & 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 r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0;
now
let r1,r2;
assume that
A15: r1<x0 and
A16: x0<r2;
consider g1,g2 such that
A17: r1<g1 and
A18: g1<x0 and
A19: g1 in dom f and
A20: g2<r2 and
A21: x0<g2 and
A22: g2 in dom f and
A23: f.g1<>0 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 r1<g1 & g1<x0 & g1 in dom(f^) & g2<r2 & x0<g2 & g2 in dom(f^) by A1
,A17,A18,A19,A20,A21,A22,A25,XBOOLE_0:def 5;
end;
hence f^ is_convergent_in x0 by A3;
hence thesis by A3,Def4;
end;
theorem
f is_convergent_in x0 & lim(f,x0)=0 & (for r1,r2 st r1<x0 & x0<r2 ex
g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 &
f.g2<>0) & (ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)
holds 0<=f.g) implies f^ is_divergent_to+infty_in x0
proof
assume that
A1: f is_convergent_in x0 and
A2: lim(f,x0)=0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0;
given r such that
A4: 0<r and
A5: for g st g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) holds 0<=f.g;
thus for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f^) &
g2<r2 & x0<g2 & g2 in dom(f^)
proof
let r1,r2;
assume that
A6: r1<x0 and
A7: x0<r2;
consider g1,g2 such that
A8: r1<g1 and
A9: g1<x0 and
A10: g1 in dom f and
A11: g2<r2 and
A12: x0<g2 and
A13: g2 in dom f and
A14: f.g1<>0 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-r<s.n & s.n<x0+r by A4,A17,A18,Th7;
A21: rng s c=dom(f^) by A19,XBOOLE_1:1;
A22: dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A23: (f/*(s^\k))"=((f/*s)^\k)" by A21,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A19,RFUNCT_2:12,XBOOLE_1:1;
A24: rng(s^\k)c=rng s by VALUED_0:21;
A25: rng s c=dom f by A21,A22,XBOOLE_1:1;
then
A26: rng(s^\k)c=dom f by A24;
A27: rng(s^\k)c=dom (f^)\{x0} by A19,A24;
A28: rng(s^\k)c=dom f\{x0}
proof
let x be object;
assume
A29: x in rng(s^\k);
then not x in {x0} by A27,XBOOLE_0:def 5;
hence thesis by A26,A29,XBOOLE_0:def 5;
end;
A30: lim(s^\k)=x0 by A17,A18,SEQ_4:20;
then
A31: lim(f/*(s^\k))=0 by A1,A2,A17,A28,Def4;
A32: f/*(s^\k) is non-zero by A21,A24,RFUNCT_2:11,XBOOLE_1:1;
now
let n be Nat;
A33: n in NAT by ORDINAL1:def 12;
A34: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A20;
then
A35: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A20,A34;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r<g1 & g1<x0+r} by A35;
then
A36: (s^\k).n in ].x0-r,x0+r .[ by RCOMP_1:def 2;
A37: (s^\k).n in rng(s^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A27,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A36,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by A4,Th4;
then (s^\k).n in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A26,A37,
XBOOLE_0:def 4;
then
A38: 0<=f.((s^\k).n) by A5;
(f/*(s^\k)).n<>0 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 r1<x0 & x0<r2 ex
g1,g2 st r1<g1 & g1<x0 & g1 in dom f & g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 &
f.g2<>0) & (ex r st 0<r & for g st g in dom f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[)
holds f.g<=0) implies f^ is_divergent_to-infty_in x0
proof
assume that
A1: f is_convergent_in x0 and
A2: lim(f,x0)=0 and
A3: for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom f &
g2<r2 & x0<g2 & g2 in dom f & f.g1<>0 & f.g2<>0;
given r such that
A4: 0<r and
A5: for g st g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) holds f.g<=0;
thus for r1,r2 st r1<x0 & x0<r2 ex g1,g2 st r1<g1 & g1<x0 & g1 in dom(f^) &
g2<r2 & x0<g2 & g2 in dom(f^)
proof
let r1,r2;
assume that
A6: r1<x0 and
A7: x0<r2;
consider g1,g2 such that
A8: r1<g1 and
A9: g1<x0 and
A10: g1 in dom f and
A11: g2<r2 and
A12: x0<g2 and
A13: g2 in dom f and
A14: f.g1<>0 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-r<s.n & s.n<x0+r by A4,A17,A18,Th7;
A21: rng s c=dom(f^) by A19,XBOOLE_1:1;
A22: dom(f^)=dom f\f"{0} by RFUNCT_1:def 2;
then
A23: (f/*(s^\k))"=((f/*s)^\k)" by A21,VALUED_0:27,XBOOLE_1:1
.=((f/*s)")^\k by SEQM_3:18
.=((f^)/*s)^\k by A19,RFUNCT_2:12,XBOOLE_1:1;
A24: rng(s^\k)c=rng s by VALUED_0:21;
A25: rng s c=dom f by A21,A22,XBOOLE_1:1;
then
A26: rng(s^\k)c=dom f by A24;
A27: rng(s^\k)c=dom (f^)\{x0} by A19,A24;
A28: rng(s^\k)c=dom f\{x0}
proof
let x be object;
assume
A29: x in rng(s^\k);
then not x in {x0} by A27,XBOOLE_0:def 5;
hence thesis by A26,A29,XBOOLE_0:def 5;
end;
A30: lim(s^\k)=x0 by A17,A18,SEQ_4:20;
then
A31: lim(f/*(s^\k))=0 by A1,A2,A17,A28,Def4;
A32: f/*(s^\k) is non-zero by A21,A24,RFUNCT_2:11,XBOOLE_1:1;
A33:
now
let n;
A34: k<=n+k by NAT_1:12;
then s.(n+k)<x0+r by A20;
then
A35: (s^\k).n<x0+r by NAT_1:def 3;
x0-r<s.(n+k) by A20,A34;
then x0-r<(s^\k).n by NAT_1:def 3;
then (s^\k).n in {g1: x0-r<g1 & g1<x0+r} by A35;
then
A36: (s^\k).n in ].x0-r,x0+r .[ by RCOMP_1:def 2;
A37: (s^\k).n in rng(s^\k) by VALUED_0:28;
then not (s^\k).n in {x0} by A27,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0+r.[\{x0} by A36,XBOOLE_0:def 5;
then (s^\k).n in ].x0-r,x0.[\/].x0,x0+r.[ by A4,Th4;
then (s^\k).n in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A26,A37,
XBOOLE_0:def 4;
then
A38: f.((s^\k).n)<=0 by A5;
(f/*(s^\k)).n<>0 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<r & for g st g in dom
f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds 0<f.g) implies f^
is_divergent_to+infty_in x0
proof
assume that
A1: f is_convergent_in x0 and
A2: lim(f,x0)=0;
A3: f is_right_convergent_in x0 by A1,Th29;
given r such that
A4: 0<r and
A5: for g st g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) holds 0<f.g;
A6: now
let g;
assume
A7: g in dom f/\].x0,x0+r.[;
then g in ].x0,x0+r.[ by XBOOLE_0:def 4;
then
A8: g in ].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_0:def 3;
g in dom f by A7,XBOOLE_0:def 4;
then g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A8,XBOOLE_0:def 4;
hence 0<f.g by A5;
end;
A9: now
let g;
assume
A10: g in dom f/\].x0-r,x0.[;
then g in ].x0-r,x0.[ by XBOOLE_0:def 4;
then
A11: g in ].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_0:def 3;
g in dom f by A10,XBOOLE_0:def 4;
then g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A11,XBOOLE_0:def 4;
hence 0<f.g by A5;
end;
lim_right(f,x0)=0 by A1,A2,Th29;
then
A12: f^ is_right_divergent_to+infty_in x0 by A3,A4,A6,LIMFUNC2:73;
A13: f is_left_convergent_in x0 by A1,Th29;
lim_left(f,x0)=0 by A1,A2,Th29;
then f^ is_left_divergent_to+infty_in x0 by A13,A4,A9,LIMFUNC2:71;
hence thesis by A12,Th12;
end;
theorem
f is_convergent_in x0 & lim(f,x0)=0 & (ex r st 0<r & for g st g in dom
f /\ (].x0-r,x0.[ \/ ].x0,x0+r.[) holds f.g<0) implies f^
is_divergent_to-infty_in x0
proof
assume that
A1: f is_convergent_in x0 and
A2: lim(f,x0)=0;
A3: f is_right_convergent_in x0 by A1,Th29;
given r such that
A4: 0<r and
A5: for g st g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) holds f.g<0;
A6: now
let g;
assume
A7: g in dom f/\].x0,x0+r.[;
then g in ].x0,x0+r.[ by XBOOLE_0:def 4;
then
A8: g in ].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_0:def 3;
g in dom f by A7,XBOOLE_0:def 4;
then g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A8,XBOOLE_0:def 4;
hence f.g<0 by A5;
end;
A9: now
let g;
assume
A10: g in dom f/\].x0-r,x0.[;
then g in ].x0-r,x0.[ by XBOOLE_0:def 4;
then
A11: g in ].x0-r,x0.[\/].x0,x0+r.[ by XBOOLE_0:def 3;
g in dom f by A10,XBOOLE_0:def 4;
then g in dom f/\(].x0-r,x0.[\/].x0,x0+r.[) by A11,XBOOLE_0:def 4;
hence f.g<0 by A5;
end;
lim_right(f,x0)=0 by A1,A2,Th29;
then
A12: f^ is_right_divergent_to-infty_in x0 by A3,A4,A6,LIMFUNC2:74;
A13: f is_left_convergent_in x0 by A1,Th29;
lim_left(f,x0)=0 by A1,A2,Th29;
then f^ is_left_divergent_to-infty_in x0 by A13,A4,A9,LIMFUNC2:72;
hence thesis by A12,Th13;
end;