let n be Nat; :: thesis: ( n >= 2 & n is odd implies Fib (n + 1) = [/((tau * (Fib n)) - 1)\] )
assume A1: ( n >= 2 & n is odd ) ; :: thesis: Fib (n + 1) = [/((tau * (Fib n)) - 1)\]
A2: sqrt 5 > 0 by SQUARE_1:17, SQUARE_1:27;
(tau * (tau_bar to_power n)) + (sqrt 5) >= tau_bar to_power (n + 1)

proof

set tbn = tau_bar to_power n;
A3: tau_bar to_power n < 0 by A1, Th7;
tau + ((sqrt 5) / (tau_bar to_power n)) <= tau_bar

proof

n > 1 by A1, XXREAL_0:2;
then tau_bar to_power n >= - (1 / 2) by Th14;
then tau_bar to_power n > - 1 by XXREAL_0:2;
then (tau_bar to_power n) + 1 >= (- 1) + 1 by XREAL_1:6;
then ((tau_bar to_power n) + 1) / (tau_bar to_power n) <= 0 / (tau_bar to_power n) by A3;
then ((tau_bar to_power n) / (tau_bar to_power n)) + (1 / (tau_bar to_power n)) <= 0 by XCMPLX_1:62;
then 1 + (1 / (tau_bar to_power n)) <= 0 by A3, XCMPLX_1:60;
then (1 + (1 / (tau_bar to_power n))) * (sqrt 5) <= 0 * (sqrt 5) by A2;
then (1 * (sqrt 5)) + ((1 / (tau_bar to_power n)) * (sqrt 5)) <= 0 ;
then (sqrt 5) + ((sqrt 5) / (tau_bar to_power n)) <= 0 by XCMPLX_1:74;
then ((((sqrt 5) / 2) + ((sqrt 5) / (tau_bar to_power n))) + ((sqrt 5) / 2)) - ((sqrt 5) / 2) <= 0 - ((sqrt 5) / 2) by XREAL_1:9;
then (((sqrt 5) / 2) + ((sqrt 5) / (tau_bar to_power n))) + (1 / 2) <= (- ((sqrt 5) / 2)) + (1 / 2) by XREAL_1:6;
hence tau + ((sqrt 5) / (tau_bar to_power n)) <= tau_bar by FIB_NUM:def 1, FIB_NUM:def 2; :: thesis: verum

end;

then (tau + ((sqrt 5) / (tau_bar to_power n))) * (tau_bar to_power n) >= tau_bar * (tau_bar to_power n) by A3, XREAL_1:65;
then (tau + ((sqrt 5) / (tau_bar to_power n))) * (tau_bar to_power n) >= (tau_bar to_power 1) * (tau_bar to_power n) by POWER:25;
then (tau * (tau_bar to_power n)) + (((sqrt 5) / (tau_bar to_power n)) * (tau_bar to_power n)) >= tau_bar to_power (n + 1) by Th2;
hence (tau * (tau_bar to_power n)) + (sqrt 5) >= tau_bar to_power (n + 1) by A3, XCMPLX_1:87; :: thesis: verum

end;

then - ((tau * (tau_bar to_power n)) + (sqrt 5)) <= - (tau_bar to_power (n + 1)) by XREAL_1:24;
then ((- (tau * (tau_bar to_power n))) - (sqrt 5)) + (tau to_power (n + 1)) <= (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) by XREAL_1:6;
then ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) - (sqrt 5) <= (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) ;
then (((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n))) - (sqrt 5) <= (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by POWER:27;
then ((tau * (tau to_power n)) - (tau * (tau_bar to_power n))) - (sqrt 5) <= (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by POWER:25;
then ((tau * ((tau to_power n) - (tau_bar to_power n))) - (sqrt 5)) / (sqrt 5) <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by A2, XREAL_1:72;
then ((tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5)) - ((sqrt 5) / (sqrt 5)) <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by XCMPLX_1:120;
then (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) - ((sqrt 5) / (sqrt 5)) <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by XCMPLX_1:74;
then (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) - 1 <= ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by A2, XCMPLX_1:60;
then (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) - 1 <= Fib (n + 1) by FIB_NUM:7;
then A4: (tau * (Fib n)) - 1 <= Fib (n + 1) by FIB_NUM:7;
((tau * (Fib n)) - 1) + 1 > Fib (n + 1)

proof

set tn = tau to_power n;
set tbn = tau_bar to_power n;
A5: tau * (Fib n) = tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7
.= (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74 ;
A6: tau_bar to_power n < 0 by Th7, A1;
tau > tau_bar to_power 1 by POWER:25;
then tau * (tau_bar to_power n) < (tau_bar to_power 1) * (tau_bar to_power n) by A6, XREAL_1:69;
then tau * (tau_bar to_power n) < tau_bar to_power (n + 1) by Th2;
then - (tau * (tau_bar to_power n)) > - (tau_bar to_power (n + 1)) by XREAL_1:24;
then (- (tau * (tau_bar to_power n))) + (tau to_power (n + 1)) > (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) by XREAL_1:6;
then (tau to_power (n + 1)) - (tau * (tau_bar to_power n)) > (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) ;
then ((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n)) > (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by Th2;
then (tau * (tau to_power n)) - (tau * (tau_bar to_power n)) > (tau to_power (n + 1)) - (tau_bar to_power (n + 1)) by POWER:25;
then (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) > ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by A2, XREAL_1:74;
hence ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) by A5, FIB_NUM:7; :: thesis: verum

end;

hence Fib (n + 1) = [/((tau * (Fib n)) - 1)\] by A4, INT_1:def 7; :: thesis: verum