let x0 be Real; for f being PartFunc of REAL,REAL st f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g < 0 ) ) holds
f ^ is_left_divergent_to-infty_in x0
let f be PartFunc of REAL,REAL; ( f is_left_convergent_in x0 & lim_left (f,x0) = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g < 0 ) ) implies f ^ is_left_divergent_to-infty_in x0 )
assume that
A1:
f is_left_convergent_in x0
and
A2:
lim_left (f,x0) = 0
; ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ ].(x0 - r),x0.[ & not f . g < 0 ) ) or f ^ is_left_divergent_to-infty_in x0 )
given r being Real such that A3:
0 < r
and
A4:
for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g < 0
; f ^ is_left_divergent_to-infty_in x0
thus
for r1 being Real st r1 < x0 holds
ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) )
LIMFUNC2:def 3 for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f ^)) /\ (left_open_halfline x0) holds
(f ^) /* seq is divergent_to-infty proof
let r1 be
Real;
( r1 < x0 implies ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) ) )
assume
r1 < x0
;
ex g1 being Real st
( r1 < g1 & g1 < x0 & g1 in dom (f ^) )
then consider g1 being
Real such that A5:
r1 < g1
and A6:
g1 < x0
and
g1 in dom f
by A1;
now ex g2 being Real st
( r1 < g2 & g2 < x0 & g2 in dom (f ^) )per cases
( g1 <= x0 - r or x0 - r <= g1 )
;
suppose A7:
g1 <= x0 - r
;
ex g2 being Real st
( r1 < g2 & g2 < x0 & g2 in dom (f ^) )
x0 - r < x0
by A3, Lm1;
then consider g2 being
Real such that A8:
x0 - r < g2
and A9:
g2 < x0
and A10:
g2 in dom f
by A1;
take g2 =
g2;
( r1 < g2 & g2 < x0 & g2 in dom (f ^) )
g1 < g2
by A7, A8, XXREAL_0:2;
hence
(
r1 < g2 &
g2 < x0 )
by A5, A9, XXREAL_0:2;
g2 in dom (f ^)
g2 in { r2 where r2 is Real : ( x0 - r < r2 & r2 < x0 ) }
by A8, A9;
then
g2 in ].(x0 - r),x0.[
by RCOMP_1:def 2;
then
g2 in (dom f) /\ ].(x0 - r),x0.[
by A10, XBOOLE_0:def 4;
then
not
f . g2 in {0}
by A4;
then
not
g2 in f " {0}
by FUNCT_1:def 7;
then
g2 in (dom f) \ (f " {0})
by A10, XBOOLE_0:def 5;
hence
g2 in dom (f ^)
by RFUNCT_1:def 2;
verum end; suppose A11:
x0 - r <= g1
;
ex g2 being Real st
( r1 < g2 & g2 < x0 & g2 in dom (f ^) )consider g2 being
Real such that A12:
g1 < g2
and A13:
g2 < x0
and A14:
g2 in dom f
by A1, A6;
take g2 =
g2;
( r1 < g2 & g2 < x0 & g2 in dom (f ^) )thus
(
r1 < g2 &
g2 < x0 )
by A5, A12, A13, XXREAL_0:2;
g2 in dom (f ^)
x0 - r < g2
by A11, A12, XXREAL_0:2;
then
g2 in { r2 where r2 is Real : ( x0 - r < r2 & r2 < x0 ) }
by A13;
then
g2 in ].(x0 - r),x0.[
by RCOMP_1:def 2;
then
g2 in (dom f) /\ ].(x0 - r),x0.[
by A14, XBOOLE_0:def 4;
then
not
f . g2 in {0}
by A4;
then
not
g2 in f " {0}
by FUNCT_1:def 7;
then
g2 in (dom f) \ (f " {0})
by A14, XBOOLE_0:def 5;
hence
g2 in dom (f ^)
by RFUNCT_1:def 2;
verum end; end; end;
hence
ex
g1 being
Real st
(
r1 < g1 &
g1 < x0 &
g1 in dom (f ^) )
;
verum
end;
let s be Real_Sequence; ( s is convergent & lim s = x0 & rng s c= (dom (f ^)) /\ (left_open_halfline x0) implies (f ^) /* s is divergent_to-infty )
assume that
A15:
s is convergent
and
A16:
lim s = x0
and
A17:
rng s c= (dom (f ^)) /\ (left_open_halfline x0)
; (f ^) /* s is divergent_to-infty
x0 - r < x0
by A3, Lm1;
then consider k being Nat such that
A18:
for n being Nat st k <= n holds
x0 - r < s . n
by A15, A16, Th1;
A19:
lim (s ^\ k) = x0
by A15, A16, SEQ_4:20;
dom (f ^) = (dom f) \ (f " {0})
by RFUNCT_1:def 2;
then A20:
dom (f ^) c= dom f
by XBOOLE_1:36;
A21:
rng (s ^\ k) c= rng s
by VALUED_0:21;
(dom (f ^)) /\ (left_open_halfline x0) c= left_open_halfline x0
by XBOOLE_1:17;
then
rng s c= left_open_halfline x0
by A17, XBOOLE_1:1;
then A22:
rng (s ^\ k) c= left_open_halfline x0
by A21, XBOOLE_1:1;
A23:
(dom (f ^)) /\ (left_open_halfline x0) c= dom (f ^)
by XBOOLE_1:17;
then A24:
rng s c= dom (f ^)
by A17, XBOOLE_1:1;
then A25:
rng s c= dom f
by A20, XBOOLE_1:1;
then A26:
rng (s ^\ k) c= dom f
by A21, XBOOLE_1:1;
then A27:
rng (s ^\ k) c= (dom f) /\ (left_open_halfline x0)
by A22, XBOOLE_1:19;
then A28:
lim (f /* (s ^\ k)) = 0
by A1, A2, A15, A19, Def7;
then A32:
for n being Nat st 0 <= n holds
(f /* (s ^\ k)) . n < 0
;
f /* (s ^\ k) is convergent
by A1, A15, A19, A27;
then A33:
(f /* (s ^\ k)) " is divergent_to-infty
by A28, A32, LIMFUNC1:36;
(f /* (s ^\ k)) " =
((f /* s) ^\ k) "
by A24, A20, VALUED_0:27, XBOOLE_1:1
.=
((f /* s) ") ^\ k
by SEQM_3:18
.=
((f ^) /* s) ^\ k
by A17, A23, RFUNCT_2:12, XBOOLE_1:1
;
hence
(f ^) /* s is divergent_to-infty
by A33, LIMFUNC1:7; verum