let n be natural number ; :: thesis: ( n > 1 implies - (1 / 2) < tau_bar to_power n )
assume A0: n > 1 ; :: thesis: - (1 / 2) < tau_bar to_power n
ab: n - 0 is Element of NAT by NAT_1:21;
a1: n + 1 > 1 + 1 by A0, XREAL_1:10;

per cases ( n is even or not n is even ) ;

suppose n is even ; :: thesis: - (1 / 2) < tau_bar to_power n

then consider k being Element of NAT such that
d0: n = 2 * k by ab, ABIAN:def 2;
X: 0 ^2 = 0 ;
tau_bar to_power n = (tau_bar to_power k) to_power 2 by d0, NEWTON:14
.= (tau_bar to_power k) ^2 by POWER:53 ;
hence - (1 / 2) < tau_bar to_power n by X, SQUARE_1:74; :: thesis: verum

end;

suppose dd: not n is even ; :: thesis: - (1 / 2) < tau_bar to_power n

n >= 2 by a1, NAT_1:13;
then ( n = 2 or n > 2 ) by XXREAL_0:1;
then n + 1 > 2 + 1 by dd, POLYFORM:5, XREAL_1:8;
then n >= 3 by NAT_1:13;
then d0: tau_bar to_power n >= tau_bar to_power 3 by hopp9, POLYFORM:6;
sqrt 5 < sqrt ((5 / 2) ^2) by SQUARE_1:95;
then sqrt 5 < 5 / 2 by SQUARE_1:def 4;
then 2 * (sqrt 5) < 2 * (5 / 2) by XREAL_1:70;
then - (2 * (sqrt 5)) > - 5 by XREAL_1:26;
then (- (2 * (sqrt 5))) + 4 > (- 5) + 4 by XREAL_1:8;
then (2 * (2 - (sqrt 5))) / 2 > (- 1) / 2 by XREAL_1:76;
hence - (1 / 2) < tau_bar to_power n by d0, beta3, XXREAL_0:2; :: thesis: verum

end;

end;