let a, b be Real; :: thesis: for f being PartFunc of REAL,REAL st a <= b & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonpositive holds
integral (f,a,b) <= 0
let f be PartFunc of REAL,REAL; :: thesis: ( a <= b & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonpositive implies integral (f,a,b) <= 0 )
assume that
A1: a <= b and
A2: [.a,b.] c= dom f and
A3: f | [.a,b.] is bounded and
A4: f is_integrable_on ['a,b'] and
A5: f | [.a,b.] is nonpositive ; :: thesis: integral (f,a,b) <= 0
A6: f || ['a,b'] is integrable by A4, INTEGRA5:def 1;
reconsider A = [.a,b.] as non empty closed_interval Subset of REAL by A1, XXREAL_1:30, MEASURE5:def 3;
A7: [.a,b.] c= dom (- f) by A2, VALUED_1:8;
A8: (- f) | [.a,b.] is bounded by A3, RFUNCT_1:82;
A9: A = ['a,b'] by A1, INTEGRA5:def 3;
- (f | [.a,b.]) is nonnegative by A5, Th5;
then (- f) | A is nonnegative by RFUNCT_1:46;
then integral ((- f),a,b) >= 0 by A1, A7, A8, Th12;
then A10: integral ((- f),A) >= 0 by A1, A9, INTEGRA5:def 4;
dom (f | A) = A by A2, RELAT_1:62;
then reconsider f0 = f | A as Function of A,REAL by FUNCT_2:def 1, RELSET_1:5;
dom ((- f) | A) = A by A7, RELAT_1:62;
then reconsider f1 = (- f) | A as Function of A,REAL by FUNCT_2:def 1, RELSET_1:5;
A11: integral f1 >= 0 by A10, INTEGRA5:def 2;
f0 = ((- 1) (#) (- f)) | A ;
then A12: f0 = (- 1) (#) f1 by MESFUN6C:41;
A13: (- 1) (#) f = - f by VALUED_1:def 6;
A14: f1 | A is bounded by A3, RFUNCT_1:82;
f0 | A is bounded by A3;
then (- 1) (#) f0 is integrable by A6, A9, INTEGRA2:31;
then f1 is integrable by A13, MESFUN6C:41;
then integral ((- 1) (#) f1) = (- 1) * (integral f1) by A14, INTEGRA2:31;
then integral (f,A) <= 0 by A12, A11, INTEGRA5:def 2;
hence integral (f,a,b) <= 0 by A1, A9, INTEGRA5:def 4; :: thesis: verum