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'] & right_improper_integral (f,b,c) = +infty holds
( f is_right_improper_integrable_on a,c & 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'] & right_improper_integral (f,b,c) = +infty implies ( f is_right_improper_integrable_on a,c & 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'] and
A6: right_improper_integral (f,b,c) = +infty ; :: thesis: ( f is_right_improper_integrable_on a,c & right_improper_integral (f,a,c) = +infty )
consider I being PartFunc of REAL,REAL such that
A7: dom I = [.b,c.[ and
A8: for x being Real st x in dom I holds
I . x = integral (f,b,x) and
A9: ( I is_left_convergent_in c or I is_left_divergent_to+infty_in c or I is_left_divergent_to-infty_in c ) by A4;
right_improper_integral (f,b,c) <> ext_right_integral (f,b,c) by A6;
then A10: not f is_right_ext_Riemann_integrable_on b,c by A4, Th39;
reconsider AC = [.a,c.[ as non empty Subset of REAL by A1, XXREAL_1:3;
deffunc H₁( Element of AC) -> Element of REAL = In ((integral (f,a,$1)),REAL);
consider Intf being Function of AC,REAL such that
A11: for x being Element of AC holds Intf . x = H₁(x) from FUNCT_2:sch 4();
A12: dom Intf = AC by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A13: for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x)

proof

let x be Real; :: thesis: ( x in dom Intf implies Intf . x = integral (f,a,x) )
assume x in dom Intf ; :: thesis: Intf . x = integral (f,a,x)
then Intf . x = In ((integral (f,a,x)),REAL) by A11, A12;
hence Intf . x = integral (f,a,x) ; :: thesis: verum

end;

A14: for r being Real st r < c holds
ex g being Real st
( r < g & g < c & g in dom Intf )

proof

let r be Real; :: thesis: ( r < c implies ex g being Real st
( r < g & g < c & g in dom Intf ) )
assume r < c ; :: thesis: ex g being Real st
( r < g & g < c & g in dom Intf )
then consider g being Real such that
A15: ( r < g & g < c & g in dom I ) by A10, A6, A7, Def4, INTEGR10:def 1, A4, LIMFUNC2:8;
[.b,c.[ c= [.a,c.[ by A1, XXREAL_1:38;
hence ex g being Real st
( r < g & g < c & g in dom Intf ) by A15, A7, A12; :: thesis: verum

end;

A16: for g1 being Real ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
g1 < Intf . r1 ) )

proof

let g1 be Real; :: thesis: ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
g1 < Intf . r1 ) )
consider r being Real such that
A17: r < c and
A18: for r1 being Real st r < r1 & r1 < c & r1 in dom I holds
g1 - (integral (f,a,b)) < I . r1 by A10, A9, A4, A6, A7, A8, Def4, INTEGR10:def 1, LIMFUNC2:8;
set R = max (b,r);
take max (b,r) ; :: thesis: ( max (b,r) < c & ( for r1 being Real st max (b,r) < r1 & r1 < c & r1 in dom Intf holds
g1 < Intf . r1 ) )
thus max (b,r) < c by A1, A17, XXREAL_0:29; :: thesis: for r1 being Real st max (b,r) < r1 & r1 < c & r1 in dom Intf holds
g1 < Intf . r1
thus for r1 being Real st max (b,r) < r1 & r1 < c & r1 in dom Intf holds
g1 < Intf . r1 :: thesis: verum

proof

let r1 be Real; :: thesis: ( max (b,r) < r1 & r1 < c & r1 in dom Intf implies g1 < Intf . r1 )
assume A19: ( max (b,r) < r1 & r1 < c & r1 in dom Intf ) ; :: thesis: g1 < Intf . r1
( b <= max (b,r) & r <= max (b,r) ) by XXREAL_0:25;
then A20: ( b < r1 & r < r1 ) by A19, XXREAL_0:2;
then A21: a < r1 by A1, XXREAL_0:2;
r1 in dom I by A7, A19, A20, XXREAL_1:3;
then g1 - (integral (f,a,b)) < I . r1 by A18, A19, A20;
then A22: g1 - (integral (f,a,b)) < integral (f,b,r1) by A8, A20, A7, A19, XXREAL_1:3;
A23: ( f is_integrable_on ['a,r1'] & f | ['a,r1'] is bounded ) by A19, A21, A1, A2, A3, A4, A5, Lm19;
A24: ['a,r1'] = [.a,r1.] by A20, A1, XXREAL_0:2, INTEGRA5:def 3;
then ['a,r1'] c= [.a,c.[ by A19, XXREAL_1:43;
then A25: ['a,r1'] c= dom f by A2;
b in ['a,r1'] by A24, A20, A1, XXREAL_1:1;
then integral (f,a,r1) = (integral (f,a,b)) + (integral (f,b,r1)) by A21, A23, A25, INTEGRA6:17;
then integral (f,b,r1) = (integral (f,a,r1)) - (integral (f,a,b)) ;
then g1 < integral (f,a,r1) by A22, XREAL_1:9;
hence g1 < Intf . r1 by A13, A19; :: thesis: verum

end;

end;

hence A26: f is_right_improper_integrable_on a,c by A12, A13, A14, A1, A2, A3, A4, A5, Lm19, LIMFUNC2:8; :: thesis: right_improper_integral (f,a,c) = +infty
Intf is_left_divergent_to+infty_in c by A14, A16, LIMFUNC2:8;
hence right_improper_integral (f,a,c) = +infty by A12, A13, A26, Def4; :: thesis: verum