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)\]
then Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by Wn14;
then a1: ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) by INT_1:def 4;
((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 > Fib (n + 1)

proof

Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by Wn14, A0;
then C2: ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 >= Fib (n + 1) by INT_1:def 4;
((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 <> Fib (n + 1)

proof

set tn = tau to_power n;
set tbn = tau_bar to_power n;
set t1 = tau to_power (n + 1);
set t2 = tau_bar to_power (n + 1);
set s5 = sqrt 5;
b0: sqrt 5 > 0 by SQUARE_1:93;
assume ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 = Fib (n + 1) ; :: thesis: contradiction
then ((Fib n) * (1 + (sqrt 5))) + 1 = 2 * (Fib (n + 1)) ;
then ((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) + 1 = 2 * (Fib (n + 1)) by FIB_NUM:7;
then (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) + 1) * (sqrt 5) = (2 * (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5))) * (sqrt 5) by FIB_NUM:7;
then (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) * (sqrt 5)) + (1 * (sqrt 5)) = 2 * ((((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) * (sqrt 5)) ;
then (((((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) * (1 + (sqrt 5))) * (sqrt 5)) + (sqrt 5) = 2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) by b0, XCMPLX_1:88;
then (((((tau to_power n) - (tau_bar to_power n)) * (1 + (sqrt 5))) / (sqrt 5)) * (sqrt 5)) + (sqrt 5) = (2 * (tau to_power (n + 1))) - (2 * (tau_bar to_power (n + 1))) by XCMPLX_1:75;
then (((tau to_power n) - (tau_bar to_power n)) * (1 + (sqrt 5))) + (sqrt 5) = (2 * (tau to_power (n + 1))) - (2 * (tau_bar to_power (n + 1))) by b0, XCMPLX_1:88;
then (((tau to_power n) * (1 + (sqrt 5))) - ((tau_bar to_power n) + ((tau_bar to_power n) * (sqrt 5)))) + (sqrt 5) = (2 * ((tau to_power n) * (tau to_power 1))) - (2 * (tau_bar to_power (n + 1))) by JakPower32;
then (((tau to_power n) * (1 + (sqrt 5))) - ((tau_bar to_power n) * (1 + (sqrt 5)))) + (sqrt 5) = (2 * ((tau to_power n) * (tau to_power 1))) - (2 * ((tau_bar to_power n) * (tau_bar to_power 1))) by JakPower32;
then (((tau to_power n) * (1 + (sqrt 5))) - ((tau_bar to_power n) * (1 + (sqrt 5)))) + (sqrt 5) = (2 * ((tau to_power n) * tau)) - (2 * ((tau_bar to_power n) * (tau_bar to_power 1))) by POWER:30;
then (((tau to_power n) - (tau_bar to_power n)) * (1 + (sqrt 5))) + (sqrt 5) = (2 * ((tau to_power n) * tau)) - (2 * ((tau_bar to_power n) * tau_bar)) by POWER:30;
then (((tau to_power n) * ((1 + (sqrt 5)) - (2 * tau))) + ((tau_bar to_power n) * ((2 * tau_bar) - (1 + (sqrt 5))))) + (sqrt 5) = 0 ;
then ((- (2 * (tau_bar to_power n))) + 1) * (sqrt 5) = 0 by FIB_NUM:def 1, FIB_NUM:def 2;
then (- (2 * (tau_bar to_power n))) + 1 = 0 by b0;
hence contradiction by hop8, A0; :: thesis: verum

end;

hence ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 > Fib (n + 1) by C2, XXREAL_0:1; :: thesis: verum

end;

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