let n be Element of NAT ; :: thesis: abs ((tau_bar to_power n) / (sqrt 5)) < 1
set y = tau_bar to_power n;
set z = sqrt 5;
A1: abs (tau_bar to_power n) = abs (tau_bar |^ n) by POWER:46;
A2: abs ((tau_bar to_power n) / (sqrt 5)) = abs ((tau_bar to_power n) * ((sqrt 5) " ))
.= (abs (tau_bar to_power n)) * (abs ((sqrt 5) " )) by COMPLEX1:151 ;
A3: 1 / (sqrt 5) < 1 / 2 by Lm9, XREAL_1:90;
sqrt 5 > 0 by Lm9, XXREAL_0:2;
then A4: (sqrt 5) " > 0 by XREAL_1:124;
then abs ((sqrt 5) " ) = (sqrt 5) " by ABSVALUE:def 1;
then A5: abs ((sqrt 5) " ) < 1 by A3, XXREAL_0:2;
abs ((sqrt 5) " ) >= 0 by A4, ABSVALUE:def 1;
hence abs ((tau_bar to_power n) / (sqrt 5)) < 1 by A1, A2, A5, Lm14, Lm15, XREAL_1:164; :: thesis: verum