let n be non zero Nat; :: thesis: ( 'I' . (2 * n) <= 'I' . ((2 * n) -' 1) & 'I' . ((2 * n) + 1) <= 'I' . (2 * n) )
0 < 0 + n ;
then 1 <= n by NAT_1:19;
then 2 * n >= 2 * 1 by XREAL_1:64;
then A2: (2 * n) -' 1 = (2 * n) - 1 by XREAL_1:233, XXREAL_0:2;
set I0 = @ ((@ sin) |^ ((2 * n) -' 1));
set I1 = @ ((@ sin) |^ (2 * n));
set I2 = @ ((@ sin) |^ ((2 * n) + 1));
A3: ( (@ ((@ sin) |^ ((2 * n) -' 1))) | ['0,(PI / 2)'] is continuous & @ ((@ sin) |^ ((2 * n) -' 1)) is_integrable_on ['0,(PI / 2)'] & (@ ((@ sin) |^ ((2 * n) -' 1))) | ['0,(PI / 2)'] is bounded ) by Th25;
A4: ( (@ ((@ sin) |^ (2 * n))) | ['0,(PI / 2)'] is continuous & @ ((@ sin) |^ (2 * n)) is_integrable_on ['0,(PI / 2)'] & (@ ((@ sin) |^ (2 * n))) | ['0,(PI / 2)'] is bounded ) by Th25;
A5: ( (@ ((@ sin) |^ ((2 * n) + 1))) | ['0,(PI / 2)'] is continuous & @ ((@ sin) |^ ((2 * n) + 1)) is_integrable_on ['0,(PI / 2)'] & (@ ((@ sin) |^ ((2 * n) + 1))) | ['0,(PI / 2)'] is bounded ) by Th25;
A6: ( dom (@ ((@ sin) |^ ((2 * n) -' 1))) = REAL & dom (@ ((@ sin) |^ (2 * n))) = REAL & dom (@ ((@ sin) |^ ((2 * n) + 1))) = REAL ) by FUNCT_2:def 1;
A7: for x being Real st x in ['0,(PI / 2)'] holds
(@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x

proof

let x be Real; :: thesis: ( x in ['0,(PI / 2)'] implies (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x )
assume x in ['0,(PI / 2)'] ; :: thesis: (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x
then x in [.0,(PI / 2).] by INTEGRA5:def 3, COMPTRIG:5;

per cases then ( x in ].0,(PI / 2).[ or x = 0 or x = PI / 2 ) by XXREAL_1:5;

suppose x in ].0,(PI / 2).[ ; :: thesis: (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x

then ( 0 < x & x < PI / 2 ) by XXREAL_1:4;
hence (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x by Th42; :: thesis: verum

end;

suppose x = 0 ; :: thesis: (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x

then ( (@ ((@ sin) |^ (2 * n))) . x = 0 & (@ ((@ sin) |^ ((2 * n) + 1))) . x = 0 ) by Th27;
hence (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x ; :: thesis: verum

end;

suppose x = PI / 2 ; :: thesis: (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x

then ( (@ ((@ sin) |^ (2 * n))) . x = 1 & (@ ((@ sin) |^ ((2 * n) + 1))) . x = 1 ) by Th27;
hence (@ ((@ sin) |^ ((2 * n) + 1))) . x <= (@ ((@ sin) |^ (2 * n))) . x ; :: thesis: verum

end;

end;

end;

A16: for x being Real st x in ['0,(PI / 2)'] holds
(@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x

proof

let x be Real; :: thesis: ( x in ['0,(PI / 2)'] implies (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x )
assume x in ['0,(PI / 2)'] ; :: thesis: (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x
then x in [.0,(PI / 2).] by INTEGRA5:def 3, COMPTRIG:5;

per cases then ( x in ].0,(PI / 2).[ or x = 0 or x = PI / 2 ) by XXREAL_1:5;

suppose x in ].0,(PI / 2).[ ; :: thesis: (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x

then ( 0 < x & x < PI / 2 ) by XXREAL_1:4;
hence (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x by Th42; :: thesis: verum

end;

suppose x = 0 ; :: thesis: (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x

then ( (@ ((@ sin) |^ (2 * n))) . x = 0 & (@ ((@ sin) |^ ((2 * n) -' 1))) . x = 0 & (@ ((@ sin) |^ ((2 * n) + 1))) . x = 0 ) by A2, Th27;
hence (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x ; :: thesis: verum

end;

suppose x = PI / 2 ; :: thesis: (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x

then ( (@ ((@ sin) |^ (2 * n))) . x = 1 & (@ ((@ sin) |^ ((2 * n) -' 1))) . x = 1 & (@ ((@ sin) |^ ((2 * n) + 1))) . x = 1 ) by A2, Th27;
hence (@ ((@ sin) |^ (2 * n))) . x <= (@ ((@ sin) |^ ((2 * n) -' 1))) . x ; :: thesis: verum

end;

end;

end;

A25: integral ((@ ((@ sin) |^ (2 * n))),0,(PI / 2)) <= integral ((@ ((@ sin) |^ ((2 * n) -' 1))),0,(PI / 2)) by A3, A4, COMPTRIG:5, A6, A16, ORDEQ_01:48;
A26: integral ((@ ((@ sin) |^ ((2 * n) + 1))),0,(PI / 2)) <= integral ((@ ((@ sin) |^ (2 * n))),0,(PI / 2)) by A5, A4, COMPTRIG:5, A6, A7, ORDEQ_01:48;
reconsider n0 = (2 * n) -' 1, n1 = 2 * n, n2 = (2 * n) + 1 as Element of NAT by ORDINAL1:def 12;
'I' . n1 = integral ((@ ((@ sin) |^ (2 * n))),0,(PI / 2)) by Def6;
hence ( 'I' . (2 * n) <= 'I' . ((2 * n) -' 1) & 'I' . ((2 * n) + 1) <= 'I' . (2 * n) ) by Def6, A26, A25; :: thesis: verum