let f be PartFunc of REAL,REAL; :: thesis: for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] holds
( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )
let a, b, c be Real; :: thesis: ( a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_right_improper_integrable_on b,c & f is_integrable_on ['a,b'] implies ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) ) )
assume that
A1: ( a <= b & b < c ) and
A2: [.a,c.[ c= dom f and
A3: f | ['a,b'] is bounded and
A4: f is_right_improper_integrable_on b,c and
A5: f is_integrable_on ['a,b'] ; :: thesis: ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )

per cases ( f is_right_ext_Riemann_integrable_on b,c or not f is_right_ext_Riemann_integrable_on b,c ) ;

suppose f is_right_ext_Riemann_integrable_on b,c ; :: thesis: ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )

then right_improper_integral (f,b,c) = ext_right_integral (f,b,c) by A4, Th39;
hence ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) ) by A1, A2, A3, A4, A5, Lm20; :: thesis: verum

end;

suppose not f is_right_ext_Riemann_integrable_on b,c ; :: thesis: ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )

per cases then ( right_improper_integral (f,b,c) = +infty or right_improper_integral (f,b,c) = -infty ) by A4, Th39;

suppose right_improper_integral (f,b,c) = +infty ; :: thesis: ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )

hence ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) ) by A1, A2, A3, A4, A5, Lm21; :: thesis: verum

end;

suppose right_improper_integral (f,b,c) = -infty ; :: thesis: ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) )

hence ( f is_right_improper_integrable_on a,c & ( right_improper_integral (f,b,c) = ext_right_integral (f,b,c) implies right_improper_integral (f,a,c) = (right_improper_integral (f,b,c)) + (integral (f,a,b)) ) & ( right_improper_integral (f,b,c) = +infty implies right_improper_integral (f,a,c) = +infty ) & ( right_improper_integral (f,b,c) = -infty implies right_improper_integral (f,a,c) = -infty ) ) by A1, A2, A3, A4, A5, Lm22; :: thesis: verum

end;

end;

end;

end;