let f be PartFunc of REAL,REAL; ( ex r being Real st
( f | (right_open_halfline r) is non-increasing & not f | (right_open_halfline r) is bounded_below ) & ( for r being Real ex g being Real st
( r < g & g in dom f ) ) implies f is divergent_in+infty_to-infty )
given r1 being Real such that A1:
f | (right_open_halfline r1) is non-increasing
and
A2:
not f | (right_open_halfline r1) is bounded_below
; ( ex r being Real st
for g being Real holds
( not r < g or not g in dom f ) or f is divergent_in+infty_to-infty )
A3:
now for seq being Real_Sequence st seq is divergent_to+infty & rng seq c= dom f holds
f /* seq is divergent_to-infty let seq be
Real_Sequence;
( seq is divergent_to+infty & rng seq c= dom f implies f /* seq is divergent_to-infty )assume that A4:
seq is
divergent_to+infty
and A5:
rng seq c= dom f
;
f /* seq is divergent_to-infty now for r being Real ex n being Nat st
for m being Nat st n <= m holds
(f /* seq) . m < rlet r be
Real;
ex n being Nat st
for m being Nat st n <= m holds
(f /* seq) . m < rconsider g1 being
object such that A6:
g1 in (right_open_halfline r1) /\ (dom f)
and A7:
f . g1 < r
by A2, RFUNCT_1:71;
reconsider g1 =
g1 as
Real by A6;
consider n being
Nat such that A8:
for
m being
Nat st
n <= m holds
|.g1.| + |.r1.| < seq . m
by A4;
take n =
n;
for m being Nat st n <= m holds
(f /* seq) . m < rlet m be
Nat;
( n <= m implies (f /* seq) . m < r )A9:
m in NAT
by ORDINAL1:def 12;
assume
n <= m
;
(f /* seq) . m < rthen A10:
|.g1.| + |.r1.| < seq . m
by A8;
(
r1 <= |.r1.| &
0 <= |.g1.| )
by ABSVALUE:4, COMPLEX1:46;
then
0 + r1 <= |.g1.| + |.r1.|
by XREAL_1:7;
then
r1 < seq . m
by A10, XXREAL_0:2;
then
seq . m in { g2 where g2 is Real : r1 < g2 }
;
then
(
seq . m in rng seq &
seq . m in right_open_halfline r1 )
by VALUED_0:28, XXREAL_1:230;
then A11:
seq . m in (right_open_halfline r1) /\ (dom f)
by A5, XBOOLE_0:def 4;
(
g1 <= |.g1.| &
0 <= |.r1.| )
by ABSVALUE:4, COMPLEX1:46;
then
g1 + 0 <= |.g1.| + |.r1.|
by XREAL_1:7;
then
g1 < seq . m
by A10, XXREAL_0:2;
then
f . (seq . m) <= f . g1
by A1, A6, A11, RFUNCT_2:23;
then
f . (seq . m) < r
by A7, XXREAL_0:2;
hence
(f /* seq) . m < r
by A5, FUNCT_2:108, A9;
verum end; hence
f /* seq is
divergent_to-infty
;
verum end;
assume
for r being Real ex g being Real st
( r < g & g in dom f )
; f is divergent_in+infty_to-infty
hence
f is divergent_in+infty_to-infty
by A3; verum