let n be non zero Nat; for x being Real st 0 < x & x < PI / 2 holds
( (sin . x) |^ (2 * n) < (sin . x) |^ ((2 * n) -' 1) & (sin . x) |^ ((2 * n) + 1) < (sin . x) |^ (2 * n) )
let x be Real; ( 0 < x & x < PI / 2 implies ( (sin . x) |^ (2 * n) < (sin . x) |^ ((2 * n) -' 1) & (sin . x) |^ ((2 * n) + 1) < (sin . x) |^ (2 * n) ) )
assume
( 0 < x & x < PI / 2 )
; ( (sin . x) |^ (2 * n) < (sin . x) |^ ((2 * n) -' 1) & (sin . x) |^ ((2 * n) + 1) < (sin . x) |^ (2 * n) )
then A2:
( 0 < sin . x & sin . x < 1 )
by Th39;
0 < 0 + n
;
then
1 <= n
by NAT_1:19;
then
2 * n >= 2 * 1
by XREAL_1:64;
then
2 * n > 1
by XXREAL_0:2;
then A3:
(2 * n) -' 1 < 2 * n
by XREAL_1:237;
2 * n < (2 * n) + 1
by XREAL_1:39;
hence
( (sin . x) |^ (2 * n) < (sin . x) |^ ((2 * n) -' 1) & (sin . x) |^ ((2 * n) + 1) < (sin . x) |^ (2 * n) )
by A3, A2, Th40; verum