let n be non zero Nat; :: thesis: for x being Real st 0 < x & x < PI / 2 holds
( (@ ((@ sin) |^ (2 * n))) . x < (@ ((@ sin) |^ ((2 * n) -' 1))) . x & (@ ((@ sin) |^ ((2 * n) + 1))) . x < (@ ((@ sin) |^ (2 * n))) . x )
let x be Real; :: thesis: ( 0 < x & x < PI / 2 implies ( (@ ((@ sin) |^ (2 * n))) . x < (@ ((@ sin) |^ ((2 * n) -' 1))) . x & (@ ((@ sin) |^ ((2 * n) + 1))) . x < (@ ((@ sin) |^ (2 * n))) . x ) )
assume A1: ( 0 < x & x < PI / 2 ) ; :: thesis: ( (@ ((@ sin) |^ (2 * n))) . x < (@ ((@ sin) |^ ((2 * n) -' 1))) . x & (@ ((@ sin) |^ ((2 * n) + 1))) . x < (@ ((@ sin) |^ (2 * n))) . x )
then A2: 0 < (@ (@ sin)) . x by Th39;
then A3: (@ ((@ sin) |^ ((2 * n) -' 1))) . x = (sin . x) |^ ((2 * n) -' 1) by Th22;
A4: (@ ((@ sin) |^ (2 * n))) . x = (sin . x) |^ (2 * n) by A2, Th22;
(@ ((@ sin) |^ ((2 * n) + 1))) . x = (sin . x) |^ ((2 * n) + 1) by A2, Th22;
hence ( (@ ((@ sin) |^ (2 * n))) . x < (@ ((@ sin) |^ ((2 * n) -' 1))) . x & (@ ((@ sin) |^ ((2 * n) + 1))) . x < (@ ((@ sin) |^ (2 * n))) . x ) by A3, Th41, A1, A4; :: thesis: verum