let n be Nat; [\(((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:120
.=
(((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 Th17;
then A2:
(((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) + (Fib n) > 0 + (Fib n)
by XREAL_1:6;
((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1
by Th17;
then
(((tau_bar to_power n) / (sqrt 5)) + (1 / 2)) - (1 / 2) < 1 - (1 / 2)
by XREAL_1:9;
then
- ((tau_bar to_power n) / (sqrt 5)) > - (1 / 2)
by XREAL_1:24;
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:6;
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:120;
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 A2, A1, INT_1:def 6; verum