let n be Element of NAT ; :: thesis: |.((Fib n) - ((tau to_power n) / (sqrt 5))).| < 1
set k = Fib n;
set x = tau to_power n;
set y = tau_bar to_power n;
set z = sqrt 5;
Fib n = ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Th7
.= ((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) ;
then |.(- ((Fib n) - ((tau to_power n) / (sqrt 5)))).| < 1 by Lm16;
hence |.((Fib n) - ((tau to_power n) / (sqrt 5))).| < 1 by COMPLEX1:52; :: thesis: verum