let a, b, c, d be Real; :: thesis: for f being PartFunc of REAL,REAL st c <= d & [.c,d.] c= [.a,b.] & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonnegative holds
integral (f,c,d) <= integral (f,a,b)
let f be PartFunc of REAL,REAL; :: thesis: ( c <= d & [.c,d.] c= [.a,b.] & [.a,b.] c= dom f & f | [.a,b.] is bounded & f is_integrable_on ['a,b'] & f | [.a,b.] is nonnegative implies integral (f,c,d) <= integral (f,a,b) )
assume that
A1: c <= d and
A2: [.c,d.] c= [.a,b.] and
A3: [.a,b.] c= dom f and
A4: f | [.a,b.] is bounded and
A5: f is_integrable_on ['a,b'] and
A6: f | [.a,b.] is nonnegative ; :: thesis: integral (f,c,d) <= integral (f,a,b)
A7: ( a <= c & d <= b ) by A1, A2, XXREAL_1:50;
then A8: a <= d by A1, XXREAL_0:2;
then A9: a <= b by A7, XXREAL_0:2;
A10: [.a,b.] = ['a,b'] by A8, A7, XXREAL_0:2, INTEGRA5:def 3;
then c in ['a,b'] by A1, A2, XXREAL_1:1;
then A11: integral (f,a,b) = (integral (f,a,c)) + (integral (f,c,b)) by A9, A3, A4, A5, A10, INTEGRA6:17;
A12: c <= b by A1, A7, XXREAL_0:2;
then [.a,c.] c= [.a,b.] by XXREAL_1:34;
then A13: [.a,c.] c= dom f by A3;
A14: f | [.a,c.] is bounded by A4, A12, XXREAL_1:34, RFUNCT_1:74;
(f | [.a,b.]) | [.a,c.] is nonnegative by A6, MESFUNC6:55;
then f | [.a,c.] is nonnegative by A12, XXREAL_1:34, RELAT_1:74;
then 0 <= integral (f,a,c) by A7, A13, A14, Th12;
then A15: integral (f,c,b) <= integral (f,a,b) by A11, XREAL_1:31;
A16: ( f is_integrable_on ['c,b'] & f | ['c,b'] is bounded ) by A3, A4, A5, A10, A7, A12, INTEGRA6:18;
A17: [.c,b.] = ['c,b'] by A1, A7, XXREAL_0:2, INTEGRA5:def 3;
[.c,b.] c= [.a,b.] by A7, XXREAL_1:34;
then A18: ['c,b'] c= dom f by A3, A17;
d in ['c,b'] by A1, A7, A17, XXREAL_1:1;
then A19: integral (f,c,b) = (integral (f,c,d)) + (integral (f,d,b)) by A12, A16, A18, INTEGRA6:17;
[.d,b.] c= [.a,b.] by A8, XXREAL_1:34;
then A20: [.d,b.] c= dom f by A3;
A21: f | [.d,b.] is bounded by A4, A8, XXREAL_1:34, RFUNCT_1:74;
(f | [.a,b.]) | [.d,b.] is nonnegative by A6, MESFUNC6:55;
then f | [.d,b.] is nonnegative by A8, XXREAL_1:34, RELAT_1:74;
then 0 <= integral (f,d,b) by A7, A20, A21, Th12;
then integral (f,c,d) <= integral (f,c,b) by A19, XREAL_1:31;
hence integral (f,c,d) <= integral (f,a,b) by A15, XXREAL_0:2; :: thesis: verum