let n be natural number ; :: thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2
X: 2 < sqrt 5 by SQUARE_1:85, SQUARE_1:95;
then c2: 2 / 2 < (sqrt 5) / 2 by XREAL_1:76;
set b = tau_bar ;
a1: sqrt 5 <> 0 by SQUARE_1:82, SQUARE_1:95;
a4: sqrt 5 > 0 by SQUARE_1:93;

per cases ( n <> 0 or n = 0 ) ;

suppose K1: n <> 0 ; :: thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2

( abs tau_bar < 1 & abs tau_bar > 0 ) by hop3;
then (abs tau_bar) to_power n < 1 to_power n by K1, POWER:42;
then (abs tau_bar) to_power n < 1 by POWER:31;
then (abs tau_bar) to_power n < (sqrt 5) / 2 by c2, XXREAL_0:2;
then ((abs tau_bar) to_power n) / ((sqrt 5) / 1) < ((sqrt 5) / 2) / ((sqrt 5) / 1) by a4, XREAL_1:76;
then ((abs tau_bar) to_power n) / (sqrt 5) < (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:85;
then ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:100;
hence ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 by a1, XCMPLX_1:92; :: thesis: verum

end;

suppose n = 0 ; :: thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2

then (abs tau_bar) to_power n = 1 by POWER:29;
hence ((abs tau_bar) to_power n) * (1 / (sqrt 5)) < 1 / 2 by X, XREAL_1:78; :: thesis: verum

end;

end;