let n be natural number ; :: thesis: ( n >= 2 implies Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/] )
assume A0: n >= 2 ; :: thesis: Fib n = [\((1 / tau) * ((Fib (n + 1)) + (1 / 2)))/]
then AA: n > 1 by XXREAL_0:2;
set tbn = tau_bar to_power n;
sqrt 5 < sqrt (5 ^2) by SQUARE_1:95;
then sqrt 5 < 5 by SQUARE_1:def 4;
then B4: (sqrt 5) - 5 < 5 - 5 by XREAL_1:11;
A1: (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 not n is even ) ;

suppose C2: 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 D1, AA, hop9;
then ((sqrt 5) / (((sqrt 5) - 5) * tau)) * (((sqrt 5) - 5) * tau) >= (tau_bar to_power n) * (((sqrt 5) - 5) * tau) by B4, XREAL_1:67;
then C0: sqrt 5 >= (tau_bar to_power n) * (((sqrt 5) - 5) * tau) by B4, XCMPLX_1:88;
C3: tau_bar to_power n > 0 by pom1, C2;
then (sqrt 5) / (tau_bar to_power n) >= ((tau * ((sqrt 5) - 5)) * (tau_bar to_power n)) / (tau_bar to_power n) by C0, XREAL_1:74;
then (sqrt 5) / (tau_bar to_power n) >= tau * ((sqrt 5) - 5) by C3, XCMPLX_1:90;
then ((sqrt 5) / (tau_bar to_power n)) / tau >= (((sqrt 5) - 5) * tau) / tau by XREAL_1:74;
then ((sqrt 5) / (tau_bar to_power n)) / tau >= (sqrt 5) - 5 by XCMPLX_1:90;
then (sqrt 5) / ((tau_bar to_power n) * tau) >= (sqrt 5) - 5 by XCMPLX_1:79;
then ((sqrt 5) / ((tau_bar to_power n) * tau)) + ((- (sqrt 5)) + 5) >= ((sqrt 5) - 5) + ((- (sqrt 5)) + 5) by XREAL_1:8;
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:8;
then ((- ((sqrt 5) / ((tau_bar to_power n) * tau))) + ((sqrt 5) - 3)) / 2 <= 2 / 2 by XREAL_1:74;
then (- (((sqrt 5) / ((tau_bar to_power n) * tau)) / 2)) + (tau_bar / tau) <= 1 by albet2;
then (- ((sqrt 5) / (((tau_bar to_power n) * tau) * 2))) + (tau_bar / tau) <= 1 by XCMPLX_1:79;
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 C3, XREAL_1:66;
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:75;
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 by POWER:30;
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 JakPower32;
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:79;
hence ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n by C3, XCMPLX_1:88; :: thesis: verum

end;

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

then C3: tau_bar to_power n < 0 by pom2;
(sqrt 5) / (tau * ((sqrt 5) - 5)) <= tau_bar to_power n by D1, AA, hop9;
then ((sqrt 5) / (tau * ((sqrt 5) - 5))) * ((sqrt 5) - 5) >= (tau_bar to_power n) * ((sqrt 5) - 5) by B4, XREAL_1:67;
then (((sqrt 5) / tau) / ((sqrt 5) - 5)) * ((sqrt 5) - 5) >= (tau_bar to_power n) * ((sqrt 5) - 5) by XCMPLX_1:79;
then (sqrt 5) / tau >= (tau_bar to_power n) * ((sqrt 5) - 5) by B4, XCMPLX_1:88;
then ((sqrt 5) / tau) / (tau_bar to_power n) <= ((tau_bar to_power n) * ((sqrt 5) - 5)) / (tau_bar to_power n) by C3, XREAL_1:75;
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:79;
then (sqrt 5) / (tau * (tau_bar to_power n)) <= (sqrt 5) - 5 by C3, XCMPLX_1:90;
then - ((sqrt 5) / (tau * (tau_bar to_power n))) >= - ((sqrt 5) - 5) by XREAL_1:26;
then (- ((sqrt 5) / (tau * (tau_bar to_power n)))) + ((sqrt 5) - 3) >= ((- (sqrt 5)) + 5) + ((sqrt 5) - 3) by XREAL_1:8;
then ((- ((sqrt 5) / (tau * (tau_bar to_power n)))) + ((sqrt 5) - 3)) / 2 >= 2 / 2 by XREAL_1:74;
then (tau_bar / tau) - (((sqrt 5) / (tau * (tau_bar to_power n))) / 2) >= 1 by albet2;
then (tau_bar / tau) - ((sqrt 5) / ((tau * (tau_bar to_power n)) * 2)) >= 1 by XCMPLX_1:79;
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 C3, XREAL_1:67;
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:79;
then ((tau_bar / tau) * (tau_bar to_power n)) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by C3, XCMPLX_1:88;
then ((tau_bar * (tau_bar to_power n)) / tau) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by XCMPLX_1:75;
then (((tau_bar to_power 1) * (tau_bar to_power n)) / tau) - ((sqrt 5) / (tau * 2)) <= tau_bar to_power n by POWER:30;
hence ((tau_bar to_power (n + 1)) / tau) - ((sqrt 5) / (2 * tau)) <= tau_bar to_power n by JakPower32; :: 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:26;
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:8;
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:121;
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:90;
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) by POWER:30;
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 JakPower32;
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 B2, XREAL_1:74;
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:63;
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:105;
then ((Fib (n + 1)) / tau) + ((1 / (2 * tau)) * 1) >= Fib n by B2, XCMPLX_1:60;
then ((Fib (n + 1)) / tau) + ((1 / 2) / tau) >= Fib n by XCMPLX_1:79;
then ((Fib (n + 1)) + (1 / 2)) / tau >= Fib n by XCMPLX_1:63;
hence (1 / tau) * ((Fib (n + 1)) + (1 / 2)) >= Fib n by XCMPLX_1:100; :: thesis: verum

end;

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

proof

1 < sqrt 5 by SQUARE_1:83, SQUARE_1:95;
then 1 / 2 < (sqrt 5) / 2 by XREAL_1:76;
then tau_bar to_power n < (sqrt 5) / 2 by hop8, A0, XXREAL_0:2;
then (tau_bar to_power n) * (sqrt 5) < (tau - (1 / 2)) * (sqrt 5) by B2, FIB_NUM:def 1, XREAL_1:70;
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) by POWER:30;
then ((tau_bar to_power n) * tau) - (tau_bar to_power (n + 1)) < (tau * (sqrt 5)) - ((sqrt 5) / 2) by JakPower32;
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:8;
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:11;
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:11;
then (((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) - (tau * (sqrt 5))) / tau < (- ((tau_bar to_power n) * tau)) / tau by XREAL_1:76;
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:125;
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:188;
then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - ((tau * (sqrt 5)) / tau) < - (tau_bar to_power n) by XCMPLX_1:90;
then ((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) - (sqrt 5) < - (tau_bar to_power n) by XCMPLX_1:90;
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:8;
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 B2, XREAL_1:76;
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:75;
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:121;
then ((((- ((tau_bar to_power (n + 1)) / tau)) + (((sqrt 5) / 2) / tau)) + (((tau to_power n) * tau) / tau)) / (sqrt 5)) - 1 < Fib n by B2, 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:188;
then (((((- (tau_bar to_power (n + 1))) + ((sqrt 5) / 2)) + ((tau to_power n) * tau)) / tau) / (sqrt 5)) - 1 < Fib n by XCMPLX_1:64;
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:100;
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:63;
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 by POWER:30;
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 JakPower32;
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 B2, XCMPLX_1:60; :: thesis: verum

end;

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