let f be PartFunc of REAL,REAL; :: thesis: for b being Real st f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = -infty holds
for Intf being PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) holds
Intf is divergent_in-infty_to-infty
let b be Real; :: thesis: ( f is_-infty_improper_integrable_on b & improper_integral_-infty (f,b) = -infty implies for Intf being PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) holds
Intf is divergent_in-infty_to-infty )
assume that
A1: f is_-infty_improper_integrable_on b and
A2: improper_integral_-infty (f,b) = -infty ; :: thesis: for Intf being PartFunc of REAL,REAL st dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) holds
Intf is divergent_in-infty_to-infty
let Intf be PartFunc of REAL,REAL; :: thesis: ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ) implies Intf is divergent_in-infty_to-infty )
assume that
A3: dom Intf = left_closed_halfline b and
A4: for x being Real st x in dom Intf holds
Intf . x = integral (f,x,b) ; :: thesis: Intf is divergent_in-infty_to-infty
consider I being PartFunc of REAL,REAL such that
A5: ( dom I = left_closed_halfline b & ( for x being Real st x in dom I holds
I . x = integral (f,x,b) ) & ( ( I is convergent_in-infty & improper_integral_-infty (f,b) = lim_in-infty I ) or ( I is divergent_in-infty_to+infty & improper_integral_-infty (f,b) = +infty ) or ( I is divergent_in-infty_to-infty & improper_integral_-infty (f,b) = -infty ) ) ) by A1, Def3;
for x being Element of REAL st x in dom I holds
I . x = Intf . x
proof
let x be Element of REAL ; :: thesis: ( x in dom I implies I . x = Intf . x )
assume x in dom I ; :: thesis: I . x = Intf . x
then ( I . x = integral (f,x,b) & Intf . x = integral (f,x,b) ) by A3, A4, A5;
hence I . x = Intf . x ; :: thesis: verum
end;
hence Intf is divergent_in-infty_to-infty by A2, A3, A5, PARTFUN1:5; :: thesis: verum