let n be natural number ; :: 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:121 ;
T1: sqrt 5 > 0 by SQUARE_1:82, SQUARE_1:95;
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 pomoc2 ;
(- tau_bar ) to_power ((2 * n) + 1) > 0 by POWER:39;
hence tau_bar to_power ((2 * n) + 1) < 0 by a3; :: thesis: verum

end;

then S1: (tau to_power ((2 * n) + 1)) / (sqrt 5) <= Fib ((2 * n) + 1) by A1, XREAL_1:48, T1;
((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) + (1 / 2) > 0 by Lemat11;
then S2: (((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) + (1 / 2)) - (1 / 2) > 0 - (1 / 2) by XREAL_1:11;
(tau_bar to_power ((2 * n) + 1)) / (sqrt 5) > - 1 by S2, XXREAL_0:2;
then - ((tau_bar to_power ((2 * n) + 1)) / (sqrt 5)) < - (- 1) by XREAL_1:26;
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:10;
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:121;
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 S1, INT_1:def 5; :: thesis: verum