let A be non empty closed_interval Subset of REAL; :: thesis: for f being Function of A,REAL st f | A is bounded & f is integrable holds
( abs f is integrable & |.(integral f).| <= integral (abs f) )
let f be Function of A,REAL; :: thesis: ( f | A is bounded & f is integrable implies ( abs f is integrable & |.(integral f).| <= integral (abs f) ) )
assume that
A1: f | A is bounded and
A2: f is integrable ; :: thesis: ( abs f is integrable & |.(integral f).| <= integral (abs f) )
A3: max- f is integrable by A1, A2, Th22;
A4: (max+ f) | A is bounded_above by A1, Th14;
A5: (max- f) | A is bounded_above by A1, Th16;
A6: max+ f is total by Th13;
A7: (max- f) | A is bounded_below by Th17;
A8: (max+ f) | A is bounded_below by Th15;
A9: max- f is total by Th13;
A10: max+ f is integrable by A1, A2, Th20;
then (max+ f) + (max- f) is integrable by A6, A9, A4, A8, A5, A7, A3, INTEGRA1:57;
hence abs f is integrable by RFUNCT_3:34; :: thesis: |.(integral f).| <= integral (abs f)
A11: (integral (max+ f)) - (integral (max- f)) = integral ((max+ f) - (max- f)) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA2:33
.= integral f by RFUNCT_3:34 ;
A12: (integral (max+ f)) + (integral (max- f)) = integral ((max+ f) + (max- f)) by A6, A9, A4, A8, A5, A7, A10, A3, INTEGRA1:57
.= integral (abs f) by RFUNCT_3:34 ;
then A13: (integral (abs f)) - (integral f) = 2 * (integral (max- f)) by A11;
for x being Real st x in A holds
(max- f) . x >= 0 by RFUNCT_3:40;
then integral (max- f) >= 0 by A9, A5, A7, INTEGRA2:32;
then A14: integral (abs f) >= integral f by A13, XREAL_1:49;
A15: (integral (abs f)) + (integral f) = 2 * (integral (max+ f)) by A12, A11;
for x being Real st x in A holds
(max+ f) . x >= 0 by RFUNCT_3:37;
then integral (max+ f) >= 0 by A6, A4, A8, INTEGRA2:32;
then - (integral (abs f)) <= integral f by A15, XREAL_1:61;
hence |.(integral f).| <= integral (abs f) by A14, ABSVALUE:5; :: thesis: verum