let x0 be Real; :: thesis: for f being PartFunc of REAL,REAL st f is_convergent_in x0 & lim (f,x0) = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ) ) holds
f ^ is_divergent_to-infty_in x0
let f be PartFunc of REAL,REAL; :: thesis: ( f is_convergent_in x0 & lim (f,x0) = 0 & ex r being Real st
( 0 < r & ( for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ) ) implies f ^ is_divergent_to-infty_in x0 )
assume that
A1: f is_convergent_in x0 and
A2: lim (f,x0) = 0 ; :: thesis: ( for r being Real holds
( not 0 < r or ex g being Real st
( g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) & not f . g < 0 ) ) or f ^ is_divergent_to-infty_in x0 )
A3: f is_right_convergent_in x0 by A1, Th29;
given r being Real such that A4: 0 < r and
A5: for g being Real st g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) holds
f . g < 0 ; :: thesis: f ^ is_divergent_to-infty_in x0
A6: now :: thesis: for g being Real st g in (dom f) /\ ].x0,(x0 + r).[ holds
f . g < 0
let g be Real; :: thesis: ( g in (dom f) /\ ].x0,(x0 + r).[ implies f . g < 0 )
assume A7: g in (dom f) /\ ].x0,(x0 + r).[ ; :: thesis: f . g < 0
then g in ].x0,(x0 + r).[ by XBOOLE_0:def 4;
then A8: g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
g in dom f by A7, XBOOLE_0:def 4;
then g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A8, XBOOLE_0:def 4;
hence f . g < 0 by A5; :: thesis: verum
end;
A9: now :: thesis: for g being Real st g in (dom f) /\ ].(x0 - r),x0.[ holds
f . g < 0
let g be Real; :: thesis: ( g in (dom f) /\ ].(x0 - r),x0.[ implies f . g < 0 )
assume A10: g in (dom f) /\ ].(x0 - r),x0.[ ; :: thesis: f . g < 0
then g in ].(x0 - r),x0.[ by XBOOLE_0:def 4;
then A11: g in ].(x0 - r),x0.[ \/ ].x0,(x0 + r).[ by XBOOLE_0:def 3;
g in dom f by A10, XBOOLE_0:def 4;
then g in (dom f) /\ (].(x0 - r),x0.[ \/ ].x0,(x0 + r).[) by A11, XBOOLE_0:def 4;
hence f . g < 0 by A5; :: thesis: verum
end;
lim_right (f,x0) = 0 by A1, A2, Th29;
then A12: f ^ is_right_divergent_to-infty_in x0 by A3, A4, A6, LIMFUNC2:74;
A13: f is_left_convergent_in x0 by A1, Th29;
lim_left (f,x0) = 0 by A1, A2, Th29;
then f ^ is_left_divergent_to-infty_in x0 by A13, A4, A9, LIMFUNC2:72;
hence f ^ is_divergent_to-infty_in x0 by A12, Th13; :: thesis: verum