let n be natural number ; :: thesis: ( n >= 2 & not n is even implies Fib (n + 1) = [/((tau * (Fib n)) - 1)\] )
assume A0: ( n >= 2 & not n is even ) ; :: thesis: Fib (n + 1) = [/((tau * (Fib n)) - 1)\]
B1: sqrt 5 > 0 by SQUARE_1:82, SQUARE_1:95;
(tau * (tau_bar to_power n)) + (sqrt 5) >= tau_bar to_power (n + 1)

proof

set tbn = tau_bar to_power n;
dd: tau_bar to_power n < 0 by A0, pom2;
tau + ((sqrt 5) / (tau_bar to_power n)) <= tau_bar

proof

n > 1 by A0, XXREAL_0:2;
then tau_bar to_power n >= - (1 / 2) by hop9;
then tau_bar to_power n > - 1 by XXREAL_0:2;
then (tau_bar to_power n) + 1 >= (- 1) + 1 by XREAL_1:8;
then ((tau_bar to_power n) + 1) / (tau_bar to_power n) <= 0 / (tau_bar to_power n) by dd;
then ((tau_bar to_power n) / (tau_bar to_power n)) + (1 / (tau_bar to_power n)) <= 0 by XCMPLX_1:63;
then 1 + (1 / (tau_bar to_power n)) <= 0 by dd, XCMPLX_1:60;
then (1 + (1 / (tau_bar to_power n))) * (sqrt 5) <= 0 * (sqrt 5) by B1;
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:75;
then ((((sqrt 5) / 2) + ((sqrt 5) / (tau_bar to_power n))) + ((sqrt 5) / 2)) - ((sqrt 5) / 2) <= 0 - ((sqrt 5) / 2) by XREAL_1:11;
then (((sqrt 5) / 2) + ((sqrt 5) / (tau_bar to_power n))) + (1 / 2) <= (- ((sqrt 5) / 2)) + (1 / 2) by XREAL_1:8;
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 dd, XREAL_1:67;
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:30;
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 JakPower32;
hence (tau * (tau_bar to_power n)) + (sqrt 5) >= tau_bar to_power (n + 1) by dd, XCMPLX_1:88; :: thesis: verum

end;

then - ((tau * (tau_bar to_power n)) + (sqrt 5)) <= - (tau_bar to_power (n + 1)) by XREAL_1:26;
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:8;
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:32;
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:30;
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 B1, XREAL_1:74;
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:121;
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:75;
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 B1, 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 A1: (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;
c1: 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:75 ;
c3: tau_bar to_power n < 0 by pom2, A0;
tau > tau_bar to_power 1 by POWER:30;
then tau * (tau_bar to_power n) < (tau_bar to_power 1) * (tau_bar to_power n) by c3, XREAL_1:71;
then tau * (tau_bar to_power n) < tau_bar to_power (n + 1) by JakPower32;
then - (tau * (tau_bar to_power n)) > - (tau_bar to_power (n + 1)) by XREAL_1:26;
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:8;
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 JakPower32;
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:30;
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 B1, XREAL_1:76;
hence ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) by c1, FIB_NUM:7; :: thesis: verum

end;

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