let n be Nat; :: thesis: ( n >= 2 implies Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\] )
assume A1: 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 Th24;
then A2: ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) by INT_1:def 6;
((((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 Th24, A1;
then A3: ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 >= Fib (n + 1) by INT_1:def 6;
((((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;
A4: sqrt 5 > 0 by SQUARE_1:25;
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 A4, XCMPLX_1:87;
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:74;
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 A4, XCMPLX_1:87;
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 Th2;
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 Th2;
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))) ;
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)) ;
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 A4;
hence contradiction by Th8, A1; :: thesis: verum
end;
hence ((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2) + 1 > Fib (n + 1) by A3, XXREAL_0:1; :: thesis: verum
end;
hence Fib (n + 1) = [/((((Fib n) + ((sqrt 5) * (Fib n))) - 1) / 2)\] by A2, INT_1:def 7; :: thesis: verum