let n be natural number ; :: thesis: ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] )
assume A0: n >= 2 ; :: thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]
CC: sqrt 5 > 0 by SQUARE_1:93;
set tn = tau to_power n;
set tb = tau_bar ;
set s5 = sqrt 5;
set tbn = tau_bar to_power n;

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

suppose ST1: n is even ; :: thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]

then C1: tau_bar to_power n > 0 by pom1;
B1: (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1)

proof

tau_bar to_power n <= 1 / 2 by hop8, A0;
then 2 * (tau_bar to_power n) <= 2 * (1 / 2) by XREAL_1:66;
then (2 * (tau_bar to_power n)) / (tau_bar to_power n) <= 1 / (tau_bar to_power n) by C1, XREAL_1:74;
then 2 <= 1 / (tau_bar to_power n) by C1, XCMPLX_1:90;
then 2 * (sqrt 5) <= (1 / (tau_bar to_power n)) * (sqrt 5) by CC, XREAL_1:66;
then (sqrt 5) + (sqrt 5) <= (1 * (sqrt 5)) / (tau_bar to_power n) by XCMPLX_1:75;
then ((sqrt 5) + (sqrt 5)) - (sqrt 5) <= ((1 * (sqrt 5)) / (tau_bar to_power n)) - (sqrt 5) by XREAL_1:11;
then - (sqrt 5) >= - (((sqrt 5) / (tau_bar to_power n)) - (sqrt 5)) by XREAL_1:26;
then (- (sqrt 5)) + 1 >= ((- ((sqrt 5) / (tau_bar to_power n))) + (sqrt 5)) + 1 by XREAL_1:8;
then tau_bar >= (((sqrt 5) + 1) - ((sqrt 5) / (tau_bar to_power n))) / 2 by FIB_NUM:def 2, XREAL_1:74;
then tau_bar * (tau_bar to_power n) >= (tau - (((sqrt 5) / (tau_bar to_power n)) / 2)) * (tau_bar to_power n) by C1, FIB_NUM:def 1, XREAL_1:66;
then tau_bar * (tau_bar to_power n) >= (tau - (((sqrt 5) / 2) / (tau_bar to_power n))) * (tau_bar to_power n) by XCMPLX_1:48;
then tau_bar * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((((sqrt 5) / 2) / (tau_bar to_power n)) * (tau_bar to_power n)) ;
then tau_bar * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by C1, XCMPLX_1:88;
then (tau_bar to_power 1) * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by POWER:30;
then tau_bar to_power (n + 1) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by JakPower32;
then - (tau_bar to_power (n + 1)) <= - ((tau * (tau_bar to_power n)) - ((sqrt 5) / 2)) by XREAL_1:26;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= ((- (tau * (tau_bar to_power n))) + ((sqrt 5) / 2)) + (tau to_power (n + 1)) by XREAL_1:8;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) ;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= (((tau to_power n) * (tau to_power 1)) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) by JakPower32;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= (((tau to_power n) * tau ) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) by POWER:30;
then ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) + ((sqrt 5) / 2)) / (sqrt 5) by CC, XREAL_1:74;
then Fib (n + 1) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) + ((sqrt 5) / 2)) / (sqrt 5) by FIB_NUM:7;
then Fib (n + 1) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:63;
then Fib (n + 1) <= (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) + (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:75;
then Fib (n + 1) <= (tau * (Fib n)) + (((sqrt 5) / 2) / (sqrt 5)) by FIB_NUM:7;
then Fib (n + 1) <= (tau * (Fib n)) + (((sqrt 5) / (sqrt 5)) / 2) by XCMPLX_1:48;
then Fib (n + 1) <= (tau * (Fib n)) + (1 / 2) by CC, XCMPLX_1:60;
hence (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) by FIB_NUM:def 1; :: thesis: verum

end;

((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1)

proof

Fib (n + 1) = [\((tau * (Fib n)) + 1)/] by A0, ST1, Tw13a;
then B2: ((tau * (Fib n)) + 1) - 1 < Fib (n + 1) by INT_1:def 4;
((Fib n) + ((sqrt 5) * (Fib n))) + 1 <= ((Fib n) + ((sqrt 5) * (Fib n))) + 2 by XREAL_1:8;
then (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 <= (((Fib n) + ((sqrt 5) * (Fib n))) + 2) / 2 by XREAL_1:74;
then ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 <= ((tau * (Fib n)) + 1) - 1 by FIB_NUM:def 1, XREAL_1:11;
hence ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) by B2, XXREAL_0:2; :: thesis: verum

end;

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

end;

suppose ST2: not n is even ; :: thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]

B1: (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1)

proof

Fib (n + 1) = [/((tau * (Fib n)) - 1)\] by A0, ST2, Tw13b;
then c1: ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) by INT_1:def 5;
1 + ((Fib n) + ((sqrt 5) * (Fib n))) > 0 + ((Fib n) + ((sqrt 5) * (Fib n))) by XREAL_1:8;
then (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 > ((Fib n) + ((sqrt 5) * (Fib n))) / 2 by XREAL_1:76;
hence (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) by c1, FIB_NUM:def 1, XXREAL_0:2; :: thesis: verum

end;

((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1)

proof

n > 1 by A0, XXREAL_0:2;
then (2 * (sqrt 5)) * (tau_bar to_power n) > (2 * (sqrt 5)) * (- (1 / 2)) by CC, hop9, XREAL_1:70;
then - ((2 * (sqrt 5)) * (tau_bar to_power n)) < - ((2 * (sqrt 5)) * (- (1 / 2))) by XREAL_1:26;
then ((((((1 * (tau to_power n)) + ((sqrt 5) * (tau to_power n))) - ((2 * tau ) * (tau to_power n))) + ((2 * tau_bar ) * (tau_bar to_power n))) - ((sqrt 5) * (tau_bar to_power n))) - (1 * (tau_bar to_power n))) + ((2 * tau ) * (tau to_power n)) < (sqrt 5) + ((2 * tau ) * (tau to_power n)) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1:8;
then (((((tau to_power n) + ((sqrt 5) * (tau to_power n))) + ((2 * tau_bar ) * (tau_bar to_power n))) - ((sqrt 5) * (tau_bar to_power n))) - (tau_bar to_power n)) - ((2 * tau_bar ) * (tau_bar to_power n)) < ((sqrt 5) + ((2 * tau ) * (tau to_power n))) - ((2 * tau_bar ) * (tau_bar to_power n)) by XREAL_1:11;
then ((1 + (sqrt 5)) * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) < (((sqrt 5) + ((2 * tau ) * (tau to_power n))) - ((2 * tau_bar ) * (tau_bar to_power n))) / (sqrt 5) by CC, XREAL_1:76;
then (1 + (sqrt 5)) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) < (((sqrt 5) + (2 * (tau * (tau to_power n)))) - ((2 * tau_bar ) * (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:75;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau * (tau to_power n)))) - ((2 * tau_bar ) * (tau_bar to_power n))) / (sqrt 5) by FIB_NUM:7;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * ((tau to_power 1) * (tau to_power n)))) - ((2 * tau_bar ) * (tau_bar to_power n))) / (sqrt 5) by POWER:30;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * (tau_bar * (tau_bar to_power n)))) / (sqrt 5) by JakPower32;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * ((tau_bar to_power 1) * (tau_bar to_power n)))) / (sqrt 5) by POWER:30;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * (tau_bar to_power (n + 1)))) / (sqrt 5) by JakPower32;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) + (2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))))) / (sqrt 5) ;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + ((2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1)))) / (sqrt 5)) by XCMPLX_1:63;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + (2 * (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5))) by XCMPLX_1:75;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + (2 * (Fib (n + 1))) by FIB_NUM:7;
then (1 + (sqrt 5)) * (Fib n) < 1 + (2 * (Fib (n + 1))) by CC, XCMPLX_1:60;
then ((1 + (sqrt 5)) * (Fib n)) / 2 < (1 + (2 * (Fib (n + 1)))) / 2 by XREAL_1:76;
then (((1 + (sqrt 5)) * (Fib n)) / 2) - (1 / 2) < ((1 / 2) + (Fib (n + 1))) - (1 / 2) by XREAL_1:11;
hence ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) ; :: thesis: verum

end;

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

end;

end;