let f be PartFunc of REAL,REAL; for b being Real st dom f = REAL & f is_improper_integrable_on_REAL holds
( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
let b be Real; ( dom f = REAL & f is_improper_integrable_on_REAL implies ( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) ) )
assume that
A1:
dom f = REAL
and
A2:
f is_improper_integrable_on_REAL
; ( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )
consider b1 being Real such that
A3:
f is_-infty_improper_integrable_on b1
and
A4:
f is_+infty_improper_integrable_on b1
and
A5:
improper_integral_on_REAL f = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A1, A2, Def6;
per cases
( b < b1 or b >= b1 )
;
suppose A6:
b < b1
;
( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )hence
f is_-infty_improper_integrable_on b
by A3, A1, Th25;
( f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )A7:
right_closed_halfline b c= dom f
by A1;
(
f | ['b,b1'] is
bounded &
f is_integrable_on ['b,b1'] )
by A3, A6;
hence
f is_+infty_improper_integrable_on b
by A6, A4, A7, Th31;
improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b))thus
improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b))
by A1, A2, A5, Th35;
verum end; suppose A8:
b >= b1
;
( f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )A9:
left_closed_halfline b c= dom f
by A1;
(
f | ['b1,b'] is
bounded &
f is_integrable_on ['b1,b'] )
by A4, A8;
hence
f is_-infty_improper_integrable_on b
by A3, A8, A9, Th26;
( f is_+infty_improper_integrable_on b & improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) )thus
f is_+infty_improper_integrable_on b
by A8, A1, A4, Th30;
improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b))thus
improper_integral_on_REAL f = (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b))
by A1, A2, A5, Th35;
verum end; end;