let f be PartFunc of REAL,REAL; :: thesis: ( 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 ; :: thesis: 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; :: thesis: (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 ) ; :: thesis: (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)) ; :: thesis: verum
end;
suppose ( b1 < b & b <= b2 ) ; :: thesis: (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)) ; :: thesis: verum
end;
suppose ( b <= b1 & b2 < b ) ; :: thesis: (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)) ; :: thesis: verum
end;
suppose ( b <= b1 & b <= b2 ) ; :: thesis: (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)) ; :: thesis: verum
end;
end;