let f be PartFunc of REAL , REAL ; :: thesis: ( ex r being Real st
( f | (right_open_halfline r) is non-decreasing & not f | (right_open_halfline r) is bounded_above ) & ( 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-decreasing & not f | (right_open_halfline r1) is bounded_above )
; :: 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
r < (f /* seq) . mconsider g1 being
set such that A4:
(
g1 in (right_open_halfline r1) /\ (dom f) &
r < f . g1 )
by A1, RFUNCT_1:87;
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
r < (f /* seq) . mlet m be
Element of
NAT ;
:: thesis: ( n <= m implies r < (f /* seq) . m )A6:
seq . m in rng seq
by VALUED_0:28;
assume
n <= m
;
:: thesis: r < (f /* seq) . mthen 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 . g1 <= f . (seq . m)
by A1, A4, A9, RFUNCT_2:45;
then
r < f . (seq . m)
by A4, XXREAL_0:2;
hence
r < (f /* seq) . m
by A3, FUNCT_2:185;
:: thesis: verum end; hence
f /* seq is
divergent_to+infty
by Def4;
:: thesis: verum end;
hence
f is divergent_in+infty_to+infty
by A2, Def7; :: thesis: verum