let n be Nat; :: thesis: [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1)
A1: Fib ((2 * n) + 1) = ((tau to_power ((2 * n) + 1)) - (tau_bar to_power ((2 * n) + 1))) / (sqrt 5) by FIB_NUM:7
.= ((tau to_power ((2 * n) + 1)) / (sqrt 5)) - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) by XCMPLX_1:120 ;
A2: sqrt 5 > 0 by SQUARE_1:17, SQUARE_1:27;
tau_bar to_power ((2 * n) + 1) < 0

proof

set t = - tau_bar;
A3: tau_bar to_power ((2 * n) + 1) = (- (- tau_bar)) to_power ((2 * n) + 1)
.= - ((- tau_bar) to_power ((2 * n) + 1)) by Th4 ;
(- tau_bar) to_power ((2 * n) + 1) > 0 by POWER:34;
hence tau_bar to_power ((2 * n) + 1) < 0 by A3; :: thesis: verum

end;

then A4: (tau to_power ((2 * n) + 1)) / (sqrt 5) <= Fib ((2 * n) + 1) by A1, A2, XREAL_1:46;
((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) + (1 / 2) > 0 by Th17;
then (((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) + (1 / 2)) - (1 / 2) > 0 - (1 / 2) by XREAL_1:9;
then (tau_bar to_power ((2 * n) + 1)) / (sqrt 5) > - 1 by XXREAL_0:2;
then - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) < - (- 1) by XREAL_1:24;
then (- ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5))) + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) < 1 + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) by XREAL_1:8;
then ((tau to_power ((2 * n) + 1)) / (sqrt 5)) - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) < 1 + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) ;
then ((tau to_power ((2 * n) + 1)) - (tau_bar to_power ((2 * n) + 1))) / (sqrt 5) < 1 + ((tau to_power ((2 * n) + 1)) / (sqrt 5)) by XCMPLX_1:120;
then Fib ((2 * n) + 1) < ((tau to_power ((2 * n) + 1)) / (sqrt 5)) + 1 by FIB_NUM:7;
hence [/((tau to_power ((2 * n) + 1)) / (sqrt 5))\] = Fib ((2 * n) + 1) by A4, INT_1:def 7; :: thesis: verum