let f be PartFunc of REAL,REAL; :: thesis: ( ex r being Real st
( f | (left_open_halfline r) is non-decreasing & not f | (left_open_halfline r) is bounded_below ) & ( 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-decreasing and
A2: not f | (left_open_halfline r1) is bounded_below ; :: thesis: ( 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 :: thesis: 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; :: thesis: ( 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 ; :: thesis: f /* seq is divergent_to-infty
now :: thesis: for r being Real ex n being Nat st
for m being Nat st n <= m holds
(f /* seq) . m < r
let r be Real; :: thesis: ex n being Nat st
for m being Nat st n <= m holds
(f /* seq) . m < r
consider g1 being object such that
A6: g1 in (left_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
seq . m < (- |.r1.|) - |.g1.| by A4;
take n = n; :: thesis: for m being Nat st n <= m holds
(f /* seq) . m < r
let m be Nat; :: thesis: ( n <= m implies (f /* seq) . m < r )
A9: m in NAT by ORDINAL1:def 12;
assume n <= m ; :: thesis: (f /* seq) . m < r
then 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 . (seq . m) <= f . g1 by A1, A6, A11, RFUNCT_2:22;
then f . (seq . m) < r by A7, XXREAL_0:2;
hence (f /* seq) . m < r by A5, FUNCT_2:108, A9; :: thesis: verum
end;
hence f /* seq is divergent_to-infty ; :: thesis: verum
end;
assume for r being Real ex g being Real st
( g < r & g in dom f ) ; :: thesis: f is divergent_in-infty_to-infty
hence f is divergent_in-infty_to-infty by A3; :: thesis: verum