let n be Nat; :: thesis: ( n > 1 implies - (1 / 2) < tau_bar to_power n )
assume A1: n > 1 ; :: thesis: - (1 / 2) < tau_bar to_power n
A2: n + 1 > 1 + 1 by A1, XREAL_1:8;
per cases ( n is even or n is odd ) ;
suppose n is even ; :: thesis: - (1 / 2) < tau_bar to_power n
then consider k being Nat such that
A3: n = 2 * k by ABIAN:def 2;
A4: 0 ^2 = 0 ;
tau_bar to_power n = (tau_bar to_power k) to_power 2 by A3, NEWTON:9
.= (tau_bar to_power k) ^2 by POWER:46 ;
hence - (1 / 2) < tau_bar to_power n by A4, SQUARE_1:12; :: thesis: verum
end;
suppose A5: n is odd ; :: thesis: - (1 / 2) < tau_bar to_power n
n >= 2 by A2, NAT_1:13;
then ( n = 2 or n > 2 ) by XXREAL_0:1;
then n + 1 > 2 + 1 by A5, POLYFORM:5, XREAL_1:6;
then n >= 3 by NAT_1:13;
then A6: tau_bar to_power n >= tau_bar to_power 3 by Th10, POLYFORM:6;
sqrt 5 < sqrt ((5 / 2) ^2) by SQUARE_1:27;
then sqrt 5 < 5 / 2 by SQUARE_1:def 2;
then 2 * (sqrt 5) < 2 * (5 / 2) by XREAL_1:68;
then - (2 * (sqrt 5)) > - 5 by XREAL_1:24;
then (- (2 * (sqrt 5))) + 4 > (- 5) + 4 by XREAL_1:6;
then (2 * (2 - (sqrt 5))) / 2 > (- 1) / 2 by XREAL_1:74;
hence - (1 / 2) < tau_bar to_power n by A6, Lm8, XXREAL_0:2; :: thesis: verum
end;
end;