let f be PartFunc of REAL , REAL ; :: thesis: ( 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 & not f | (right_open_halfline r1) is bounded_below )
; :: thesis: ( 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 )
assume A2:
for r being Real ex g being Real st
( r < g & g in dom f )
; :: thesis: f is divergent_in+infty_to-infty
now let seq be
Real_Sequence;
:: thesis: ( seq is divergent_to+infty & rng seq c= dom f implies f /* seq is divergent_to-infty )assume A3:
(
seq is
divergent_to+infty &
rng seq c= dom f )
;
:: thesis: f /* seq is divergent_to-inftynow let r be
Real;
:: thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
(f /* seq) . m < rconsider g1 being
set such that A4:
(
g1 in (right_open_halfline r1) /\ (dom f) &
f . g1 < r )
by A1, RFUNCT_1:88;
reconsider g1 =
g1 as
Real by A4;
consider n being
Element of
NAT such that A5:
for
m being
Element of
NAT st
n <= m holds
(abs g1) + (abs r1) < seq . m
by A3, Def4;
take n =
n;
:: thesis: for m being Element of NAT st n <= m holds
(f /* seq) . m < rlet m be
Element of
NAT ;
:: thesis: ( n <= m implies (f /* seq) . m < r )A6:
seq . m in rng seq
by VALUED_0:28;
assume
n <= m
;
:: thesis: (f /* seq) . m < rthen A7:
(abs g1) + (abs r1) < seq . m
by A5;
A8:
r1 <= abs r1
by ABSVALUE:11;
0 <= abs g1
by COMPLEX1:132;
then
0 + r1 <= (abs g1) + (abs r1)
by A8, XREAL_1:9;
then
r1 < seq . m
by A7, XXREAL_0:2;
then
seq . m in { g2 where g2 is Real : r1 < g2 }
;
then
seq . m in right_open_halfline r1
by XXREAL_1:230;
then A9:
seq . m in (right_open_halfline r1) /\ (dom f)
by A3, A6, XBOOLE_0:def 4;
A10:
g1 <= abs g1
by ABSVALUE:11;
0 <= abs r1
by COMPLEX1:132;
then
g1 + 0 <= (abs g1) + (abs r1)
by A10, XREAL_1:9;
then
g1 < seq . m
by A7, XXREAL_0:2;
then
f . (seq . m) <= f . g1
by A1, A4, A9, RFUNCT_2:46;
then
f . (seq . m) < r
by A4, XXREAL_0:2;
hence
(f /* seq) . m < r
by A3, FUNCT_2:185;
:: thesis: verum end; hence
f /* seq is
divergent_to-infty
by Def5;
:: thesis: verum end;
hence
f is divergent_in+infty_to-infty
by A2, Def8; :: thesis: verum