let n be natural number ; :: thesis: ((abs tau_bar) to_power n) * (1 / (sqrt 5)) > 0
set b = tau_bar ;
sqrt 5 > 0 by SQUARE_1:93;
then ( (abs tau_bar) to_power n > 0 & 1 / (sqrt 5) > 0 ) by POWER:39;
hence ((abs tau_bar) to_power n) * (1 / (sqrt 5)) > 0 ; :: thesis: verum