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