let n be Nat; :: thesis: ( n <> 0 implies tau_bar to_power n < 1 / 2 )
assume n <> 0 ; :: thesis: tau_bar to_power n < 1 / 2
then n + 1 > 0 + 1 by XREAL_1:8;
then n + 1 >= 1 + 1 by NAT_1:13;
then A1: ( n + 1 = 2 or n >= 2 ) by NAT_1:8;
per cases ( n = 1 or n >= 2 ) by A1;
suppose n = 1 ; :: thesis: tau_bar to_power n < 1 / 2
hence tau_bar to_power n < 1 / 2 ; :: thesis: verum
end;
suppose n >= 2 ; :: thesis: tau_bar to_power n < 1 / 2
then ( n <> 0 & n <> 1 ) ;
then A2: n is non trivial Nat by NAT_2:def 1;
tau_bar to_power n < 1 / 2
proof
defpred S1[ Nat] means |.tau_bar.| to_power $1 < 1 / 2;
A3: |.tau_bar.| to_power 2 = (- tau_bar) to_power 2 by ABSVALUE:def 1
.= (- tau_bar) ^2 by POWER:46
.= (((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4 by FIB_NUM:def 2
.= ((1 - (2 * (sqrt 5))) + 5) / 4 by SQUARE_1:def 2
.= (3 - (sqrt 5)) / 2 ;
sqrt 5 > 2 by SQUARE_1:20, SQUARE_1:27;
then - (sqrt 5) < - 2 by XREAL_1:24;
then (- (sqrt 5)) + 3 < (- 2) + 3 by XREAL_1:8;
then A4: S1[2] by A3, XREAL_1:74;
A5: for k being non trivial Nat st S1[k] holds
S1[k + 1] A7: for n being non trivial Nat holds S1[n] from NAT_2:sch 2(A4, A5);
 for n being non trivial Nat holds tau_bar to_power n < 1 / 2 hence tau_bar to_power n < 1 / 2 by A2; :: thesis: verum
end;
hence tau_bar to_power n < 1 / 2 ; :: thesis: verum
end;
end;