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 nonpositive 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 nonpositive 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 nonpositive ; :: thesis: integral (f,c,d) >= integral (f,a,b)
A7: ( a <= c & d <= b ) by A2, A1, XXREAL_1:50;
then A8: ( a <= d & c <= b ) by A1, XXREAL_0:2;
then A9: a <= b by A7, XXREAL_0:2;
A10: ( [.a,b.] = ['a,b'] & [.a,c.] = ['a,c'] & [.d,b.] = ['d,b'] ) by A8, A7, XXREAL_0:2, INTEGRA5:def 3;
then c in ['a,b'] by A2, A1, 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;
( [.a,c.] c= [.a,b.] & [.d,b.] c= [.a,b.] ) by A8, XXREAL_1:34;
then A12: ( [.a,c.] c= dom f & [.d,b.] c= dom f ) by A3;
A13: ( f is_integrable_on ['a,c'] & f | ['a,c'] is bounded & f is_integrable_on ['c,b'] & f | ['c,b'] is bounded & f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A7, A8, A4, A5, A10, A3, INTEGRA6:18;
(f | [.a,b.]) | [.a,c.] is nonpositive by A6, Th4;
then f | [.a,c.] is nonpositive by A8, XXREAL_1:34, RELAT_1:74;
then 0 >= integral (f,a,c) by A7, A12, A13, A10, Th13;
then A14: integral (f,c,b) >= integral (f,a,b) by A11, XREAL_1:32;
A15: [.c,b.] = ['c,b'] by A1, A7, XXREAL_0:2, INTEGRA5:def 3;
[.c,b.] c= [.a,b.] by A7, XXREAL_1:34;
then A16: ['c,b'] c= dom f by A3, A15;
d in ['c,b'] by A1, A7, A15, XXREAL_1:1;
then A17: integral (f,c,b) = (integral (f,c,d)) + (integral (f,d,b)) by A8, A13, A16, INTEGRA6:17;
(f | [.a,b.]) | [.d,b.] is nonpositive by A6, Th4;
then f | [.d,b.] is nonpositive by A8, XXREAL_1:34, RELAT_1:74;
then 0 >= integral (f,d,b) by A7, A12, A13, A10, Th13;
then integral (f,c,d) >= integral (f,c,b) by A17, XREAL_1:32;
hence integral (f,c,d) >= integral (f,a,b) by A14, XXREAL_0:2; :: thesis: verum