let f, g be PartFunc of REAL,REAL; :: thesis: for a being Real st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) holds
( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) )
let a be Real; :: thesis: ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_improper_integrable_on a & g is_+infty_improper_integrable_on a & ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) & ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) implies ( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) ) )
assume that
A1: right_closed_halfline a c= dom f and
A2: right_closed_halfline a c= dom g and
A3: f is_+infty_improper_integrable_on a and
A4: g is_+infty_improper_integrable_on a and
A5: ( not improper_integral_+infty (f,a) = +infty or not improper_integral_+infty (g,a) = +infty ) and
A6: ( not improper_integral_+infty (f,a) = -infty or not improper_integral_+infty (g,a) = -infty ) ; :: thesis: ( f - g is_+infty_improper_integrable_on a & improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) )
A7: dom (- g) = dom g by VALUED_1:8;
A8: - g is_+infty_improper_integrable_on a by A2, A4, Th44;
A9: now :: thesis: ( improper_integral_+infty (f,a) = +infty implies not improper_integral_+infty ((- g),a) = -infty )
assume A10: ( improper_integral_+infty (f,a) = +infty & improper_integral_+infty ((- g),a) = -infty ) ; :: thesis: contradiction
then - (improper_integral_+infty (g,a)) = - +infty by A2, A4, Th44, XXREAL_3:6;
hence contradiction by A5, A10, XXREAL_3:10; :: thesis: verum
end;
A11: now :: thesis: ( improper_integral_+infty (f,a) = -infty implies not improper_integral_+infty ((- g),a) = +infty )
assume A12: ( improper_integral_+infty (f,a) = -infty & improper_integral_+infty ((- g),a) = +infty ) ; :: thesis: contradiction
then - (improper_integral_+infty (g,a)) = - -infty by A2, A4, Th44, XXREAL_3:5;
hence contradiction by A6, A12, XXREAL_3:10; :: thesis: verum
end;
hence f - g is_+infty_improper_integrable_on a by A1, A2, A7, A3, A8, A9, Th46; :: thesis: improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a))
improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) + (improper_integral_+infty ((- g),a)) by A1, A2, A7, A3, A8, A9, A11, Th46
.= (improper_integral_+infty (f,a)) + (- (improper_integral_+infty (g,a))) by A2, A4, Th44 ;
hence improper_integral_+infty ((f - g),a) = (improper_integral_+infty (f,a)) - (improper_integral_+infty (g,a)) by XXREAL_3:def 4; :: thesis: verum