let f be PartFunc of REAL,REAL; ( dom f = REAL & f is_improper_integrable_on_REAL implies for b1, b2 being Real holds (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
assume that
A1:
dom f = REAL
and
A2:
f is_improper_integrable_on_REAL
; for b1, b2 being Real holds (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
let b1, b2 be Real; (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
consider b being Real such that
A3:
f is_-infty_improper_integrable_on b
and
A4:
f is_+infty_improper_integrable_on b
and
A5:
( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty )
and
A6:
( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty )
by A2;
per cases
( ( b1 < b & b2 < b ) or ( b1 < b & b <= b2 ) or ( b <= b1 & b2 < b ) or ( b <= b1 & b <= b2 ) )
;
suppose
(
b1 < b &
b2 < b )
;
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))then
(
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) &
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
by A1, A3, A4, A5, A6, Th33;
hence
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
;
verum end; suppose
(
b1 < b &
b <= b2 )
;
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))then
(
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) &
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
by A1, A3, A4, A5, A6, Th33, Th34;
hence
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
;
verum end; suppose
(
b <= b1 &
b2 < b )
;
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))then
(
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) &
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
by A1, A3, A4, A5, A6, Th33, Th34;
hence
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
;
verum end; suppose
(
b <= b1 &
b <= b2 )
;
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))then
(
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) &
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2)) )
by A1, A3, A4, A5, A6, Th34;
hence
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = (improper_integral_-infty (f,b2)) + (improper_integral_+infty (f,b2))
;
verum end; end;