let n be Nat; :: thesis: (|.tau_bar.| to_power n) * (1 / (sqrt 5)) > 0
set b = tau_bar ;
sqrt 5 > 0 by SQUARE_1:25;
then ( |.tau_bar.| to_power n > 0 & 1 / (sqrt 5) > 0 ) by POWER:34;
hence (|.tau_bar.| to_power n) * (1 / (sqrt 5)) > 0 ; :: thesis: verum