let n be Nat; :: thesis: ( n >= 2 implies Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/] )
assume A1: n >= 2 ; :: thesis: Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/]
then A2: n > 1 by XXREAL_0:2;
set tbn = tau_bar to_power n;
sqrt 5 < sqrt (5 ^2) by SQUARE_1:27;
then sqrt 5 < 5 by SQUARE_1:def 2;
then A3: (sqrt 5) - 5 < 5 - 5 by XREAL_1:9;
A4: (1 / tau) * ((Fib (n + 1)) + (1 / 2)) >= Fib n

proof

set tbm = tau_bar to_power (n + 1);
set tn = tau to_power n;
((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n

proof

per cases ( n is even or n is odd ) ;

suppose A5: n is even ; :: thesis: ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n

(sqrt 5) / (((sqrt 5) - 5) * tau) <= tau_bar to_power n by Lm21, A2, Th14;
then ((sqrt 5) / (((sqrt 5) - 5) * tau)) * (((sqrt 5) - 5) * tau) >= (tau_bar to_power n) * (((sqrt 5) - 5) * tau) by A3, XREAL_1:65;
then A6: sqrt 5 >= (tau_bar to_power n) * (((sqrt 5) - 5) * tau) by A3, XCMPLX_1:87;
A7: tau_bar to_power n > 0 by Th6, A5;
then (sqrt 5) / (tau_bar to_power n) >= ((tau * ((sqrt 5) - 5)) * (tau_bar to_power n)) / (tau_bar to_power n) by A6, XREAL_1:72;
then (sqrt 5) / (tau_bar to_power n) >= tau * ((sqrt 5) - 5) by A7, XCMPLX_1:89;
then ((sqrt 5) / (tau_bar to_power n)) / tau >= (((sqrt 5) - 5) * tau) / tau by XREAL_1:72;
then ((sqrt 5) / (tau_bar to_power n)) / tau >= (sqrt 5) - 5 by XCMPLX_1:89;
then (sqrt 5) / ((tau_bar to_power n) * tau) >= (sqrt 5) - 5 by XCMPLX_1:78;
then ((sqrt 5) / ((tau_bar to_power n) * tau)) + ((- (sqrt 5)) + 5) >= ((sqrt 5) - 5) + ((- (sqrt 5)) + 5) by XREAL_1:6;
then - ((((sqrt 5) / ((tau_bar to_power n) * tau)) - (sqrt 5)) + 5) <= 0 ;
then (((- ((sqrt 5) / ((tau_bar to_power n) * tau))) + (sqrt 5)) - 5) + 2 <= 0 + 2 by XREAL_1:6;
then ((- ((sqrt 5) / ((tau_bar to_power n) * tau))) + ((sqrt 5) - 3)) / 2 <= 2 / 2 by XREAL_1:72;
then (- (((sqrt 5) / ((tau_bar to_power n) * tau)) / 2)) + (tau_bar / tau) <= 1 by Lm4;
then (- ((sqrt 5) / (((tau_bar to_power n) * tau) * 2))) + (tau_bar / tau) <= 1 by XCMPLX_1:78;
then ((tau_bar / tau) - ((sqrt 5) / ((2 * (tau_bar to_power n)) * tau))) * (tau_bar to_power n) <= 1 * (tau_bar to_power n) by A7, XREAL_1:64;
then ((tau_bar / tau) * (tau_bar to_power n)) - (((sqrt 5) / ((2 * (tau_bar to_power n)) * tau)) * (tau_bar to_power n)) <= tau_bar to_power n ;
then ((tau_bar * (tau_bar to_power n)) / tau) - (((sqrt 5) / ((2 * (tau_bar to_power n)) * tau)) * (tau_bar to_power n)) <= tau_bar to_power n by XCMPLX_1:74;
then (((tau_bar to_power 1) * (tau_bar to_power n)) / tau) - (((sqrt 5) / ((2 * (tau_bar to_power n)) * tau)) * (tau_bar to_power n)) <= tau_bar to_power n ;
then ((tau_bar to_power (n + 1)) / tau) - (((sqrt 5) / ((2 * tau) * (tau_bar to_power n))) * (tau_bar to_power n)) <= tau_bar to_power n by Th2;
then ((tau_bar to_power (n + 1)) / tau) - ((((sqrt 5) / (2 * tau)) / (tau_bar to_power n)) * (tau_bar to_power n)) <= tau_bar to_power n by XCMPLX_1:78;
hence ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n by A7, XCMPLX_1:87; :: thesis: verum

end;

suppose n is odd ; :: thesis: ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n

then A8: tau_bar to_power n < 0 by Th7;
(sqrt 5) / (tau * ((sqrt 5) - 5)) <= tau_bar to_power n by Lm21, A2, Th14;
then ((sqrt 5) / (tau * ((sqrt 5) - 5))) * ((sqrt 5) - 5) >= (tau_bar to_power n) * ((sqrt 5) - 5) by A3, XREAL_1:65;
then (((sqrt 5) / tau) / ((sqrt 5) - 5)) * ((sqrt 5) - 5) >= (tau_bar to_power n) * ((sqrt 5) - 5) by XCMPLX_1:78;
then (sqrt 5) / tau >= (tau_bar to_power n) * ((sqrt 5) - 5) by A3, XCMPLX_1:87;
then ((sqrt 5) / tau) / (tau_bar to_power n) <= ((tau_bar to_power n) * ((sqrt 5) - 5)) / (tau_bar to_power n) by A8, XREAL_1:73;
then (sqrt 5) / (tau * (tau_bar to_power n)) <= ((tau_bar to_power n) * ((sqrt 5) - 5)) / (tau_bar to_power n) by XCMPLX_1:78;
then (sqrt 5) / (tau * (tau_bar to_power n)) <= (sqrt 5) - 5 by A8, XCMPLX_1:89;
then - ((sqrt 5) / (tau * (tau_bar to_power n))) >= - ((sqrt 5) - 5) by XREAL_1:24;
then (- ((sqrt 5) / (tau * (tau_bar to_power n)))) + ((sqrt 5) - 3) >= ((- (sqrt 5)) + 5) + ((sqrt 5) - 3) by XREAL_1:6;
then ((- ((sqrt 5) / (tau * (tau_bar to_power n)))) + ((sqrt 5) - 3)) / 2 >= 2 / 2 by XREAL_1:72;
then (tau_bar / tau) - (((sqrt 5) / (tau * (tau_bar to_power n))) / 2) >= 1 by Lm4;
then (tau_bar / tau) - ((sqrt 5) / ((tau * (tau_bar to_power n)) * 2)) >= 1 by XCMPLX_1:78;
then ((tau_bar / tau) - ((sqrt 5) / ((tau * (tau_bar to_power n)) * 2))) * (tau_bar to_power n) <= 1 * (tau_bar to_power n) by A8, XREAL_1:65;
then ((tau_bar / tau) * (tau_bar to_power n)) - (((sqrt 5) / ((tau * 2) * (tau_bar to_power n))) * (tau_bar to_power n)) <= tau_bar to_power n ;
then ((tau_bar / tau) * (tau_bar to_power n)) - ((((sqrt 5) / (tau * 2)) / (tau_bar to_power n)) * (tau_bar to_power n)) <= tau_bar to_power n by XCMPLX_1:78;
then ((tau_bar / tau) * (tau_bar to_power n)) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by A8, XCMPLX_1:87;
then ((tau_bar * (tau_bar to_power n)) / tau) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by XCMPLX_1:74;
then (((tau_bar to_power 1) * (tau_bar to_power n)) / tau) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n ;
hence ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n by Th2; :: thesis: verum

end;

end;

end;

then - (((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau))) >= - (tau_bar to_power n) by XREAL_1:24;
then ((- ((tau_bar to_power (n + 1)) / tau)) + ((sqrt 5) / (2 * tau))) + (((tau to_power n) * tau) / tau) >= (- (tau_bar to_power n)) + (((tau to_power n) * tau) / tau) by XREAL_1:6;
then ((((tau to_power n) * tau) / tau) - ((tau_bar to_power (n + 1)) / tau)) + ((sqrt 5) / (2 * tau)) >= (- (tau_bar to_power n)) + (((tau to_power n) * tau) / tau) ;
then ((((tau to_power n) * tau) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (- (tau_bar to_power n)) + (((tau to_power n) * tau) / tau) by XCMPLX_1:120;
then ((((tau to_power n) * tau) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (- (tau_bar to_power n)) + (tau to_power n) by XCMPLX_1:89;
then ((((tau to_power n) * (tau to_power 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (tau to_power n) - (tau_bar to_power n) ;
then (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau)) >= (tau to_power n) - (tau_bar to_power n) by Th2;
then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau))) / (sqrt 5) >= ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Lm20, XREAL_1:72;
then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) + ((sqrt 5) / (2 * tau))) / (sqrt 5) >= Fib n by FIB_NUM:7;
then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / tau) / (sqrt 5)) + (((sqrt 5) / (2 * tau)) / (sqrt 5)) >= Fib n by XCMPLX_1:62;
then ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) / tau) + (((sqrt 5) / (2 * tau)) / (sqrt 5)) >= Fib n by XCMPLX_1:48;
then ((Fib (n + 1)) / tau) + (((sqrt 5) / (2 * tau)) / (sqrt 5)) >= Fib n by FIB_NUM:7;
then ((Fib (n + 1)) / tau) + ((1 / (2 * tau)) * ((sqrt 5) / (sqrt 5))) >= Fib n by XCMPLX_1:104;
then ((Fib (n + 1)) / tau) + ((1 / (2 * tau)) * 1) >= Fib n by Lm20, XCMPLX_1:60;
then ((Fib (n + 1)) / tau) + ((1 / 2) / tau) >= Fib n by XCMPLX_1:78;
then ((Fib (n + 1)) + (1 / 2)) / tau >= Fib n by XCMPLX_1:62;
hence (1 / tau) * ((Fib (n + 1)) + (1 / 2)) >= Fib n by XCMPLX_1:99; :: thesis: verum

end;

((1 / tau) * ((Fib (n + 1)) + (1 / 2))) - 1 < Fib n

proof

1 < sqrt 5 by SQUARE_1:18, SQUARE_1:27;
then 1 / 2 < (sqrt 5) / 2 by XREAL_1:74;
then tau_bar to_power n < (sqrt 5) / 2 by Th8, A1, XXREAL_0:2;
then (tau_bar to_power n) * (sqrt 5) < (tau - (1 / 2)) * (sqrt 5) by Lm20, FIB_NUM:def 1, XREAL_1:68;
then ((tau_bar to_power n) * tau) - ((tau_bar to_power n) * tau_bar) < (tau * (sqrt 5)) - ((1 * (sqrt 5)) / 2) by FIB_NUM:def 1, FIB_NUM:def 2;
then ((tau_bar to_power n) * tau) - ((tau_bar to_power n) * (tau_bar to_power 1)) < (tau * (sqrt 5)) - ((sqrt 5) / 2) ;
then ((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1)) < (tau * (sqrt 5)) - ((sqrt 5) / 2) by Th2;
then (((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1))) + ((sqrt 5) / 2) < ((tau * (sqrt 5)) - ((sqrt 5) / 2)) + ((sqrt 5) / 2) by XREAL_1:6;
then ((((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - ((tau_bar to_power n) * tau) < (tau * (sqrt 5)) - ((tau_bar to_power n) * tau) by XREAL_1:9;
then ((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - (tau * (sqrt 5)) < ((tau * (sqrt 5)) - ((tau_bar to_power n) * tau)) - (tau * (sqrt 5)) by XREAL_1:9;
then (((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - (tau * (sqrt 5))) / tau < (- ((tau_bar to_power n) * tau)) / tau by XREAL_1:74;
then (((- (tau_bar to_power (n + 1))) / tau) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < (- ((tau_bar to_power n) * tau)) / tau by XCMPLX_1:124;
then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < ((- (tau_bar to_power n)) * tau) / tau by XCMPLX_1:187;
then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < - (tau_bar to_power n) by XCMPLX_1:89;
then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5) < - (tau_bar to_power n) by XCMPLX_1:89;
then (((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * 1) < (- (tau_bar to_power n)) + (tau to_power n) by XREAL_1:6;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * 1)) / (sqrt 5) < ((tau to_power n) - (tau_bar to_power n)) / (sqrt 5) by Lm20, XREAL_1:74;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * 1)) / (sqrt 5) < Fib n by FIB_NUM:7;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5)) + ((tau to_power n) * (tau / tau))) / (sqrt 5) < Fib n by XCMPLX_1:60;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + ((tau to_power n) * (tau / tau))) - (sqrt 5)) / (sqrt 5) < Fib n ;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) - (sqrt 5)) / (sqrt 5) < Fib n by XCMPLX_1:74;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - ((sqrt 5) / (sqrt 5)) < Fib n by XCMPLX_1:120;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - 1 < Fib n by Lm20, XCMPLX_1:60;
then (((((- (tau_bar to_power (n + 1))) / tau) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - 1 < Fib n by XCMPLX_1:187;
then (((((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) + ((tau to_power n) * tau)) / tau) / (sqrt 5)) - 1 < Fib n by XCMPLX_1:63;
then (((((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) + ((tau to_power n) * tau)) / (sqrt 5)) / tau) - 1 < Fib n by XCMPLX_1:48;
then (((((- (tau_bar to_power (n + 1))) + ((tau to_power n) * tau)) + ((sqrt 5) / 2)) / (sqrt 5)) * (1 / tau)) - 1 < Fib n by XCMPLX_1:99;
then (((((- (tau_bar to_power (n + 1))) + ((tau to_power n) * tau)) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by XCMPLX_1:62;
then (((((- (tau_bar to_power (n + 1))) + ((tau to_power n) * (tau to_power 1))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n ;
then (((((- (tau_bar to_power (n + 1))) + (tau to_power (n + 1))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by Th2;
then (((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n ;
then (((Fib (n + 1)) + (((sqrt 5) / 2) / (sqrt 5))) * (1 / tau)) - 1 < Fib n by FIB_NUM:7;
then (((Fib (n + 1)) + (((sqrt 5) / (sqrt 5)) / 2)) * (1 / tau)) - 1 < Fib n by XCMPLX_1:48;
hence ((1 / tau) * ((Fib (n + 1)) + (1 / 2))) - 1 < Fib n by Lm20, XCMPLX_1:60; :: thesis: verum

end;

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