let f, g be PartFunc of REAL,REAL; :: thesis: for a, b being Real st ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = +infty ) & ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = -infty ) holds
( f - g is_improper_integrable_on a,b & improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) - (improper_integral (g,a,b)) )
let a, b be Real; :: thesis: ( ].a,b.[ c= dom f & ].a,b.[ c= dom g & f is_improper_integrable_on a,b & g is_improper_integrable_on a,b & ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = +infty ) & ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = -infty ) implies ( f - g is_improper_integrable_on a,b & improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) - (improper_integral (g,a,b)) ) )
assume that
A1: ].a,b.[ c= dom f and
A2: ].a,b.[ c= dom g and
A3: f is_improper_integrable_on a,b and
A4: g is_improper_integrable_on a,b and
A5: ( not improper_integral (f,a,b) = +infty or not improper_integral (g,a,b) = +infty ) and
A6: ( not improper_integral (f,a,b) = -infty or not improper_integral (g,a,b) = -infty ) ; :: thesis: ( f - g is_improper_integrable_on a,b & improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) - (improper_integral (g,a,b)) )
A7: dom (- g) = dom g by VALUED_1:8;
A8: - g is_improper_integrable_on a,b by A2, A4, Th62;
A9: improper_integral ((- g),a,b) = - (improper_integral (g,a,b)) by A2, A4, Th62;
then A10: ( improper_integral (f,a,b) <> +infty or improper_integral ((- g),a,b) <> -infty ) by A5, XXREAL_3:23;
A11: ( improper_integral (f,a,b) <> -infty or improper_integral ((- g),a,b) <> +infty ) by A6, A9, XXREAL_3:23;
hence f - g is_improper_integrable_on a,b by A1, A2, A3, A7, A8, A10, Th63; :: thesis: improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) - (improper_integral (g,a,b))
improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) + (improper_integral ((- g),a,b)) by A1, A2, A3, A7, A8, A10, A11, Th63
.= (improper_integral (f,a,b)) + (- (improper_integral (g,a,b))) by A2, A4, Th62 ;
hence improper_integral ((f - g),a,b) = (improper_integral (f,a,b)) - (improper_integral (g,a,b)) by XXREAL_3:def 4; :: thesis: verum