let x0 be Real; for f1, f2 being PartFunc of REAL,REAL st f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 | ].(x0 - r),x0.[ is bounded_below ) holds
f1 + f2 is_left_divergent_to+infty_in x0
let f1, f2 be PartFunc of REAL,REAL; ( f1 is_left_divergent_to+infty_in x0 & ( for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) ) ) & ex r being Real st
( 0 < r & f2 | ].(x0 - r),x0.[ is bounded_below ) implies f1 + f2 is_left_divergent_to+infty_in x0 )
assume that
A1:
f1 is_left_divergent_to+infty_in x0
and
A2:
for r being Real st r < x0 holds
ex g being Real st
( r < g & g < x0 & g in dom (f1 + f2) )
; ( for r being Real holds
( not 0 < r or not f2 | ].(x0 - r),x0.[ is bounded_below ) or f1 + f2 is_left_divergent_to+infty_in x0 )
given r being Real such that A3:
0 < r
and
A4:
f2 | ].(x0 - r),x0.[ is bounded_below
; f1 + f2 is_left_divergent_to+infty_in x0
now for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (left_open_halfline x0) holds
(f1 + f2) /* seq is divergent_to+infty let seq be
Real_Sequence;
( seq is convergent & lim seq = x0 & rng seq c= (dom (f1 + f2)) /\ (left_open_halfline x0) implies (f1 + f2) /* seq is divergent_to+infty )assume that A5:
seq is
convergent
and A6:
lim seq = x0
and A7:
rng seq c= (dom (f1 + f2)) /\ (left_open_halfline x0)
;
(f1 + f2) /* seq is divergent_to+infty
x0 - r < x0
by A3, Lm1;
then consider k being
Nat such that A8:
for
n being
Nat st
k <= n holds
x0 - r < seq . n
by A5, A6, Th1;
A9:
(dom (f1 + f2)) /\ (left_open_halfline x0) c= dom (f1 + f2)
by XBOOLE_1:17;
rng (seq ^\ k) c= rng seq
by VALUED_0:21;
then A10:
rng (seq ^\ k) c= (dom (f1 + f2)) /\ (left_open_halfline x0)
by A7, XBOOLE_1:1;
then A11:
rng (seq ^\ k) c= dom (f1 + f2)
by A9, XBOOLE_1:1;
A12:
dom (f1 + f2) = (dom f1) /\ (dom f2)
by VALUED_1:def 1;
then A13:
dom (f1 + f2) c= dom f2
by XBOOLE_1:17;
then A14:
rng (seq ^\ k) c= dom f2
by A11, XBOOLE_1:1;
dom (f1 + f2) c= dom f1
by A12, XBOOLE_1:17;
then A15:
rng (seq ^\ k) c= dom f1
by A11, XBOOLE_1:1;
then
rng (seq ^\ k) c= (dom f1) /\ (dom f2)
by A14, XBOOLE_1:19;
then A16:
(f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) =
(f1 + f2) /* (seq ^\ k)
by RFUNCT_2:8
.=
((f1 + f2) /* seq) ^\ k
by A7, A9, VALUED_0:27, XBOOLE_1:1
;
(dom (f1 + f2)) /\ (left_open_halfline x0) c= left_open_halfline x0
by XBOOLE_1:17;
then A17:
rng (seq ^\ k) c= left_open_halfline x0
by A10, XBOOLE_1:1;
then A18:
rng (seq ^\ k) c= (dom f1) /\ (left_open_halfline x0)
by A15, XBOOLE_1:19;
now ex r2 being set st
for n being Nat holds r2 < (f2 /* (seq ^\ k)) . nconsider r1 being
Real such that A19:
for
g being
object st
g in ].(x0 - r),x0.[ /\ (dom f2) holds
r1 <= f2 . g
by A4, RFUNCT_1:71;
take r2 =
r1 - 1;
for n being Nat holds r2 < (f2 /* (seq ^\ k)) . nlet n be
Nat;
r2 < (f2 /* (seq ^\ k)) . nA20:
n in NAT
by ORDINAL1:def 12;
x0 - r < seq . (n + k)
by A8, NAT_1:12;
then A21:
x0 - r < (seq ^\ k) . n
by NAT_1:def 3;
A22:
(seq ^\ k) . n in rng (seq ^\ k)
by VALUED_0:28;
then
(seq ^\ k) . n in left_open_halfline x0
by A17;
then
(seq ^\ k) . n in { g1 where g1 is Real : g1 < x0 }
by XXREAL_1:229;
then
ex
g being
Real st
(
g = (seq ^\ k) . n &
g < x0 )
;
then
(seq ^\ k) . n in { g2 where g2 is Real : ( x0 - r < g2 & g2 < x0 ) }
by A21;
then
(seq ^\ k) . n in ].(x0 - r),x0.[
by RCOMP_1:def 2;
then
(seq ^\ k) . n in ].(x0 - r),x0.[ /\ (dom f2)
by A14, A22, XBOOLE_0:def 4;
then
r1 - 1
< (f2 . ((seq ^\ k) . n)) - 0
by A19, XREAL_1:15;
hence
r2 < (f2 /* (seq ^\ k)) . n
by A11, A13, FUNCT_2:108, XBOOLE_1:1, A20;
verum end; then A23:
f2 /* (seq ^\ k) is
bounded_below
by SEQ_2:def 4;
lim (seq ^\ k) = x0
by A5, A6, SEQ_4:20;
then
f1 /* (seq ^\ k) is
divergent_to+infty
by A1, A5, A18;
then
(f1 /* (seq ^\ k)) + (f2 /* (seq ^\ k)) is
divergent_to+infty
by A23, LIMFUNC1:9;
hence
(f1 + f2) /* seq is
divergent_to+infty
by A16, LIMFUNC1:7;
verum end;
hence
f1 + f2 is_left_divergent_to+infty_in x0
by A2; verum