let x0 be Real; for f being PartFunc of REAL,REAL holds
( f is_divergent_to-infty_in x0 iff ( f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0 ) )
let f be PartFunc of REAL,REAL; ( f is_divergent_to-infty_in x0 iff ( f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0 ) )
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 ) )
( f is_left_divergent_to-infty_in x0 & f is_right_divergent_to-infty_in x0 implies f is_divergent_to-infty_in x0 )
assume that
A11:
f is_left_divergent_to-infty_in x0
and
A12:
f is_right_divergent_to-infty_in x0
; f is_divergent_to-infty_in x0
A13:
now for s being Real_Sequence st s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} holds
f /* s is divergent_to-infty let s be
Real_Sequence;
( s is convergent & lim s = x0 & rng s c= (dom f) \ {x0} implies f /* s is divergent_to-infty )assume that A14:
s is
convergent
and A15:
lim s = x0
and A16:
rng s c= (dom f) \ {x0}
;
f /* s is divergent_to-infty now f /* s is divergent_to-infty per cases
( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
s . n < x0 or for k being Element of NAT ex n being Element of NAT st
( k <= n & s . n >= x0 ) )
;
suppose A23:
for
k being
Element of
NAT ex
n being
Element of
NAT st
(
k <= n &
s . n >= x0 )
;
f /* s is divergent_to-infty now f /* s is divergent_to-infty per cases
( ex k being Element of NAT st
for n being Element of NAT st k <= n holds
x0 < s . n or for k being Element of NAT ex n being Element of NAT st
( k <= n & x0 >= s . n ) )
;
suppose A30:
for
k being
Element of
NAT ex
n being
Element of
NAT st
(
k <= n &
x0 >= s . n )
;
f /* s is divergent_to-infty defpred S1[
set ,
set ]
means for
n,
m being
Element of
NAT st $1
= n & $2
= m holds
(
n < m &
s . m < x0 & ( for
k being
Element of
NAT st
n < k &
s . k < x0 holds
m <= k ) );
defpred S2[
Nat,
set ,
set ]
means S1[$2,$3];
defpred S3[
Nat]
means s . $1
< x0;
then
ex
m1 being
Element of
NAT st
(
0 <= m1 &
s . m1 < x0 )
;
then A34:
ex
m being
Nat st
S3[
m]
;
consider M being
Nat such that A35:
(
S3[
M] & ( for
n being
Nat st
S3[
n] holds
M <= n ) )
from NAT_1:sch 5(A34);
reconsider M9 =
M as
Element of
NAT by ORDINAL1:def 12;
A39:
for
n being
Nat for
x being
Element of
NAT ex
y being
Element of
NAT st
S2[
n,
x,
y]
consider F being
sequence of
NAT such that A42:
(
F . 0 = M9 & ( for
n being
Nat holds
S2[
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 =
F as
Real_Sequence by A44, RELSET_1:4;
then reconsider F =
F as
V43()
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 S4[
Nat]
means (
s . $1
< x0 & ( for
m being
Element of
NAT holds
F . m <> $1 ) );
A51:
for
n being
Element of
NAT st
s . n < x0 holds
ex
m being
Element of
NAT st
F . m = n
defpred S5[
Nat]
means s . $1
> x0;
then
ex
mn being
Element of
NAT st
(
0 <= mn &
s . mn > x0 )
;
then A69:
ex
m being
Nat st
S5[
m]
;
consider N being
Nat such that A70:
(
S5[
N] & ( for
n being
Nat st
S5[
n] holds
N <= n ) )
from NAT_1:sch 5(A69);
defpred S6[
Nat]
means (s * F) . $1
< x0;
A71:
for
k being
Nat st
S6[
k] holds
S6[
k + 1]
proof
let k be
Nat;
( S6[k] implies S6[k + 1] )
assume
(s * F) . k < x0
;
S6[k + 1]
S1[
F . k,
F . (k + 1)]
by A42;
then
s . (F . (k + 1)) < x0
;
hence
S6[
k + 1]
by FUNCT_2:15;
verum
end; A72:
S6[
0 ]
by A35, A42, FUNCT_2:15;
A73:
for
k being
Nat holds
S6[
k]
from NAT_1:sch 2(A72, A71);
A74:
rng (s * F) c= (dom f) /\ (left_open_halfline x0)
defpred S7[
set ,
set ]
means for
n,
m being
Element of
NAT st $1
= n & $2
= m holds
(
n < m &
s . m > x0 & ( for
k being
Element of
NAT st
n < k &
s . k > x0 holds
m <= k ) );
defpred S8[
Nat,
set ,
set ]
means S7[$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;
A83:
for
n being
Nat for
x being
Element of
NAT ex
y being
Element of
NAT st
S8[
n,
x,
y]
consider G being
sequence of
NAT such that A86:
(
G . 0 = N9 & ( for
n being
Nat holds
S8[
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 =
G as
Real_Sequence by A88, RELSET_1:4;
then reconsider G =
G as
V43()
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 S9[
Nat]
means (
s . $1
> x0 & ( for
m being
Element of
NAT holds
G . m <> $1 ) );
A95:
for
n being
Element of
NAT st
s . n > x0 holds
ex
m being
Element of
NAT st
G . m = n
defpred S10[
Nat]
means (s * G) . $1
> x0;
A110:
for
k being
Nat st
S10[
k] holds
S10[
k + 1]
proof
let k be
Nat;
( S10[k] implies S10[k + 1] )
assume
(s * G) . k > x0
;
S10[k + 1]
S7[
G . k,
G . (k + 1)]
by A86;
then
s . (G . (k + 1)) > x0
;
hence
S10[
k + 1]
by FUNCT_2:15;
verum
end; A111:
S10[
0 ]
by A70, A86, FUNCT_2:15;
A112:
for
k being
Nat holds
S10[
k]
from NAT_1:sch 2(A111, A110);
A113:
rng (s * G) c= (dom f) /\ (right_open_halfline x0)
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;
hence
f /* s is
divergent_to-infty
;
verum end; end; end; hence
f /* s is
divergent_to-infty
;
verum end; end; end; hence
f /* s is
divergent_to-infty
;
verum end;
now for r1, r2 being Real st r1 < x0 & x0 < r2 holds
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )let r1,
r2 be
Real;
( r1 < x0 & x0 < r2 implies ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f ) )assume that A126:
r1 < x0
and A127:
x0 < r2
;
ex g1, g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )consider g1 being
Real such that A128:
r1 < g1
and A129:
g1 < x0
and A130:
g1 in dom f
by A11, A126, LIMFUNC2:def 3;
consider g2 being
Real such that A131:
g2 < r2
and A132:
x0 < g2
and A133:
g2 in dom f
by A12, A127, LIMFUNC2:def 6;
take g1 =
g1;
ex g2 being Real st
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )take g2 =
g2;
( r1 < g1 & g1 < x0 & g1 in dom f & g2 < r2 & x0 < g2 & g2 in dom f )thus
(
r1 < g1 &
g1 < x0 &
g1 in dom f &
g2 < r2 &
x0 < g2 &
g2 in dom f )
by A128, A129, A130, A131, A132, A133;
verum end;
hence
f is_divergent_to-infty_in x0
by A13; verum