let n be Nat; :: 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 A1: n <> 0 ; :: thesis: [/(((tau to_power n) / (sqrt 5)) - (1 / 2))\] = Fib n
A2: sqrt 5 > 0 by SQUARE_1:25;
A3: ((tau to_power n) / (sqrt 5)) - (1 / 2) <= Fib n

proof

1 <= sqrt 5 by SQUARE_1:18, SQUARE_1:26;
then 1 / 2 <= (sqrt 5) / 2 by XREAL_1:72;
then tau_bar to_power n <= (sqrt 5) / 2 by A1, Th8, XXREAL_0:2;
then (tau_bar to_power n) / (sqrt 5) <= ((sqrt 5) / 2) / (sqrt 5) by A2, XREAL_1:72;
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 A2, XCMPLX_1:60;
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) >= ((tau to_power n) / (sqrt 5)) - (1 / 2) by XCMPLX_1:120;
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 A1, XREAL_1:6;
then A4: n >= 1 by NAT_1:13;

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

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

then A6: (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 = ((tau / (sqrt 5)) - (1 / 2)) + 1
.= (((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:62
.= (((1 / (sqrt 5)) + 1) + 1) / 2 by A2, XCMPLX_1:60
.= ((1 / (sqrt 5)) / 2) + (2 / 2) ;
((1 / (sqrt 5)) / 2) + 1 > 0 + 1 by A2, XREAL_1:6;
hence (((tau to_power n) / (sqrt 5)) - (1 / 2)) + 1 > Fib n by A5, A6, PRE_FF:1; :: thesis: verum

end;

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

1 < sqrt 5 by SQUARE_1:18, SQUARE_1:27;
then 1 / 2 < (sqrt 5) / 2 by XREAL_1:74;
then A8: - (1 / 2) > - ((sqrt 5) / 2) by XREAL_1:24;
tau_bar to_power n > - (1 / 2) by A7, Th14;
then tau_bar to_power n > - ((sqrt 5) / 2) by A8, XXREAL_0:2;
then (tau_bar to_power n) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by A2, XREAL_1:74;
then (tau_bar to_power n) / (sqrt 5) > - (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:187;
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 A2, XCMPLX_1:60;
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;
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 A3, INT_1:def 7; :: thesis: verum