let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) holds
abs f is_right_divergent_to+infty_in x0
let f be PartFunc of REAL,REAL; :: thesis: ( ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) implies abs f is_right_divergent_to+infty_in x0 )
assume A1: ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) ; :: thesis: abs f is_right_divergent_to+infty_in x0
now :: thesis: abs f is_right_divergent_to+infty_in x0
per cases ( f is_right_divergent_to+infty_in x0 or f is_right_divergent_to-infty_in x0 ) by A1;
suppose A2: f is_right_divergent_to+infty_in x0 ; :: thesis: abs f is_right_divergent_to+infty_in x0
A3: now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (right_open_halfline x0) holds
(abs f) /* seq is divergent_to+infty
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (right_open_halfline x0) implies (abs f) /* seq is divergent_to+infty )
assume that
A4: seq is convergent and
A5: lim seq = x0 and
A6: rng seq c= (dom (abs f)) /\ (right_open_halfline x0) ; :: thesis: (abs f) /* seq is divergent_to+infty
A7: rng seq c= (dom f) /\ (right_open_halfline x0) by A6, VALUED_1:def 11;
then f /* seq is divergent_to+infty by A2, A4, A5;
then A8: abs (f /* seq) is divergent_to+infty by LIMFUNC1:25;
(dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;
then rng seq c= dom f by A7, XBOOLE_1:1;
hence (abs f) /* seq is divergent_to+infty by A8, RFUNCT_2:10; :: thesis: verum
end;
now :: thesis: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (abs f) )
let r be Real; :: thesis: ( x0 < r implies ex g being Real st
( g < r & x0 < g & g in dom (abs f) ) )
assume x0 < r ; :: thesis: ex g being Real st
( g < r & x0 < g & g in dom (abs f) )
then consider g being Real such that
A9: g < r and
A10: x0 < g and
A11: g in dom f by A2;
take g = g; :: thesis: ( g < r & x0 < g & g in dom (abs f) )
thus ( g < r & x0 < g & g in dom (abs f) ) by A9, A10, A11, VALUED_1:def 11; :: thesis: verum
end;
hence abs f is_right_divergent_to+infty_in x0 by A3; :: thesis: verum
end;
suppose A12: f is_right_divergent_to-infty_in x0 ; :: thesis: abs f is_right_divergent_to+infty_in x0
A13: now :: thesis: for seq being Real_Sequence st seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (right_open_halfline x0) holds
(abs f) /* seq is divergent_to+infty
let seq be Real_Sequence; :: thesis: ( seq is convergent & lim seq = x0 & rng seq c= (dom (abs f)) /\ (right_open_halfline x0) implies (abs f) /* seq is divergent_to+infty )
assume that
A14: seq is convergent and
A15: lim seq = x0 and
A16: rng seq c= (dom (abs f)) /\ (right_open_halfline x0) ; :: thesis: (abs f) /* seq is divergent_to+infty
A17: rng seq c= (dom f) /\ (right_open_halfline x0) by A16, VALUED_1:def 11;
then f /* seq is divergent_to-infty by A12, A14, A15;
then A18: abs (f /* seq) is divergent_to+infty by LIMFUNC1:25;
(dom f) /\ (right_open_halfline x0) c= dom f by XBOOLE_1:17;
then rng seq c= dom f by A17, XBOOLE_1:1;
hence (abs f) /* seq is divergent_to+infty by A18, RFUNCT_2:10; :: thesis: verum
end;
now :: thesis: for r being Real st x0 < r holds
ex g being Real st
( g < r & x0 < g & g in dom (abs f) )
let r be Real; :: thesis: ( x0 < r implies ex g being Real st
( g < r & x0 < g & g in dom (abs f) ) )
assume x0 < r ; :: thesis: ex g being Real st
( g < r & x0 < g & g in dom (abs f) )
then consider g being Real such that
A19: g < r and
A20: x0 < g and
A21: g in dom f by A12;
take g = g; :: thesis: ( g < r & x0 < g & g in dom (abs f) )
thus ( g < r & x0 < g & g in dom (abs f) ) by A19, A20, A21, VALUED_1:def 11; :: thesis: verum
end;
hence abs f is_right_divergent_to+infty_in x0 by A13; :: thesis: verum
end;
end;
end;
hence abs f is_right_divergent_to+infty_in x0 ; :: thesis: verum