let f, f1 be PartFunc of REAL,REAL; :: thesis: ( f1 is divergent_in+infty_to+infty & ex r being Real st
( right_open_halfline r c= (dom f) /\ (dom f1) & ( for g being Real st g in right_open_halfline r holds
f1 . g <= f . g ) ) implies f is divergent_in+infty_to+infty )
assume A1: f1 is divergent_in+infty_to+infty ; :: thesis: ( for r being Real holds
( not right_open_halfline r c= (dom f) /\ (dom f1) or ex g being Real st
( g in right_open_halfline r & not f1 . g <= f . g ) ) or f is divergent_in+infty_to+infty )
given r1 being Real such that A2: right_open_halfline r1 c= (dom f) /\ (dom f1) and
A3: for g being Real st g in right_open_halfline r1 holds
f1 . g <= f . g ; :: thesis: f is divergent_in+infty_to+infty
A4: now :: thesis: for r being Real ex g being Real st
( r < g & g in dom f )
let r be Real; :: thesis: ex g being Real st
( r < g & g in dom f )
consider g being Real such that
A5: |.r.| + |.r1.| < g by XREAL_1:1;
take g = g; :: thesis: ( r < g & g in dom f )
( 0 <= |.r1.| & r <= |.r.| ) by ABSVALUE:4, COMPLEX1:46;
then 0 + r <= |.r.| + |.r1.| by XREAL_1:7;
hence r < g by A5, XXREAL_0:2; :: thesis: g in dom f
( 0 <= |.r.| & r1 <= |.r1.| ) by ABSVALUE:4, COMPLEX1:46;
then 0 + r1 <= |.r.| + |.r1.| by XREAL_1:7;
then r1 < g by A5, XXREAL_0:2;
then g in { g2 where g2 is Real : r1 < g2 } ;
then g in right_open_halfline r1 by XXREAL_1:230;
hence g in dom f by A2, XBOOLE_0:def 4; :: thesis: verum
end;
now :: thesis: ( (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) & ( for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
f1 . g <= f . g ) )
(dom f) /\ (dom f1) c= dom f by XBOOLE_1:17;
then A6: (dom f) /\ (right_open_halfline r1) = right_open_halfline r1 by A2, XBOOLE_1:1, XBOOLE_1:28;
(dom f) /\ (dom f1) c= dom f1 by XBOOLE_1:17;
hence (dom f) /\ (right_open_halfline r1) c= (dom f1) /\ (right_open_halfline r1) by A2, A6, XBOOLE_1:1, XBOOLE_1:28; :: thesis: for g being Real st g in (dom f) /\ (right_open_halfline r1) holds
f1 . g <= f . g
let g be Real; :: thesis: ( g in (dom f) /\ (right_open_halfline r1) implies f1 . g <= f . g )
assume g in (dom f) /\ (right_open_halfline r1) ; :: thesis: f1 . g <= f . g
hence f1 . g <= f . g by A3, A6; :: thesis: verum
end;
hence f is divergent_in+infty_to+infty by A1, A4, Th70; :: thesis: verum