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;
abs (tau_bar to_power n) = abs (tau_bar |^ n) by POWER:46;
then A1: abs (tau_bar to_power n) <= 1 by Lm14, Lm15;
A2: abs (tau_bar to_power n) >= 0 by COMPLEX1:132;
A3: 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 ;
sqrt 5 > 0 by Lm9, XXREAL_0:2;
then A4: (sqrt 5) " > 0 by XREAL_1:124;
then A5: abs ((sqrt 5) " ) = (sqrt 5) " by ABSVALUE:def 1;
1 / (sqrt 5) < 1 / 2 by Lm9, XREAL_1:90;
then 1 / (sqrt 5) < 1 by XXREAL_0:2;
then A6: abs ((sqrt 5) " ) < 1 by A5;
abs ((sqrt 5) " ) >= 0 by A4, ABSVALUE:def 1;
hence abs ((tau_bar to_power n) / (sqrt 5)) < 1 by A1, A2, A3, A6, XREAL_1:164; :: thesis: verum