let f be PartFunc of REAL,REAL; :: thesis: for b, c being Real st b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) holds
( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b)) )
let b, c be Real; :: thesis: ( b >= c & right_closed_halfline c c= dom f & f | ['c,b'] is bounded & f is_+infty_improper_integrable_on b & f is_integrable_on ['c,b'] & improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) implies ( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b)) ) )
assume that
A1: b >= c and
A2: right_closed_halfline c c= dom f and
A3: f | ['c,b'] is bounded and
A4: f is_+infty_improper_integrable_on b and
A5: f is_integrable_on ['c,b'] and
A6: improper_integral_+infty (f,b) = infty_ext_right_integral (f,b) ; :: thesis: ( f is_+infty_improper_integrable_on c & improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b)) )
consider I being PartFunc of REAL,REAL such that
A7: dom I = right_closed_halfline b and
A8: for x being Real st x in dom I holds
I . x = integral (f,b,x) and
A9: ( I is convergent_in+infty or I is divergent_in+infty_to+infty or I is divergent_in+infty_to-infty ) by A4;
A10: now :: thesis: not I is divergent_in+infty_to+infty
assume I is divergent_in+infty_to+infty ; :: thesis: contradiction
then not f is_+infty_ext_Riemann_integrable_on b by A7, A8, Th28;
hence contradiction by A4, A6, Th27; :: thesis: verum
end;
now :: thesis: not I is divergent_in+infty_to-infty
assume I is divergent_in+infty_to-infty ; :: thesis: contradiction
then not f is_+infty_ext_Riemann_integrable_on b by A7, A8, Th28;
hence contradiction by A4, A6, Th27; :: thesis: verum
end;
then f is_+infty_ext_Riemann_integrable_on b by A4, A7, A8, A9, A10, INTEGR10:def 5;
then A11: ( f is_+infty_ext_Riemann_integrable_on c & infty_ext_right_integral (f,c) = (infty_ext_right_integral (f,b)) + (integral (f,c,b)) ) by A1, A2, A3, A5, Th18;
ex Intf being PartFunc of REAL,REAL st
( dom Intf = right_closed_halfline c & ( for x being Real st x in dom Intf holds
Intf . x = integral (f,c,x) ) & Intf is convergent_in+infty ) by A11, INTEGR10:def 5;
hence f is_+infty_improper_integrable_on c by A1, A2, A3, A4, A5, Lm14; :: thesis: improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b))
then improper_integral_+infty (f,c) = (infty_ext_right_integral (f,b)) + (integral (f,c,b)) by A11, Th27;
hence improper_integral_+infty (f,c) = (improper_integral_+infty (f,b)) + (integral (f,c,b)) by A6, XXREAL_3:def 2; :: thesis: verum