let n be natural number ; :: thesis: ( n <> 0 implies [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n )
set tn = tau to_power n;
set tbn = tau_bar to_power n;
assume A0: n <> 0 ; :: thesis: [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n
B0: sqrt 5 > 0 by SQUARE_1:93;
A1: ((tau to_power n) / (sqrt 5)) - (1 / 2) <= Fib n

proof

1 <= sqrt 5 by SQUARE_1:83, SQUARE_1:94;
then 1 / 2 <= (sqrt 5) / 2 by XREAL_1:74;
then tau_bar to_power n <= (sqrt 5) / 2 by A0, hop8, XXREAL_0:2;
then (tau_bar to_power n) / (sqrt 5) <= ((sqrt 5) / 2) / (sqrt 5) by B0, XREAL_1:74;
then (tau_bar to_power n) / (sqrt 5) <= ((sqrt 5) / (sqrt 5)) / 2 by XCMPLX_1:48;
then (tau_bar to_power n) / (sqrt 5) <= 1 / 2 by B0, XCMPLX_1:60;
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) >= ((tau to_power n) / (sqrt 5)) - (1 / 2) by XCMPLX_1:121;
hence ((tau to_power n) / (sqrt 5)) - (1 / 2) <= Fib n by FIB_NUM:7; :: thesis: verum

end;

(((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n

proof

n + 1 > 0 + 1 by A0, XREAL_1:8;
then pc: n >= 1 by NAT_1:13;

per cases ( n = 1 or n > 1 ) by pc, XXREAL_0:1;

suppose AA: n = 1 ; :: thesis: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n

then C1: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 = ((tau / (sqrt 5)) - (1 / 2)) + 1 by POWER:30
.= (((1 + (sqrt 5)) / 2) / (sqrt 5)) + (1 - (1 / 2)) by FIB_NUM:def 1
.= (((1 + (sqrt 5)) / (sqrt 5)) / 2) + (1 / 2) by XCMPLX_1:48
.= (((1 + (sqrt 5)) / (sqrt 5)) + 1) / 2
.= (((1 / (sqrt 5)) + ((sqrt 5) / (sqrt 5))) + 1) / 2 by XCMPLX_1:63
.= (((1 / (sqrt 5)) + 1) + 1) / 2 by B0, XCMPLX_1:60
.= ((1 / (sqrt 5)) / 2) + (2 / 2) ;
((1 / (sqrt 5)) / 2) + 1 > 0 + 1 by B0, XREAL_1:8;
hence (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n by AA, C1, PRE_FF:1; :: thesis: verum

end;

suppose AA: n > 1 ; :: thesis: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n

1 < sqrt 5 by SQUARE_1:83, SQUARE_1:95;
then 1 / 2 < (sqrt 5) / 2 by XREAL_1:76;
then B1: - (1 / 2) > - ((sqrt 5) / 2) by XREAL_1:26;
tau_bar to_power n > - (1 / 2) by AA, hop9;
then tau_bar to_power n > - ((sqrt 5) / 2) by B1, XXREAL_0:2;
then (tau_bar to_power n) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by B0, XREAL_1:76;
then (tau_bar to_power n) / (sqrt 5) > - (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:188;
then (tau_bar to_power n) / (sqrt 5) > - (((sqrt 5) / (sqrt 5)) / 2) by XCMPLX_1:48;
then (tau_bar to_power n) / (sqrt 5) > - (1 / 2) by B0, XCMPLX_1:60;
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;
hence (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n by FIB_NUM:7; :: thesis: verum

end;

end;

end;

hence [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n by A1, INT_1:def 5; :: thesis: verum