let f be PartFunc of REAL,REAL; ( ex r being Real st
( f | (left_open_halfline r) is non-increasing & not f | (left_open_halfline r) is bounded_above ) & ( for r being Real ex g being Real st
( g < r & g in dom f ) ) implies f is divergent_in-infty_to+infty )
given r1 being Real such that A1:
f | (left_open_halfline r1) is non-increasing
and
A2:
not f | (left_open_halfline r1) is bounded_above
; ( ex r being Real st
for g being Real holds
( not g < r 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
r < (f /* seq) . mlet r be
Real;
ex n being Nat st
for m being Nat st n <= m holds
r < (f /* seq) . mconsider g1 being
object such that A6:
g1 in (left_open_halfline r1) /\ (dom f)
and A7:
r < f . g1
by A2, RFUNCT_1:70;
reconsider g1 =
g1 as
Real by A6;
consider n being
Nat such that A8:
for
m being
Nat st
n <= m holds
seq . m < (- |.r1.|) - |.g1.|
by A4;
take n =
n;
for m being Nat st n <= m holds
r < (f /* seq) . mlet m be
Nat;
( n <= m implies r < (f /* seq) . m )A9:
m in NAT
by ORDINAL1:def 12;
assume
n <= m
;
r < (f /* seq) . mthen A10:
seq . m < (- |.r1.|) - |.g1.|
by A8;
(
- |.r1.| <= r1 &
0 <= |.g1.| )
by ABSVALUE:4, COMPLEX1:46;
then
(- |.r1.|) - |.g1.| <= r1 - 0
by XREAL_1:13;
then
seq . m < r1
by A10, XXREAL_0:2;
then
seq . m in { g2 where g2 is Real : g2 < r1 }
;
then
(
seq . m in rng seq &
seq . m in left_open_halfline r1 )
by VALUED_0:28, XXREAL_1:229;
then A11:
seq . m in (left_open_halfline r1) /\ (dom f)
by A5, XBOOLE_0:def 4;
(
- |.g1.| <= g1 &
0 <= |.r1.| )
by ABSVALUE:4, COMPLEX1:46;
then
(- |.g1.|) - |.r1.| <= g1 - 0
by XREAL_1:13;
then
seq . m < g1
by A10, XXREAL_0:2;
then
f . g1 <= f . (seq . m)
by A1, A6, A11, RFUNCT_2:23;
then
r < f . (seq . m)
by A7, XXREAL_0:2;
hence
r < (f /* seq) . m
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
( g < r & g in dom f )
; f is divergent_in-infty_to+infty
hence
f is divergent_in-infty_to+infty
by A3; verum