let f be PartFunc of REAL,REAL; :: thesis: for b, c being Real st b <= c & left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c holds
( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
let b, c be Real; :: thesis: ( b <= c & left_closed_halfline c c= dom f & f is_-infty_improper_integrable_on c implies ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) ) )
assume that
A1: b <= c and
A2: left_closed_halfline c c= dom f and
A3: f is_-infty_improper_integrable_on c ; :: thesis: ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
per cases ( f is_-infty_ext_Riemann_integrable_on c or not f is_-infty_ext_Riemann_integrable_on c ) ;
suppose f is_-infty_ext_Riemann_integrable_on c ; :: thesis: ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
then improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) by A3, Th22;
hence ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) ) by A1, A2, A3, Lm3; :: thesis: verum
end;
suppose not f is_-infty_ext_Riemann_integrable_on c ; :: thesis: ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
per cases then ( improper_integral_-infty (f,c) = +infty or improper_integral_-infty (f,c) = -infty ) by A3, Th22;
suppose improper_integral_-infty (f,c) = +infty ; :: thesis: ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
hence ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) ) by A1, A2, A3, Lm4; :: thesis: verum
end;
suppose improper_integral_-infty (f,c) = -infty ; :: thesis: ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) )
hence ( f is_-infty_improper_integrable_on b & ( improper_integral_-infty (f,c) = infty_ext_left_integral (f,c) implies improper_integral_-infty (f,b) = infty_ext_left_integral (f,b) ) & ( improper_integral_-infty (f,c) = +infty implies improper_integral_-infty (f,b) = +infty ) & ( improper_integral_-infty (f,c) = -infty implies improper_integral_-infty (f,b) = -infty ) ) by A1, A2, A3, Lm5; :: thesis: verum
end;
end;
end;
end;