let n be natural number ; [\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n
set tn = tau_bar to_power n;
a1: Fib n =
((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) + (1 / 2)) - (1 / 2)
by FIB_NUM:7
.=
((((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5))) + (1 / 2)) - (1 / 2)
by XCMPLX_1:121
.=
(((tau to_power n) / (sqrt 5)) + (1 / 2)) - (((tau_bar to_power n) / (sqrt 5)) + (1 / 2))
;
((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0
by Lemat11;
then a3:
(((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) + (Fib n) > 0 + (Fib n)
by XREAL_1:8;
((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1
by Lemat11;
then
(((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) - (1 / 2) < 1 - (1 / 2)
by XREAL_1:11;
then
- ((tau_bar to_power n) / (sqrt 5)) > - (1 / 2)
by XREAL_1:26;
then
(- ((tau_bar to_power n) / (sqrt 5))) + ((tau to_power n) / (sqrt 5)) > (- (1 / 2)) + ((tau to_power n) / (sqrt 5))
by XREAL_1:8;
then
((tau to_power n) / (sqrt 5)) - ((tau_bar to_power n) / (sqrt 5)) > (- (1 / 2)) + ((tau to_power n) / (sqrt 5))
;
then
((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) > (- (1 / 2)) + ((tau to_power n) / (sqrt 5))
by XCMPLX_1:121;
then
Fib n > (((tau to_power n) / (sqrt 5)) + (1 / 2)) - 1
by FIB_NUM:7;
hence
[\(((tau to_power n) / (sqrt 5)) + (1 / 2))/] = Fib n
by a3, a1, INT_1:def 4; verum